The continuity equation along the linear interpolation of a map

Let μ be a finite measure on a finite-dimensional real normed space E and T : E → E a measurable map, for instance a transport map from μ to its image law T₊ μ. Moving each point x at constant speed along the segment from x to T x gives the curve of laws

μₜ = (Fₜ)₊ μ, where Fₜ x = (1 - t) • x + t • T x,

from μ₀ = μ to μ₁ = T₊ μ. When μ and T₊ μ are probability laws of finite p-th moment and the graph plan of T is an optimal coupling for W_p, these laws trace a geodesic segment of P_p (E) (TauCeti.WassersteinSpace.exists_isGeodesicSegment_map_smul_add_smul). This file describes the curve in Eulerian terms. It is the displacement interpolation of the graph plan of T, so apart from the description of the barycentric velocity as a conditional expectation, the results are the case π = graphPlan T μ of those for plans (TauCeti.exists_isContinuityEquation_map_smul_fst_add_smul_snd_of_injOn and its companions).

If the displacement T x - x has finite first moment, then μₜ solves the continuity equation on (0, 1) with the barycentric velocity vₜ y = E_μ [T X - X | Fₜ X = y], the average displacement of the particles found at y at time t. Precisely, v evaluated at (t, Fₜ x) is the conditional expectation of T x - x given (t, Fₜ x), for the measure dt ⊗ μ on (0, 1) × E. Its p-action is at most the p-th moment of the displacement, ∫₀¹ ∫ ‖vₜ‖ ^ p dμₜ dt ≤ ∫ ‖T x - x‖ ^ p dμ for every p ≥ 1.

If moreover no two particles meet at the same time and place once a dt ⊗ μ-null set of times and particles is discarded (for instance if almost every Fₜ is injective on a measurable set carrying μ), then no averaging takes place: vₜ (Fₜ x) = T x - x for almost every t ∈ (0, 1) and μ-almost every x, and the p-action of v equals the p-th moment of the displacement for every exponent p.

These curves are the map-induced competitors in the Benamou–Brenier formula: when the graph plan of T is optimal for the cost ‖x - y‖ ^ p, the p-th moment of the displacement is W_p (μ, T₊ μ) ^ p, so the action of the barycentric velocity is at most W_p (μ, T₊ μ) ^ p. If moreover E is strictly convex and 1 < p < ∞, optimality rules out crossings: the optimal plan is concentrated on a cyclically monotone set, on which every intermediate interpolating map Fₜ is injective (TauCeti.IsCyclicallyMonotone.injOn_smul_add_smul). The velocity is then the displacement itself and the action bound is an equality, ∫₀¹ ∫ ‖vₜ‖ ^ p dμₜ dt = W_p (μ, T₊ μ) ^ p.

Main results

• TauCeti.exists_isContinuityEquation_map_smul_add_smul: the linear interpolation of a map with displacement of finite first moment solves the continuity equation with its barycentric velocity, whose p-action is at most the p-th moment of the displacement.
• TauCeti.exists_isContinuityEquation_map_smul_add_smul_of_injOn: when for every t the interpolating map Fₜ is injective on the fibre at t of a measurable set of full dt ⊗ μ measure, the velocity field is the displacement read along the interpolation, and its p-action equals the p-th moment of the displacement.
• TauCeti.exists_isContinuityEquation_map_smul_add_smul_of_ae_injOn: the special case in which almost every interpolating map is injective on one measurable set carrying μ.
• TauCeti.exists_isContinuityEquation_map_smul_add_smul_of_isOptimalCoupling: on a strictly convex space and for 1 < p < ∞, if the graph plan of T is optimal for the cost d(x, y) ^ p at finite Wasserstein distance, the velocity field is the displacement read along the interpolation, and its p-action is W_p (μ, T₊ μ) ^ p.

References

