OAI/Analysis/CircleDomains/Topology/SphereModelLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Applying normalized compactness to sphere models

All complex-plane hypotheses of the compactness theorem are obtained from actual normalized smooth sphere equivalences and their retained holomorphic cores. The exterior estimate follows from the univalent area theorem.

  1. theorem OAI.CircleDomainRigidity.finite_part_injOn line 21
  2. theorem OAI.CircleDomainRigidity.finite_part_differentiableOn line 36
  3. theorem OAI.CircleDomainRigidity.normalized_sphere_model_exterior_decay line 48
  4. theorem OAI.CircleDomainRigidity.exists_normalized_limit_of_sphere_models line 73