The action of a limit of piecewise constant interpolants

Implicit time discretizations, such as the minimizing movement scheme for gradient flows, produce for a time step τ > 0 a sequence of points U 0, U 1, U 2, …, and the piecewise constant interpolant t ↦ U ⌈t / τ⌉₊. Its discrete p-action up to time T is

∑_{n < ⌈T / τ⌉₊} d(U n, U (n + 1)) ^ p / τ ^ (p - 1),

that is, the sum of τ (d(U n, U (n + 1)) / τ) ^ p: the p-action of the curve that would cover each step at constant speed in time τ. The interpolants are not continuous, so the lower semicontinuity of the action under pointwise convergence of absolutely continuous curves (TauCeti.curveAction_le_liminf) does not apply to them. This file proves its discrete counterpart: if the interpolants for time steps τ i → 0 converge to a curve u on [0, T], in the weak sense that

d(u s, u t) ≤ liminf_i d(U i ⌈s / τ i⌉₊, U i ⌈t / τ i⌉₊)

for all s, t ∈ [0, T], and their discrete p-actions have finite lower limit, for an exponent 1 < p, then u is absolutely continuous on [0, T] and its p-action is at most that lower limit. The weak form of convergence covers convergence for a topology weaker than that of the metric, for which the distance is lower semicontinuous, as for narrow convergence of probability measures and the Wasserstein distance. The discrete sequences may take values in a different weak extended pseudometric space from the pseudometric space of the limit curve; the comparison of distances is the only relation required between the two carriers. Positivity of the time steps is required only eventually along the convergence filter.

Both results rest on the discrete Hölder estimate: the distance between the interpolant at times s ≤ t is at most the sum of the steps taken in between, of which there are at most (t - s) / τ + 1, so that d(U ⌈s / τ⌉₊, U ⌈t / τ⌉₊) ^ p ≤ ((t - s) / τ + 1) ^ (p - 1) times the sum of the p-th powers of these steps. Summed over a disjoint family of intervals this gives the bound of TauCeti.absolutelyContinuousOnInterval_of_sum_edist_rpow_le, up to an error that vanishes with τ; integrated over the windows [t, t + h] it bounds the difference quotients of the action formula AbsolutelyContinuousOnInterval.tendsto_lintegral_edist_div_rpow.

Main results

• TauCeti.sum_edist_ceil_div_rpow_le: the discrete Hölder estimate for a disjoint family of intervals in [0, T].
• TauCeti.absolutelyContinuousOnInterval_of_liminf_sum_edist_rpow_ne_top: a limit of piecewise constant interpolants with bounded discrete p-actions is absolutely continuous.
• TauCeti.curveAction_le_liminf_sum_edist_rpow: its p-action is at most the lower limit of the discrete p-actions.
• TauCeti.curveAction_div_two_le_liminf_sum_edist_sq_div: half its quadratic action is at most the lower limit of the accumulated squared-distance penalties.

References

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

theorem TauCeti.sum_edist_ceil_div_rpow_le {X : Type u_1} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {p : ℝ} {τ : NNReal} {U : ℕ → X} (hp : 1 ≤ p) (hτ : 0 < τ) {T : ℝ} (hT : 0 ≤ T) {E : ℕ × (ℕ → ℝ × ℝ)} (hE : E ∈ AbsolutelyContinuousOnInterval.disjWithin 0 T) : (∑ i ∈ Finset.range E.1, edist (U ⌈(E.2 i).1 / ↑τ⌉₊) (U ⌈(E.2 i).2 / ↑τ⌉₊)) ^ p ≤ (MeasureTheory.volume (⋃ i ∈ Finset.range E.1, Set.uIoc (E.2 i).1 (E.2 i).2) + ↑E.1 * ↑τ) ^ (p - 1) * ∑ n ∈ Finset.range ⌈T / ↑τ⌉₊, edist (U n) (U (n + 1)) ^ p / ↑τ ^ (p - 1)

Discrete Hölder estimate for a disjoint family of intervals (sᵢ, tᵢ] in [0, T]: the p-th power of the sum of the distances between the piecewise constant interpolant at times sᵢ and tᵢ is at most (|⋃ (sᵢ, tᵢ]| + k τ) ^ (p - 1) times the discrete p-action up to time T, where k is the number of intervals. As τ → 0 the factor tends to the one in the Hölder estimate AbsolutelyContinuousOnInterval.edist_rpow_le_mul_curveAction for curves.

