Posterior parameterization and log-partition function

Definition

KLSModular_FunctionalInequalities_Probability_Posterior_LogPartition

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

The private parameter-space constructions identify $E\times(E\toL[\mathbb{R}]E)$ with a Euclidean coordinate space, define the linear score $\langle c,x\rangle-\frac12\langle Qx,x\rangle$ , represent it as a parameter-space feature, and push a probability measure forward to partitionLaw. The public definition logPartition μ c Q is $\psi(c,Q)=\log\int_E\exp(\langle c,x\rangle-\frac12\langle Qx,x\rangle)\,d\mu(x)$ for a probability measure $\mu$ on a finite-dimensional complete real inner-product space. The bundle also proves continuity of the score and feature maps and constructs the associated measurable pushforward.

Original module imports

import FunctionalInequalities.Probability.Posterior.JointRegularity
import FunctionalInequalities.Analysis.BakryEmery.Cumulant.Basic

Original declaration excerpt

Shown in the original module context.

private abbrev partitionParameterSpace :=
  EuclideanSpace ℝ (Fin (Module.finrank ℝ (E × (E →L[ℝ] E))))

Module navigation

Direct project imports: Probability/Posterior/JointRegularity, Analysis/BakryEmery/Cumulant/Basic.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_JointRegularity
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Basic

noncomputable section
open MeasureTheory ProbabilityTheory
open scoped RealInnerProductSpace ContDiff
namespace FunctionalInequalities
namespace Probability
namespace Posterior
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
 abbrev partitionParameterSpace :=
  EuclideanSpace ℝ (Fin (Module.finrank ℝ (E × (E →L[ℝ] E))))
 def partitionParameterChart : (E × (E →L[ℝ] E)) ≃L[ℝ]
    FunctionalInequalities.Probability.Posterior.partitionParameterSpace (E := E) :=
  (Module.finBasis ℝ (E × (E →L[ℝ] E))).equivFunL.trans
    (PiLp.continuousLinearEquiv 2 ℝ
      (fun _ : Fin (Module.finrank ℝ (E × (E →L[ℝ] E))) => ℝ)).symm
 def partitionParameterScore (x : E) :
    (E × (E →L[ℝ] E)) →L[ℝ] ℝ :=
  (innerSL ℝ x).comp (ContinuousLinearMap.fst ℝ E (E →L[ℝ] E)) -
    (1 / 2 : ℝ) • ((innerSL ℝ x).comp
      ((ContinuousLinearMap.apply ℝ E x).comp
        (ContinuousLinearMap.snd ℝ E (E →L[ℝ] E))))
omit [CompleteSpace E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] in
 theorem partitionParameterScore_continuous :
    Continuous (FunctionalInequalities.Probability.Posterior.partitionParameterScore (E := E)) := by
  have hi : Continuous (fun x : E => innerSL ℝ x) :=
    (InnerProductSpace.toDualMap ℝ E).continuous
  have he : Continuous (fun x : E =>
      (ContinuousLinearMap.apply ℝ E x).comp
        (ContinuousLinearMap.snd ℝ E (E →L[ℝ] E))) :=
    (ContinuousLinearMap.apply ℝ E).continuous.clm_comp_const _
  exact (hi.clm_comp_const _).sub
    ((hi.clm_comp he).const_smul (1 / 2 : ℝ))
 def partitionParameterFeature (x : E) :
    FunctionalInequalities.Probability.Posterior.partitionParameterSpace (E := E) :=
  (InnerProductSpace.toDual ℝ _).symm
    ((FunctionalInequalities.Probability.Posterior.partitionParameterScore x).comp
      (FunctionalInequalities.Probability.Posterior.partitionParameterChart (E := E)).symm.toContinuousLinearMap)
omit [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] in
 theorem partitionParameterFeature_continuous :
    Continuous (FunctionalInequalities.Probability.Posterior.partitionParameterFeature (E := E)) :=
  (InnerProductSpace.toDual ℝ _).symm.continuous.comp
    ((FunctionalInequalities.Probability.Posterior.partitionParameterScore_continuous (E := E)).clm_comp_const
      (FunctionalInequalities.Probability.Posterior.partitionParameterChart (E := E)).symm.toContinuousLinearMap)
 def partitionLaw (μ : ProbabilityMeasure E) :
    ProbabilityMeasure (FunctionalInequalities.Probability.Posterior.partitionParameterSpace (E := E)) :=
  μ.map (FunctionalInequalities.Probability.Posterior.partitionParameterFeature_continuous (E := E)).measurable.aemeasurable
/-- The log-partition function `ψ(c, Q) = log ∫ e^{⟪c,x⟫ − ½⟪Qx,x⟫} dμ(x)` of the BKL posterior (67). -/
def logPartition (μ : ProbabilityMeasure E) (c : E) (Q : E →L[ℝ] E) : ℝ :=
  Real.log (∫ x, Real.exp (quadraticExponent c Q x) ∂(μ : Measure E))
end Posterior
end Probability
end FunctionalInequalities

Source

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

View graph