Prove2Me

Smoothness of the Joint Log-Partition Function

Proved
FunctionalInequalities.Probability.Posterior.contDiff_logPartition_joint_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement establishes the joint smoothness of the posterior log-partition function described in Section 4 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let EE be a complete finite-dimensional real inner-product space with its Borel measurable structure. If μ\mu is a probability law on EE whose support is compact, then the function

(c,Q)⟼ψ(c,Q)=log⁡∫Eexp⁡ ⁣(⟨c,x⟩−12⟨Qx,x⟩) dμ(x)(c,Q)\longmapsto \psi(c,Q) =\log\int_E\exp\!\left(\langle c,x\rangle-\frac12\langle Qx,x\rangle\right)\,d\mu(x)

is C∞C^\infty on E×(E→E)E\times(E\to E):

ContDiff⁡(R,∞,ψ).\operatorname{ContDiff}(\mathbb{R},\infty,\psi).

The result provides the regularity needed for differentiating posterior cumulants and generator expressions with respect to both posterior parameters.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.Posterior. Shown in its original module context. Proof omitted.

theorem contDiff_logPartition_joint
    [CompleteSpace E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E]
    (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) :
    ContDiff ℝ ∞ (fun p : E × (E →L[ℝ] E) => logPartition μ p.1 p.2)

Module navigation

Module: Probability/Posterior/LogPartition.

Next: logLaplace_compactPosterior.

Source excerpt, lines 134–139 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_LogPartition

open MeasureTheory ProbabilityTheory
open scoped RealInnerProductSpace ContDiff
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
omit [CompleteSpace E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
Formal statement

theorem FunctionalInequalities.Probability.Posterior.contDiff_logPartition_joint_readable
    [CompleteSpace E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E]
    (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) :
    ContDiff ℝ ∞ (fun p : E × (E →L[ℝ] E) => logPartition μ p.1 p.2) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Posterior/LogPartition.lean#L131-L202 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.LogPartition`, declaration `FunctionalInequalities.Probability.Posterior.contDiff_logPartition_joint`; the repository is private at upload time).

View graph