Positive Definiteness of a Regular Law's Covariance

This statement asserts strict positivity of the covariance quadratic form of a regular law on every nonzero vector.

Let $E$ be a finite-dimensional complete real inner product space with its Borel measurable structure. Let $V:E\to\mathbb R$ and $a,b\in\mathbb R$, and assume $h_V:$ KLS.RegularPotential V a b. Let $\mu$ be the associated probability law RegularPotential.law hV, and let $\Sigma_\mu$ denote Covariance.operator. For every $v\in E$ with $v\ne0$,

This positivity statement supplies the nondegeneracy needed for covariance whitening of regular laws.

Formalization Note The regularity and curvature requirements are those of the supplied RegularPotential predicate with parameters $a,b$; there is no additional hypothesis $b>0$ in this declaration. Dimension zero is allowed.

Original Lean declaration header

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

theorem covariance_pos (hV : KLS.RegularPotential V a b) {v : E} (hv : v ≠ 0) :
    0 < inner ℝ (Covariance.operator (hV.law : Measure E) v) v

Module navigation

Module: KLS/LogConcave/Regular/Isotropic.

Definition modules: Probability/Covariance/Basic, KLS/LogConcave/Regular/Basic.

Supporting theorems: convexOn_of_hessian_ge, isBorellDensity_of_eq_tilted, memLp_id_two.

Next: isotropic_comp_affine_of_whitening.

Source excerpt, lines 46–47 · Frozen source 408915f.