OAI/Analysis/CircleDomains/Sobolev/QuasiconformalSobolev.lean

Quasiconformal change of variables for continuous Sobolev functions.

Oliva--Prats, Sharp bounds for composition with quasiconformal mappings in Sobolev spaces, J. Math. Anal. Appl. 451 (2017), 1026--1044, DOI 10.1016/j.jmaa.2017.02.016: Definition 2.1, Theorem 2.2 (null-set preservation and inverse regularity), and Theorem 2.7, critical case p = n = 2, with the chain rule in its proof; https://arxiv.org/pdf/1612.00689, sections 2.1--2.2, pp. 4--7.

We assume only inverse weak derivatives, forward preservation of null sets, and the scalar Sobolev chain rule for continuous compactly supported functions. The squared Frobenius bound below is stronger than the operator norm bound in Definition 2.1. No model or extremality assertion is assumed.