Generator of the Squared Linear Parameter Norm

Proved

FunctionalInequalities.KLS.BKL.Localization.generator_norm_sq_fst_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 norm of the linear parameter.

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_1\|^2\bigr)(p) =2\left\langle c,\operatorname{cov}(\mu,p)^{-1}a(\mu;p)\right\rangle +\operatorname{stdTrace}\!\left(\operatorname{cov}(\mu,p)^{-1}\right),

where $a(\mu;p)$ is the posterior mean, cov is the posterior covariance operator, and stdTrace is the standard trace of the inverse covariance. This is an exact Lyapunov-generator identity.

Original Lean declaration header

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

theorem generator_norm_sq_fst (hiso : KLS.Isotropic μ) (p : Param n) :
    generator μ hc (fun q : Param n => ‖q.1‖ ^ 2) p =
      2 * ⟪p.1, Ring.inverse (cov μ hc p) (posteriorMean μ p.1 p.2)⟫ + stdTrace (Ring.inverse (cov μ hc p))

Module navigation

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

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

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: contDiff_lyapunov · Next: generator_hsNormSq_snd.

Source excerpt, lines 255–257 · 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_norm_sq_fst_readable (hiso : KLS.Isotropic μ) (p : Param n) :
    generator μ hc (fun q : Param n => ‖q.1‖ ^ 2) p =
      2 * ⟪p.1, Ring.inverse (cov μ hc p) (posteriorMean μ p.1 p.2)⟫ + stdTrace (Ring.inverse (cov μ hc p)) := by sorry

Source

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

View graph