OAI/Analysis/CircleDomains/Uniformization/PrincipalFiniteModel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Principally normalized finite metric circle models

The spherical metric near infinity supplies an actual open neighborhood where the metric model is holomorphic. The affine normalization there preserves the circle domain, the smooth inverse, and the retained core.

  1. theorem OAI.CircleDomainRigidity.conformal_neighborhood_of_infty line 24
  2. theorem OAI.CircleDomainRigidity.smoothSphereEquivalence_affine line 45
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.principal_finite_metric_circle_model line 60