Potential energy and its displacement convexity

The potential energy of a measure μ in a potential V : X → ℝ is ∫ V dμ. It is one of the three basic energies on the Wasserstein space (with the interaction and internal energies), and the drift term of the Fokker–Planck equation as a Wasserstein gradient flow.

Since V need not be integrable, the energy takes values in EReal, with the convention TauCeti.potentialEnergy: it is ⊤ when the positive part of V has infinite integral, and otherwise the integral of the positive part minus that of the negative part, which may be ⊥. It agrees with the Bochner integral for integrable V (TauCeti.potentialEnergy_of_integrable), and a lower bound by an integrable function rules out the value ⊥ (TauCeti.potentialEnergy_ne_bot_of_le). For a lower semicontinuous potential bounded below, the potential energy is a lower semicontinuous function of a probability measure for narrow convergence (TauCeti.lowerSemicontinuous_potentialEnergy), the property consumed by the direct method for the Jordan–Kinderlehrer–Otto step.

On a real normed space E, convexity of V passes to the potential energy along every interpolation of measures by a plan. If V is m-strongly convex in Mathlib's sense (StrongConvexOn univ m V, where m may be negative) and π is a measure on E × E, then for t ∈ [0, 1], with μ_t the law of (1 - t) • x + t • y under π,

∫ V dμ_t ≤ (1 - t) ∫ V dπ.fst + t ∫ V dπ.snd - (m / 2) t (1 - t) ∫ ‖x - y‖² dπ

(StrongConvexOn.potentialEnergy_map_le). This is the pointwise convexity inequality integrated against π. For an optimal plan for the quadratic cost, the last integral is the squared 2-Wasserstein distance of the two marginals and μ_t is a Wasserstein geodesic, so the potential energy is m-geodesically convex on the space P₂(E) of laws with finite second moment, as soon as V grows at most quadratically from below (StrongConvexOn.geodesicallyConvex_potentialEnergy). The geodesic used is the interpolation of an optimal plan (TauCeti.WassersteinSpace.exists_isGeodesicSegment_map_smul_add_smul), so this is the weak form of displacement convexity: two laws are joined by some geodesic along which the inequality holds. The plan-level inequality does not need the plan to be optimal, so it also applies to interpolations along non-optimal plans: applied to generalized geodesics, it makes the potential energy m-convex along every generalized-geodesic plan based at every law of P₂(E) (StrongConvexOn.convexAlongGeneralizedGeodesics_potentialEnergy). Thus it can be added to an energy convex along some generalized-geodesic plan while retaining the convexity under which the Jordan–Kinderlehrer–Otto step is unique.

Main definitions

• TauCeti.potentialEnergy V μ: the potential energy ∫ V dμ, as an extended real.

Main results

• TauCeti.potentialEnergy_of_integrable: for integrable V, the potential energy is the Bochner integral of V.
• TauCeti.integrable_iff_potentialEnergy_ne_top_and_ne_bot: an almost everywhere strongly measurable potential is integrable exactly when its potential energy is finite.
• TauCeti.potentialEnergy_mono: the potential energy is monotone in the potential.
• TauCeti.potentialEnergy_add_of_integrable: adding an integrable function adds its integral.
• TauCeti.potentialEnergy_le_mul_add_mul: a potential bounded by a convex combination of two potentials has at most the same convex combination of their potential energies.
• TauCeti.potentialEnergy_dirac: the potential energy of a Dirac mass at x is V x.
• TauCeti.potentialEnergy_ne_bot_of_hasFiniteMoment: a potential with at most quadratic negative part has potential energy ≠ ⊥ against every finite measure with finite second moment.
• TauCeti.integrable_comp_of_norm_gradient_le: a differentiable potential whose gradient grows at most linearly is integrable against the law of every square-integrable random vector.
• TauCeti.hasDerivAt_integral_comp_add_smul: the first variation ∫ ⟪∇V, ξ⟫ dρ of the potential energy of such a potential along the perturbation x ↦ x + h • ξ x of a law of finite second moment.
• TauCeti.potentialEnergy_eq_lintegral_add_sub: for an almost everywhere measurable potential almost everywhere bounded below by -c, the potential energy of a probability measure is ∫⁻ (V + c) - c.
• TauCeti.lowerSemicontinuous_potentialEnergy: the potential energy of a lower semicontinuous potential bounded below is narrowly lower semicontinuous on probability measures.
• StrongConvexOn.potentialEnergy_map_le: the convexity inequality of the potential energy of an m-strongly convex potential along the interpolation of a plan.
• StrongConvexOn.geodesicallyConvex_potentialEnergy: the potential energy of an m-strongly convex potential with at most quadratic negative part is m-geodesically convex on the 2-Wasserstein space of a separable Banach space.
• StrongConvexOn.convexAlongGeneralizedGeodesics_potentialEnergy: the same potential energy is m-convex along every generalized-geodesic plan based at every law of finite second moment.

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd ed., Birkhäuser 2008, §9.3, Proposition 9.3.2.
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Birkhäuser 2015, §7.3.

