Squared Noise Derivative Bound for Inverse-Covariance Trace

Proved

FunctionalInequalities.KLS.BKL.Localization.sum_sq_fderiv_stdTrace_ringInverse_cov_noise_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This bounds the sum of squared noise derivatives of the inverse-covariance trace.

Let $\mu$ be a compactly supported isotropic log-concave probability measure on $\mathbb{R}^n$ , assume CumulantBoundCompact 2 8, and let $p=(c,Q)$ have self-adjoint positive-semidefinite $Q$ . Then

\sum_k\left(D\!\left[\operatorname{tr}(A^{-1})\right]_p[\operatorname{noise}_k]\right)^2 \le 8n\,\operatorname{tr}(A(p)^{-1})^2.

The result is a quantitative derivative estimate for the inverse-covariance component of the localization Lyapunov function.

Original Lean declaration header

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

set_option maxHeartbeats 1000000 in
theorem sum_sq_fderiv_stdTrace_ringInverse_cov_noise_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⟫) :
    ∑ k, (fderiv ℝ (fun q : Param n => stdTrace (Ring.inverse (cov μ hc q))) p (noise μ hc p k)) ^ 2 ≤
      8 * n * stdTrace (Ring.inverse (cov μ hc p)) ^ 2

Module navigation

Module: KLS/BKL/Localization/Lyapunov/Bound.

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

Selected supporting theorems: inner_self_pos_of_comp_eq_id, inner_self_pos_of_isPositive_of_isUnit, norm_apply_sq_le_hsNormSq_mul, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, fderiv_stdTrace_ringInverse_cov_noise.

Previous: generator_stdTrace_ringInverse_cov_le · Next: exists_generator_lyapunov_le.

Source excerpt, lines 224–229 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Lyapunov_Bound

open scoped RealInnerProductSpace ContDiff
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
  FunctionalInequalities.Analysis.BakryEmery FunctionalInequalities.Probability.Diffusion
  FunctionalInequalities.Analysis.CoordinateTensor
variable {n : ℕ} (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support)
set_option maxHeartbeats 1000000

Formal statement

theorem FunctionalInequalities.KLS.BKL.Localization.sum_sq_fderiv_stdTrace_ringInverse_cov_noise_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⟫) :
    ∑ k, (fderiv ℝ (fun q : Param n => stdTrace (Ring.inverse (cov μ hc q))) p (noise μ hc p k)) ^ 2 ≤
      8 * n * stdTrace (Ring.inverse (cov μ hc p)) ^ 2 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/Lyapunov/Bound.lean#L224-L377 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.Lyapunov.Bound`, declaration `FunctionalInequalities.KLS.BKL.Localization.sum_sq_fderiv_stdTrace_ringInverse_cov_noise_le`; the repository is private at upload time).

View graph