Exponential Formula for Posterior Expectations

Proved

FunctionalInequalities.KLS.BKL.Localization.posteriorExpectation_exp_inner_eq_exp_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This expresses an exponential posterior expectation through the log-partition function.

Let $\mu$ be a compactly supported probability measure on $\mathbb{R}^n$ , let $z\in\mathbb{R}^n$ , and let $q=(c,Q)$ be a localization parameter. Then

\mathbb E_{\mu_{c,Q}}\!\left[e^{\langle z,X\rangle}\right] =\exp\!\left(\psi(c+z,Q)-\psi(c,Q)\right).

The formal statement uses posteriorExpectation and logPartition. It is the algebraic bridge between posterior exponential moments and the posterior log-Laplace transform.

Original Lean declaration header

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

theorem posteriorExpectation_exp_inner_eq_exp (z : EuclideanSpace ℝ (Fin n)) (q : Param n) :
    posteriorExpectation μ q.1 q.2 (fun x => Real.exp ⟪z, x⟫) =
      Real.exp (logPartition μ (q.1 + z) q.2 - logPartition μ q.1 q.2)

Module navigation

Module: KLS/BKL/Localization/LogLaplaceGenerator.

Definition modules: KLS/BKL/Localization/Coefficients, Probability/Posterior/LogPartition, Probability/Posterior/Generator.

Previous: generator_posteriorExpectation_exp_inner · Next: fderiv_logLaplace_fst_dir.

Source excerpt, lines 239–241 · 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)
include hc

Formal statement


theorem FunctionalInequalities.KLS.BKL.Localization.posteriorExpectation_exp_inner_eq_exp_readable (z : EuclideanSpace ℝ (Fin n)) (q : Param n) :
    posteriorExpectation μ q.1 q.2 (fun x => Real.exp ⟪z, x⟫) =
      Real.exp (logPartition μ (q.1 + z) q.2 - logPartition μ q.1 q.2) := by sorry

Source

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

View graph