Strict Covariance Positivity from Full Affine Support

This proves strict positivity of the covariance operator under full affine support.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure, and let $\mu$ be a probability measure on $E$ such that $\operatorname{id}\in L^2(\mu)$. Assume that the affine support of $\mu$ is all of $E$:

Then every nonzero vector $v\in E$ satisfies

Thus the ambient covariance quadratic form is positive definite under the stated support condition.

The result is useful for obtaining invertibility or coercivity of covariance on a full affine support.

Original Lean declaration header

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

theorem Covariance.inner_operator_self_pos_of_affineSupport_eq_top (μ : ProbabilityMeasure E)
    (h2 : MemLp id 2 (μ : Measure E)) (hfull : Probability.affineSupport μ = ⊤)
    {v : E} (hv : v ≠ 0) : 0 < ⟪Covariance.operator (μ : Measure E) v, v⟫

Module navigation

Module: Probability/Covariance/Positivity.

Definition modules: Probability/Covariance/Basic, Probability/AffineSupport.

Source excerpt, lines 21–23 · Frozen source 408915f.