OAI/Analysis/CircleDomains/Topology/RoundDiskCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Euclidean coordinates for bounded round disks

Completing the square for a fractional linear map identifies a round spherical disk avoiding infinity with an ordinary Euclidean closed disk. This provides the center/radius coordinates used for marked ends.

  1. theorem OAI.CircleDomainRigidity.fractional_norm_square_identity line 20
  2. theorem OAI.CircleDomainRigidity.fractional_norm_region_eq_closedBall line 29