The metric derivative of a curve

For a curve γ : ℝ → X in an extended pseudometric space, the metric derivative at t is |γ'|(t) = limsup_{s → t, s ≠ t} edist (γ s) (γ t) / |s - t|, the metric replacement for the norm of the velocity of a curve in a seminormed space (HasDerivAt.metricDerivative_eq). It is the speed that the action ∫ |γ'|(t)ᵖ dt of a curve integrates, and so the basic object behind absolutely continuous curves in metric spaces, dynamic transport plans and metric gradient flows.

The main result is the fundamental theorem for absolutely continuous metric-valued curves (Ambrosio–Gigli–Savaré, Theorem 1.1.2). For a curve γ that is absolutely continuous on [a, b] in Mathlib's sense, AbsolutelyContinuousOnInterval γ a b:

• the difference quotients edist (γ s) (γ t) / edist s t converge, so the limsup defining the metric derivative is a genuine limit, at almost every t ∈ [a, b];
• the metric derivative has finite integral over [a, b], and edist (γ s) (γ u) ≤ ∫⁻ r in Ι s u, |γ'|(r) for all s, u ∈ [a, b];
• it is the smallest such density: any almost everywhere measurable m with finite integral over [a, b] satisfying the same bound dominates the metric derivative almost everywhere on [a, b].

Conversely a curve admitting such an integrable density is absolutely continuous, so absolute continuity of a metric-valued curve is exactly the existence of an integrable density bounding its distances, which is the definition used by Ambrosio–Gigli–Savaré (absolutelyContinuousOnInterval_iff_exists_edist_le_lintegral).

The proof of the fundamental theorem follows Ambrosio–Gigli–Savaré. The image of [a, b] is compact, hence separable, so it has a countable dense subset c. Each distance profile r ↦ dist (γ r) x with x ∈ c is a real absolutely continuous function, hence the integral of its derivative, and the supremum m of the absolute values of these derivatives bounds edist (γ s) (γ u) by ∫⁻ r in Ι s u, m r. Every difference quotient of γ dominates those of the profiles, so m is a lower bound for the liminf, while the Lebesgue differentiation theorem makes m an upper bound for the limsup. Finiteness of ∫⁻ m comes from the variation function of γ, a monotone real function whose increments dominate the distances along γ, so that its integrable derivative bounds the metric derivative almost everywhere.

For continuous curves the limsup defining the metric derivative can be taken along rational increments, which makes the metric derivative jointly measurable in the time and in the parameter of a measurable family of continuous curves, and absolute continuity can be tested on rational times. On the space C([a, b], X) of continuous paths with its Borel structure, the space on which dynamic transport plans live, this gives the measurability of the metric derivative and of the set of absolutely continuous paths, which the action functional of a dynamic plan integrates.

Main definitions

• TauCeti.metricDerivative γ t: the metric derivative of γ at t, as an extended nonnegative real.

Main results

• HasDerivAt.tendsto_edist_div and HasDerivAt.metricDerivative_eq: on a seminormed space the difference quotients converge to the norm of the derivative, which is the metric derivative.
• TauCeti.continuousAt_of_metricDerivative_ne_top: a curve is continuous wherever its metric derivative is finite.
• LipschitzWith.metricDerivative_le, LipschitzOnWith.metricDerivative_le and LipschitzWith.metricDerivative_comp_le: Lipschitz bounds on a curve, globally or near a time, and under Lipschitz post-composition.
• Isometry.metricDerivative_comp: post-composition with an isometry preserves the metric derivative.
• BoundedVariationOn.ae_metricDerivative_le_enorm_deriv_variationOnFromTo: for a curve of bounded variation, the metric derivative is almost everywhere at most the derivative of the variation.
• TauCeti.ae_metricDerivative_le: minimality of the metric derivative among the integrable densities bounding the distances along a curve.
• AbsolutelyContinuousOnInterval.ae_tendsto_metricDerivative, AbsolutelyContinuousOnInterval.lintegral_metricDerivative_lt_top and AbsolutelyContinuousOnInterval.edist_le_lintegral_metricDerivative: the fundamental theorem for absolutely continuous curves.
• TauCeti.absolutelyContinuousOnInterval_iff_exists_edist_le_lintegral: absolute continuity as the existence of an integrable density bounding the distances along a curve.
• TauCeti.measurable_metricDerivative and Continuous.measurable_metricDerivative: joint measurability of the metric derivative in a measurable family of continuous curves, and measurability for a single continuous curve.
• TauCeti.absolutelyContinuousOnInterval_iff_forall_rat_edist_le_lintegral and TauCeti.measurableSet_absolutelyContinuousOnInterval: absolute continuity of a continuous curve tested on rational times, and the measurability of the absolutely continuous members of a measurable family of continuous curves.
• TauCeti.measurable_metricDerivative_IccExtend and TauCeti.measurableSet_absolutelyContinuousOnInterval_IccExtend: the same statements on the path space C([a, b], X), with TauCeti.measurable_metricDerivative_IccExtend_apply for the speed at a fixed time.

