The p-action of a curve and its lower semicontinuity

For a curve γ : ℝ → X in an extended pseudometric space and an exponent p, the p-action of γ over the interval between a and b is A_p(γ) = ∫ |γ'|(t) ^ p dt, the integral of the p-th power of the metric derivative |γ'|, with no factor 1 / p. The curves of finite p-action among the absolutely continuous ones are the curves ACᵖ of Ambrosio–Gigli–Savaré, and the action measures the cost of a path in the dynamic formulation of optimal transport and in metric gradient flows.

The main results concern an absolutely continuous curve γ on [a, b] and 1 ≤ p.

• The Hölder estimate d(γ s, γ u) ^ p ≤ |u - s| ^ (p - 1) * A_p(γ; s, u): for 1 < p, a curve of finite p-action is (1 - 1 / p)-Hölder continuous. Applied on each cell of a uniform grid of step h, it bounds the discrete action ∑ k, d(γ t_k, γ t_(k+1)) ^ p * h ^ (1 - p) of the samples at the grid times by A_p(γ).
• The difference-quotient formula: the action is the limit, as h → 0⁺, of the integrated difference quotients ∫_a^(b - h) (d(γ t, γ (t + h)) / h) ^ p dt. Each of these is at most the action, by the Hölder estimate on the windows [t, t + h] and Tonelli's theorem, and the action is at most their lower limit by Fatou's lemma, since the quotients tend to |γ'|(t) at almost every t.
• Lower semicontinuity: if curves γᵢ, eventually absolutely continuous on [a, b], converge pointwise on [a, b], along a countably generated filter, to an absolutely continuous curve γ, then A_p(γ) ≤ liminf A_p(γᵢ). For each step h, Fatou's lemma passes the integrated difference quotients to the limit, and the difference-quotient formula recovers the action.
• For 1 < p, a pointwise limit of eventually absolutely continuous curves whose actions have finite lower limit is itself absolutely continuous, by the Hölder estimate on finite unions of intervals. Lower semicontinuity therefore holds with no hypothesis on the limit curve.

The action is moreover a measurable function of the curve in a measurable family of continuous curves, in particular on the path space C([a, b], X) with its Borel structure, so that it can be integrated against a dynamic plan.

The difference-quotient formula is the metric counterpart of the characterisation of the Sobolev space W^{1,p} on an interval by difference quotients.

Main definitions

• TauCeti.curveAction p γ a b: the p-action ∫ t in Ι a b, |γ'|(t) ^ p of γ.

Main results

• AbsolutelyContinuousOnInterval.edist_rpow_le_mul_curveAction: the Hölder estimate, with its real-valued form AbsolutelyContinuousOnInterval.dist_rpow_le_mul_toReal_curveAction and its case AbsolutelyContinuousOnInterval.edist_rpow_le_curveAction between the ends of [0, 1], also stated for paths in C([0, 1], X) as AbsolutelyContinuousOnInterval.edist_rpow_le_curveAction_IccExtend.
• TauCeti.curveAction_eq_sum_range: the action splits over the cells of a uniform grid.
• TauCeti.sum_edist_rpow_mul_rpow_one_sub_le_curveAction: the discrete action of the samples at the grid times is at most the action.
• AbsolutelyContinuousOnInterval.lintegral_edist_div_rpow_le_curveAction and AbsolutelyContinuousOnInterval.tendsto_lintegral_edist_div_rpow: the integrated difference quotients are bounded by the action and converge to it.
• TauCeti.absolutelyContinuousOnInterval_of_sum_edist_rpow_le: for 1 < p, a curve satisfying the Hölder estimate on finite unions of intervals is absolutely continuous.
• TauCeti.absolutelyContinuousOnInterval_of_tendsto_of_liminf_ne_top: for 1 < p, pointwise limits of curves with bounded actions are absolutely continuous.
• TauCeti.curveAction_le_liminf and TauCeti.curveAction_le_liminf_of_one_lt: lower semicontinuity of the action under pointwise convergence.
• TauCeti.isClosed_setOfPred_absolutelyContinuousOnInterval_and_curveAction_le: for 1 < p, the absolutely continuous paths of action at most C < ∞ form a closed subset of C([a, b], X).
• TauCeti.measurable_curveAction and TauCeti.measurable_curveAction_IccExtend: measurability of the action in a measurable family of continuous curves and on the path space C([a, b], X).

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.
• H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Springer 2011, Section 8.2.

