Pointwise Lower-Drift Square-Sum Bound

Proved

FunctionalInequalities.KLS.BKL.sqrt_sum_lowerDrift_sq_le_aux_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the Section 6 pointwise estimate with order parameter $m=k+1$ .

Let $\nu$ be a compactly supported probability measure on $\mathbb{R}^n$ with invertible covariance operator that is strictly positive on nonzero vectors. Let $k\in\mathbb{N}$ , let $b:\mathbb{N}\to\mathbb{R}$ , and assume that for every $r$ with $2\le r<k+1$ and every $v$ ,

E_{r-1}(v)\le b(r)\langle Av,v\rangle.

Then for every $u\in\mathbb{R}^n$ ,

\sqrt{\sum_{J:\operatorname{Fin}(k)\to\operatorname{Fin}(n)} L(\nu)(u,\sigma e_{J_1},\ldots,\sigma e_{J_k})^2} \le \sum_{a\in[2,k-1]} \binom{k}{a-1} \sqrt{b(k+2-a)E_a(u)}.

Here lowerDrift, sigmaBasis, and cumulantEnergy are the formalized quantities. The result supplies the pointwise middle-term estimate used in the cumulant-energy induction.

Original Lean declaration header

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

theorem sqrt_sum_lowerDrift_sq_le_aux (ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
    (hc : IsCompact (ν : Measure (EuclideanSpace ℝ (Fin n))).support)
    (hA : IsUnit (Covariance.operator (ν : Measure (EuclideanSpace ℝ (Fin n)))))
    (hApos : ∀ v, v ≠ 0 → 0 < ⟪Covariance.operator (ν : Measure (EuclideanSpace ℝ (Fin n))) v, v⟫)
    (k : ℕ) (b : ℕ → ℝ)
    (h100 : ∀ r, 2 ≤ r → r < k + 1 → ∀ v : EuclideanSpace ℝ (Fin n),
      cumulantEnergy (ν : Measure (EuclideanSpace ℝ (Fin n))) (r - 1) v ≤
        b r * ⟪Covariance.operator (ν : Measure (EuclideanSpace ℝ (Fin n))) v, v⟫)
    (u : EuclideanSpace ℝ (Fin n)) :
    Real.sqrt (∑ J : Fin k → Fin n,
        lowerDrift (ν : Measure (EuclideanSpace ℝ (Fin n)))
          (Fin.cons u fun i => inverseSqrt (Covariance.operator (ν : Measure (EuclideanSpace ℝ (Fin n))))
            (EuclideanSpace.basisFun (Fin n) ℝ (J i)) : Fin (k + 1) → EuclideanSpace ℝ (Fin n)) 0 ^ 2) ≤
      ∑ a ∈ Finset.Icc 2 (k - 1), (k.choose (a - 1) : ℝ) *
        Real.sqrt (b (k + 2 - a) * cumulantEnergy (ν : Measure (EuclideanSpace ℝ (Fin n))) a u)

Module navigation

Module: KLS/BKL/CumulantEnergy/Basic.

Definition modules: Probability/Covariance/Basic, Analysis/Operator/InverseSqrt.

Supporting theorems: sqrt_sum_sq_sum_le, sum_selected_eq, sum_sq_pairTerm_ofFn_le.

Previous: sum_sq_pairTerm_ofFn_le.

Source excerpt, lines 433–447 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_CumulantEnergy_Basic

open MeasureTheory
open FunctionalInequalities.Analysis FunctionalInequalities.Analysis.BakryEmery
open scoped RealInnerProductSpace
variable {n : ℕ}

Formal statement


theorem FunctionalInequalities.KLS.BKL.sqrt_sum_lowerDrift_sq_le_aux_readable (ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
    (hc : IsCompact (ν : Measure (EuclideanSpace ℝ (Fin n))).support)
    (hA : IsUnit (Covariance.operator (ν : Measure (EuclideanSpace ℝ (Fin n)))))
    (hApos : ∀ v, v ≠ 0 → 0 < ⟪Covariance.operator (ν : Measure (EuclideanSpace ℝ (Fin n))) v, v⟫)
    (k : ℕ) (b : ℕ → ℝ)
    (h100 : ∀ r, 2 ≤ r → r < k + 1 → ∀ v : EuclideanSpace ℝ (Fin n),
      cumulantEnergy (ν : Measure (EuclideanSpace ℝ (Fin n))) (r - 1) v ≤
        b r * ⟪Covariance.operator (ν : Measure (EuclideanSpace ℝ (Fin n))) v, v⟫)
    (u : EuclideanSpace ℝ (Fin n)) :
    Real.sqrt (∑ J : Fin k → Fin n,
        lowerDrift (ν : Measure (EuclideanSpace ℝ (Fin n)))
          (Fin.cons u fun i => inverseSqrt (Covariance.operator (ν : Measure (EuclideanSpace ℝ (Fin n))))
            (EuclideanSpace.basisFun (Fin n) ℝ (J i)) : Fin (k + 1) → EuclideanSpace ℝ (Fin n)) 0 ^ 2) ≤
      ∑ a ∈ Finset.Icc 2 (k - 1), (k.choose (a - 1) : ℝ) *
        Real.sqrt (b (k + 2 - a) * cumulantEnergy (ν : Measure (EuclideanSpace ℝ (Fin n))) a u) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/CumulantEnergy/Basic.lean#L432-L527 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.CumulantEnergy.Basic`, declaration `FunctionalInequalities.KLS.BKL.sqrt_sum_lowerDrift_sq_le_aux`; the repository is private at upload time).

View graph