Lisini's superposition principle

Let X be a complete separable metric space and 1 < p < ∞. A curve μ in the finite-moment Wasserstein space P_p(X) that is absolutely continuous on [a, b] with finite p-action A_p(μ) is the curve of time marginals of a law on paths: there is a probability measure η on the path space C([a, b], X), concentrated on absolutely continuous paths, such that

• the law of γ t under η is μ t for every t ∈ [a, b];
• the expected p-action of the paths is the p-action of the curve, ∫ A_p(γ) dη = A_p(μ);
• the averaged speed of the paths is the metric speed of the curve, |μ'|(t) ^ p = ∫ |γ'|(t) ^ p dη(γ) for almost every t ∈ [a, b].

Every law on absolutely continuous paths with time marginals μ has expected action at least A_p(μ) (TauCeti.curveAction_le_lintegral_of_coe_eq_map_IccExtend), so η is a representation of minimal action.

The theorem is first proved in a separable Banach space E. There η is a narrow limit of the polygonal laws on the dyadic grids of [a, b] (TauCeti.exists_map_IccExtend_eq_lintegral_curveAction_le), whose expected actions are at most A_p(μ) and whose time marginals at each dyadic time are eventually the value of μ there. For 1 < p this family is tight (isTightMeasureSet_of_map_eval_of_absolutelyContinuousOnInterval_of_lintegral_curveAction_le), and the laws concentrated on absolutely continuous paths with expected action at most A_p(μ) form a weakly closed set (isClosed_setOfPred_ae_absolutelyContinuousOnInterval_and_lintegral_le), so Prokhorov's theorem provides a limit law with the same properties. Its time marginals agree with μ at the dyadic times, hence everywhere on [a, b] by continuity.

A complete separable metric space X embeds isometrically, as a closed subset, into a separable Banach space E (TauCeti.exists_isometry_separableSpace_completeSpace). Pushforward along the embedding is an isometry of Wasserstein spaces, so it carries μ to a curve in P_p(E) with the same metric derivative and action. The law on paths in E that represents this curve is concentrated on paths with values in the closed image of X, because its time marginals are, and so it is the image of a law on C([a, b], X), which represents μ.

Main results

• TauCeti.exists_map_IccExtend_eq_lintegral_curveAction_eq: Lisini's superposition principle in a complete separable metric space.

References

• S. Lisini, Characterization of absolutely continuous curves in Wasserstein spaces, Calc. Var. Partial Differential Equations 28 (2007), 85--120, 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, Theorem 8.2.1, for the Euclidean case.

theorem TauCeti.exists_map_IccExtend_eq_lintegral_curveAction_eq {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] [CompleteSpace X] {p : ENNReal} [Fact (1 ≤ p)] (hp1 : 1 < p) (hp : p ≠ ⊤) {μ : ℝ → WassersteinSpace p X} {a b : ℝ} (hab : a < b) (hμ : AbsolutelyContinuousOnInterval μ a b) (hA : curveAction p.toReal μ a b ≠ ⊤) : ∃ (η : MeasureTheory.Measure C(↑(Set.Icc a b), X)), MeasureTheory.IsProbabilityMeasure η ∧ (∀ᵐ (γ : C(↑(Set.Icc a b), X)) ∂η, AbsolutelyContinuousOnInterval (Set.IccExtend ⋯ ⇑γ) a b) ∧ (∀ t ∈ Set.Icc a b, MeasureTheory.Measure.map (fun (γ : C(↑(Set.Icc a b), X)) => Set.IccExtend ⋯ (⇑γ) t) η = ↑↑(μ t)) ∧ ∫⁻ (γ : C(↑(Set.Icc a b), X)), curveAction p.toReal (Set.IccExtend ⋯ ⇑γ) a b ∂η = curveAction p.toReal μ a b ∧ ∀ᵐ (t : ℝ), t ∈ Set.Icc a b → metricDerivative μ t ^ p.toReal = ∫⁻ (γ : C(↑(Set.Icc a b), X)), metricDerivative (Set.IccExtend ⋯ ⇑γ) t ^ p.toReal ∂η

Lisini's superposition principle in a complete separable metric space. Let 1 < p < ∞ and let μ be a curve in P_p(X), absolutely continuous on [a, b] with finite p-action, where a < b. There is a probability measure η on C([a, b], X), concentrated on absolutely continuous paths, whose law at each time t ∈ [a, b] is μ t, whose expected p-action is the p-action of μ, and whose averaged speed is the metric speed of μ: |μ'|(t) ^ p = ∫ |γ'|(t) ^ p dη at almost every t ∈ [a, b].