Regular-Class Matrix Variance Bound

Let $n>0$, let $K\subset\mathbb R^n$ be compact and convex with nonempty interior, let $\kappa>0$, and let $W:\mathbb R^n\to\mathbb R$ be smooth with $W(y)-\frac\kappa2\|y\|^2$ convex. Let $\mu$ be the normalized isotropic probability measure whose density is $1_Ke^{-W}$ with respect to Lebesgue measure. For every symmetric matrix $M\in\mathbb R^{n\times n}$,

The theorem is the regular-class quadratic variance estimate. The Lean statement quantifies over all symmetric matrices, including singular and indefinite ones.

Original Lean declaration header

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

include hn hκ hK hKc hKint hW hstrong hμ hiso in
set_option maxHeartbeats 1500000 in
theorem regularClass_matrix_variance_le_eight :
    ∀ M : Matrix (Fin n) (Fin n) ℝ, M.IsSymm →
      variance (fun x : EuclideanSpace ℝ (Fin n) => ∑ i, ∑ j, M i j*x i*x j)
        (μ : Measure _) ≤ 8 * Matrix.trace (M*M)

Module navigation

Module: KLS/Letwin/RegularClass.

Definition modules: KLS/Isotropic.

Selected supporting theorems: exists_symmetric_isUnit_matrix_sequence, integral_fderiv_tilted_eq_integral_mul_fderiv_of_bounded_lipschitz, symmetric_matrix_spectral_geometry, symmetric_trace_integral_extension_mul_of_ae_posSemidef, gaussianLaw_exp_norm_integrable.

Source excerpt, lines 66–71 · Frozen source 408915f.

Literature

This formalizes Theorem 1.2 of Letwin (arXiv:2607.24164v1), cited as “Quadratic-form Poincaré inequality.”