Metric variation of a continuously differentiable curve

For a continuously differentiable curve in a complete real normed space, its metric total variation equals the integral of the norm of its derivative.

The upper bound sums the fundamental theorem of calculus over finite partitions. For the reverse bound, the curve is clamped to the compact parameter interval. The resulting globally Lipschitz curve has bounded variation, and its associated vector measure has density given by the derivative on the interval.

Main result

• TauCeti.eVariationOn_eq_lintegral_enorm_derivWithin: metric variation equals the integral of the derivative norm.

Roadmap alignment

This module advances the Regular reparametrization and limits target under Layer 0: the reconciled Riemannian distance in roadmap/HopfRinow/README.md. It supplies the vector metric-variation identity used as an analytic prerequisite by the lower-semicontinuity comparison; this file does not claim the broader Hopf--Rinow dependency path.

Provenance

The partition-comparison architecture follows DoCarmoLib/Riemannian/Geodesic/HopfRinow/EVariationLePathELength.lean in the Apache-2.0 frenzymath/Poincare-Conjecture source at revision 24f32e4d600878bfaac6bc2f2f9324175571c321. That source proves the forward comparison with Riemannian path length. The reverse derivative-integral comparison here is a Tau Ceti proof using Mathlib's clamped-curve and vector-measure APIs; it is not asserted to be present in that source.

References

• M. P. do Carmo, Riemannian Geometry, Chapter 7, Section 2.
• The source-first Lean snapshot above, revision 24f32e4d600878bfaac6bc2f2f9324175571c321, supplies the partition architecture via eVariationOn_le_pathELength; the reverse inequality is original to this module.

theorem TauCeti.eVariationOn_le_lintegral_enorm_derivWithin {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ} (hf : ContDiffOn ℝ 1 f (Set.Icc a b)) : eVariationOn f (Set.Icc a b) ≤ ∫⁻ (t : ℝ) in Set.Icc a b, ‖derivWithin f (Set.Icc a b) t‖ₑ

For a C¹ curve in a real normed space, metric total variation is bounded by the integral of the norm of its derivative.

theorem TauCeti.lintegral_enorm_derivWithin_le_eVariationOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℝ → F} {a b : ℝ} (hf : ContDiffOn ℝ 1 f (Set.Icc a b)) : ∫⁻ (t : ℝ) in Set.Icc a b, ‖derivWithin f (Set.Icc a b) t‖ₑ ≤ eVariationOn f (Set.Icc a b)

For a C¹ curve in a complete real normed space, the integral of the norm of its derivative is bounded by its metric total variation.

theorem TauCeti.eVariationOn_eq_lintegral_enorm_derivWithin {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℝ → F} {a b : ℝ} (hf : ContDiffOn ℝ 1 f (Set.Icc a b)) : eVariationOn f (Set.Icc a b) = ∫⁻ (t : ℝ) in Set.Icc a b, ‖derivWithin f (Set.Icc a b) t‖ₑ

The metric total variation of a C¹ curve in a complete real normed space equals the integral of the norm of its derivative.