Constant speed and metric derivatives

Mathlib's HasConstantSpeedOnWith specifies the variation on every subinterval. This file identifies that condition with absolute continuity and an almost everywhere constant metric derivative. In particular, unit-speed arclength curves have metric derivative one almost everywhere, and their difference quotients converge to one there. Singleton intervals and speed zero are included. The natural parameterization of a continuous curve of bounded variation is absolutely continuous on its length interval (BoundedVariationOn.absolutelyContinuousOnInterval_naturalParameterization).

For finite-dimensional real normed targets, the norm of the usual derivative equals the specified speed almost everywhere. No differentiability of a metric-valued curve is assumed.

This gives the constant-speed energy identity: along a curve of constant speed on [a, b], (b - a) ∫ₐᵇ ‖γ'‖² = L², where L is the length of the curve (HasConstantSpeedOnWith.mul_integral_norm_deriv_sq). For an arbitrary absolutely continuous curve with square-integrable derivative the left side is at least L² (AbsolutelyContinuousOnInterval.eVariationOn_toReal_sq_le_mul_integral_norm_deriv_sq), with equality exactly for constant speed (AbsolutelyContinuousOnInterval.mul_integral_norm_deriv_sq_eq_eVariationOn_toReal_sq_iff). Thus, among absolutely continuous curves of a given length on a fixed interval, exactly the constant-speed ones have least energy, and bounds proved through energy turn into length bounds for them without loss.

The main inputs are Mathlib's constant-speed predicate and the metric fundamental theorem and variation identity in TauCeti.MeasureTheory.Function.MetricDerivative.Variation.

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd ed., Birkhäuser 2008, §1.1.

theorem HasConstantSpeedOnWith.eVariationOn_uIcc {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} {l : NNReal} (hγ : HasConstantSpeedOnWith γ (Set.uIcc a b) l) : eVariationOn γ (Set.uIcc a b) = ENNReal.ofReal (↑l * |b - a|)

A curve of constant speed l on [a, b] has length l |b - a| there, in either order of the endpoints.

theorem HasConstantSpeedOnWith.ae_metricDerivative_eq {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} {l : NNReal} (hγ : HasConstantSpeedOnWith γ (Set.uIcc a b) l) : TauCeti.metricDerivative γ =ᵐ[MeasureTheory.volume.restrict (Set.uIcc a b)] fun (x : ℝ) => ↑l

A curve of constant variation speed has that metric derivative almost everywhere on its parameter interval. This applies in particular to unit-speed arclength curves.

theorem AbsolutelyContinuousOnInterval.hasConstantSpeedOnWith_of_ae_metricDerivative_eq {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} {l : NNReal} (hγ : AbsolutelyContinuousOnInterval γ a b) (hspeed : TauCeti.metricDerivative γ =ᵐ[MeasureTheory.volume.restrict (Set.uIcc a b)] fun (x : ℝ) => ↑l) : HasConstantSpeedOnWith γ (Set.uIcc a b) l

For an absolutely continuous curve, an almost everywhere constant metric derivative implies constant variation speed on every subinterval. Absolute continuity is essential here.

theorem TauCeti.hasConstantSpeedOnWith_iff_absolutelyContinuousOnInterval_metricDerivative_eq {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} {l : NNReal} : HasConstantSpeedOnWith γ (Set.uIcc a b) l ↔ AbsolutelyContinuousOnInterval γ a b ∧ metricDerivative γ =ᵐ[MeasureTheory.volume.restrict (Set.uIcc a b)] fun (x : ℝ) => ↑l

Constant variation speed is equivalent to absolute continuity with that metric derivative almost everywhere. The statement includes zero speed and either order of the endpoints.

theorem BoundedVariationOn.absolutelyContinuousOnInterval_naturalParameterization {a b : ℝ} {X : Type u_2} [MetricSpace X] {γ : ℝ → X} (hγ : BoundedVariationOn γ (Set.Icc a b)) (hcont : ContinuousOn γ (Set.Icc a b)) (hab : a ≤ b) : AbsolutelyContinuousOnInterval (naturalParameterization γ (Set.Icc a b) a) 0 (eVariationOn γ (Set.Icc a b)).toReal