• J.-D. Benamou and Y. Brenier, A computational fluid mechanics solution to the Monge–Kantorovich mass transfer problem, Numer. Math. 84 (2000), 375--393.
• L. Ambrosio, N. Gigli and G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, Birkhäuser, 2nd ed. 2008, §8.1 and §8.3.

theorem TauCeti.exists_isContinuityEquation_map_smul_add_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {T : E → E} (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasure μ] (hT : Measurable T) (hint : ∫⁻ (x : E), ‖T x - x‖ₑ ∂μ < ⊤) : ∃ (v : ℝ → E → E), IsContinuityEquation (fun (t : ℝ) => MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • T x) μ) v 0 1 ∧ (fun (q : ℝ × E) => v q.1 ((1 - q.1) • q.2 + q.1 • T q.2)) = ((MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod μ)[fun (q : ℝ × E) => T q.2 - q.2 | MeasurableSpace.comap (fun (q : ℝ × E) => (q.1, (1 - q.1) • q.2 + q.1 • T q.2)) inferInstance] ∧ ∀ (p : ℝ), 1 ≤ p → ∫⁻ (t : ℝ) in Set.Ioo 0 1, ∫⁻ (y : E), ‖v t y‖ₑ ^ p ∂MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • T x) μ ≤ ∫⁻ (x : E), ‖T x - x‖ₑ ^ p ∂μ

The continuity equation along the linear interpolation of a map. Let μ be a finite measure on E and T a measurable map whose displacement T x - x has finite first moment. Then the laws μₜ of (1 - t) • x + t • T x under μ solve the continuity equation on (0, 1) with the barycentric velocity v: its value at (t, (1 - t) • x + t • T x) is the conditional expectation of the displacement T x - x given the time t and the position (1 - t) • x + t • T x, for the measure dt ⊗ μ on (0, 1) × E. For every p ≥ 1 its p-action is at most the p-th moment of the displacement: ∫₀¹ ∫ ‖vₜ‖ ^ p dμₜ dt ≤ ∫ ‖T x - x‖ ^ p dμ.

theorem TauCeti.exists_isContinuityEquation_map_smul_add_smul_of_injOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {T : E → E} (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasure μ] (hT : Measurable T) (hint : ∫⁻ (x : E), ‖T x - x‖ₑ ∂μ < ⊤) {A : Set (ℝ × E)} (hA : MeasurableSet A) (hAμ : ∀ᵐ (q : ℝ × E) ∂(MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod μ, q ∈ A) (hinj : ∀ (t : ℝ), Set.InjOn (fun (x : E) => (1 - t) • x + t • T x) {x : E | (t, x) ∈ A}) : ∃ (v : ℝ → E → E), IsContinuityEquation (fun (t : ℝ) => MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • T x) μ) v 0 1 ∧ (∀ᵐ (t : ℝ), t ∈ Set.Ioo 0 1 → ∀ᵐ (x : E) ∂μ, v t ((1 - t) • x + t • T x) = T x - x) ∧ ∀ (p : ℝ), ∫⁻ (t : ℝ) in Set.Ioo 0 1, ∫⁻ (y : E), ‖v t y‖ₑ ^ p ∂MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • T x) μ = ∫⁻ (x : E), ‖T x - x‖ₑ ^ p ∂μ

The velocity along an injective linear interpolation. Let μ be a finite measure on E and T a measurable map whose displacement T x - x has finite first moment, and let A be a measurable set of times and particles carrying dt ⊗ μ on (0, 1) × E such that for every t the map x ↦ (1 - t) • x + t • T x is injective on the particles x with (t, x) ∈ A. Then the laws μₜ of (1 - t) • x + t • T x under μ solve the continuity equation on (0, 1) with a velocity field v equal to the displacement along the interpolation: vₜ ((1 - t) • x + t • T x) = T x - x for almost every t ∈ (0, 1) and μ-almost every x. Consequently, for every exponent p the p-action of v is the p-th moment of the displacement: ∫₀¹ ∫ ‖vₜ‖ ^ p dμₜ dt = ∫ ‖T x - x‖ ^ p dμ.

