Cauchy–Schwarz Inequality

Statement

For any two vectors $u$ and $v$ in an inner product space:

Equality holds if and only if $u$ and $v$ are linearly dependent (one is a scalar multiple of the other).

In $\mathbb{R}^n$ with the dot product, this reads:

The geometric consequence: $|\cos\theta| \leq 1$ for the angle $\theta$ between two vectors.

Visualization

Worked example in $\mathbb{R}^3$ with $u = (1, 2, 2)$ and $v = (2, 1, -2)$:

u = (1, 2, 2)        v = (2, 1, -2)

  dot product:          norms:
  u·v = 1·2            ‖u‖ = √(1²+2²+2²) = √9 = 3
      + 2·1            ‖v‖ = √(2²+1²+2²) = √9 = 3
      + 2·(-2)
      = 2+2-4 = 0      ‖u‖·‖v‖ = 3·3 = 9

  |u·v| = 0  ≤  9 = ‖u‖·‖v‖   ✓   (vectors are orthogonal)

Another example with $u = (1, 1, 0)$ and $v = (1, 0, 1)$:

Quantity	Value
$u \cdot v = 1{\cdot}1 + 1{\cdot}0 + 0{\cdot}1$	$1$
$\|u\| = \sqrt{1^2+1^2+0^2}$	$\sqrt{2} \approx 1.414$
$\|v\| = \sqrt{1^2+0^2+1^2}$	$\sqrt{2} \approx 1.414$
$\|u\| \cdot \|v\|$	$2$
<span class="math-inline" data-latex="	u \cdot v
$\cos\theta = (u\cdot v)/(\|u\|\|v\|)$	$0.5$, so $\theta = 60°$

When $u = (a, a)$ and $v = (b, b)$ (parallel), equality holds: $|ab + ab| = \sqrt{2a^2}\cdot\sqrt{2b^2} = 2|ab|$.

Proof Sketch

Fix $v \neq 0$ and consider the real-valued function $f(t) = \|u - tv\|^2 \geq 0$:

This quadratic in $t$ is always non-negative, so its discriminant must be $\leq 0$:

Therefore $|\langle u, v\rangle| \leq \|u\|\|v\|$.

Connections

Cauchy–Schwarz is a cornerstone of analysis and algebra:

• AM–GM InequalityAM–GM Inequality$$\frac{a_1+\cdots+a_n}{n} \geq \sqrt[n]{a_1 \cdots a_n}$$The arithmetic mean is always at least as large as the geometric meanRead more → — a one-dimensional shadow; both follow from convexity / Jensen's inequality
• Quadratic FormulaQuadratic Formula$$x = \frac{-b \pm \sqrt{b^2 - 4ac}}{2a}$$Solve any quadratic equation using the discriminantRead more → — the discriminant condition $b^2 \leq 4ac$ in disguise
• Binomial TheoremBinomial Theorem$$(x+y)^n = \sum_{k=0}^{n} \binom{n}{k} x^k y^{n-k}$$Expanding powers of a sum via binomial coefficientsRead more → — the "cross term" bound in $\|u+v\|^2$ is Cauchy–Schwarz
• Geometric SeriesGeometric Series$$\sum_{k=0}^{n-1} x^k = \frac{x^n - 1}{x - 1}$$Partial sums and convergence of the geometric progressionRead more → — Bessel's inequality for orthonormal expansions uses Cauchy–Schwarz
• Vieta Formulas — in the Gram matrix approach to polynomial roots, Cauchy–Schwarz controls error

Lean4 Proof

Mathlib provides norm_inner_le_norm in Mathlib.Analysis.InnerProductSpace.Basic, which is exactly the Cauchy–Schwarz inequality for inner product spaces.

import Mathlib.Analysis.InnerProductSpace.Basic

/-- Cauchy–Schwarz inequality: the norm of the inner product is bounded by
    the product of the norms. This is `norm_inner_le_norm` in Mathlib.  -/
theorem cauchy_schwarz
    {E : Type*} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E]
    (u v : E) : ‖(inner u v : ℝ)‖ ≤ ‖u‖ * ‖v‖ :=
  norm_inner_le_norm u v

/-- Consequence: the cosine of the angle between two vectors has absolute value ≤ 1. -/
theorem cos_angle_le_one
    {E : Type*} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E]
    (u v : E) (hu : ‖u‖ ≠ 0) (hv : ‖v‖ ≠ 0) :
    ‖(inner u v : ℝ)‖ / (‖u‖ * ‖v‖) ≤ 1 := by
  apply div_le_one_of_le
  · exact norm_inner_le_norm u v
  · positivity

/-- The real dot-product version: (Σ uᵢvᵢ)² ≤ (Σ uᵢ²)(Σ vᵢ²). -/
theorem cauchy_schwarz_sum (n : ℕ) (u v : Fin n → ℝ) :
    (∑ i, u i * v i) ^ 2 ≤ (∑ i, u i ^ 2) * (∑ i, v i ^ 2) := by
  have h := norm_inner_le_norm (𝕜 := ℝ) (E := EuclideanSpace ℝ (Fin n)) u v
  simp only [EuclideanSpace.inner_eq_star_mulVec, Matrix.dotProduct, EuclideanSpace.norm_sq] at h
  nlinarith [sq_nonneg (∑ i, u i * v i), h]