OAI/Analysis/CircleDomains/Modulus/NormalizedMetricUniformization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite circle models fixing infinity

Postcomposing the actual finite metric model by the explicit Möbius normalizer retains all conformality conclusions. Injectivity then ensures that every finite source point has a finite target coordinate.

  1. theorem OAI.CircleDomainRigidity.finite_image_of_fixes_infty line 23
  2. theorem OAI.CircleDomainRigidity.normalize_metric_circle_model line 30
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.uniformize_finite_metric_completion_fixing_infty line 52