McCann's displacement convexity of internal energies

Let E be a real inner product space of finite dimension n ≥ 1 with an additive Haar measure ρ, and let U : ℝ → ℝ satisfy U 0 = 0 and McCann's condition:

s ↦ sⁿ U(s⁻ⁿ) is convex and nonincreasing on (0, ∞).

For instance U(r) = r log r, U(r) = rᵐ / (m - 1) for m > 1, and, when n ≥ 2, U(r) = -r^{1 - 1/n} satisfy it. McCann's theorem says that the internal energy 𝓤(μ) = ∫ U(dμ/dρ) dρ + U'(∞) μˢ(E) (TauCeti.internalEnergy) is convex along displacement interpolations. Here, for a convex f : E → EReal with real representative F and a σ-finite measure μ ≪ ρ carried by the interior D of the effective domain of f, the interpolant at time t ∈ [0, 1] is μₜ = (Tₜ)₊ μ with Tₜ x = (1 - t) • x + t • ∇F x, and

𝓤(μₜ) ≤ (1 - t) 𝓤(μ) + t 𝓤((∇F)₊ μ) (TauCeti.internalEnergy_map_smul_add_smul_gradient_le),

provided neither endpoint energy 𝓤(μ), 𝓤((∇F)₊ μ) is ⊥.

When ∇F is the Brenier map of μ, these interpolants form McCann's displacement interpolation, the quadratic Wasserstein geodesic from μ to its target, so under the same restriction on the endpoint energies the internal energy is convex along it (TauCeti.WassersteinSpace.exists_isGeodesicSegment_convexAlong_internalEnergy). The target need not be absolutely continuous: its singular part is charged at the recession constant U'(∞), and the theorem holds with that convention.

The proof moves the time dependence of 𝓤(μₜ) into the Jacobian of Tₜ. Write r for the density of μ and H x for the Alexandrov Hessian of F. For t < 1 the interpolant is absolutely continuous with 𝓤(μₜ) = ∫_D Jₜ U(r / Jₜ) dρ, where Jₜ x = det ((1 - t) • 1 + t • H x) (TauCeti.internalEnergy_map_smul_add_smul_gradient), by the change of variables of TauCeti.lintegral_comp_rnDeriv_map_smul_add_smul_gradient. At t = 1, the gradient collapses the degenerate set {det (H x) = 0} to a null set, which carries the singular part of (∇F)₊ μ (TauCeti.singularPart_map_gradient_apply_univ), and 𝓤((∇F)₊ μ) is the integral over D of J₁ U(r / J₁), or of U'(∞) r where J₁ = 0 (TauCeti.internalEnergy_map_gradient).

Pointwise, Jₜ U(r / Jₜ) = r φ(Jₜ^{1/n} r^{-1/n}) with φ(s) = sⁿ U(s⁻ⁿ). By Minkowski's determinant inequality t ↦ Jₜ^{1/n} is concave (LinearMap.concaveOn_det_rpow), and a convex nonincreasing function of a concave function is convex. When J₁ = 0, the value U'(∞) r at t = 1 is the limit of r φ(s) as s → 0⁺; it suffices that it bounds r φ from above, which holds because U'(∞) is the upper limit of U(r) / r as r → ∞ and U(r) / r = φ(r^{-1/n}).

Main statements

• TauCeti.internalEnergy_map_smul_add_smul_gradient: the internal energy of an interpolant at time t < 1, as an integral over the source.
• TauCeti.internalEnergy_map_gradient: the internal energy of the endpoint (∇F)₊ μ, as an integral over the source charging the degenerate set at the recession constant.
• TauCeti.internalEnergy_map_smul_add_smul_gradient_le: McCann's displacement convexity of the internal energy, when neither endpoint energy is ⊥.
• TauCeti.WassersteinSpace.exists_isGeodesicSegment_convexAlong_internalEnergy: for laws of finite second moment, the first absolutely continuous, and neither of internal energy ⊥, the internal energy is convex along a geodesic of the quadratic Wasserstein space joining them, the displacement interpolation of the Brenier map.

References

• R. J. McCann, A convexity principle for interacting gases, Adv. Math. 128 (1997), 153–179, Theorem 2.2.
• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, American Mathematical Society, 2003, Theorem 5.15.
• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd ed., Birkhäuser 2008, Proposition 9.3.9.

