Existence of a Variational Maximizer

Let $E$ be a finite-dimensional real inner-product space with Borel measurable structure, let $dx$ be an additive Haar measure, and let $\mu$ be a probability measure. Assume:

1. If a linear subspace $V\subseteq E$ satisfies $\mu(V^c)=0$, then $V=E$.
2. The identity map is integrable under $\mu$.
3. The barycenter is zero: $\int x\,d\mu=0$.

Then there exists $\phi:E\to\overline{\mathbb{R}}$ such that $\phi$ is a convex lower-semicontinuous potential, is potential-integrable under $\mu$, and

$$\operatorname{mass}_{dx}(\phi^*)=1.$$

For every potential-integrable competitor $f:E\to\overline{\mathbb{R}}$,

$$I_{dx,\mu}(f)\le I_{dx,\mu}(\phi),$$

where $\phi^*$ is legendre, the mass is mass, and $I_{dx,\mu}$ is variationalFunctional. This is the formalized variational-attainment conclusion; it does not assert essential continuity, an Euler–Lagrange identity, or a moment-map formula.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.CEK. Shown in its original module context. Proof omitted.

theorem exists_variational_maximum (dx μ : Measure E)
    [dx.IsAddHaarMeasure] [IsProbabilityMeasure μ]
    (hsub : ∀ V : Submodule ℝ E, μ (V : Set E)ᶜ = 0 → V = ⊤)
    (hfirstMoment : Integrable (fun x : E => x) μ) (hbar : ∫ x, x ∂μ = 0) :
    ∃ φ : E → EReal, ConvexPotential φ ∧ LowerSemicontinuous φ ∧ PotentialIntegrable φ μ ∧
      mass dx (legendre φ) = 1 ∧
      ∀ f : E → EReal, PotentialIntegrable f μ →
        variationalFunctional dx μ f ≤ variationalFunctional dx μ φ

Module navigation

Module: KLS/CEK/VariationalMaximum.

Definition modules: Probability/MomentMeasure/Basic, Analysis/Convex/Legendre.

Selected supporting theorems: convex_epigraph_affineSubtract, legendre_affineSubtract, lowerTruncate_convexification, exists_limit_ge_normalized_supremum, exists_normalized_competitor.

Previous: exists_limit_ge_normalized_supremum.

Source excerpt, lines 138–145 · Frozen source 408915f.

Literature

This formalizes Proposition 12, display (38), of Cordero–Klartag (arXiv:1304.0630v1).

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_CEK_VariationalMaximum

open FunctionalInequalities.Analysis
open FunctionalInequalities.Probability.MomentMeasure
open MeasureTheory Filter Set
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

theorem FunctionalInequalities.KLS.CEK.exists_variational_maximum_readable (dx μ : Measure E)
    [dx.IsAddHaarMeasure] [IsProbabilityMeasure μ]
    (hsub : ∀ V : Submodule ℝ E, μ (V : Set E)ᶜ = 0 → V = ⊤)
    (hfirstMoment : Integrable (fun x : E => x) μ) (hbar : ∫ x, x ∂μ = 0) :
    ∃ φ : E → EReal, ConvexPotential φ ∧ LowerSemicontinuous φ ∧ PotentialIntegrable φ μ ∧
      mass dx (legendre φ) = 1 ∧
      ∀ f : E → EReal, PotentialIntegrable f μ →
        variationalFunctional dx μ f ≤ variationalFunctional dx μ φ := by sorry