Generator Cancellation for Posterior Exponential Expectations

Proved

FunctionalInequalities.KLS.BKL.Localization.generator_posteriorExpectation_exp_inner_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the generator cancellation for exponential posterior expectations.

Let $\mu$ be a compactly supported isotropic probability measure on $\mathbb{R}^n$ , let $z\in\mathbb{R}^n$ , and let $p$ be a localization parameter. For the function

F(q)=\operatorname{posteriorExpectation}(\mu,q_1,q_2)\bigl[x\mapsto e^{\langle z,x\rangle}\bigr],

one has

\operatorname{generator}(\mu)(F)(p)=0.

This is the joint-parameter form of the posterior cancellation identity used in the generator calculation for the log-Laplace transform.

Original Lean declaration header

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

theorem generator_posteriorExpectation_exp_inner (hiso : KLS.Isotropic μ)
    (z : EuclideanSpace ℝ (Fin n)) (p : Param n) :
    generator μ hc
      (fun q : Param n => posteriorExpectation μ q.1 q.2 (fun x => Real.exp ⟪z, x⟫)) p = 0

Module navigation

Module: KLS/BKL/Localization/LogLaplaceGenerator.

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.

Previous: sum_inner_inverseSqrt_sq · Next: posteriorExpectation_exp_inner_eq_exp.

Source excerpt, lines 220–223 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_LogLaplaceGenerator

open scoped RealInnerProductSpace
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
  FunctionalInequalities.Probability.Diffusion
variable {n : ℕ} (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support)

Formal statement


theorem FunctionalInequalities.KLS.BKL.Localization.generator_posteriorExpectation_exp_inner_readable (hiso : KLS.Isotropic μ)
    (z : EuclideanSpace ℝ (Fin n)) (p : Param n) :
    generator μ hc
      (fun q : Param n => posteriorExpectation μ q.1 q.2 (fun x => Real.exp ⟪z, x⟫)) p = 0 := by sorry

Source

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

View graph