OAI/Analysis/CircleDomains/Uniformization/JordanCircularizationCompactness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normal-family compactness for the actual successive circularizations. The source exterior radius supplies uniform bounds for every cumulative map and every omitted component, without assuming a circular limit.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.circularization_uniform_bounds line 18
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.exists_circularization_normal_limit_along line 44
  3. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.exists_circularization_normal_limit line 69