A positive definite quadratic form is bounded below by a multiple of the squared norm

Proved

posDef_quadratic_form_lower_bound

by olivier · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebramatrix-analysispositive-definitequadratic-form

Let $M$ be a real symmetric positive definite $n \times n$ matrix. Then there is a constant $c > 0$ such that

c \, x^{\top} x \le x^{\top} M x \qquad \text{for every } x \in \mathbb{R}^{n} .

Positive definiteness gives $x^{\top}Mx > 0$ for each individual $x \ne 0$ ; the content of the statement is that this positivity is uniform, a single constant serving for all $x$ at once. The largest such constant is the smallest eigenvalue of $M$ , by the Rayleigh-Ritz theorem.

This is the standard bridge from an algebraic hypothesis to an analytic conclusion. It converts the vanishing of a quadratic form into the vanishing of its argument, and boundedness of $x^{\top}Mx$ into boundedness of $x$ , which is what allows compactness arguments to run. In control theory it is what makes a positive definite matrix usable as a Lyapunov function: a decreasing quadratic form then forces the trajectory to be bounded, and a form tending to zero forces the trajectory to zero.

Formalization Note The squared norm appears as the dot product $x \cdot x$ rather than $\lVert x \rVert^{2}$ , because Mathlib equips Fin n → ℝ with the supremum norm rather than the Euclidean one. The statement is existential rather than naming the smallest eigenvalue, which keeps it usable without invoking the spectral theorem. The degenerate case $n = 0$ is included and holds trivially.

Preamble

import Mathlib

open Matrix

Formal statement

theorem posDef_quadratic_form_lower_bound {n : ℕ} {M : Matrix (Fin n) (Fin n) ℝ}
    (hM : M.PosDef) :
    ∃ c : ℝ, 0 < c ∧ ∀ x : Fin n → ℝ, c * (x ⬝ᵥ x) ≤ x ⬝ᵥ (M *ᵥ x) := by sorry

Source

R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press, 2013, Theorem 4.2.2 (Rayleigh-Ritz): for Hermitian M one has lambda_min(M) x*x <= x*Mx <= lambda_max(M) x*x. The present statement is the lower bound, with lambda_min(M) > 0 for positive definite M.

View graph