OAI/Analysis/CircleDomains/Uniformization/JordanCircularizationSequence.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The actual sequence of finite Jordan configurations and normalized conformal maps obtained by successive one-hole circularizations.

  1. structure OAI.CircleDomainRigidity.FiniteJordanConfiguration line 14
  2. def OAI.CircleDomainRigidity.FiniteJordanConfiguration.region line 21
  3. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.region_open line 23
  4. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.region_connected line 26
  5. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.infty_mem_region line 30
  6. structure OAI.CircleDomainRigidity.FiniteJordanConfiguration.Step line 35
  7. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.step_nonempty line 48
  8. def OAI.CircleDomainRigidity.FiniteJordanConfiguration.chosenStep line 53
  9. def OAI.CircleDomainRigidity.FiniteJordanConfiguration.iterate line 56
  10. def OAI.CircleDomainRigidity.FiniteJordanConfiguration.stageMap line 60
  11. def OAI.CircleDomainRigidity.FiniteJordanConfiguration.cumulativeMap line 63
  12. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.stageMap_principal line 67
  13. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.stageMap_conformal line 71
  14. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.cumulativeMap_principal line 76
  15. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.cumulativeMap_conformal line 85
  16. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.iterate_selected_round line 92
  17. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.stageMap_other_hole line 98