OAI/Analysis/CircleDomains/Topology/RectifiableSubarcs.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual short rectifiable arcs between nearby parameters of a finite-cost curve, with either orientation.

  1. theorem OAI.CircleDomainRigidity.pathOccupation_affine line 19
  2. theorem OAI.CircleDomainRigidity.pathCost_affine line 32
  3. def OAI.CircleDomainRigidity.constantRectifiablePath line 39
  4. theorem OAI.CircleDomainRigidity.pathOccupation_constant line 47
  5. theorem OAI.CircleDomainRigidity.exists_rectifiable_subarc line 52
  6. theorem OAI.CircleDomainRigidity.exists_small_rectifiable_subarcs line 85