OAI/Analysis/CircleDomains/Topology/PrincipalHomeomorphBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative bounds for a principally normalized plane homeomorphism. A topological plane homeomorphism cannot maximize its image norm in the interior of a disk. No holomorphic assumption inside the disk is used.

  1. lemma OAI.CircleDomainRigidity.homeomorph_disk_bound line 15
  2. lemma OAI.CircleDomainRigidity.principal_homeomorph_pointwise_bounds line 45
  3. lemma OAI.CircleDomainRigidity.principal_homeomorph_displacement_bound line 71