noncomputable def TauCeti.curveAction {X : Type u_1} [PseudoEMetricSpace X] (p : ℝ) (γ : ℝ → X) (a b : ℝ) : ENNReal

The p-action ∫ |γ'|(t) ^ p dt of a curve γ : ℝ → X over the interval between a and b: the integral of the p-th power of its metric derivative, with no factor 1 / p. When X is a pseudometric space and 1 ≤ p: for a curve absolutely continuous on [a, b] with a ≤ b, the integrated difference quotients converge to it as the step tends to 0⁺ (AbsolutelyContinuousOnInterval.tendsto_lintegral_edist_div_rpow); and it is lower semicontinuous under pointwise convergence on [a, b], along a countably generated filter, of eventually absolutely continuous curves to an absolutely continuous one (TauCeti.curveAction_le_liminf).

theorem TauCeti.curveAction_def {X : Type u_1} [PseudoEMetricSpace X] (p : ℝ) (γ : ℝ → X) (a b : ℝ) : curveAction p γ a b = ∫⁻ (t : ℝ) in Set.uIoc a b, metricDerivative γ t ^ p

The defining formula of the p-action, as an integral of a power of the metric derivative.

theorem Isometry.curveAction_comp {X : Type u_1} [PseudoEMetricSpace X] {Y : Type u_2} [PseudoEMetricSpace Y] {f : X → Y} (hf : Isometry f) (p : ℝ) (γ : ℝ → X) (a b : ℝ) : TauCeti.curveAction p (f ∘ γ) a b = TauCeti.curveAction p γ a b

Post-composing a curve with an isometry leaves its p-action unchanged.

theorem TauCeti.curveAction_comm {X : Type u_1} [PseudoEMetricSpace X] (p : ℝ) (γ : ℝ → X) (a b : ℝ) : curveAction p γ a b = curveAction p γ b a

The p-action does not depend on the orientation of the interval.

@[simp]

theorem TauCeti.curveAction_self {X : Type u_1} [PseudoEMetricSpace X] (p : ℝ) (γ : ℝ → X) (a : ℝ) : curveAction p γ a a = 0

The p-action over a degenerate interval vanishes.

theorem TauCeti.curveAction_mono {X : Type u_1} [PseudoEMetricSpace X] (p : ℝ) (γ : ℝ → X) {a b s u : ℝ} (h : Set.uIoc s u ⊆ Set.uIoc a b) : curveAction p γ s u ≤ curveAction p γ a b

The p-action is monotone in the interval.

theorem TauCeti.curveAction_add {X : Type u_1} [PseudoEMetricSpace X] (p : ℝ) (γ : ℝ → X) {a b c : ℝ} (hb : b ∈ Set.uIcc a c) : curveAction p γ a b + curveAction p γ b c = curveAction p γ a c

The p-action is additive over adjacent intervals.

theorem TauCeti.add_natCast_mul_mem_Icc (a : ℝ) {h : ℝ} (hh : 0 ≤ h) {k N : ℕ} (hk : k ≤ N) : a + ↑k * h ∈ Set.Icc a (a + ↑N * h)

The grid time a + k * h, k ≤ N, of a uniform grid of step h ≥ 0 lies in [a, a + N * h].

theorem TauCeti.Icc_add_natCast_mul_subset_Icc (a : ℝ) {h : ℝ} (hh : 0 ≤ h) {k N : ℕ} (hk : k < N) : Set.Icc (a + ↑k * h) (a + (↑k + 1) * h) ⊆ Set.Icc a (a + ↑N * h)

The cell [a + k * h, a + (k + 1) * h], k < N, of a uniform grid of step h ≥ 0 lies in [a, a + N * h].

