OAI/Analysis/CircleDomains/Uniformization/CircularizationPhaseLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A phase of the actual cyclic construction has a conformal normal limit which omits the entire limiting selected disk, including a possible radius-zero disk. This does not yet identify the other holes.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.planeRegion_nontrivial line 19
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.not_constant_of_injOn line 31
  3. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.region_eq_plane_with_infty line 38
  4. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.conformal_limit line 43
  5. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.selected_disk_omitted line 57
  6. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.exists_cyclic_phase_limit line 71