Hilbert–Schmidt Bound for Conjugated Noise Operators

Proved

FunctionalInequalities.KLS.BKL.Localization.sum_hsNormSq_conjugatedNoiseOperator_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This bounds the total Hilbert–Schmidt size of the conjugated noise operators.

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\in\operatorname{Fin}(n)} \left\|\widetilde H_k\right\|_{\mathrm{HS}}^2 \le 8n.

Here the operators are conjugatedNoiseOperator and hsNormSq denotes the formalized squared Hilbert–Schmidt norm. The statement is a summed operator-norm estimate used in subsequent generator bounds.

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_hsNormSq_conjugatedNoiseOperator_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, hsNormSq (conjugatedNoiseOperator μ hc p k) ≤ 8 * n

Module navigation

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

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

Supporting theorems: stdMatrix_conjugatedNoiseOperator, sum_sq_conjugatedNoiseMatrix_mulVec_le.

Next: generator_stdTrace_ringInverse_cov_le.

Source excerpt, lines 97–101 · 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_hsNormSq_conjugatedNoiseOperator_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, hsNormSq (conjugatedNoiseOperator μ hc p k) ≤ 8 * n := by sorry

Source

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

View graph