theorem LinearMap.BilinForm.posDef_of_nonneg_of_nondegenerate {E : Type u} [AddCommGroup E] [Module ℝ E] (B : LinearMap.BilinForm ℝ E) (hB_nonneg : ∀ (v : E), 0 ≤ (B v) v) (hB_symm : B.IsSymm) (hB_nondeg : B.Nondegenerate) : (BilinMap.toQuadraticMap B).PosDef

A symmetric nonnegative bilinear form is positive definite as soon as it is nondegenerate.

theorem abs_apply_le_dualNorm_mul_primalSeminorm {E : Type u} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] (B : LinearMap.BilinForm ℝ E) (hB_nonneg : ∀ (v : E), 0 ≤ (B v) v) (hB_symm : B.IsSymm) (hB_nondeg : B.Nondegenerate) (g : Module.Dual ℝ E) (h : E) : have hPos := ⋯; |g h| ≤ B.dualNorm hPos g * (B.primalSeminorm hPos) h

Proposition 5.0.21: if B is symmetric, nonnegative on diagonal values, and nondegenerate, then the pairing between a covector and a vector is bounded by the B-dual norm of the covector times the B-primal norm of the vector. The positive-definite owner data are obtained canonically from these textbook hypotheses.