theorem TauCeti.curveAction_eq_sum_range {X : Type u_1} [PseudoEMetricSpace X] (p : ℝ) (γ : ℝ → X) (a h : ℝ) (n : ℕ) : curveAction p γ a (a + ↑n * h) = ∑ k ∈ Finset.range n, curveAction p γ (a + ↑k * h) (a + (↑k + 1) * h)

The p-action over [a, a + n * h] is the sum of the actions over the cells [a + k * h, a + (k + 1) * h] of the uniform grid of step h.

theorem LipschitzWith.curveAction_le {X : Type u_1} [PseudoEMetricSpace X] {p : ℝ} {γ : ℝ → X} {K : NNReal} (hγ : LipschitzWith K γ) (hp : 0 ≤ p) (a b : ℝ) : TauCeti.curveAction p γ a b ≤ ↑K ^ p * edist a b

The p-action of a K-Lipschitz curve over the interval between a and b is at most K ^ p times the length of the interval.

theorem TauCeti.measurable_curveAction {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)) (p a b : ℝ) : Measurable fun (x : α) => curveAction p (F x) a b

Measurability of the action 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 x ↦ A_p(F x) is measurable.

theorem TauCeti.measurable_curveAction_IccExtend {X : Type u_1} [PseudoEMetricSpace X] {a b : ℝ} (hab : a ≤ b) (p s u : ℝ) : Measurable fun (γ : C(↑(Set.Icc a b), X)) => curveAction p (Set.IccExtend hab ⇑γ) s u

On the space C([a, b], X) of continuous paths with its Borel structure, the p-action over [s, u] of the path extended by constants outside [a, b] is a measurable function of the path.

theorem AbsolutelyContinuousOnInterval.edist_rpow_le_mul_curveAction {X : Type u_1} [PseudoMetricSpace X] {p : ℝ} {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hp : 1 ≤ p) {s u : ℝ} (hs : s ∈ Set.uIcc a b) (hu : u ∈ Set.uIcc a b) : edist (γ s) (γ u) ^ p ≤ edist s u ^ (p - 1) * TauCeti.curveAction p γ s u

Hölder estimate along a curve: if γ is absolutely continuous on [a, b] and 1 ≤ p, then edist (γ s) (γ u) ^ p ≤ edist s u ^ (p - 1) * curveAction p γ s u for all s, u ∈ [a, b]. In particular a curve of finite p-action with 1 < p is (1 - 1 / p)-Hölder continuous.

theorem AbsolutelyContinuousOnInterval.dist_rpow_le_mul_toReal_curveAction {X : Type u_1} [PseudoMetricSpace X] {p : ℝ} {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hp : 1 ≤ p) {s u : ℝ} (hs : s ∈ Set.uIcc a b) (hu : u ∈ Set.uIcc a b) (hsu : s ≤ u) (hfin : TauCeti.curveAction p γ s u ≠ ⊤) : dist (γ s) (γ u) ^ p ≤ (u - s) ^ (p - 1) * (TauCeti.curveAction p γ s u).toReal

The Hölder estimate with real distances: if γ is absolutely continuous on [a, b], 1 ≤ p, and s ≤ u are points of [a, b] such that the p-action of γ on [s, u] is finite, then dist (γ s) (γ u) ^ p ≤ (u - s) ^ (p - 1) * A_p(γ; s, u).

theorem AbsolutelyContinuousOnInterval.edist_rpow_le_curveAction {X : Type u_1} [PseudoMetricSpace X] {p : ℝ} {γ : ℝ → X} (hγ : AbsolutelyContinuousOnInterval γ 0 1) (hp : 1 ≤ p) : edist (γ 0) (γ 1) ^ p ≤ TauCeti.curveAction p γ 0 1

The Hölder estimate between the ends of [0, 1]: for 1 ≤ p, the p-action of a curve absolutely continuous on [0, 1] is at least d(γ 0, γ 1) ^ p.

