The Jacobian equation along the interpolation of a convex gradient

Let E be a finite-dimensional real inner product space with an additive Haar measure ρ, and let f : E → EReal be convex (convex real epigraph, never ⊥), with real representative F x = (f x).toReal and D the interior of its effective domain. For 0 ≤ t ≤ 1 the interpolating map Tₜ x = (1 - t) • x + t • ∇F x moves each point a fraction t of the way to its image under the gradient. For a law μ, the laws μₜ = (Tₜ)₊ μ form McCann's displacement interpolation from μ₀ = μ to μ₁ = (∇F)₊ μ; when ∇F is the Brenier map of μ they trace the quadratic Wasserstein geodesic from μ to its target.

This file shows that for t < 1 the interpolating map never concentrates mass, however degenerate ∇F is. At a point x where the subdifferential of f is the single gradient ∇F x with a first-order expansion y' = ∇F x + H x (x' - x) + o(‖x' - x‖) (by Alexandrov's theorem, almost every point of D), the interpolating map has derivative Jₜ x = (1 - t) • 1 + t • H x within the set of such points. Since H x is a positive operator, det (Jₜ x) > 0 for t < 1. Monotonicity of the subdifferential gives (1 - t) ‖x₁ - x₂‖ ≤ ‖Tₜ x₁ - Tₜ x₂‖, so Tₜ is injective there. Mathlib's change of variables formula therefore applies with no degenerate part:

∫_{Tₜ(s)} g dρ = ∫_s det (Jₜ x) g (Tₜ x) dρ.

Consequently, for 0 ≤ t < 1 and every measure μ ≪ ρ carried by D (s-finite for the last two statements):

• μₜ is absolutely continuous with respect to ρ, even when μ₁ is not;
• the densities satisfy the Jacobian equation dμ/dρ (x) = det (Jₜ x) * dμₜ/dρ (Tₜ x) for ρ-almost every x ∈ D, and dμ/dρ = 0 almost everywhere off D;
• integrals of the density of μₜ are integrals over the source: ∫ Φ (dμₜ/dρ) dρ = ∫_D det (Jₜ x) Φ (dμ/dρ (x) / det (Jₜ x)) dρ whenever Φ 0 = 0.

The last formula, applied to the positive and negative parts of U, rewrites the internal energy ∫ U (dμₜ/dρ) dρ of the interpolant as an integral against the fixed source, in which t enters only through det (Jₜ x). Since A ↦ det A ^ (1 / n) is concave on positive operators (LinearMap.concaveOn_det_rpow), this is the formula behind McCann's displacement convexity of internal energies.

At t = 1 the interpolating map is the gradient itself, whose Jacobian det (H x) may vanish. The gradient is injective where det (H x) ≠ 0 and maps the degenerate set {det (H x) = 0} to a null set, so the endpoint μ₁ = (∇F)₊ μ splits into an absolutely continuous part, the image of μ restricted to the nondegenerate set, and a singular part of total mass μ {det (H x) = 0}. The integral formula above then holds at t = 1 for the absolutely continuous part.

Main statements

• TauCeti.withDensity_image_smul_add_smul_gradient_eq_setLIntegral — the change of variables formula along the interpolating map;
• TauCeti.map_smul_add_smul_gradient_absolutelyContinuous — the interpolants of an absolutely continuous law are absolutely continuous;
• TauCeti.rnDeriv_ae_eq_indicator_ofReal_det_mul_rnDeriv_map_smul_add_smul_gradient — the Jacobian equation of the interpolating map;
• TauCeti.lintegral_comp_rnDeriv_map_smul_add_smul_gradient — integrals of functions of the density of an interpolant, as integrals over the source;
• TauCeti.singularPart_map_gradient_apply_univ — the singular part of the endpoint (∇F)₊ μ has total mass μ {det (H x) = 0};
• TauCeti.lintegral_comp_rnDeriv_map_gradient — integrals of functions of the density of the endpoint, as integrals over the source.

References

• R. J. McCann, A convexity principle for interacting gases, Adv. Math. 128 (1997), 153–179, Section 4, for the Jacobian equation along the interpolation of a convex gradient and its use in displacement convexity.
• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, American Mathematical Society, 2003, Chapters 4 and 5.

