Hadamard's Inequality

Statement

Let $A$ be an $n \times n$ real matrix with columns $A_1, A_2, \ldots, A_n \in \mathbb{R}^n$. Then

where $\|A_j\| = \sqrt{\sum_i a_{ij}^2}$ is the Euclidean norm of column $j$.

Equality holds if and only if the columns are pairwise orthogonal (or at least one column is zero).

Visualization

Example 1 — identity matrix:

Example 2 — non-orthogonal matrix:

Geometric meaning:

Shape	Volume / Area	Bound
Parallelepiped spanned by orthonormal vectors	$1$	$\prod \|v_i\| = 1$
Parallelepiped with tilted vectors	$< \prod \|v_i\|$	always $\le$ product of lengths

The volume of a parallelepiped is maximized (for fixed side lengths) when sides are orthogonal — exactly the equality case.

Proof Sketch

1. Orthonormal case. If the columns of $A$ are already orthonormal, $A^\top A = I$, so $\det A = \pm 1$ and $\|A_j\| = 1$ for all $j$. The inequality holds with $1 \le 1$.
2. Gram–Schmidt reduction. Apply Gram–Schmidt to the columns: write $A = QR$ (QR decomposition). Then $\det A = \det Q \cdot \det R = \pm \prod_j r_{jj}$. The diagonal entries $r_{jj}$ satisfy $r_{jj} = \|a_j^{\perp}\| \le \|A_j\|$ (projection can only shorten vectors). Hence $|\det A| = \prod_j |r_{jj}| \le \prod_j \|A_j\|$.
3. Equality. Equality in each step requires $a_j^{\perp} = a_j$, i.e., $a_j$ is already orthogonal to all previous columns.
4. Cauchy–Schwarz link. Each step uses $\|a_j^{\perp}\| \le \|a_j\|$, a direct consequence of the Cauchy–Schwarz InequalityCauchy–Schwarz Inequality$$|\langle u, v \rangle| \leq \|u\| \, \|v\|$$The inner product of two vectors is bounded by the product of their normsRead more → ($\|\text{projection}\| \le \|\text{vector}\|$).

Connections

Hadamard's inequality follows from QR DecompositionQR Decomposition$$A = QR,\quad Q^\top Q = I,\; R \text{ upper triangular}$$Every invertible real matrix factors as a product of an orthogonal matrix and an upper-triangular matrix.Read more → (Gram–Schmidt) combined with Cauchy–Schwarz InequalityCauchy–Schwarz Inequality$$|\langle u, v \rangle| \leq \|u\| \, \|v\|$$The inner product of two vectors is bounded by the product of their normsRead more →, and is equivalent to positivity of the Gram matrix. It is used in bounding determinants in Cauchy–Binet FormulaCauchy–Binet Formula$$\det(AB) = \sum_{S \subseteq [n],\, |S|=m} \det(A_S) \det(B^S)$$The determinant of a product AB equals the sum over all maximal minors of A times the corresponding minors of B.Read more → for rectangular matrices and in numerical analysis to estimate conditioning.

-- We prove the 2x2 instance of Hadamard's inequality explicitly using decide-style arithmetic.
-- The key algebraic fact: |ad - bc|^2 <= (a^2+b^2)(c^2+d^2)
-- which follows from the Cauchy–Schwarz inequality (a^2+b^2)(c^2+d^2) >= (ac+bd)^2
-- and (ad-bc)^2 + (ac+bd)^2 = (a^2+b^2)(c^2+d^2).
theorem hadamard_identity_2x2 (a b c d : ℝ) :
    (a * d - b * c) ^ 2 + (a * c + b * d) ^ 2 = (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) := by
  ring

-- Immediate consequence: the Hadamard bound for 2x2 real matrices.
theorem hadamard_bound_2x2 (a b c d : ℝ) :
    (a * d - b * c) ^ 2 ≤ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) := by
  nlinarith [sq_nonneg (a * c + b * d), sq_nonneg (a * d - b * c),
             hadamard_identity_2x2 a b c d]