OAI/Analysis/CircleDomains/Modulus/NormalizedLimitEquivalence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The normalized limit as a sphere conformal equivalence

The source includes infinity. The inverse on the image is constructed by the local inverse theorem, so the limiting map satisfies the same two-sided conformal predicate as the final circle-domain target.

  1. theorem OAI.CircleDomainRigidity.isOpen_finite_domain_with_infty line 21
  2. theorem OAI.CircleDomainRigidity.injOn_extendAtInfinity line 35
  3. theorem OAI.CircleDomainRigidity.normalized_limit_conformal_equivalence line 49
  4. theorem OAI.CircleDomainRigidity.exists_conformal_limit_of_sphere_models line 61