OAI/Analysis/CircleDomains/Reflection/AnalyticJordanCap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Analytic circle parametrizations of the actual compact Jordan holes. The neighborhood and injectivity are retained so that a later circularization has the proved local continuation.

  1. def OAI.CircleDomainRigidity.IsAnalyticJordanCap line 15
  2. lemma OAI.CircleDomainRigidity.isAnalyticJordanCap_of_round line 20
  3. lemma OAI.CircleDomainRigidity.IsAnalyticJordanCap.conformal_image line 25
  4. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.Step.analytic_selected line 59
  5. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.Step.analytic_other line 63
  6. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.iterate_analytic_of_visited line 75