C-Derivative of a Posterior Cumulant

This formalizes the parameter derivative identity for posterior cumulants.

Let $\mu$ be a compactly supported probability measure on $\mathbb{R}^n$, let $m\ge 1$, let $h:\operatorname{Fin}(m)\to\mathbb{R}^n$, let $p=(c,Q)$ be a localization parameter, and let $v\in\mathbb{R}^n$. Differentiating only in the $c$-direction $(v,0)$ gives

where the right-hand list is represented by Fin.snoc h v, and the cumulants are the formalized cumulant of the compact posterior.

The result provides the basic conversion between localization-parameter derivatives and higher posterior cumulants.

Original Lean declaration header

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

theorem fderiv_cumulant_posterior_apply {m : ℕ} (hm : 1 ≤ m) (h : Fin m → EuclideanSpace ℝ (Fin n))
    (p : Param n) (v : EuclideanSpace ℝ (Fin n)) :
    fderiv ℝ (fun q : Param n =>
        cumulant (compactPosterior μ hc q.1 q.2 : Measure (EuclideanSpace ℝ (Fin n))) m h) p (v, 0) =
      cumulant (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) (m + 1) (Fin.snoc h v)

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.

Previous: contDiff_cumulant_posterior · Next: inner_cov_apply.

Source excerpt, lines 128–132 · Frozen source 408915f.