OAI/Analysis/CircleDomains/Modulus/NormalizedLimits.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Normalized limits on exhausting retained cores

The uniform finite-model bounds give local boundedness. The common decaying exterior remainder passes to the limit and prevents a constant limit on any retained core containing the exterior. Hurwitz then gives global injectivity. A further subsequence retains all these conclusions and converges for every marked complementary disk simultaneously.

  1. theorem OAI.CircleDomainRigidity.exterior_decay_le_radius line 23
  2. theorem OAI.CircleDomainRigidity.not_constant_of_exterior_decay line 28
  3. theorem OAI.CircleDomainRigidity.principal_remainder_of_exterior_decay line 48
  4. theorem OAI.CircleDomainRigidity.exists_normalized_univalent_limit line 57
  5. theorem OAI.CircleDomainRigidity.locally_uniform_subsequence line 96
  6. theorem OAI.CircleDomainRigidity.exists_normalized_marked_limit line 104