Coercivity and level-set bounds for positive-definite quadratic forms

A positive-definite quadratic form on a finite-dimensional real normed space dominates a positive multiple of the squared norm. Its level sets are therefore bounded. The returned coercivity constant is useful to consumers that need uniform quantitative bounds.

theorem QuadraticMap.PosDef.exists_pos_mul_norm_sq_le {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} (hQ : PosDef Q) : ∃ (c : ℝ), 0 < c ∧ ∀ (x : M), c * ‖x‖ ^ 2 ≤ Q x

A positive definite form on a finite-dimensional real space is coercive.

theorem QuadraticMap.PosDef.isBounded_setOf_eq {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] [FiniteDimensional ℝ M] {Q : QuadraticForm ℝ M} (hQ : PosDef Q) (r : ℝ) : Bornology.IsBounded {x : M | Q x = r}

A positive definite form has bounded level sets.