References

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

noncomputable def TauCeti.metricDerivative {X : Type u_1} [PseudoEMetricSpace X] (γ : ℝ → X) (t : ℝ) : ENNReal

The metric derivative of a curve γ : ℝ → X at t, the upper limit of the difference quotients edist (γ s) (γ t) / edist s t as s → t with s ≠ t. For an absolutely continuous curve these quotients converge at almost every time (AbsolutelyContinuousOnInterval.ae_tendsto_metricDerivative); taking the upper limit makes the metric derivative defined at every time.

Equations

• TauCeti.metricDerivative γ t = Filter.limsup (fun (s : ℝ) => edist (γ s) (γ t) / edist s t) (nhdsWithin t {t}ᶜ)

theorem TauCeti.metricDerivative_def {X : Type u_1} [PseudoEMetricSpace X] (γ : ℝ → X) (t : ℝ) : metricDerivative γ t = Filter.limsup (fun (s : ℝ) => edist (γ s) (γ t) / edist s t) (nhdsWithin t {t}ᶜ)

The defining formula of the metric derivative, as an upper limit of difference quotients.

theorem TauCeti.metricDerivative_eq_of_tendsto {X : Type u_1} [PseudoEMetricSpace X] {γ : ℝ → X} {t : ℝ} {l : ENNReal} (h : Filter.Tendsto (fun (s : ℝ) => edist (γ s) (γ t) / edist s t) (nhdsWithin t {t}ᶜ) (nhds l)) : metricDerivative γ t = l

If the difference quotients of γ at t converge, their limit is the metric derivative.

theorem TauCeti.continuousAt_of_metricDerivative_ne_top {X : Type u_1} [PseudoEMetricSpace X] {γ : ℝ → X} {t : ℝ} (h : metricDerivative γ t ≠ ⊤) : ContinuousAt γ t

A curve with finite metric derivative at t is continuous at t.

theorem LipschitzOnWith.metricDerivative_le {X : Type u_1} [PseudoEMetricSpace X] {γ : ℝ → X} {t : ℝ} {K : NNReal} {s : Set ℝ} (hγ : LipschitzOnWith K γ s) (hs : s ∈ nhds t) : TauCeti.metricDerivative γ t ≤ ↑K

The metric derivative at t of a curve that is K-Lipschitz on a neighbourhood of t is at most K.

theorem LipschitzWith.metricDerivative_le {X : Type u_1} [PseudoEMetricSpace X] {γ : ℝ → X} {K : NNReal} (hγ : LipschitzWith K γ) (t : ℝ) : TauCeti.metricDerivative γ t ≤ ↑K

The metric derivative of a K-Lipschitz curve is at most K everywhere.

