Generator of the Hilbert–Schmidt Norm of $Q$

Proved

FunctionalInequalities.KLS.BKL.Localization.generator_hsNormSq_snd_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement computes the localization generator applied to the squared Hilbert–Schmidt norm of the quadratic parameter, namely the identity described by $\mathcal L\|Q\|_{\mathrm{HS}}^2$ .

Let $\mu$ be a compactly supported isotropic probability law on $\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n)$ and let $p=(c,Q)$ be a localization parameter. Then

\operatorname{generator}\bigl(\mu,h_c,q\mapsto\|q_2\|_{\mathrm{HS}}^2\bigr)(p) =2\sum_{j=1}^{n} \left\langle Qe_j,\operatorname{cov}(\mu,p)^{-1}e_j\right\rangle.

The formula has no diffusion contribution acting on $Q$ and is an exact generator-calculus identity.

Original Lean declaration header

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

theorem generator_hsNormSq_snd (hiso : KLS.Isotropic μ) (p : Param n) :
    generator μ hc (fun q : Param n => hsNormSq q.2) p =
      2 * ∑ j, ⟪p.2 (EuclideanSpace.basisFun (Fin n) ℝ j),
        Ring.inverse (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ j)⟫

Module navigation

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

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

Supporting theorems: inner_self_pos_of_isPositive_of_isUnit, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, fderiv_fderiv_fst_dir, sum_bilin_inverseSqrt_eq.

Previous: generator_norm_sq_fst · Next: fderiv_stdTrace_ringInverse_cov_noise.

Source excerpt, lines 284–287 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Lyapunov_Basic

open scoped RealInnerProductSpace ContDiff
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
  FunctionalInequalities.Analysis.BakryEmery FunctionalInequalities.Probability.Diffusion
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.generator_hsNormSq_snd_readable (hiso : KLS.Isotropic μ) (p : Param n) :
    generator μ hc (fun q : Param n => hsNormSq q.2) p =
      2 * ∑ j, ⟪p.2 (EuclideanSpace.basisFun (Fin n) ℝ j),
        Ring.inverse (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ j)⟫ := by sorry

Source

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

View graph

Generator of the Hilbert–Schmidt Norm of QQQ

Generator of the Hilbert–Schmidt Norm of $Q$