Upper Bound for the Inverse-Covariance Trace Generator

This gives an upper bound for the generator of the inverse-covariance trace Lyapunov term.

Let $\mu$ be a compactly supported isotropic log-concave probability measure on $\mathbb{R}^n$, assume CumulantBoundCompact 2 8, and let $p=(c,Q)$ have self-adjoint positive-semidefinite $Q$. Then

where $A(p)=\operatorname{cov}(\mu,p)$ and the generator is the formalized generator.

This estimate combines the exact inverse-covariance generator identity with the conjugated-noise Hilbert–Schmidt bound.

Original Lean declaration header

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

set_option maxHeartbeats 1000000 in
theorem generator_stdTrace_ringInverse_cov_le (hiso : KLS.Isotropic μ) (hLC : KLS.LogConcave μ)
    (h8 : LogConcave.Suspension.CumulantBoundCompact 2 8) (p : Param n)
    (hSym : IsSelfAdjoint p.2) (hQ : ∀ x, 0 ≤ ⟪p.2 x, x⟫) :
    generator μ hc (fun q : Param n => stdTrace (Ring.inverse (cov μ hc q))) p ≤
      (1 + 8 * n) * stdTrace (Ring.inverse (cov μ hc p))

Module navigation

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

Definition modules: Analysis/Operator/HilbertSchmidt, KLS/BKL/Localization/Coefficients, Probability/LogConcave, KLS/Isotropic, KLS/BKL/CompactReduction.

Selected supporting theorems: inner_self_pos_of_comp_eq_id, inner_self_pos_of_isPositive_of_isUnit, norm_apply_sq_le_hsNormSq_mul, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, generator_stdTrace_ringInverse_cov.

Previous: sum_hsNormSq_conjugatedNoiseOperator_le · Next: sum_sq_fderiv_stdTrace_ringInverse_cov_noise_le.

Source excerpt, lines 148–153 · Frozen source 408915f.