Matrix Representation of the Conjugated Noise Operator

This identifies the coordinate matrix of each conjugated noise operator.

Let $\mu$ be a compactly supported isotropic probability measure on $\mathbb{R}^n$. For a localization parameter $p$ and $k\in\operatorname{Fin}(n)$, let $P=A(p)^{-1/2}$ and $H_k=D_cA(p)[\operatorname{noise}(\mu,p,k)]$. Then the standard matrix of the operator $P H_k P$ is the matrix whose entries are

In the formal statement this is stdMatrix (conjugatedNoiseOperator μ hc p k) = conjugatedNoiseMatrix μ hc p k. It supplies the coordinate form needed for Hilbert–Schmidt and vector norm estimates.

Original Lean declaration header

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

set_option maxHeartbeats 1000000 in
theorem stdMatrix_conjugatedNoiseOperator (hiso : KLS.Isotropic μ)
    (p : Param n) (k : Fin n) :
    stdMatrix (conjugatedNoiseOperator μ hc p k) =
      conjugatedNoiseMatrix μ hc p k

Module navigation

Module: KLS/BKL/Localization/Energy/Generator.

Definition modules: KLS/BKL/Localization/Coefficients, KLS/Isotropic, KLS/BKL/Localization/NoiseBound, Analysis/Tensor/EnergyForm.

Supporting theorems: inner_self_pos_of_isPositive_of_isUnit, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, fderiv_cumulant_posterior_apply, inner_cov_apply, contDiff_posteriorCovariance_joint.

Next: generator_cumulantEnergy_eq.

Source excerpt, lines 186–190 · Frozen source 408915f.