The natural parameterization of a continuous curve of bounded variation on [a, b] is absolutely continuous on its length interval, because it has unit speed and is therefore 1-Lipschitz there.

theorem HasConstantSpeedOnWith.ae_tendsto_edist_div {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} {l : NNReal} (hγ : HasConstantSpeedOnWith γ (Set.uIcc a b) l) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.uIcc a b), Filter.Tendsto (fun (s : ℝ) => edist (γ s) (γ t) / edist s t) (nhdsWithin t {t}ᶜ) (nhds ↑l)

Along a curve of constant variation speed, the metric difference quotients converge to the specified speed at almost every interior time. In particular, unit variation speed gives a genuine metric-derivative limit of one.

theorem HasConstantSpeedOnWith.ae_norm_deriv_eq {a b : ℝ} {l : NNReal} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} (hγ : HasConstantSpeedOnWith γ (Set.uIcc a b) l) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.uIcc a b), DifferentiableAt ℝ γ t ∧ ‖deriv γ t‖ = ↑l

In finite-dimensional real normed spaces a constant-speed curve is differentiable almost everywhere, with derivative norm equal to its variation speed.

theorem HasConstantSpeedOnWith.memLp_deriv {a b : ℝ} {l : NNReal} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} (hγ : HasConstantSpeedOnWith γ (Set.uIcc a b) l) (p : ENNReal) : MeasureTheory.MemLp (deriv γ) p (MeasureTheory.volume.restrict (Set.uIoc a b))

The canonical derivative of a constant-speed curve is bounded by its speed almost everywhere, so it lies in every Lᵖ space on the parameter interval.

theorem HasConstantSpeedOnWith.integral_norm_deriv_pow {a b : ℝ} {l : NNReal} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} (hγ : HasConstantSpeedOnWith γ (Set.uIcc a b) l) (n : ℕ) : ∫ (t : ℝ) in a..b, ‖deriv γ t‖ ^ n = ↑l ^ n * (b - a)

The constant-speed energy identity. Along a curve of constant speed l on [a, b], the n-th power of the speed integrates to l ^ n (b - a).

theorem HasConstantSpeedOnWith.mul_integral_norm_deriv_sq {a b : ℝ} {l : NNReal} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} (hγ : HasConstantSpeedOnWith γ (Set.uIcc a b) l) : (b - a) * ∫ (t : ℝ) in a..b, ‖deriv γ t‖ ^ 2 = (eVariationOn γ (Set.uIcc a b)).toReal ^ 2

Along a curve of constant speed on [a, b], the energy ∫ₐᵇ ‖γ'‖² multiplied by the length b - a of the parameter interval is the square of the length of the curve.

theorem AbsolutelyContinuousOnInterval.eVariationOn_toReal_sq_le_mul_integral_norm_deriv_sq {a b : ℝ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} (hγ : AbsolutelyContinuousOnInterval γ a b) (hL2 : MeasureTheory.MemLp (deriv γ) 2 (MeasureTheory.volume.restrict (Set.uIoc a b))) : (eVariationOn γ (Set.uIcc a b)).toReal ^ 2 ≤ (b - a) * ∫ (t : ℝ) in a..b, ‖deriv γ t‖ ^ 2

Energy bounds length. For an absolutely continuous curve on [a, b] with square-integrable derivative, the square of its length is at most b - a times its energy ∫ₐᵇ ‖γ'‖². Both sides are symmetric in a and b.

theorem AbsolutelyContinuousOnInterval.mul_integral_norm_deriv_sq_eq_eVariationOn_toReal_sq_iff {a b : ℝ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} (hγ : AbsolutelyContinuousOnInterval γ a b) (hL2 : MeasureTheory.MemLp (deriv γ) 2 (MeasureTheory.volume.restrict (Set.uIoc a b))) : (b - a) * ∫ (t : ℝ) in a..b, ‖deriv γ t‖ ^ 2 = (eVariationOn γ (Set.uIcc a b)).toReal ^ 2 ↔ ∃ (l : NNReal), HasConstantSpeedOnWith γ (Set.uIcc a b) l

Equality of energy and length. For an absolutely continuous curve on [a, b] with square-integrable derivative, (b - a) ∫ₐᵇ ‖γ'‖² equals the square of the length of the curve exactly when the curve has constant speed on [a, b].