OAI/Analysis/CircleDomains/Uniformization/FiniteCompletionUniformization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite uniformization of the actual terminal-disk complement

The complementary components are exactly the closed physical terminal caps. In particular they are finite and nondegenerate. The published finite circle theorem therefore applies after compact metric uniformization; the resulting map is conformal on the retained core.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.closedTerminalCap line 21
  2. def OAI.CircleDomainRigidity.FiniteTransfer.openCompletedRegion line 24
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.isCompact_closedTerminalCap line 27
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.isPreconnected_closedTerminalCap line 30
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.nontrivial_closedTerminalCap line 33
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.disjoint_closedTerminalCaps line 44
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.isOpen_openCompletedRegion line 53
  8. theorem OAI.CircleDomainRigidity.FiniteTransfer.isConnected_openCompletedRegion line 57
  9. theorem OAI.CircleDomainRigidity.FiniteTransfer.uniformize_finite_completion_after_homeomorphism line 88