OAI/Analysis/CircleDomains/Uniformization/EventualSelectedSeparation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform radius and separation estimates for arbitrary Jordan input, by restarting the actual iteration after its first analytic cycle.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.selectedRadii_eventual_lower_bound line 16
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.selectedCircles_eventual_separation line 26