theorem AbsolutelyContinuousOnInterval.edist_rpow_le_curveAction_IccExtend {X : Type u_1} [PseudoMetricSpace X] {p : ℝ} {c : C(↑unitInterval, X)} (hc : AbsolutelyContinuousOnInterval (Set.IccExtend ⋯ ⇑c) 0 1) (hp : 1 ≤ p) : edist (c 0) (c 1) ^ p ≤ TauCeti.curveAction p (Set.IccExtend ⋯ ⇑c) 0 1

The Hölder estimate along a path c : C([0, 1], X): for 1 ≤ p, if the extension of c to ℝ is absolutely continuous on [0, 1], then its p-action is at least d(c 0, c 1) ^ p.

theorem TauCeti.sum_edist_rpow_mul_rpow_one_sub_le_curveAction {X : Type u_1} [PseudoMetricSpace X] {p : ℝ} {γ : ℝ → X} {a h : ℝ} {N : ℕ} (hh : 0 < h) (hp : 1 ≤ p) (hγ : AbsolutelyContinuousOnInterval γ a (a + ↑N * h)) : ∑ k ∈ Finset.range N, edist (γ (a + ↑k * h)) (γ (a + (↑k + 1) * h)) ^ p * ENNReal.ofReal h ^ (1 - p) ≤ curveAction p γ a (a + ↑N * h)

The discrete action of grid samples is at most the action. For 1 ≤ p and a curve γ absolutely continuous on [a, a + N * h] with h > 0, the samples at the grid times a + k * h satisfy ∑ k < N, d(γ (a + k * h), γ (a + (k + 1) * h)) ^ p * h ^ (1 - p) ≤ A_p(γ), by the Hölder estimate on each cell. The left side is the action of the polygonal interpolation of the samples (TauCeti.curveAction_eq_sum_edist_rpow_mul_rpow_one_sub_of_eqOn_polygonalInterpolation).

theorem AbsolutelyContinuousOnInterval.lintegral_edist_div_rpow_le_curveAction {X : Type u_1} [PseudoMetricSpace X] {p : ℝ} {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hp : 1 ≤ p) {h : ℝ} (hh : 0 < h) : ∫⁻ (t : ℝ) in Set.Ioc a (b - h), (edist (γ t) (γ (t + h)) / ENNReal.ofReal h) ^ p ≤ TauCeti.curveAction p γ a b

The integrated p-th power of the difference quotients of an absolutely continuous curve over a step h > 0 is at most its p-action, for 1 ≤ p.

theorem AbsolutelyContinuousOnInterval.tendsto_lintegral_edist_div_rpow {X : Type u_1} [PseudoMetricSpace X] {p : ℝ} {γ : ℝ → X} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (hp : 1 ≤ p) (hab : a ≤ b) : Filter.Tendsto (fun (h : ℝ) => ∫⁻ (t : ℝ) in Set.Ioc a (b - h), (edist (γ t) (γ (t + h)) / ENNReal.ofReal h) ^ p) (nhdsWithin 0 (Set.Ioi 0)) (nhds (TauCeti.curveAction p γ a b))

Difference-quotient formula for the action. For a curve γ absolutely continuous on [a, b] and 1 ≤ p, the integrated p-th powers of the difference quotients ∫⁻ t in Ioc a (b - h), (edist (γ t) (γ (t + h)) / h) ^ p converge to the p-action of γ as h → 0⁺.

theorem TauCeti.absolutelyContinuousOnInterval_of_sum_edist_rpow_le {X : Type u_1} [PseudoMetricSpace X] {p : ℝ} {γ : ℝ → X} {a b : ℝ} (hp : 1 < p) {C : ENNReal} (hC : C ≠ ⊤) (h : ∀ E ∈ AbsolutelyContinuousOnInterval.disjWithin a b, (∑ i ∈ Finset.range E.1, edist (γ (E.2 i).1) (γ (E.2 i).2)) ^ p ≤ MeasureTheory.volume (⋃ i ∈ Finset.range E.1, Set.uIoc (E.2 i).1 (E.2 i).2) ^ (p - 1) * C) : AbsolutelyContinuousOnInterval γ a b

