Posterior expectations and means

Definition

KLSModular_FunctionalInequalities_Probability_Posterior_Generator

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a probability measure $\mu$ on a finite-dimensional real inner-product space, posteriorExpectation μ c Q f is the integral of a real-valued function $f$ against the tilt of $\mu$ by $\langle c,x\rangle-\frac12\langle Qx,x\rangle$ . Under completeness of the space, posteriorMean μ c Q is the vector integral $\int x\,d\mu_{c,Q}$ for that same tilted measure. These declarations are definitions only; they do not assert differentiability, covariance formulas, or a generator identity.

Original module imports

import FunctionalInequalities.Probability.Posterior.CompactQuadratic
import FunctionalInequalities.Analysis.BakryEmery.Tilt.Local
import FunctionalInequalities.Analysis.BakryEmery.Calculus
import Mathlib.Analysis.Calculus.Deriv.Comp
import Mathlib.Analysis.InnerProductSpace.PiL2

Original declaration excerpt

Shown in the original module context.

def posteriorExpectation (μ : ProbabilityMeasure E) (c : E) (Q : E →L[ℝ] E) (f : E → ℝ) : ℝ :=
  ∫ x, f x ∂((μ : Measure E).tilted (quadraticExponent c Q))

Module navigation

Direct project imports: Probability/Posterior/CompactQuadratic, Analysis/BakryEmery/Tilt/Local, Analysis/BakryEmery/Calculus.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Probability.Posterior.Generator · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_CompactQuadratic
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_Local
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Calculus
import Mathlib.Analysis.Calculus.Deriv.Comp
import Mathlib.Analysis.InnerProductSpace.PiL2

noncomputable section
open MeasureTheory Filter Topology ProbabilityTheory
open FunctionalInequalities.Analysis.BakryEmery
open scoped RealInnerProductSpace ContDiff
namespace FunctionalInequalities
namespace Probability
namespace Posterior
section Smooth
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
/-- The expectation `∫ f dμ_{c,Q}` of `f` under the posterior with parameters `(c, Q)`. -/
def posteriorExpectation (μ : ProbabilityMeasure E) (c : E) (Q : E →L[ℝ] E) (f : E → ℝ) : ℝ :=
  ∫ x, f x ∂((μ : Measure E).tilted (quadraticExponent c Q))
end Smooth
section Mean
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
/-- The mean `a = ∫ x dμ_{c,Q}` of the posterior. -/
def posteriorMean (μ : ProbabilityMeasure E) (c : E) (Q : E →L[ℝ] E) : E :=
  ∫ x, x ∂((μ : Measure E).tilted (quadraticExponent c Q))
variable {ι : Type*} [Fintype ι]
end Mean
end Posterior
end Probability
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Posterior/Generator.lean#L29-L181 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.Generator`, definition bundle `KLSModular_FunctionalInequalities_Probability_Posterior_Generator`; the repository is private at upload time).

View graph