theorem TauCeti.withDensity_image_smul_add_smul_gradient_eq_setLIntegral {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} [MeasurableSpace E] [BorelSpace E] (ρ : MeasureTheory.Measure E) [ρ.IsAddHaarMeasure] {H : E → E →L[ℝ] E} {s : Set E} (hs : MeasurableSet s) (hP : ∀ x ∈ s, subdifferential (innerₗ E) f x = {gradient (fun (x' : E) => (f x').toReal) x} ∧ (H x).IsPositive ∧ ∀ ε > 0, ∀ᶠ (x' : E) in nhds x, ∀ y' ∈ subdifferential (innerₗ E) f x', ‖y' - gradient (fun (x' : E) => (f x').toReal) x - (H x) (x' - x)‖ ≤ ε * ‖x' - x‖) {t : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t < 1) (g : E → ENNReal) : (ρ.withDensity g) ((fun (x : E) => (1 - t) • x + t • gradient (fun (x' : E) => (f x').toReal) x) '' s) = ∫⁻ (x : E) in s, ENNReal.ofReal ((1 - t) • ContinuousLinearMap.id ℝ E + t • H x).det * g ((1 - t) • x + t • gradient (fun (x' : E) => (f x').toReal) x) ∂ρ

Change of variables along the interpolating map. Let s be a measurable set at each point of which the subdifferential of f : E → EReal is the single gradient ∇F x of its real representative, with the expansion y' = ∇F x + H x (x' - x) + o(‖x' - x‖) for a positive H x. For 0 ≤ t < 1 the interpolating map Tₜ x = (1 - t) • x + t • ∇F x is injective on s, with derivative (1 - t) • 1 + t • H x of positive determinant, so for every additive Haar measure ρ and every g, ∫_{Tₜ(s)} g dρ = ∫_s det ((1 - t) • 1 + t • H x) g (Tₜ x) dρ.

theorem TauCeti.map_smul_add_smul_gradient_absolutelyContinuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} [MeasurableSpace E] [BorelSpace E] (ρ : MeasureTheory.Measure E) [ρ.IsAddHaarMeasure] (hf : Convex ℝ {p : E × ℝ | f p.1 ≤ ↑p.2}) (hbot : ∀ (x : E), f x ≠ ⊥) {μ : MeasureTheory.Measure E} (hμ : μ.AbsolutelyContinuous ρ) (hμD : ∀ᵐ (x : E) ∂μ, x ∈ interior {x : E | f x ≠ ⊤}) {t : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t < 1) : (MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • gradient (fun (x' : E) => (f x').toReal) x) μ).AbsolutelyContinuous ρ

Interpolants of an absolutely continuous law are absolutely continuous. Let f : E → EReal be convex (convex real epigraph, never ⊥), with real representative F, and let μ be a measure absolutely continuous with respect to an additive Haar measure ρ and carried by the interior of the effective domain of f. For 0 ≤ t < 1, the pushforward of μ by the interpolating map x ↦ (1 - t) • x + t • ∇F x is absolutely continuous with respect to ρ. This holds whether or not the pushforward (∇F)₊ μ at t = 1 is absolutely continuous.

theorem TauCeti.rnDeriv_ae_eq_indicator_ofReal_det_mul_rnDeriv_map_smul_add_smul_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} [MeasurableSpace E] [BorelSpace E] (ρ : MeasureTheory.Measure E) [ρ.IsAddHaarMeasure] (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) : μ.rnDeriv ρ =ᵐ[ρ] (interior {x : E | f x ≠ ⊤}).indicator fun (x : E) => ENNReal.ofReal ((1 - t) • ContinuousLinearMap.id ℝ E + t • H x).det * (MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • gradient (fun (x' : E) => (f x').toReal) x) μ).rnDeriv ρ ((1 - t) • x + t • gradient (fun (x' : E) => (f x').toReal) x)

The Jacobian equation 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, see rnDeriv_mongeAmpereMeasure_withDensity_ae_eq). Let μ be an s-finite measure, absolutely continuous with respect to an additive Haar measure ρ and carried by D, and let 0 ≤ t < 1. Then the density of μ and the density of its interpolant μₜ = (Tₜ)₊ μ, with Tₜ x = (1 - t) • x + t • ∇F x, satisfy dμ/dρ (x) = det ((1 - t) • 1 + t • H x) * dμₜ/dρ (Tₜ x) for almost every x ∈ D, and dμ/dρ = 0 almost everywhere off D.

