OAI/Analysis/CircleDomains/Sobolev/DifferentiableCurveLength.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact arclength on a bounded Borel set where a plane curve is differentiable. No continuity of the derivative or open-domain assumption is used.

  1. lemma OAI.CircleDomainRigidity.differentiable_curve_upper_error line 13
  2. lemma OAI.CircleDomainRigidity.differentiable_curve_lower_error line 43
  3. lemma OAI.CircleDomainRigidity.differentiable_curve_hausdorff_eq line 76