The Benamou–Brenier formula

Let E be a finite-dimensional real normed space and 1 ≤ p < ∞. The Benamou–Brenier formula identifies the p-th power of the Wasserstein distance between two probability measures μ₀ and μ₁ on E with the infimal kinetic action needed to move μ₀ to μ₁:

W_p (μ₀, μ₁) ^ p = inf ∫₀¹ ∫ ‖vₜ‖ ^ p dνₜ dt,

the infimum being over the curves t ↦ νₜ of finite measures, narrowly continuous on [0, 1] with ν₀ = μ₀ and ν₁ = μ₁, that solve the continuity equation ∂ₜ νₜ + div (vₜ νₜ) = 0 on (0, 1) with velocity v. Both sides may be ∞; when W_p (μ₀, μ₁) is finite, the infimum is attained, so it is a minimum. It is the Eulerian description of optimal transport: the static problem over couplings becomes a dynamic problem over flows of mass.

The upper bound and the minimiser come from the displacement interpolation of an optimal coupling, whose barycentric velocity has action at most W_p (μ₀, μ₁) ^ p (TauCeti.exists_isContinuityEquation_map_smul_fst_add_smul_snd_of_isOptimalCoupling_le).

The lower bound holds on every interval [a, b]: W_p (ν_a, ν_b) ^ p ≤ (b - a) ^ (p - 1) * ∫_a^b ∫ ‖vₜ‖ ^ p dνₜ dt. By Kantorovich duality with bounded continuous potentials, it suffices to bound ∫ φ dν_a + ∫ ψ dν_b for a feasible pair φ x + ψ y ≤ ‖x - y‖ ^ p. The Hopf–Lax formula with Lagrangian ‖·‖ ^ p propagates -φ to a function u (t, x) with u (a, ·) ≤ -φ and u (b, ·) ≥ ψ (up to the factor (b - a) ^ (p - 1)), which is a subsolution of the Hamilton–Jacobi equation ∂ₜ u + ⟨∇ₓ u, w⟩ ≤ ‖w‖ ^ p; testing the continuity equation against u bounds ∫ u (b, ·) dν_b - ∫ u (a, ·) dν_a by the action (TauCeti.IsContinuityEquation.ofReal_integral_sub_integral_le_lintegral_of_add_smul_le). To make u continuous up to the time a, the Hopf–Lax evolution is started slightly before a, and the endpoint is recovered by narrow continuity of ν at b.

Main results

• TauCeti.IsContinuityEquation.wassersteinEDist_rpow_le: the Benamou–Brenier lower bound W_p (ν_a, ν_b) ^ p ≤ (b - a) ^ (p - 1) * ∫_a^b ∫ ‖vₜ‖ ^ p dνₜ dt for a narrowly continuous solution of the continuity equation.
• TauCeti.isLeast_lintegral_isContinuityEquation: the Benamou–Brenier formula at finite Wasserstein distance, with the minimum attained.
• TauCeti.wassersteinEDist_rpow_eq_sInf_lintegral_isContinuityEquation: the formula as an infimum, with both sides possibly infinite.

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.
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 7.
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Birkhäuser 2015, §5.3.

theorem TauCeti.IsContinuityEquation.wassersteinEDist_rpow_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {ν : ℝ → MeasureTheory.FiniteMeasure E} {v : ℝ → E → E} {a b : ℝ} (h : IsContinuityEquation (fun (t : ℝ) => ↑(ν t)) v a b) (hν : ContinuousOn ν (Set.Icc a b)) (hab : a ≤ b) [MeasureTheory.IsProbabilityMeasure ↑(ν a)] {p : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) : wassersteinEDist p ↑(ν a) ↑(ν b) ^ p.toReal ≤ ENNReal.ofReal ((b - a) ^ (p.toReal - 1)) * ∫⁻ (t : ℝ) in Set.Ioo a b, ∫⁻ (x : E), ‖v t x‖ₑ ^ p.toReal ∂↑(ν t)

The Benamou–Brenier lower bound. Let t ↦ νₜ be a curve of finite measures, narrowly continuous on [a, b] with a ≤ b, solving the continuity equation with velocity v on (a, b), whose initial law ν_a is a probability measure (by conservation of mass, so is ν_b). Then for 1 ≤ p < ∞ the p-Wasserstein distance between the endpoint laws is controlled by the p-action of v: W_p (ν_a, ν_b) ^ p ≤ (b - a) ^ (p - 1) * ∫_a^b ∫ ‖vₜ‖ ^ p dνₜ dt.

On [0, 1] the factor is 1, and this is the inequality W_p (ν₀, ν₁) ^ p ≤ ∫₀¹ ∫ ‖vₜ‖ ^ p dνₜ dt of the Benamou–Brenier formula.

theorem TauCeti.isLeast_lintegral_isContinuityEquation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {μ₀ μ₁ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ₀] [MeasureTheory.IsProbabilityMeasure μ₁] {p : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) (hfin : wassersteinEDist p μ₀ μ₁ ≠ ⊤) : IsLeast {A : ENNReal | ∃ (ν : ℝ → MeasureTheory.FiniteMeasure E) (v : ℝ → E → E), IsContinuityEquation (fun (t : ℝ) => ↑(ν t)) v 0 1 ∧ ContinuousOn ν (Set.Icc 0 1) ∧ ↑(ν 0) = μ₀ ∧ ↑(ν 1) = μ₁ ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 1, ∫⁻ (x : E), ‖v t x‖ₑ ^ p.toReal ∂↑(ν t) = A} (wassersteinEDist p μ₀ μ₁ ^ p.toReal)

The Benamou–Brenier formula. For 1 ≤ p < ∞ and probability measures μ₀, μ₁ on a finite-dimensional real normed space at finite Wasserstein distance, W_p (μ₀, μ₁) ^ p is the least p-action ∫₀¹ ∫ ‖vₜ‖ ^ p dνₜ dt of a curve t ↦ νₜ of finite measures, narrowly continuous on [0, 1] and joining μ₀ to μ₁, solving the continuity equation with velocity v on (0, 1). The minimum is attained by the displacement interpolation of an optimal coupling.

theorem TauCeti.wassersteinEDist_rpow_eq_sInf_lintegral_isContinuityEquation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [FiniteDimensional ℝ E] [BorelSpace E] {μ₀ μ₁ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ₀] [MeasureTheory.IsProbabilityMeasure μ₁] {p : ENNReal} (hp : 1 ≤ p) (hp_top : p ≠ ⊤) : wassersteinEDist p μ₀ μ₁ ^ p.toReal = sInf {A : ENNReal | ∃ (ν : ℝ → MeasureTheory.FiniteMeasure E) (v : ℝ → E → E), IsContinuityEquation (fun (t : ℝ) => ↑(ν t)) v 0 1 ∧ ContinuousOn ν (Set.Icc 0 1) ∧ ↑(ν 0) = μ₀ ∧ ↑(ν 1) = μ₁ ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 1, ∫⁻ (x : E), ‖v t x‖ₑ ^ p.toReal ∂↑(ν t) = A}

The Benamou–Brenier formula, as an infimum. For 1 ≤ p < ∞ and probability measures μ₀, μ₁ on a finite-dimensional real normed space, W_p (μ₀, μ₁) ^ p is the infimum of the p-actions ∫₀¹ ∫ ‖vₜ‖ ^ p dνₜ dt of the curves t ↦ νₜ of finite measures, narrowly continuous on [0, 1] and joining μ₀ to μ₁, solving the continuity equation with velocity v on (0, 1). Both sides may be infinite.