OAI/Analysis/CircleDomains/Reflection/AnalyticReflectionData.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual data for finite analytic uniformization by invariant Beltrami coefficients. Conformality of the straightened comparison and roundness of its boundary images are not fields and remain to be proved.

  1. structure OAI.CircleDomainRigidity.AnalyticReflectionData line 17
  2. def OAI.CircleDomainRigidity.AnalyticReflectionData.principal line 49
  3. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.principal_decay line 51
  4. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.principal_weak line 54
  5. lemma OAI.CircleDomainRigidity.exists_analytic_reflection_data line 61