theorem TauCeti.absolutelyContinuousOnInterval_of_liminf_sum_edist_rpow_ne_top {X : Type u_1} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {p : ℝ} {Y : Type u_2} {ι : Type u_3} {l : Filter ι} {τ : ι → NNReal} {U : ι → ℕ → X} {u : ℝ → Y} {T : ℝ} [PseudoMetricSpace Y] (hp : 1 < p) (hτ : ∀ᶠ (i : ι) in l, 0 < τ i) (hτ0 : Filter.Tendsto τ l (nhds 0)) (hT : 0 ≤ T) (hu : ∀ s ∈ Set.Icc 0 T, ∀ t ∈ Set.Icc 0 T, edist (u s) (u t) ≤ Filter.liminf (fun (i : ι) => edist (U i ⌈s / ↑(τ i)⌉₊) (U i ⌈t / ↑(τ i)⌉₊)) l) (hS : Filter.liminf (fun (i : ι) => ∑ n ∈ Finset.range ⌈T / ↑(τ i)⌉₊, edist (U i n) (U i (n + 1)) ^ p / ↑(τ i) ^ (p - 1)) l ≠ ⊤) : AbsolutelyContinuousOnInterval u 0 T

Absolute continuity of a limit of piecewise constant interpolants. Let U i be sequences of points in a weak extended pseudometric space with eventually positive time steps tending to 0, and let u be a curve in a possibly different pseudometric space with d(u s, u t) ≤ liminf_i d(U i ⌈s / τ i⌉₊, U i ⌈t / τ i⌉₊) for all s, t ∈ [0, T]. If the discrete p-actions ∑_{n < ⌈T / τ i⌉₊} d(U i n, U i (n + 1)) ^ p / τ i ^ (p - 1) have finite lower limit, for an exponent 1 < p, then u is absolutely continuous on [0, T].

theorem TauCeti.curveAction_le_liminf_sum_edist_rpow {X : Type u_1} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {p : ℝ} {Y : Type u_2} {ι : Type u_3} {l : Filter ι} {τ : ι → NNReal} {U : ι → ℕ → X} {u : ℝ → Y} {T : ℝ} [PseudoMetricSpace Y] [l.IsCountablyGenerated] (hp : 1 < p) (hτ : ∀ᶠ (i : ι) in l, 0 < τ i) (hτ0 : Filter.Tendsto τ l (nhds 0)) (hT : 0 ≤ T) (hu : ∀ s ∈ Set.Icc 0 T, ∀ t ∈ Set.Icc 0 T, edist (u s) (u t) ≤ Filter.liminf (fun (i : ι) => edist (U i ⌈s / ↑(τ i)⌉₊) (U i ⌈t / ↑(τ i)⌉₊)) l) : curveAction p u 0 T ≤ Filter.liminf (fun (i : ι) => ∑ n ∈ Finset.range ⌈T / ↑(τ i)⌉₊, edist (U i n) (U i (n + 1)) ^ p / ↑(τ i) ^ (p - 1)) l

Lower semicontinuity of the action along piecewise constant interpolants. Let U i be sequences of points in a weak extended pseudometric space with eventually positive time steps tending to 0 along a countably generated filter, and let u be a curve in a possibly different pseudometric space with d(u s, u t) ≤ liminf_i d(U i ⌈s / τ i⌉₊, U i ⌈t / τ i⌉₊) for all s, t ∈ [0, T]. Then for 1 < p the p-action of u over [0, T] is at most the lower limit of the discrete p-actions ∑_{n < ⌈T / τ i⌉₊} d(U i n, U i (n + 1)) ^ p / τ i ^ (p - 1). When this lower limit is finite, u is absolutely continuous on [0, T] by TauCeti.absolutelyContinuousOnInterval_of_liminf_sum_edist_rpow_ne_top.

theorem TauCeti.curveAction_div_two_le_liminf_sum_edist_sq_div {X : Type u_1} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {Y : Type u_2} {ι : Type u_3} {l : Filter ι} {τ : ι → NNReal} {U : ι → ℕ → X} {u : ℝ → Y} {T : ℝ} [PseudoMetricSpace Y] [l.IsCountablyGenerated] (hτ : ∀ᶠ (i : ι) in l, 0 < τ i) (hτ0 : Filter.Tendsto τ l (nhds 0)) (hT : 0 ≤ T) (hu : ∀ s ∈ Set.Icc 0 T, ∀ t ∈ Set.Icc 0 T, edist (u s) (u t) ≤ Filter.liminf (fun (i : ι) => edist (U i ⌈s / ↑(τ i)⌉₊) (U i ⌈t / ↑(τ i)⌉₊)) l) : curveAction 2 u 0 T / 2 ≤ Filter.liminf (fun (i : ι) => ∑ n ∈ Finset.range ⌈T / ↑(τ i)⌉₊, edist (U i n) (U i (n + 1)) ^ 2 / (2 * ↑(τ i))) l

Action bound by accumulated penalties. Along eventually positive time steps tending to zero, half the quadratic action of a limit curve is bounded by the lower limit of the accumulated penalties of the piecewise constant interpolants. Only the lower-limit bound on pairwise distances is required, not the minimizing movement property.