Covariance Operator Eigenfunction Identity

Proved

FunctionalInequalities.KLS.BKL.Localization.generator_inner_cov_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the generator identity corresponding to BKL (69).

Let $n\in\mathbb N$ , let $\mu$ be an isotropic compactly supported probability measure on EuclideanSpace ℝ (Fin n), and let $p$ be a posterior parameter. For all $x,y\in\mathbb R^n$ , the generator applied to the scalar covariance-operator coefficient satisfies

\mathcal L\left[q\mapsto\langle \operatorname{Cov}(\mu_q)x,y\rangle\right](p) =-\langle\operatorname{Cov}(\mu_p)x,y\rangle.

Here cov μ hc q is the posterior covariance operator and Localization.generator is the uncut posterior generator. This identity is the operator-valued decay relation used in the covariance-generator analysis.

Original Lean declaration header

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

theorem generator_inner_cov (hiso : KLS.Isotropic μ) (p : Param n) (x y : EuclideanSpace ℝ (Fin n)) :
    generator μ hc (fun q : Param n => ⟪cov μ hc q x, y⟫) p = -⟪cov μ hc p x, y⟫

Module navigation

Module: KLS/BKL/Localization/CovarianceGenerator.

Definition modules: KLS/BKL/Localization/Coefficients, KLS/Isotropic.

Selected supporting theorems: inner_self_pos_of_comp_eq_id, inner_self_pos_of_isPositive_of_isUnit, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, generator_posteriorExpectation, diffusionGenerator_mul.

Previous: generator_posteriorExpectation.

Source excerpt, lines 78–79 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_CovarianceGenerator

open scoped RealInnerProductSpace ContDiff
variable {n : ℕ} (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support)

Formal statement


theorem FunctionalInequalities.KLS.BKL.Localization.generator_inner_cov_readable (hiso : KLS.Isotropic μ) (p : Param n) (x y : EuclideanSpace ℝ (Fin n)) :
    generator μ hc (fun q : Param n => ⟪cov μ hc q x, y⟫) p = -⟪cov μ hc p x, y⟫ := by sorry

Source

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

View graph