Positivity of coercive bilinear forms

IsCoercive.apply_self_pos extracts the strict diagonal positivity argument shared by TauCeti.coerciveRiemannianMetric and IsCoercive.pos_of_forall_apply_eq_smul_inner. It requires neither symmetry nor finite dimension.

theorem IsCoercive.apply_self_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : E →L[ℝ] E →L[ℝ] ℝ} (hB : IsCoercive B) {v : E} (hv : v ≠ 0) : 0 < (B v) v

A coercive form is strictly positive on nonzero diagonal arguments.