Positive-semidefinite bilinear forms

This file records a pointwise characterization of positive semidefiniteness for symmetric bilinear forms. It converts IsPosSemidef into diagonal nonnegativity, the form consumed by quadratic-form signature criteria and other pointwise positivity arguments.

Main results

• LinearMap.BilinForm.isPosSemidef_iff_forall_nonneg: a symmetric bilinear form is positive-semidefinite exactly when its diagonal values are nonnegative.

theorem LinearMap.BilinForm.isPosSemidef_iff_forall_nonneg {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [LE R] (B : LinearMap.BilinForm R M) (hB : B.IsSymm) : B.IsPosSemidef ↔ ∀ (x : M), 0 ≤ (B x) x

A symmetric bilinear form is positive-semidefinite if and only if its values on all vectors are nonnegative.