theorem TauCeti.exists_isContinuityEquation_map_smul_add_smul_of_ae_injOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {T : E → E} (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasure μ] (hT : Measurable T) (hint : ∫⁻ (x : E), ‖T x - x‖ₑ ∂μ < ⊤) {S : Set E} (hS : MeasurableSet S) (hSμ : ∀ᵐ (x : E) ∂μ, x ∈ S) (hinj : ∀ᵐ (t : ℝ), t ∈ Set.Ioo 0 1 → Set.InjOn (fun (x : E) => (1 - t) • x + t • T x) S) : ∃ (v : ℝ → E → E), IsContinuityEquation (fun (t : ℝ) => MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • T x) μ) v 0 1 ∧ (∀ᵐ (t : ℝ), t ∈ Set.Ioo 0 1 → ∀ᵐ (x : E) ∂μ, v t ((1 - t) • x + t • T x) = T x - x) ∧ ∀ (p : ℝ), ∫⁻ (t : ℝ) in Set.Ioo 0 1, ∫⁻ (y : E), ‖v t y‖ₑ ^ p ∂MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • T x) μ = ∫⁻ (x : E), ‖T x - x‖ₑ ^ p ∂μ

The velocity along a linear interpolation injective on a fixed set. The special case of exists_isContinuityEquation_map_smul_add_smul_of_injOn in which, for almost every t ∈ (0, 1), the map x ↦ (1 - t) • x + t • T x is injective on one measurable set S carrying μ: then vₜ ((1 - t) • x + t • T x) = T x - x for almost every t ∈ (0, 1) and μ-almost every x, and for every exponent p the p-action of v is the p-th moment of the displacement.

theorem TauCeti.exists_isContinuityEquation_map_smul_add_smul_of_isOptimalCoupling {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {T : E → E} [StrictConvexSpace ℝ E] (μ : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasure μ] {ν : MeasureTheory.Measure E} (hT : Measurable T) {p : ENNReal} (hp : 1 < p) (hp_top : p ≠ ⊤) (hopt : IsOptimalCoupling (fun (z : E × E) => edist z.1 z.2 ^ p.toReal) (graphPlan T μ) μ ν) (hfin : wassersteinEDist p μ ν ≠ ⊤) : ∃ (v : ℝ → E → E), IsContinuityEquation (fun (t : ℝ) => MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • T x) μ) v 0 1 ∧ (∀ᵐ (t : ℝ), t ∈ Set.Ioo 0 1 → ∀ᵐ (x : E) ∂μ, v t ((1 - t) • x + t • T x) = T x - x) ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 1, ∫⁻ (y : E), ‖v t y‖ₑ ^ p.toReal ∂MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • T x) μ = wassersteinEDist p μ ν ^ p.toReal

The velocity along an optimal linear interpolation. Let E be strictly convex, let 1 < p < ∞, and let μ be a finite measure on E and T a measurable map whose graph plan is an optimal coupling of μ and ν for the cost d(x, y) ^ p, at finite Wasserstein distance W_p (μ, ν). Then the laws μₜ of (1 - t) • x + t • T x under μ solve the continuity equation on (0, 1) with a velocity field v equal to the displacement along the interpolation, vₜ ((1 - t) • x + t • T x) = T x - x for almost every t ∈ (0, 1) and μ-almost every x, and the p-action of v is the p-th power of the Wasserstein distance: ∫₀¹ ∫ ‖vₜ‖ ^ p dμₜ dt = W_p (μ, ν) ^ p.

The optimal plan is concentrated on its support, which is cyclically monotone, and transport segments between points of a cyclically monotone set do not cross (TauCeti.IsCyclicallyMonotone.injOn_smul_add_smul), so no averaging takes place.