Conjugated Noise Matrix Vector Bound

Proved

FunctionalInequalities.KLS.BKL.Localization.sum_sq_conjugatedNoiseMatrix_mulVec_le_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the conjugated form of BKL (79), p. 24.

Let $\mu$ be a compactly supported isotropic log-concave probability measure on $\mathbb{R}^n$ . Assume the compact cumulant bound CumulantBoundCompact 2 8. Let $p=(c,Q)$ be a localization parameter such that $Q$ is self-adjoint and positive semidefinite, and let $v:\operatorname{Fin}(n)\to\mathbb{R}$ . Then

\sum_{i,a}\left(\sum_b \widetilde H_i(a,b)v_b\right)^2 \le 8\sum_a v_a^2,

where $\widetilde H_i$ is represented by conjugatedNoiseMatrix μ hc p i.

This is the coordinate-vector estimate underlying the Hilbert–Schmidt and Lyapunov generator bounds.

Original Lean declaration header

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

theorem sum_sq_conjugatedNoiseMatrix_mulVec_le (hiso : KLS.Isotropic μ) (hLC : KLS.LogConcave μ)
    (h8 : LogConcave.Suspension.CumulantBoundCompact 2 8) (p : Param n)
    (hSym : IsSelfAdjoint p.2) (hQ : ∀ x, 0 ≤ ⟪p.2 x, x⟫) (v : Fin n → ℝ) :
    ∑ i, ∑ a, (∑ b, conjugatedNoiseMatrix μ hc p i a b * v b) ^ 2 ≤ 8 * ∑ a, v a ^ 2

Module navigation

Module: KLS/BKL/Localization/NoiseBound.

Definition modules: KLS/BKL/Localization/Coefficients, Probability/LogConcave, KLS/Isotropic, KLS/BKL/CompactReduction.

Supporting theorems: inner_self_pos_of_isPositive_of_isUnit, inverseSqrt_mul_mul_inverseSqrt, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, compactPosterior_cumulant_bound, cumulant_middle_sum.

Previous: cumulantEnergy_succ_eq.

Source excerpt, lines 199–202 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_NoiseBound

open scoped RealInnerProductSpace
variable {n : ℕ}
variable (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support)

Formal statement


theorem FunctionalInequalities.KLS.BKL.Localization.sum_sq_conjugatedNoiseMatrix_mulVec_le_readable (hiso : KLS.Isotropic μ) (hLC : KLS.LogConcave μ)
    (h8 : LogConcave.Suspension.CumulantBoundCompact 2 8) (p : Param n)
    (hSym : IsSelfAdjoint p.2) (hQ : ∀ x, 0 ≤ ⟪p.2 x, x⟫) (v : Fin n → ℝ) :
    ∑ i, ∑ a, (∑ b, conjugatedNoiseMatrix μ hc p i a b * v b) ^ 2 ≤ 8 * ∑ a, v a ^ 2 := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Lemma 5.1, p. 22. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/NoiseBound.lean#L196-L361 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.NoiseBound`, declaration `FunctionalInequalities.KLS.BKL.Localization.sum_sq_conjugatedNoiseMatrix_mulVec_le`; the repository is private at upload time).

View graph