noncomputable def TauCeti.potentialEnergy {X : Type u_1} [MeasurableSpace X] (V : X → ℝ) (μ : MeasureTheory.Measure X) : EReal

The potential energy ∫ V dμ of a measure μ in a potential V : X → ℝ, as an extended real. It is ⊤ when the positive part of V has infinite integral against μ; otherwise it is the integral of the positive part minus the integral of the negative part, which is ⊥ when only the latter is infinite.

theorem TauCeti.potentialEnergy_of_lintegral_ne_top {X : Type u_1} [MeasurableSpace X] {V : X → ℝ} {μ : MeasureTheory.Measure X} (h : ∫⁻ (x : X), ENNReal.ofReal (V x) ∂μ ≠ ⊤) : potentialEnergy V μ = ↑(∫⁻ (x : X), ENNReal.ofReal (V x) ∂μ) - ↑(∫⁻ (x : X), ENNReal.ofReal (-V x) ∂μ)

When the positive part of the potential has finite integral, the potential energy is the integral of the positive part minus that of the negative part.

theorem TauCeti.potentialEnergy_eq_top_iff {X : Type u_1} [MeasurableSpace X] {V : X → ℝ} {μ : MeasureTheory.Measure X} : potentialEnergy V μ = ⊤ ↔ ∫⁻ (x : X), ENNReal.ofReal (V x) ∂μ = ⊤

The potential energy is ⊤ exactly when the positive part of the potential has infinite integral.

theorem TauCeti.potentialEnergy_eq_bot_iff {X : Type u_1} [MeasurableSpace X] {V : X → ℝ} {μ : MeasureTheory.Measure X} : potentialEnergy V μ = ⊥ ↔ ∫⁻ (x : X), ENNReal.ofReal (V x) ∂μ ≠ ⊤ ∧ ∫⁻ (x : X), ENNReal.ofReal (-V x) ∂μ = ⊤

The potential energy is ⊥ exactly when the positive part of the potential has finite integral and its negative part has infinite integral.

theorem TauCeti.potentialEnergy_of_integrable {X : Type u_1} [MeasurableSpace X] {V : X → ℝ} {μ : MeasureTheory.Measure X} (h : MeasureTheory.Integrable V μ) : potentialEnergy V μ = ↑(∫ (x : X), V x ∂μ)

For an integrable potential, the potential energy is the Bochner integral of the potential.

theorem TauCeti.potentialEnergy_of_nonneg_ae {X : Type u_1} [MeasurableSpace X] {V : X → ℝ} {μ : MeasureTheory.Measure X} (h : 0 ≤ᵐ[μ] V) : potentialEnergy V μ = ↑(∫⁻ (x : X), ENNReal.ofReal (V x) ∂μ)

For an almost everywhere nonnegative potential, the potential energy is the lower Lebesgue integral of the potential.

