OAI/Analysis/CircleDomains/Modulus/MobiusNormalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Concrete Möbius normalizations

Affine changes and inversion are homeomorphisms of the concrete sphere. Their matrix actions agree with the projective-line action used in the definition of round disks.

  1. def OAI.CircleDomainRigidity.affineHomeomorph line 20
  2. def OAI.CircleDomainRigidity.affineSphere line 28
  3. def OAI.CircleDomainRigidity.affineMobius line 31
  4. def OAI.CircleDomainRigidity.inversionMobius line 34
  5. theorem OAI.CircleDomainRigidity.affineSphere_eq_smul line 37
  6. theorem OAI.CircleDomainRigidity.inversion_eq_smul line 43
  7. theorem OAI.CircleDomainRigidity.isRoundClosedDisk_image_mobius line 53