Prove2Me

Joint Smoothness of Posterior Cumulants

Proved
FunctionalInequalities.KLS.BKL.Localization.contDiff_cumulant_posterior_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement records the joint smoothness of posterior cumulants in the parameter pair p=(c,Q)p=(c,Q) for compactly supported priors.

Let μ\mu be a probability law on EuclideanSpace⁡(R,Fin⁡n)\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n) with compact support. Let m≥1m\ge1 and let h:Fin⁡m→EuclideanSpace⁡(R,Fin⁡n)h:\operatorname{Fin}m\to\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n). Then

p⟼κm(μp1,p2)(h)p\longmapsto \kappa_m(\mu_{p_1,p_2})(h)

is C∞C^\infty on the full parameter space:

ContDiff⁡(R,∞,p↦cumulant⁡(μp1,p2,m)(h)).\operatorname{ContDiff}(\mathbb{R},\infty,p\mapsto \operatorname{cumulant}(\mu_{p_1,p_2},m)(h)).

This regularity result supports differentiation of cumulant-valued quantities along the localization parameter space.

Original Lean declaration header

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

theorem contDiff_cumulant_posterior {m : ℕ} (hm : 1 ≤ m) (h : Fin m → EuclideanSpace ℝ (Fin n)) :
    ContDiff ℝ ∞ (fun q : Param n =>
      cumulant (compactPosterior μ hc q.1 q.2 : Measure (EuclideanSpace ℝ (Fin n))) m h)

Module navigation

Module: KLS/BKL/Localization/CumulantDerivative.

Definition modules: KLS/BKL/Localization/Coefficients, Analysis/BakryEmery/Cumulant/Basic, Probability/Posterior/CompactDomain.

Supporting theorems: contDiff_logPartition_joint, cumulant_compactPosterior.

Next: fderiv_cumulant_posterior_apply.

Source excerpt, lines 93–95 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_CumulantDerivative

open MeasureTheory
open scoped RealInnerProductSpace ContDiff
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
  FunctionalInequalities.Analysis.BakryEmery
variable {n : ℕ} (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support)
Formal statement

theorem FunctionalInequalities.KLS.BKL.Localization.contDiff_cumulant_posterior_readable {m : ℕ} (hm : 1 ≤ m) (h : Fin m → EuclideanSpace ℝ (Fin n)) :
    ContDiff ℝ ∞ (fun q : Param n =>
      cumulant (compactPosterior μ hc q.1 q.2 : Measure (EuclideanSpace ℝ (Fin n))) m h) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/CumulantDerivative.lean#L90-L124 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.CumulantDerivative`, declaration `FunctionalInequalities.KLS.BKL.Localization.contDiff_cumulant_posterior`; the repository is private at upload time).

View graph