Posterior Covariance as a Second Cumulant

This identifies the bilinear form of the posterior covariance with a second cumulant.

Let $\mu$ be a compactly supported probability measure on $\mathbb{R}^n$, let $p$ be a localization parameter, and let $x,y\in\mathbb{R}^n$. If $A(p)=\operatorname{cov}(\mu,p)$ and $\mu_p$ is the compact posterior, then

The two-vector argument is represented formally by ![x, y]. This is a reusable identification of covariance entries with cumulant data.

Original Lean declaration header

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

theorem inner_cov_apply (p : Param n) (x y : EuclideanSpace ℝ (Fin n)) :
    ⟪cov μ hc p x, y⟫ =
      cumulant (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) 2 ![x, y]

Module navigation

Module: KLS/BKL/Localization/CumulantDerivative.

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

Supporting theorems: cumulant_two_eq_centered_moment_of_integrable_exp, memLp_of_polynomial_bound_of_integrable_exp.

Previous: fderiv_cumulant_posterior_apply.

Source excerpt, lines 195–197 · Frozen source 408915f.