theorem TauCeti.integrable_iff_potentialEnergy_ne_top_and_ne_bot {X : Type u_1} [MeasurableSpace X] {V : X → ℝ} {μ : MeasureTheory.Measure X} (hV : MeasureTheory.AEStronglyMeasurable V μ) : MeasureTheory.Integrable V μ ↔ potentialEnergy V μ ≠ ⊤ ∧ potentialEnergy V μ ≠ ⊥

An almost everywhere strongly measurable potential is integrable exactly when its potential energy is finite.

theorem TauCeti.potentialEnergy_mono {X : Type u_1} [MeasurableSpace X] {V W : X → ℝ} {μ : MeasureTheory.Measure X} (h : V ≤ᵐ[μ] W) : potentialEnergy V μ ≤ potentialEnergy W μ

The potential energy is monotone in the potential.

theorem TauCeti.potentialEnergy_congr_ae {X : Type u_1} [MeasurableSpace X] {V W : X → ℝ} {μ : MeasureTheory.Measure X} (h : V =ᵐ[μ] W) : potentialEnergy V μ = potentialEnergy W μ

The potential energy depends on the potential only up to μ-almost everywhere equality.

theorem TauCeti.potentialEnergy_ne_bot_of_le {X : Type u_1} [MeasurableSpace X] {V W : X → ℝ} {μ : MeasureTheory.Measure X} (hW : MeasureTheory.Integrable W μ) (h : W ≤ᵐ[μ] V) : potentialEnergy V μ ≠ ⊥

A potential bounded below by an integrable function has potential energy ≠ ⊥.

theorem TauCeti.potentialEnergy_add_of_integrable {X : Type u_1} [MeasurableSpace X] {V W : X → ℝ} {μ : MeasureTheory.Measure X} (hV : MeasureTheory.AEStronglyMeasurable V μ) (hW : MeasureTheory.Integrable W μ) : potentialEnergy (fun (x : X) => V x + W x) μ = potentialEnergy V μ + ↑(∫ (x : X), W x ∂μ)

Adding an integrable function to a potential adds its integral to the potential energy. The potential itself need not be integrable: if its energy is ⊤ or ⊥, then so is the energy of the sum.

theorem TauCeti.potentialEnergy_eq_of_lintegral_eq {X : Type u_1} [MeasurableSpace X] {V W : X → ℝ} {μ : MeasureTheory.Measure X} (hpos : ∫⁻ (x : X), ENNReal.ofReal (V x) ∂μ = ∫⁻ (x : X), ENNReal.ofReal (W x) ∂μ) (hneg : ∫⁻ (x : X), ENNReal.ofReal (-V x) ∂μ = ∫⁻ (x : X), ENNReal.ofReal (-W x) ∂μ) : potentialEnergy V μ = potentialEnergy W μ

Two potentials whose positive parts, and whose negative parts, have the same integrals have the same potential energy.

theorem TauCeti.potentialEnergy_le_mul_add_mul {X : Type u_1} [MeasurableSpace X] {V : X → ℝ} {μ : MeasureTheory.Measure X} {V₀ V₁ : X → ℝ} (hV₀ : MeasureTheory.AEStronglyMeasurable V₀ μ) (hV₁ : MeasureTheory.AEStronglyMeasurable V₁ μ) (h₀ : potentialEnergy V₀ μ ≠ ⊥) (h₁ : potentialEnergy V₁ μ ≠ ⊥) {t : ℝ} (ht : t ∈ Set.Icc 0 1) (h : ∀ᵐ (x : X) ∂μ, V x ≤ (1 - t) * V₀ x + t * V₁ x) : potentialEnergy V μ ≤ ↑(1 - t) * potentialEnergy V₀ μ + ↑t * potentialEnergy V₁ μ

The potential energy of a pointwise convex combination. If V ≤ (1 - t) V₀ + t V₁ almost everywhere for some t ∈ [0, 1], then the potential energy of V is at most the same convex combination of the potential energies of V₀ and V₁, provided neither of them is ⊥.

@[simp]

theorem TauCeti.potentialEnergy_zero_measure {X : Type u_1} [MeasurableSpace X] (V : X → ℝ) : potentialEnergy V 0 = 0

