Normalized Maximizing Sequence For The Variational Functional

This formalizes a partial compactness consequence related to Proposition 12 of Cordero–Erausquin–Klartag, Moment measures (arXiv:1304.0630v1), cited as a stronger paper statement.

Let $E$ be finite-dimensional with additive Haar measure $dx$, and let $\mu$ be a probability measure satisfying:

1. Every linear subspace with full $\mu$-measure is all of $E$.
2. The identity map is $\mu$-integrable.
3. $\int x\,d\mu(x)=0$.

Then there exist $S\in\mathbb R$ and a sequence $\phi_j:E\to\overline{\mathbb R}$ such that, for every $j$, ConvexPotential (φ j), PotentialIntegrable (φ j) μ, $\phi_j\ge0$, and $\phi_j(0)=0$. Moreover,

$$\operatorname{variationalFunctional}(dx,\mu,\phi_j)\longrightarrow(S:\overline{\mathbb R})$$

as $j\to\infty$, and every nonnegative normalized convex potential $\psi$ with PotentialIntegrable ψ μ satisfies

$$\operatorname{variationalFunctional}(dx,\mu,\psi)\le(S:\overline{\mathbb R}).$$

This provides a normalized maximizing sequence and an upper-bound value, but does not assert mass convergence or attainment by a single potential.

Original Lean declaration header

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

theorem exists_normalized_maximizing_sequence (dx μ : Measure E)
    [dx.IsAddHaarMeasure] [IsProbabilityMeasure μ]
    (hsub : ∀ V : Submodule ℝ E, μ (V : Set E)ᶜ = 0 → V = ⊤)
    (hfirst : Integrable (fun x : E => x) μ) (hbar : ∫ x, x ∂μ = 0) :
    ∃ (S : ℝ) (φ : ℕ → E → EReal),
      (∀ j, ConvexPotential (φ j)) ∧ (∀ j, PotentialIntegrable (φ j) μ) ∧
      (∀ j x, 0 ≤ φ j x) ∧ (∀ j, φ j 0 = 0) ∧
      Tendsto (fun j => variationalFunctional dx μ (φ j)) atTop (𝓝 (S : EReal)) ∧
      ∀ ψ : E → EReal, ConvexPotential ψ → PotentialIntegrable ψ μ →
        (∀ x, 0 ≤ ψ x) → ψ 0 = 0 → variationalFunctional dx μ ψ ≤ (S : EReal)

Module navigation

Module: KLS/CEK/VariationalMaximum.

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

Supporting theorems: legendre_norm, exists_uniform_functional_upper.

Next: exists_limit_ge_normalized_supremum.

Source excerpt, lines 35–44 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_CEK_VariationalMaximum

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

theorem FunctionalInequalities.KLS.CEK.exists_normalized_maximizing_sequence_readable (dx μ : Measure E)
    [dx.IsAddHaarMeasure] [IsProbabilityMeasure μ]
    (hsub : ∀ V : Submodule ℝ E, μ (V : Set E)ᶜ = 0 → V = ⊤)
    (hfirst : Integrable (fun x : E => x) μ) (hbar : ∫ x, x ∂μ = 0) :
    ∃ (S : ℝ) (φ : ℕ → E → EReal),
      (∀ j, ConvexPotential (φ j)) ∧ (∀ j, PotentialIntegrable (φ j) μ) ∧
      (∀ j x, 0 ≤ φ j x) ∧ (∀ j, φ j 0 = 0) ∧
      Tendsto (fun j => variationalFunctional dx μ (φ j)) atTop (𝓝 (S : EReal)) ∧
      ∀ ψ : E → EReal, ConvexPotential ψ → PotentialIntegrable ψ μ →
        (∀ x, 0 ≤ ψ x) → ψ 0 = 0 → variationalFunctional dx μ ψ ≤ (S : EReal) := by sorry