OAI/Analysis/CircleDomains/Probability/SimpleArcOccupation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact arclength occupation of an injective continuous path. This identifies weighted path cost with the Hausdorff integral on its image.

  1. theorem OAI.CircleDomainRigidity.arc_variation_eq_hausdorff_interval line 15
  2. theorem OAI.CircleDomainRigidity.simple_arc_length_measure line 28
  3. theorem OAI.CircleDomainRigidity.simple_arc_occupation line 38
  4. theorem OAI.CircleDomainRigidity.simple_arc_weighted_cost line 46
  5. theorem OAI.CircleDomainRigidity.simple_arc_rectifiable_of_finite_length line 52