The continuity equation along the displacement interpolation of a plan

Let π be a finite measure on E × E, where E is a finite-dimensional real normed space, for instance a coupling of two laws μ and ν. Moving the mass of each pair (x, y) at constant speed along the segment from x to y gives the curve of laws

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

from μ₀ = π.fst to μ₁ = π.snd. When 1 ≤ p, both marginals are probability measures with finite p-th moment, and π is an optimal coupling for W_p, this is the displacement interpolation of μ and ν, a geodesic segment of P_p (E) (TauCeti.WassersteinSpace.exists_isGeodesicSegment_map_smul_add_smul). This file describes the curve in Eulerian terms. Unlike the linear interpolation of a map (TauCeti.exists_isContinuityEquation_map_smul_add_smul), no transport map is needed: the mass at a point may split, so the statements cover every source law, atoms included.

If the displacement y - x has finite first moment under π, then μₜ solves the continuity equation on (0, 1) with the barycentric velocity vₜ w = E_π [Y - X | Fₜ (X, Y) = w], the average displacement of the pairs whose interpolating point at time t is w. Its p-action is at most the p-th moment of the displacement, ∫₀¹ ∫ ‖vₜ‖ ^ p dμₜ dt ≤ ∫ ‖y - x‖ ^ p dπ for every p ≥ 1.

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

For an optimal coupling of μ and ν at finite Wasserstein distance W_p (μ, ν), with 1 ≤ p < ∞, the p-th moment of the displacement is W_p (μ, ν) ^ p, so the displacement interpolation solves the continuity equation with action at most W_p (μ, ν) ^ p: this is the upper bound in the Benamou–Brenier formula W_p (μ, ν) ^ p = inf ∫₀¹ ∫ ‖vₜ‖ ^ p dμₜ dt, over the solutions of the continuity equation joining μ to ν. If E is strictly convex and 1 < p, an optimal coupling is concentrated on its support, which is cyclically monotone, and the segments joining the pairs of a cyclically monotone set do not cross (TauCeti.IsCyclicallyMonotone.injOn_smul_add_smul). The velocity is then the displacement itself and the action is exactly W_p (μ, ν) ^ p. Combined with the lower bound W_p (μ, ν) ^ p ≤ ∫₀¹ ∫ ‖vₜ‖ ^ p dμₜ dt for every solution joining μ to ν (TauCeti.IsContinuityEquation.wassersteinEDist_rpow_le), this makes the displacement interpolation a minimiser in the Benamou–Brenier formula (TauCeti.isLeast_lintegral_isContinuityEquation).

Main results

• TauCeti.exists_isContinuityEquation_map_smul_fst_add_smul_snd: the displacement interpolation of a plan whose displacement has 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_fst_add_smul_snd_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_fst_add_smul_snd_of_ae_injOn: the special case in which almost every interpolating map is injective on one measurable set carrying the plan.
• TauCeti.exists_isContinuityEquation_map_smul_fst_add_smul_snd_of_isOptimalCoupling_le: for 1 ≤ p < ∞, the displacement interpolation of an optimal coupling at finite Wasserstein distance solves the continuity equation with p-action at most W_p (μ, ν) ^ p.
• TauCeti.exists_isContinuityEquation_map_smul_fst_add_smul_snd_of_isOptimalCoupling: on a strictly convex space and for 1 < p < ∞, the velocity of the displacement interpolation of an optimal coupling is the displacement, and its p-action is W_p (μ, ν) ^ 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.
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Birkhäuser 2015, §5.4.

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

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

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

The velocity along a non-crossing displacement interpolation. Let π be a finite measure on E × E whose displacement y - x has finite first moment, and let A be a measurable set of times and pairs carrying dt ⊗ π on (0, 1) × (E × E) such that for every t the interpolating map (x, y) ↦ (1 - t) • x + t • y is injective on the pairs (x, y) with (t, (x, y)) ∈ A. Then the laws μₜ of (1 - t) • x + t • y 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 • y) = y - x for almost every t ∈ (0, 1) and π-almost every (x, y). Consequently, for every exponent p the p-action of v is the p-th moment of the displacement: ∫₀¹ ∫ ‖vₜ‖ ^ p dμₜ dt = ∫ ‖y - x‖ ^ p dπ.

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

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

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

The Benamou–Brenier upper bound. Let 1 ≤ p < ∞, and let π be an optimal coupling of a finite measure μ and a measure ν on E for the cost d(x, y) ^ p, at finite Wasserstein distance W_p (μ, ν). Then the displacement interpolation, the laws μₜ of (1 - t) • x + t • y under π, solves the continuity equation on (0, 1) with a velocity field of p-action at most W_p (μ, ν) ^ p: ∫₀¹ ∫ ‖vₜ‖ ^ p dμₜ dt ≤ W_p (μ, ν) ^ p.

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

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

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