Polygonal laws on paths through an absolutely continuous curve of laws

Let E be a separable Banach space, 1 ≤ p < ∞, and let μ be a curve in the finite-moment Wasserstein space P_p(E), absolutely continuous on [a, b]. For every number N ≥ 1 of steps this file constructs a probability measure η on the path space C([a, b], E), concentrated on absolutely continuous paths, such that

• at each grid time t_k = a + k * (b - a) / N, the law of γ t_k under η is μ t_k;
• the expected p-action of the paths is at most the p-action of the curve μ: ∫ A_p(γ) dη(γ) ≤ A_p(μ).

The construction glues optimal couplings of consecutive laws μ t_k and μ t_(k+1) into a law on sequences (TauCeti.Measure.chainMeasure) and pushes it forward along the polygonal interpolation of a sequence on the grid (TauCeti.polygonalInterpolation). The expected action of the interpolated paths is the expected discrete action ∑ k < N, W_p(μ t_k, μ t_(k+1)) ^ p * h ^ (1 - p), with step h = (b - a) / N, and Hölder's inequality bounds each term by the action of μ over [t_k, t_(k+1)], because W_p(μ t_k, μ t_(k+1)) ≤ ∫_(t_k)^(t_(k+1)) |μ'|.

These are the approximating laws in Lisini's superposition principle: along dyadic grids their time marginals are eventually fixed at every dyadic time and their expected actions stay bounded by A_p(μ), which for 1 < p makes the family tight, by the tightness criterion for laws of curves with bounded expected action. The linear structure of E is used only to interpolate between consecutive points.

Main results

• TauCeti.exists_map_IccExtend_eq_lintegral_curveAction_le: the polygonal law on paths with prescribed time marginals on the grid and expected action at most that of μ.

References

• S. Lisini, Characterization of absolutely continuous curves in Wasserstein spaces, Calc. Var. Partial Differential Equations 28 (2007), 85--120, proof of Theorem 5.
• L. Ambrosio, N. Gigli and G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd ed., Birkhäuser 2008, §8.2.

theorem TauCeti.exists_map_IccExtend_eq_lintegral_curveAction_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) {μ : ℝ → WassersteinSpace p E} {a b : ℝ} (hab : a < b) (hμ : AbsolutelyContinuousOnInterval μ a b) {N : ℕ} (hN : N ≠ 0) : ∃ (η : MeasureTheory.Measure C(↑(Set.Icc a b), E)), MeasureTheory.IsProbabilityMeasure η ∧ (∀ᵐ (γ : C(↑(Set.Icc a b), E)) ∂η, AbsolutelyContinuousOnInterval (Set.IccExtend ⋯ ⇑γ) a b) ∧ (∀ k ≤ N, MeasureTheory.Measure.map (fun (γ : C(↑(Set.Icc a b), E)) => Set.IccExtend ⋯ (⇑γ) (a + ↑k * ((b - a) / ↑N))) η = ↑↑(μ (a + ↑k * ((b - a) / ↑N)))) ∧ ∫⁻ (γ : C(↑(Set.Icc a b), E)), curveAction p.toReal (Set.IccExtend ⋯ ⇑γ) a b ∂η ≤ curveAction p.toReal μ a b

Polygonal laws on paths through an absolutely continuous curve of laws. Let E be a separable Banach space, 1 ≤ p < ∞, and let μ be a curve in P_p(E) absolutely continuous on [a, b], with a < b. For every N ≠ 0 there is a probability measure η on C([a, b], E), concentrated on absolutely continuous paths, whose law at each grid time a + k * ((b - a) / N), k ≤ N, is the value of μ there, and whose expected p-action is at most the p-action of μ over [a, b].