A criterion for absolute continuity. For 1 < p, a curve γ is absolutely continuous on [a, b] if, for some finite C, every finite disjoint family of intervals in [a, b] satisfies the Hölder-type bound (∑ d(γ sᵢ, γ tᵢ)) ^ p ≤ |⋃ (sᵢ, tᵢ]| ^ (p - 1) * C, as a curve of p-action at most C does.

theorem TauCeti.absolutelyContinuousOnInterval_of_tendsto_of_liminf_ne_top {X : Type u_1} [PseudoMetricSpace X] {p : ℝ} {γ : ℝ → X} {a b : ℝ} {ι : Type u_2} {l : Filter ι} {γs : ι → ℝ → X} (hp : 1 < p) (hγs : ∀ᶠ (i : ι) in l, AbsolutelyContinuousOnInterval (γs i) a b) (hlim : ∀ t ∈ Set.uIcc a b, Filter.Tendsto (fun (i : ι) => γs i t) l (nhds (γ t))) (hA : Filter.liminf (fun (i : ι) => curveAction p (γs i) a b) l ≠ ⊤) : AbsolutelyContinuousOnInterval γ a b

For 1 < p, a pointwise limit on [a, b] of curves γs i, eventually absolutely continuous on [a, b], whose p-actions have finite lower limit is absolutely continuous on [a, b].

theorem TauCeti.curveAction_le_liminf {X : Type u_1} [PseudoMetricSpace X] {p : ℝ} {γ : ℝ → X} {a b : ℝ} {ι : Type u_2} {l : Filter ι} {γs : ι → ℝ → X} [l.IsCountablyGenerated] (hp : 1 ≤ p) (hγs : ∀ᶠ (i : ι) in l, AbsolutelyContinuousOnInterval (γs i) a b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hlim : ∀ t ∈ Set.uIcc a b, Filter.Tendsto (fun (i : ι) => γs i t) l (nhds (γ t))) : curveAction p γ a b ≤ Filter.liminf (fun (i : ι) => curveAction p (γs i) a b) l

Lower semicontinuity of the action. If curves γs i, eventually absolutely continuous on [a, b], converge pointwise on [a, b] along a countably generated filter to a curve γ absolutely continuous on [a, b], then the p-action of γ is at most the lower limit of their p-actions, for 1 ≤ p.

theorem TauCeti.curveAction_le_liminf_of_one_lt {X : Type u_1} [PseudoMetricSpace X] {p : ℝ} {γ : ℝ → X} {a b : ℝ} {ι : Type u_2} {l : Filter ι} {γs : ι → ℝ → X} [l.IsCountablyGenerated] (hp : 1 < p) (hγs : ∀ᶠ (i : ι) in l, AbsolutelyContinuousOnInterval (γs i) a b) (hlim : ∀ t ∈ Set.uIcc a b, Filter.Tendsto (fun (i : ι) => γs i t) l (nhds (γ t))) : curveAction p γ a b ≤ Filter.liminf (fun (i : ι) => curveAction p (γs i) a b) l

Lower semicontinuity of the action for 1 < p: if curves γs i, eventually absolutely continuous on [a, b], converge pointwise on [a, b] along a countably generated filter to γ, then the p-action of γ is at most the lower limit of their p-actions. When that lower limit is finite, γ is absolutely continuous by TauCeti.absolutelyContinuousOnInterval_of_tendsto_of_liminf_ne_top.

theorem TauCeti.isClosed_setOfPred_absolutelyContinuousOnInterval_and_curveAction_le {X : Type u_1} [PseudoMetricSpace X] {p a b : ℝ} (hab : a ≤ b) (hp : 1 < p) {C : ENNReal} (hC : C ≠ ⊤) : IsClosed {γ : C(↑(Set.Icc a b), X) | AbsolutelyContinuousOnInterval (Set.IccExtend hab ⇑γ) a b ∧ curveAction p (Set.IccExtend hab ⇑γ) a b ≤ C}

Closedness of action sublevels in path space. For 1 < p and C ≠ ∞, the paths in C([a, b], X) that are absolutely continuous on [a, b] with p-action at most C form a closed set for the uniform topology. The bound C ≠ ∞ is needed: uniform limits of absolutely continuous paths need not be absolutely continuous.