OAI/Analysis/CircleDomains/Selection/LiftedMeanContinuity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Continuous local representatives of the geometric mean index. Point avoidance is transported through the actual injective Jordan map.

  1. def OAI.CircleDomainRigidity.liftedMeanGeometricIndex line 15
  2. theorem OAI.CircleDomainRigidity.liftedMeanGeometricIndex_eq line 20
  3. theorem OAI.CircleDomainRigidity.continuousOn_liftedMeanGeometricIndex line 26
  4. theorem OAI.CircleDomainRigidity.bounded_liftedMeanGeometricIndex_on_compact line 47
  5. theorem OAI.CircleDomainRigidity.ae_mapped_arc_avoids line 75