OAI/Analysis/CircleDomains/Modulus/ConformalNormalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Conformal point-to-infinity normalization

The explicit normalizer and its inverse are conformal in every sphere chart. Postcomposition therefore preserves the conformal equivalence, not just the topology and the round complementary components.

  1. theorem OAI.CircleDomainRigidity.affineSphere_symm_eq line 20
  2. theorem OAI.CircleDomainRigidity.isConformalAt_affineSphere_symm line 31
  3. theorem OAI.CircleDomainRigidity.isConformalAt_pointToInfinity line 36
  4. theorem OAI.CircleDomainRigidity.isConformalAt_pointToInfinity_symm line 44
  5. theorem OAI.CircleDomainRigidity.isConformalEquivalence_of_homeomorph line 52
  6. theorem OAI.CircleDomainRigidity.isConformalEquivalence_pointToInfinity line 63