OAI/Analysis/CircleDomains/Modulus/PhysicalCompactLength.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite dyadic domain length controls every compact physical subinterval. In particular it implies the local rectifiability required by the manuscript.

  1. theorem OAI.CircleDomainRigidity.timeClip_mapsTo_of_inter line 16
  2. theorem OAI.CircleDomainRigidity.timeClip_eq_const_of_disjoint line 24
  3. theorem OAI.CircleDomainRigidity.physicalSubpath_clip_agree line 46
  4. theorem OAI.CircleDomainRigidity.physicalSubpath_variation_le_cell line 61
  5. theorem OAI.CircleDomainRigidity.physicalSubpath_length_le_domain line 88
  6. theorem OAI.CircleDomainRigidity.physicalSubpath_rectifiable line 97