Convergence of Covariance Operators from Low Moments

Proved

FunctionalInequalities.KLS.covariance_tendsto_one_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This auxiliary lemma shows convergence of covariance operators from support and moment hypotheses.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure. Let $(λ_k)$ and $μ$ be probability measures on $E$ , and assume Isotropic μ. Fix $R\in\mathbb R$ . Suppose:

every $λ_k$ gives measure zero to the complement of the closed ball $\overline B(0,R)$ ;
for every degree $d\le 4$ and every family $v:\operatorname{Fin}(d)\to E$ , the mixed moments of $λ_k$ converge to those of $μ$ :

\int_E\prod_i\langle v_i,x\rangle\,dλ_k(x) \longrightarrow \int_E\prod_i\langle v_i,x\rangle\,dμ(x).

Then the covariance operators converge to the identity operator:

\operatorname{Covariance.operator}(λ_k)\longrightarrow I

in the operator topology.

Original Lean declaration header

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

private lemma covariance_tendsto_one
    {lam : ℕ → ProbabilityMeasure E} {μ : ProbabilityMeasure E}
    (hiso : Isotropic μ) {R : ℝ}
    (hsupp : ∀ k, (lam k : Measure E) (closedBall (0 : E) R)ᶜ = 0)
    (hmom : ∀ d : ℕ, d ≤ 4 → ∀ v : Fin d → E,
      Tendsto (fun k => ∫ x, ∏ i, ⟪v i, x⟫ ∂(lam k : Measure E)) atTop
        (𝓝 (∫ x, ∏ i, ⟪v i, x⟫ ∂(μ : Measure E)))) :
    Tendsto (fun k => Covariance.operator (lam k : Measure E)) atTop (𝓝 1)

Module navigation

Module: KLS/LogConcave/BallConditioning.

Definition modules: Probability/Covariance/Basic, KLS/Isotropic.

Previous: exists_regularClass_of_cond_closedBall_map · Next: whitening_sequence.

Source excerpt, lines 321–328 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_BallConditioning

open MeasureTheory Set Metric Filter
open scoped Topology RealInnerProductSpace MatrixOrder Matrix.Norms.L2Operator
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
variable [MeasurableSpace E] [BorelSpace E]

Formal statement

 lemma FunctionalInequalities.KLS.covariance_tendsto_one_readable
    {lam : ℕ → ProbabilityMeasure E} {μ : ProbabilityMeasure E}
    (hiso : Isotropic μ) {R : ℝ}
    (hsupp : ∀ k, (lam k : Measure E) (closedBall (0 : E) R)ᶜ = 0)
    (hmom : ∀ d : ℕ, d ≤ 4 → ∀ v : Fin d → E,
      Tendsto (fun k => ∫ x, ∏ i, ⟪v i, x⟫ ∂(lam k : Measure E)) atTop
        (𝓝 (∫ x, ∏ i, ⟪v i, x⟫ ∂(μ : Measure E)))) :
    Tendsto (fun k => Covariance.operator (lam k : Measure E)) atTop (𝓝 1) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/BallConditioning.lean#L321-L369 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.BallConditioning`, declaration `_private.FunctionalInequalities.KLS.LogConcave.BallConditioning.0.FunctionalInequalities.KLS.covariance_tendsto_one`; the repository is private at upload time).

View graph