The potential energy of the zero measure is 0.

@[simp]

theorem TauCeti.potentialEnergy_dirac {X : Type u_1} [MeasurableSpace X] [MeasurableSingletonClass X] (V : X → ℝ) (x : X) : potentialEnergy V (MeasureTheory.Measure.dirac x) = ↑(V x)

The potential energy of a Dirac mass at x is V x.

theorem TauCeti.potentialEnergy_map {X : Type u_1} [MeasurableSpace X] {V : X → ℝ} {Y : Type u_2} [MeasurableSpace Y] {f : Y → X} {ν : MeasureTheory.Measure Y} (hV : Measurable V) (hf : AEMeasurable f ν) : potentialEnergy V (MeasureTheory.Measure.map f ν) = potentialEnergy (fun (y : Y) => V (f y)) ν

The potential energy of a pushforward measure is the potential energy of the composed potential.

theorem TauCeti.potentialEnergy_ne_bot_of_hasFiniteMoment {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] {V : E → ℝ} {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] (hμ : HasFiniteMoment 2 μ) {A B : ℝ} (hVAB : ∀ (x : E), -(A + B * ‖x‖ ^ 2) ≤ V x) : potentialEnergy V μ ≠ ⊥

A potential whose negative part grows at most quadratically has potential energy ≠ ⊥ against every finite measure with finite second moment.