theorem TauCeti.internalEnergy_map_smul_add_smul_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ρ : MeasureTheory.Measure E) [ρ.IsAddHaarMeasure] {f : E → EReal} {U : ℝ → ℝ} (hU0 : U 0 = 0) (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {H : E → E →L[ℝ] E} (hH : ∀ᵐ (x : E) ∂ρ, x ∈ interior {x : E | f x ≠ ⊤} → ∃ (y : E), ∀ ε > 0, ∀ᶠ (x' : E) in nhds x, ∀ y' ∈ subdifferential (innerₗ E) f x', ‖y' - y - (H x) (x' - x)‖ ≤ ε * ‖x' - x‖) {μ : MeasureTheory.Measure E} [MeasureTheory.SFinite μ] (hμ : μ.AbsolutelyContinuous ρ) (hμD : ∀ᵐ (x : E) ∂μ, x ∈ interior {x : E | f x ≠ ⊤}) {t : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t < 1) : internalEnergy U ρ (MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • gradient (fun (x' : E) => (f x').toReal) x) μ) = potentialEnergy ((interior {x : E | f x ≠ ⊤}).indicator fun (x : E) => ((1 - t) • ContinuousLinearMap.id ℝ E + t • H x).det * U ((μ.rnDeriv ρ x).toReal / ((1 - t) • ContinuousLinearMap.id ℝ E + t • H x).det)) ρ

The internal energy along the interpolation of a convex gradient. Let f : E → EReal be convex (convex real epigraph, never ⊥), with real representative F and D the interior of its effective domain, and let H x be, for almost every x ∈ D, a first-order expansion of the subdifferential of f at x (the Alexandrov Hessian). Let μ be an s-finite measure, absolutely continuous with respect to an additive Haar measure ρ and carried by D, and let U 0 = 0. For 0 ≤ t < 1, the internal energy of the interpolant μₜ = (Tₜ)₊ μ, Tₜ x = (1 - t) • x + t • ∇F x, is the potential energy against ρ of x ↦ Jₜ x * U(dμ/dρ (x) / Jₜ x) on D, where Jₜ x = det ((1 - t) • 1 + t • H x).

theorem TauCeti.internalEnergy_map_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ρ : MeasureTheory.Measure E) [ρ.IsAddHaarMeasure] {f : E → EReal} {U : ℝ → ℝ} (hU0 : U 0 = 0) (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {H : E → E →L[ℝ] E} (hH : ∀ᵐ (x : E) ∂ρ, x ∈ interior {x : E | f x ≠ ⊤} → ∃ (y : E), ∀ ε > 0, ∀ᶠ (x' : E) in nhds x, ∀ y' ∈ subdifferential (innerₗ E) f x', ‖y' - y - (H x) (x' - x)‖ ≤ ε * ‖x' - x‖) {μ : MeasureTheory.Measure E} [MeasureTheory.SigmaFinite μ] (hμ : μ.AbsolutelyContinuous ρ) (hμD : ∀ᵐ (x : E) ∂μ, x ∈ interior {x : E | f x ≠ ⊤}) {L : ℝ} (hL : recessionConstant U = ↑L ∨ μ {x : E | (H x).det = 0} = 0) : internalEnergy U ρ (MeasureTheory.Measure.map (gradient fun (x' : E) => (f x').toReal) μ) = potentialEnergy ((interior {x : E | f x ≠ ⊤}).indicator fun (x : E) => if (H x).det = 0 then L * (μ.rnDeriv ρ x).toReal else (H x).det * U ((μ.rnDeriv ρ x).toReal / (H x).det)) ρ

The internal energy of the endpoint of the interpolation. Under the hypotheses of internalEnergy_map_smul_add_smul_gradient, with μ σ-finite, let L be the recession constant of U, or any real number if μ gives no mass to the degenerate set {x | det (H x) = 0}. Then the internal energy of (∇F)₊ μ is the potential energy against ρ of the function equal on D to det (H x) * U(dμ/dρ (x) / det (H x)) where det (H x) ≠ 0, and to L * dμ/dρ (x) where det (H x) = 0. The degenerate set carries the singular part of (∇F)₊ μ (singularPart_map_gradient_apply_univ), which the internal energy charges at the recession constant.

theorem TauCeti.internalEnergy_map_smul_add_smul_gradient_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ρ : MeasureTheory.Measure E) [ρ.IsAddHaarMeasure] {f : E → EReal} {U : ℝ → ℝ} [Nontrivial E] (hU0 : U 0 = 0) (hc : ConvexOn ℝ (Set.Ioi 0) fun (s : ℝ) => s ^ Module.finrank ℝ E * U (s ^ Module.finrank ℝ E)⁻¹) (ha : AntitoneOn (fun (s : ℝ) => s ^ Module.finrank ℝ E * U (s ^ Module.finrank ℝ E)⁻¹) (Set.Ioi 0)) (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {μ : MeasureTheory.Measure E} [MeasureTheory.SigmaFinite μ] (hμ : μ.AbsolutelyContinuous ρ) (hμD : ∀ᵐ (x : E) ∂μ, x ∈ interior {x : E | f x ≠ ⊤}) (h₀ : internalEnergy U ρ μ ≠ ⊥) (h₁ : internalEnergy U ρ (MeasureTheory.Measure.map (gradient fun (x' : E) => (f x').toReal) μ) ≠ ⊥) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : internalEnergy U ρ (MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • gradient (fun (x' : E) => (f x').toReal) x) μ) ≤ ↑(1 - t) * internalEnergy U ρ μ + ↑t * internalEnergy U ρ (MeasureTheory.Measure.map (gradient fun (x' : E) => (f x').toReal) μ)

McCann's displacement convexity of internal energies. Let E be a real inner product space of finite dimension n ≥ 1 with an additive Haar measure ρ, and let U : ℝ → ℝ satisfy U 0 = 0 and McCann's condition: s ↦ sⁿ U(s⁻ⁿ) is convex and nonincreasing on (0, ∞). Let f : E → EReal be convex (convex real epigraph, never ⊥), with real representative F, and let μ be a σ-finite measure, absolutely continuous with respect to ρ and carried by the interior of the effective domain of f. Then the internal energy is convex along the interpolation μₜ = (Tₜ)₊ μ, Tₜ x = (1 - t) • x + t • ∇F x: 𝓤(μₜ) ≤ (1 - t) 𝓤(μ) + t 𝓤((∇F)₊ μ) for t ∈ [0, 1], provided neither endpoint has energy ⊥. The endpoint (∇F)₊ μ need not be absolutely continuous; its singular part is charged at the recession constant U'(∞).

theorem TauCeti.WassersteinSpace.exists_isGeodesicSegment_convexAlong_internalEnergy {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (ρ : MeasureTheory.Measure E) [ρ.IsAddHaarMeasure] {U : ℝ → ℝ} [Nontrivial E] (hU0 : U 0 = 0) (hc : ConvexOn ℝ (Set.Ioi 0) fun (s : ℝ) => s ^ Module.finrank ℝ E * U (s ^ Module.finrank ℝ E)⁻¹) (ha : AntitoneOn (fun (s : ℝ) => s ^ Module.finrank ℝ E * U (s ^ Module.finrank ℝ E)⁻¹) (Set.Ioi 0)) {μ ν : WassersteinSpace 2 E} (hμ : (↑↑μ).AbsolutelyContinuous ρ) (h₀ : internalEnergy U ρ ↑↑μ ≠ ⊥) (h₁ : internalEnergy U ρ ↑↑ν ≠ ⊥) : ∃ (γ : ℝ → WassersteinSpace 2 E), IsGeodesicSegment γ μ ν ∧ ConvexAlong 0 (fun (ξ : WassersteinSpace 2 E) => internalEnergy U ρ ↑↑ξ) γ

McCann's displacement convexity in the quadratic Wasserstein space. Let E be a real inner product space of finite dimension n ≥ 1 with an additive Haar measure ρ, and let U satisfy U 0 = 0 and McCann's condition: s ↦ sⁿ U(s⁻ⁿ) is convex and nonincreasing on (0, ∞). For laws μ, ν of finite second moment with μ ≪ ρ, the internal energy is convex along McCann's displacement interpolation, a geodesic of P₂(E) from μ to ν, provided neither endpoint has energy ⊥.