OAI/Analysis/CircleDomains/Reflection/PrincipalComplexBeltrami.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The compactly supported complex-coefficient principal solution used in finite reflection constructions. The L2 density is solved by the actual Beurling contraction and the homeomorphism is the strong smooth limit.

  1. lemma OAI.CircleDomainRigidity.exists_compact_complex_beltrami_density line 17
  2. lemma OAI.CircleDomainRigidity.exists_principal_complex_beltrami_limit line 33
  3. lemma OAI.CircleDomainRigidity.exists_principal_complex_beltrami_data line 52