theorem TauCeti.integrable_comp_of_norm_gradient_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {V : E → ℝ} {C : ℝ} {α : Type u_2} [MeasurableSpace α] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ρ] {T : α → E} (hV : Differentiable ℝ V) (hV' : ∀ (x : E), ‖gradient V x‖ ≤ C * (1 + ‖x‖)) (hT : MeasureTheory.MemLp T 2 ρ) : MeasureTheory.Integrable (fun (a : α) => V (T a)) ρ

A differentiable potential whose gradient grows at most linearly, ‖∇V x‖ ≤ C (1 + ‖x‖), is integrable against the law of every square-integrable random vector: for a finite measure ρ and T ∈ L²(ρ; E), the function V ∘ T is integrable.

theorem TauCeti.hasDerivAt_integral_comp_add_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {ξ : E → E} {V : E → ℝ} {C : ℝ} {ρ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure ρ] (hV : Differentiable ℝ V) (hV' : ∀ (x : E), ‖gradient V x‖ ≤ C * (1 + ‖x‖)) (hρ : MeasureTheory.MemLp id 2 ρ) (hξ : MeasureTheory.MemLp ξ 2 ρ) : HasDerivAt (fun (h : ℝ) => ∫ (x : E), V (x + h • ξ x) ∂ρ) (∫ (x : E), inner ℝ (gradient V x) (ξ x) ∂ρ) 0

The first variation of the potential energy. Let V be a differentiable potential whose gradient grows at most linearly, ‖∇V x‖ ≤ C (1 + ‖x‖), and let ρ be a finite measure with finite second moment. For every vector field ξ ∈ L²(ρ; E), the potential energy h ↦ ∫ V (x + h • ξ x) dρ of the perturbation of ρ along ξ has derivative ∫ ⟪∇V x, ξ x⟫ dρ at h = 0.

theorem TauCeti.potentialEnergy_eq_lintegral_add_sub {X : Type u_1} [MeasurableSpace X] {V : X → ℝ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (hV : AEMeasurable V μ) {c : ℝ} (hc : ∀ᵐ (x : X) ∂μ, -c ≤ V x) : potentialEnergy V μ = ↑(∫⁻ (x : X), ENNReal.ofReal (V x + c) ∂μ) - ↑c

For a potential almost everywhere measurable and bounded below by -c, the potential energy of a probability measure is the integral of the almost everywhere nonnegative potential V + c, minus c.

theorem TauCeti.lowerSemicontinuous_potentialEnergy {X : Type u_1} [MeasurableSpace X] {V : X → ℝ} [PseudoMetricSpace X] [OpensMeasurableSpace X] (hV : LowerSemicontinuous V) (hb : BddBelow (Set.range V)) : LowerSemicontinuous fun (μ : MeasureTheory.ProbabilityMeasure X) => potentialEnergy V ↑μ

The potential energy is narrowly lower semicontinuous. For a lower semicontinuous potential V bounded below on a pseudometric space, μ ↦ ∫ V dμ is lower semicontinuous on probability measures for the topology of narrow convergence.

theorem StrongConvexOn.potentialEnergy_map_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {V : E → ℝ} {m : ℝ} (hV : StrongConvexOn Set.univ m V) (hVm : Measurable V) {π : MeasureTheory.Measure (E × E)} (h₀ : TauCeti.potentialEnergy V π.fst ≠ ⊥) (h₁ : TauCeti.potentialEnergy V π.snd ≠ ⊥) (hπ : MeasureTheory.Integrable (fun (z : E × E) => ‖z.1 - z.2‖ ^ 2) π) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : TauCeti.potentialEnergy V (MeasureTheory.Measure.map (fun (z : E × E) => (1 - t) • z.1 + t • z.2) π) ≤ ↑(1 - t) * TauCeti.potentialEnergy V π.fst + ↑t * TauCeti.potentialEnergy V π.snd - ↑(m / 2 * t * (1 - t) * ∫ (z : E × E), ‖z.1 - z.2‖ ^ 2 ∂π)

Convexity of the potential energy along a plan. If V is m-strongly convex, then along the interpolation t ↦ μ_t, with μ_t the law of (1 - t) • x + t • y under a measure π on E × E, the potential energy satisfies, for t ∈ [0, 1], ∫ V dμ_t ≤ (1 - t) ∫ V dπ.fst + t ∫ V dπ.snd - (m / 2) t (1 - t) ∫ ‖x - y‖² dπ. The potential energies of the two marginals must not be ⊥, and ‖x - y‖² must be integrable.

theorem StrongConvexOn.geodesicallyConvex_potentialEnergy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {V : E → ℝ} {m : ℝ} [CompleteSpace E] (hV : StrongConvexOn Set.univ m V) (hVm : Measurable V) {A B : ℝ} (hVAB : ∀ (x : E), -(A + B * ‖x‖ ^ 2) ≤ V x) : TauCeti.GeodesicallyConvex m fun (μ : TauCeti.WassersteinSpace 2 E) => TauCeti.potentialEnergy V ↑↑μ

Displacement convexity of the potential energy. On a separable Banach space E, the potential energy of an m-strongly convex measurable potential V whose negative part grows at most quadratically is m-geodesically convex on the 2-Wasserstein space P₂(E): two laws of finite potential energy are joined by a Wasserstein geodesic, the interpolation of an optimal plan, along which ∫ V dμ_t ≤ (1 - t) ∫ V dμ₀ + t ∫ V dμ₁ - (m / 2) t (1 - t) W₂(μ₀, μ₁)².

theorem StrongConvexOn.convexAlongGeneralizedGeodesics_potentialEnergy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {V : E → ℝ} {m : ℝ} (hV : StrongConvexOn Set.univ m V) (hVm : Measurable V) {A B : ℝ} (hVAB : ∀ (x : E), -(A + B * ‖x‖ ^ 2) ≤ V x) (μ : TauCeti.WassersteinSpace 2 E) : TauCeti.ConvexAlongGeneralizedGeodesics m (fun (ν : TauCeti.WassersteinSpace 2 E) => TauCeti.potentialEnergy V ↑↑ν) μ

Convexity of the potential energy along every generalized-geodesic plan. On a separable normed space E, the potential energy of an m-strongly convex measurable potential V whose negative part grows at most quadratically is m-convex along every quadratic generalized-geodesic plan based at every μ ∈ P₂(E). For its interpolation ν_t, ∫ V dν_t ≤ (1 - t) ∫ V dν₀ + t ∫ V dν₁ - (m / 2) t (1 - t) ∫ ‖y₀ - y₁‖² dγ.