Gradient of the Posterior Log-Partition Function

Proved

FunctionalInequalities.Probability.Posterior.fderiv_logPartition_c_apply_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This identifies the $c$ -gradient of the posterior log-partition function with the posterior mean.

Let $E$ be a finite-dimensional real inner-product space, let $\mu$ be a compactly supported probability measure on $E$ , let $c,h\in E$ , and let $Q:E\to E$ be a continuous linear map. For

\psi(c,Q)=\log\int \exp\!\left(\langle c,x\rangle-\tfrac12\langle Qx,x\rangle\right)\,d\mu(x),

one has

D_c\psi(c,Q)[h]=\langle h,\operatorname{posteriorMean}(\mu,c,Q)\rangle.

The formal definitions are logPartition and posteriorMean. Compact support supplies the differentiability and integrability assumptions required by the statement.

Original Lean declaration header

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

theorem fderiv_logPartition_c_apply (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (c : E) (Q : E →L[ℝ] E) (h : E) :
    fderiv ℝ (fun y => logPartition μ y Q) c h = ⟪h, posteriorMean μ c Q⟫

Module navigation

Module: Probability/Posterior/LogPartition.

Definition modules: Probability/Posterior/Generator.

Supporting theorems: contDiff_weighted_integral_quadraticExponent_of_compact, exists_uniform_norm_moments_tilted_quadraticExponent_of_compact, hasDerivAt_weighted_integral_of_compact.

Previous: cumulant_compactPosterior.

Source excerpt, lines 306–308 · 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]

Formal statement


theorem FunctionalInequalities.Probability.Posterior.fderiv_logPartition_c_apply_readable (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (c : E) (Q : E →L[ℝ] E) (h : E) :
    fderiv ℝ (fun y => logPartition μ y Q) c h = ⟪h, posteriorMean μ c Q⟫ := by sorry

Source

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

View graph