Stability of the Quadratic Bound Under Moment Convergence

Proved

FunctionalInequalities.Analysis.BakryEmery.letwinQuadraticBound_of_tendsto_moments_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This formalizes the limiting assertion in Lemma A.1 of Letwin (arXiv:2607.24164v1).

Let $(\mu_k)_{k\in\mathbb N}$ and $\nu$ be probability measures on a finite-dimensional real inner-product space $E$ . Assume:

Each identity map belongs to $L^4(\mu_k)$ and to $L^4(\nu)$ .
For every $d\le4$ and every $v:\operatorname{Fin}(d)\to E$ , the mixed moments converge:

\int\prod_i\langle v_i,x\rangle\,d\mu_k(x)\longrightarrow\int\prod_i\langle v_i,x\rangle\,d\nu(x).

Every $\mu_k$ satisfies LetwinQuadraticBound.

Then $\nu$ also satisfies LetwinQuadraticBound.

The result supplies closure of the quadratic-form estimate under convergence of moments through degree four.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.BakryEmery. Shown in its original module context. Proof omitted.

theorem letwinQuadraticBound_of_tendsto_moments [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E]
    [BorelSpace E] (μ : ℕ → Measure E) (ν : Measure E) [∀ k, IsProbabilityMeasure (μ k)]
    [IsProbabilityMeasure ν] (hμ : ∀ k, MemLp id 4 (μ k)) (hν : MemLp id 4 ν)
    (hmom : ∀ d : ℕ, d ≤ 4 → ∀ v : Fin d → E,
      Tendsto (fun k => ∫ x, ∏ i, ⟪v i, x⟫ ∂(μ k)) atTop (𝓝 (∫ x, ∏ i, ⟪v i, x⟫ ∂ν)))
    (hL : ∀ k, LetwinQuadraticBound (μ k)) : LetwinQuadraticBound ν

Module navigation

Module: Analysis/BakryEmery/Cumulant/Basic.

Previous: cumulant_map_affine.

Source excerpt, lines 1060–1065 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Basic

open MeasureTheory
open scoped RealInnerProductSpace ContDiff
universe u
open ProbabilityTheory Filter Topology
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]

Formal statement


theorem FunctionalInequalities.Analysis.BakryEmery.letwinQuadraticBound_of_tendsto_moments_readable [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E]
    [BorelSpace E] (μ : ℕ → Measure E) (ν : Measure E) [∀ k, IsProbabilityMeasure (μ k)]
    [IsProbabilityMeasure ν] (hμ : ∀ k, MemLp id 4 (μ k)) (hν : MemLp id 4 ν)
    (hmom : ∀ d : ℕ, d ≤ 4 → ∀ v : Fin d → E,
      Tendsto (fun k => ∫ x, ∏ i, ⟪v i, x⟫ ∂(μ k)) atTop (𝓝 (∫ x, ∏ i, ⟪v i, x⟫ ∂ν)))
    (hL : ∀ k, LetwinQuadraticBound (μ k)) : LetwinQuadraticBound ν := by sorry

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Lemma A.1. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Cumulant/Basic.lean#L1055-L1131 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Cumulant.Basic`, declaration `FunctionalInequalities.Analysis.BakryEmery.letwinQuadraticBound_of_tendsto_moments`; the repository is private at upload time).

View graph