Zero Generator Drift for Posterior Expectations

This is the deterministic zero-drift identity associated with Equation (68) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $n\in\mathbb N$, let $\mu$ be an isotropic probability measure on EuclideanSpace ℝ (Fin n) with compact support, and let $f$ be measurable and bounded on the support: for some $C\ge0$, $\lVert f(x)\rVert\le C$. For every posterior parameter $p\in\operatorname{Param}(n)$, the uncut generator applied to the posterior expectation is zero:

In Lean, the function is represented as fun q => posteriorExpectation μ q.1 q.2 f, and the generator is Localization.generator. The statement is finite-dimensional and concerns the deterministic generator identity only.

Original Lean declaration header

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

theorem generator_posteriorExpectation (hiso : KLS.Isotropic μ)
    {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : Measurable f) {C : ℝ} (hC : 0 ≤ C)
    (hfb : ∀ x ∈ (μ : Measure (EuclideanSpace ℝ (Fin n))).support, ‖f x‖ ≤ C) (p : Param n) :
    generator μ hc (fun q : Param n => posteriorExpectation μ q.1 q.2 f) p = 0

Module navigation

Module: KLS/BKL/Localization/CovarianceGenerator.

Definition modules: KLS/BKL/Localization/Coefficients, Probability/Posterior/Generator, 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, fderiv_fderiv_fst_dir, sum_bilin_inverseSqrt_eq.

Next: generator_inner_cov.

Source excerpt, lines 61–64 · Frozen source 408915f.