OAI/Analysis/CircleDomains/Modulus/ShrinkingLengthFibers.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Diameter covers for codimension-one fibers. The estimate is also useful on the critical set, where a positive chart Jacobian is unavailable.

  1. lemma OAI.CircleDomainRigidity.hausdorff_one_fiber_le_liminf_cover line 13
  2. lemma OAI.CircleDomainRigidity.iSup_nonempty_ediam_sq line 45
  3. lemma OAI.CircleDomainRigidity.exists_small_quadratic_hausdorff_cover line 51