Noise Derivative of the Inverse-Covariance Trace

This is the directional derivative formula for the inverse-covariance trace along a noise direction.

Let $\mu$ be a compactly supported isotropic probability measure on $\mathbb{R}^n$, let $p$ be a localization parameter, and let $k\in\operatorname{Fin}(n)$. With $A(p)=\operatorname{cov}(\mu,p)$, $S=A(p)^{-1/2}$, and $H_k=D_cA(p)[\operatorname{noise}(\mu,p,k)]$, one has

This exact first-derivative identity is used to estimate the squared noise derivatives of the Lyapunov term.

Original Lean declaration header

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

theorem fderiv_stdTrace_ringInverse_cov_noise (hiso : KLS.Isotropic μ) (p : Param n) (k : Fin n) :
    fderiv ℝ (fun q : Param n => stdTrace (Ring.inverse (cov μ hc q))) p (noise μ hc p k) =
      -∑ i, ⟪inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ 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))⟫

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, contDiff_posteriorCovariance_joint.

Previous: generator_hsNormSq_snd · Next: generator_stdTrace_ringInverse_cov.

Source excerpt, lines 327–331 · Frozen source 408915f.