Generator of the Standard Trace of Inverse Covariance

This is an exact generator identity for the standard trace of the inverse posterior covariance.

Let $\mu$ be a probability measure on $\mathbb{R}^n\simeq\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}(n))$ with compact support, and assume that $\mu$ is isotropic. For a localization parameter $p$, let $A(p)=\operatorname{cov}(\mu,p)$, let $H_k=D_cA(p)[\operatorname{noise}(\mu,p,k)]$, and let $S=A(p)^{-1/2}$. Then

where the sums range over $k,i\in\operatorname{Fin}(n)$ and $e_i$ is the Euclidean coordinate basis. Here generator, cov, stdTrace, inverseSqrt, and noise are the formalized constructions.

This identity is the exact second-order calculus used to bound the Lyapunov generator in the localization argument.

Original Lean declaration header

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

theorem generator_stdTrace_ringInverse_cov (hiso : KLS.Isotropic μ) (p : Param n) :
    generator μ hc (fun q : Param n => stdTrace (Ring.inverse (cov μ hc q))) p =
      stdTrace (Ring.inverse (cov μ hc p)) +
        ∑ k, ∑ i, ‖(inverseSqrt (cov μ hc p) * fderiv ℝ (cov μ hc) p (noise μ hc p k) * inverseSqrt (cov μ hc p))
          (inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ i))‖ ^ 2

Module navigation

Module: KLS/BKL/Localization/Lyapunov/Basic.

Definition modules: Analysis/Operator/HilbertSchmidt, KLS/BKL/Localization/Coefficients, KLS/Isotropic, Analysis/Operator/InverseSqrt.

Supporting theorems: inner_self_pos_of_isPositive_of_isUnit, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, generator_inner_cov, vectorGenerator_clm_comp, contDiff_posteriorCovariance_joint.

Previous: fderiv_stdTrace_ringInverse_cov_noise.

Source excerpt, lines 365–369 · Frozen source 408915f.