OAI/Analysis/CircleDomains/Rigidity/PrincipalRealBeltrami.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The precise classical real-coefficient principal Beltrami input.

Published source: Clop and Cruz, Weighted estimates for Beltrami equations, Ann. Acad. Sci. Fenn. Math. 38 (2013), 91–113, DOI 10.5186/aasfm.2013.3818, section 4, opening paragraph, p. 107. Their theorem states existence of a principal W^{1,2}_loc plane homeomorphism for compactly supported measurable coefficients mu, nu with |mu|+|nu| bounded by k<1. We use only mu=0 and real nu=q.

No height, energy inequality, extremality, circle model, or limiting assertion is included in this input.

  1. structure OAI.CircleDomainRigidity.PlaneLocalWeakComplex line 24
  2. def OAI.CircleDomainRigidity.PrincipalRealBeltrami line 34
  3. def OAI.CircleDomainRigidity.conductivityValue line 46
  4. theorem OAI.CircleDomainRigidity.conductivityCoefficient_ratio line 50
  5. theorem OAI.CircleDomainRigidity.exists_principal_conductivity_coordinate line 56