theorem TauCeti.lintegral_comp_rnDeriv_map_smul_add_smul_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} [MeasurableSpace E] [BorelSpace E] (ρ : MeasureTheory.Measure E) [ρ.IsAddHaarMeasure] (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) {Φ : ENNReal → ENNReal} (hΦ : Φ 0 = 0) : ∫⁻ (y : E), Φ ((MeasureTheory.Measure.map (fun (x : E) => (1 - t) • x + t • gradient (fun (x' : E) => (f x').toReal) x) μ).rnDeriv ρ y) ∂ρ = ∫⁻ (x : E) in interior {x : E | f x ≠ ⊤}, ENNReal.ofReal ((1 - t) • ContinuousLinearMap.id ℝ E + t • H x).det * Φ (μ.rnDeriv ρ x / ENNReal.ofReal ((1 - t) • ContinuousLinearMap.id ℝ E + t • H x).det) ∂ρ

Integrals of the density of an interpolant, as integrals over the source. Under the hypotheses of rnDeriv_ae_eq_indicator_ofReal_det_mul_rnDeriv_map_smul_add_smul_gradient, let μₜ = (Tₜ)₊ μ with Tₜ x = (1 - t) • x + t • ∇F x and 0 ≤ t < 1, and write Jₜ x = (1 - t) • 1 + t • H x. For every Φ : ℝ≥0∞ → ℝ≥0∞ with Φ 0 = 0, ∫ Φ (dμₜ/dρ) dρ = ∫_D det (Jₜ x) * Φ (dμ/dρ (x) / det (Jₜ x)) dρ, where D is the interior of the effective domain of f. For an internal energy ∫ U (dμₜ/dρ) dρ with U 0 = 0, applied to the positive and negative parts of U, this moves the time dependence from the density into the Jacobian det (Jₜ x).

The endpoint t = 1

theorem TauCeti.singularPart_map_gradient_apply_univ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} [MeasurableSpace E] [BorelSpace E] (ρ : MeasureTheory.Measure E) [ρ.IsAddHaarMeasure] (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 ≠ ⊤}) : ((MeasureTheory.Measure.map (gradient fun (x' : E) => (f x').toReal) μ).singularPart ρ) Set.univ = μ {x : E | (H x).det = 0}

The singular part of the pushforward by the 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, see rnDeriv_mongeAmpereMeasure_withDensity_ae_eq). Let μ be an s-finite measure, absolutely continuous with respect to an additive Haar measure ρ and carried by D. Then the singular part of the endpoint μ₁ = (∇F)₊ μ of the interpolation with respect to ρ has total mass μ {x | det (H x) = 0}: the gradient collapses the degenerate set, and only it, to a null set.

theorem TauCeti.lintegral_comp_rnDeriv_map_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} [MeasurableSpace E] [BorelSpace E] (ρ : MeasureTheory.Measure E) [ρ.IsAddHaarMeasure] (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 ≠ ⊤}) {Φ : ENNReal → ENNReal} (hΦ : Φ 0 = 0) : ∫⁻ (y : E), Φ ((MeasureTheory.Measure.map (gradient fun (x' : E) => (f x').toReal) μ).rnDeriv ρ y) ∂ρ = ∫⁻ (x : E) in interior {x : E | f x ≠ ⊤}, ENNReal.ofReal (H x).det * Φ (μ.rnDeriv ρ x / ENNReal.ofReal (H x).det) ∂ρ

Integrals of the density of the pushforward by the gradient, as integrals over the source. Under the hypotheses of singularPart_map_gradient_apply_univ, for every Φ : ℝ≥0∞ → ℝ≥0∞ with Φ 0 = 0, the absolutely continuous part of the endpoint μ₁ = (∇F)₊ μ satisfies ∫ Φ (dμ₁/dρ) dρ = ∫_D det (H x) * Φ (dμ/dρ (x) / det (H x)) dρ. This is the formula of lintegral_comp_rnDeriv_map_smul_add_smul_gradient at t = 1, where the Jacobian det (H x) may vanish: the degenerate set contributes nothing to the right side, and its image carries the singular part of μ₁.