Prove2Me

Pointwise Limsup Bound For Legendre Densities

Proved
FunctionalInequalities.Probability.MomentMeasure.limsup_density_legendre_le_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the pointwise density component of the upper semicontinuity statement associated with Lemma 17 of Cordero–Erausquin–Klartag, Moment measures (arXiv:1304.0630v1), cited there as a partial formalization.

Let EE be a real-inner-product normed additive group, let ϕj:E→R‾\phi_j:E\to\overline{\mathbb R}, let ψ:E→R‾\psi:E\to\overline{\mathbb R}, and let K⊆EK\subseteq E. Assume:

  1. For every x∈Kx\in K, ϕj(x)→ψ(x)\phi_j(x)\to\psi(x).
  2. For every y∈Ey\in E,
ψ∗(y)=sup⁡x∈K(⟨x,y⟩−ψ(x)).\psi^*(y)=\sup_{x\in K}\bigl(\langle x,y\rangle-\psi(x)\bigr).

Then, for every y∈Ey\in E,

lim sup⁡j→∞density⁡(ϕj∗)(y)≤density⁡(ψ∗)(y).\limsup_{j\to\infty}\operatorname{density}(\phi_j^*)(y)\le\operatorname{density}(\psi^*)(y).

The result allows extended-real conjugate values and density values in [0,∞][0,\infty].

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.MomentMeasure. Shown in its original module context. Proof omitted.

theorem limsup_density_legendre_le
    (φ : ℕ → E → EReal) (ψ : E → EReal) {K : Set E}
    (hlim : ∀ x ∈ K, Tendsto (fun j => φ j x) atTop (𝓝 (ψ x)))
    (hsup : ∀ y, legendre ψ y = ⨆ x ∈ K, (inner ℝ x y : EReal) - ψ x)
    (y : E) :
    limsup (fun j => density (legendre (φ j)) y) atTop ≤ density (legendre ψ) y

Module navigation

Module: Probability/MomentMeasure/ConjugateMass.

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

Previous: integrable_exp_sub_norm · Next: exists_integrable_exponential_domination.

Source excerpt, lines 69–74 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_MomentMeasure_ConjugateMass

open MeasureTheory Filter Set
open scoped ENNReal Topology
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
open FunctionalInequalities.Analysis
Formal statement

theorem FunctionalInequalities.Probability.MomentMeasure.limsup_density_legendre_le_readable
    (φ : ℕ → E → EReal) (ψ : E → EReal) {K : Set E}
    (hlim : ∀ x ∈ K, Tendsto (fun j => φ j x) atTop (𝓝 (ψ x)))
    (hsup : ∀ y, legendre ψ y = ⨆ x ∈ K, (inner ℝ x y : EReal) - ψ x)
    (y : E) :
    limsup (fun j => density (legendre (φ j)) y) atTop ≤ density (legendre ψ) y := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/MomentMeasure/ConjugateMass.lean#L66-L102 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.MomentMeasure.ConjugateMass`, declaration `FunctionalInequalities.Probability.MomentMeasure.limsup_density_legendre_le`; the repository is private at upload time).

View graph