theorem LipschitzWith.metricDerivative_comp_le {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {f : X → Y} {K : NNReal} (hf : LipschitzWith K f) (γ : ℝ → X) (t : ℝ) : TauCeti.metricDerivative (f ∘ γ) t ≤ ↑K * TauCeti.metricDerivative γ t

Post-composing a curve with a K-Lipschitz map multiplies its metric derivative by at most K.

theorem Isometry.metricDerivative_comp {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {f : X → Y} (hf : Isometry f) (γ : ℝ → X) (t : ℝ) : TauCeti.metricDerivative (f ∘ γ) t = TauCeti.metricDerivative γ t

Post-composing a curve with an isometry leaves its metric derivative unchanged.

theorem TauCeti.ae_metricDerivative_le {X : Type u_1} [PseudoEMetricSpace X] {γ : ℝ → X} {m : ℝ → ENNReal} {a b : ℝ} (hm : AEMeasurable m (MeasureTheory.volume.restrict (Set.uIoc a b))) (hfin : ∫⁻ (r : ℝ) in Set.uIoc a b, m r ≠ ⊤) (h : ∀ s ∈ Set.uIcc a b, ∀ u ∈ Set.uIcc a b, edist (γ s) (γ u) ≤ ∫⁻ (r : ℝ) in Set.uIoc s u, m r) : ∀ᵐ (t : ℝ), t ∈ Set.uIcc a b → metricDerivative γ t ≤ m t

Minimality of the metric derivative. If m has finite integral over [a, b] and bounds the distances along γ by edist (γ s) (γ u) ≤ ∫⁻ r in Ι s u, m r for all s, u ∈ [a, b], then the metric derivative of γ is at most m almost everywhere on [a, b].

theorem HasDerivAt.tendsto_edist_div {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : E} {t : ℝ} (h : HasDerivAt γ v t) : Filter.Tendsto (fun (s : ℝ) => edist (γ s) (γ t) / edist s t) (nhdsWithin t {t}ᶜ) (nhds ‖v‖ₑ)

The difference quotients edist (γ s) (γ t) / edist s t of a curve in a seminormed space converge to the norm of its derivative.

theorem HasDerivAt.metricDerivative_eq {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {v : E} {t : ℝ} (h : HasDerivAt γ v t) : TauCeti.metricDerivative γ t = ‖v‖ₑ

On a seminormed space the metric derivative of a curve is the norm of its derivative.

theorem BoundedVariationOn.ae_metricDerivative_le_enorm_deriv_variationOnFromTo {X : Type u_1} [PseudoEMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : BoundedVariationOn γ (Set.uIcc a b)) : ∀ᵐ (t : ℝ), t ∈ Set.uIcc a b → TauCeti.metricDerivative γ t ≤ ‖deriv (variationOnFromTo γ (Set.uIcc a b) a) t‖ₑ

At almost every time of [a, b], the metric derivative of a curve of bounded variation on [a, b] is at most the derivative of its variation function variationOnFromTo γ (uIcc a b) a.

theorem AbsolutelyContinuousOnInterval.ae_tendsto_metricDerivative {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : ∀ᵐ (t : ℝ), t ∈ Set.uIcc a b → Filter.Tendsto (fun (s : ℝ) => edist (γ s) (γ t) / edist s t) (nhdsWithin t {t}ᶜ) (nhds (TauCeti.metricDerivative γ t))

Fundamental theorem for absolutely continuous curves, existence of the metric derivative: for an absolutely continuous curve γ on [a, b], at almost every t ∈ [a, b] the difference quotients edist (γ s) (γ t) / edist s t converge to the metric derivative as s → t.

theorem AbsolutelyContinuousOnInterval.aemeasurable_metricDerivative {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : AEMeasurable (TauCeti.metricDerivative γ) (MeasureTheory.volume.restrict (Set.uIoc a b))

The metric derivative of an absolutely continuous curve on [a, b] is almost everywhere measurable on [a, b].

theorem AbsolutelyContinuousOnInterval.lintegral_metricDerivative_lt_top {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) : ∫⁻ (r : ℝ) in Set.uIoc a b, TauCeti.metricDerivative γ r < ⊤

Fundamental theorem for absolutely continuous curves, integrability: the metric derivative of an absolutely continuous curve on [a, b] has finite integral over [a, b].

theorem AbsolutelyContinuousOnInterval.edist_le_lintegral_metricDerivative {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) {s u : ℝ} (hs : s ∈ Set.uIcc a b) (hu : u ∈ Set.uIcc a b) : edist (γ s) (γ u) ≤ ∫⁻ (r : ℝ) in Set.uIoc s u, TauCeti.metricDerivative γ r

Fundamental theorem for absolutely continuous curves, the distance bound: along an absolutely continuous curve on [a, b], the distance between two times of [a, b] is at most the integral of the metric derivative between them.

theorem TauCeti.absolutelyContinuousOnInterval_of_edist_le_lintegral {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} {m : ℝ → ENNReal} (hfin : ∫⁻ (r : ℝ) in Set.uIoc a b, m r ≠ ⊤) (h : ∀ s ∈ Set.uIcc a b, ∀ u ∈ Set.uIcc a b, edist (γ s) (γ u) ≤ ∫⁻ (r : ℝ) in Set.uIoc s u, m r) : AbsolutelyContinuousOnInterval γ a b

A curve whose distances on [a, b] are bounded by the integrals of a density m with finite integral over [a, b] is absolutely continuous on [a, b].

theorem TauCeti.absolutelyContinuousOnInterval_iff_exists_edist_le_lintegral {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} : AbsolutelyContinuousOnInterval γ a b ↔ ∃ (m : ℝ → ENNReal), ∫⁻ (r : ℝ) in Set.uIoc a b, m r ≠ ⊤ ∧ ∀ s ∈ Set.uIcc a b, ∀ u ∈ Set.uIcc a b, edist (γ s) (γ u) ≤ ∫⁻ (r : ℝ) in Set.uIoc s u, m r

Absolute continuity of a metric-valued curve is the existence of an integrable density bounding its distances: γ is absolutely continuous on [a, b] exactly when some m with finite integral over [a, b] bounds edist (γ s) (γ u) by ∫⁻ r in Ι s u, m r for all s, u ∈ [a, b]. The metric derivative is such an m, and by TauCeti.ae_metricDerivative_le it is almost everywhere below every almost everywhere measurable one.

theorem TauCeti.metricDerivative_eq_iInf_iSup_rat {X : Type u_1} [PseudoEMetricSpace X] {γ : ℝ → X} (hγ : Continuous γ) (t : ℝ) : metricDerivative γ t = ⨅ (n : ℕ), ⨆ r ∈ {r : ℚ | r ≠ 0 ∧ |↑r| < 1 / (↑n + 1)}, edist (γ (t + ↑r)) (γ t) / ‖↑r‖ₑ

For a continuous curve, the upper limit defining the metric derivative can be taken along rational increments: |γ'|(t) is the infimum over n of the supremum of the difference quotients edist (γ (t + r)) (γ t) / |r| over the rationals 0 < |r| < 1 / (n + 1).

theorem TauCeti.measurable_metricDerivative {X : Type u_1} [PseudoEMetricSpace X] {α : Type u_2} [MeasurableSpace α] {F : α → ℝ → X} (hF : ∀ (x : α), Continuous (F x)) (hm : ∀ (s u : ℝ), Measurable fun (x : α) => edist (F x s) (F x u)) : Measurable fun (q : α × ℝ) => metricDerivative (F q.1) q.2

Joint measurability of the metric derivative of a measurable family of continuous curves: if each curve F x is continuous and the distances edist (F x s) (F x u) depend measurably on x, then (x, t) ↦ |(F x)'|(t) is measurable.

theorem Continuous.measurable_metricDerivative {X : Type u_1} [PseudoEMetricSpace X] {γ : ℝ → X} (hγ : Continuous γ) : Measurable (TauCeti.metricDerivative γ)

The metric derivative of a continuous curve is measurable.

theorem TauCeti.measurable_metricDerivative_IccExtend {X : Type u_1} [PseudoEMetricSpace X] {a b : ℝ} (hab : a ≤ b) : Measurable fun (q : C(↑(Set.Icc a b), X) × ℝ) => metricDerivative (Set.IccExtend hab ⇑q.1) q.2

On the space C([a, b], X) of continuous paths with its Borel structure, the metric derivative (γ, t) ↦ |γ'|(t) of the path extended by constants outside [a, b] is jointly measurable.

theorem TauCeti.measurable_metricDerivative_IccExtend_apply {X : Type u_1} [PseudoEMetricSpace X] {a b : ℝ} (hab : a ≤ b) (t : ℝ) : Measurable fun (γ : C(↑(Set.Icc a b), X)) => metricDerivative (Set.IccExtend hab ⇑γ) t

On the space C([a, b], X) of continuous paths, the metric derivative γ ↦ |γ'|(t) at a fixed time of the path extended by constants outside [a, b] is measurable.

theorem TauCeti.absolutelyContinuousOnInterval_iff_forall_rat_edist_le_lintegral {X : Type u_1} [PseudoMetricSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : ContinuousOn γ (Set.uIcc a b)) : AbsolutelyContinuousOnInterval γ a b ↔ ∫⁻ (r : ℝ) in Set.uIoc a b, metricDerivative γ r ≠ ⊤ ∧ ∀ (q r : ℚ), ↑q ∈ Set.uIcc a b → ↑r ∈ Set.uIcc a b → edist (γ ↑q) (γ ↑r) ≤ ∫⁻ (x : ℝ) in Set.uIoc ↑q ↑r, metricDerivative γ x

Absolute continuity on rational times. A curve continuous on [a, b] is absolutely continuous there exactly when its metric derivative has finite integral over [a, b] and bounds the distances between the rational times of [a, b]: edist (γ q) (γ r) ≤ ∫⁻ x in Ι q r, |γ'|(x).

theorem TauCeti.measurableSet_absolutelyContinuousOnInterval {X : Type u_1} [PseudoMetricSpace X] {α : Type u_2} [MeasurableSpace α] {F : α → ℝ → X} (hF : ∀ (x : α), Continuous (F x)) (hm : ∀ (s u : ℝ), Measurable fun (x : α) => edist (F x s) (F x u)) (a b : ℝ) : MeasurableSet {x : α | AbsolutelyContinuousOnInterval (F x) a b}

Measurability of absolute continuity in a measurable family of continuous curves: if each curve F x is continuous and the distances edist (F x s) (F x u) depend measurably on x, then the parameters x for which F x is absolutely continuous on [a, b] form a measurable set.

theorem TauCeti.measurableSet_absolutelyContinuousOnInterval_IccExtend {X : Type u_1} [PseudoMetricSpace X] {a b : ℝ} (hab : a ≤ b) (s u : ℝ) : MeasurableSet {γ : C(↑(Set.Icc a b), X) | AbsolutelyContinuousOnInterval (Set.IccExtend hab ⇑γ) s u}

On the space C([a, b], X) of continuous paths with its Borel structure, the paths whose extension by constants outside [a, b] is absolutely continuous on [s, u] form a measurable set.