OAI/Analysis/CircleDomains/Reflection/AnalyticCircularization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

After one complete cycle every actual hole has an analytic circle parametrization. The next one-hole map therefore has the constructed holomorphic continuation in each source boundary chart.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.cyclic_iterate_analytic line 16
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.Step.analytic_boundary_continuation line 27
  3. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.cyclic_stage_boundary_continuation line 45