Hahn–Banach Theorem

Statement

Let $E$ be a normed space over $\mathbb{R}$ (or $\mathbb{C}$), $p \subseteq E$ a subspace, and $f : p \to \mathbb{R}$ a bounded linear functional. Then there exists a bounded linear functional $g : E \to \mathbb{R}$ such that

The extension preserves the norm exactly — it does not "inflate" the functional. This is the analytic (norm-extension) form; the geometric form gives separating hyperplanes for convex sets.

Visualization

Extend $f(t) = 3t$ defined on the subspace $p = \mathbb{R} \cdot e_1 \subseteq \mathbb{R}^2$:

  E = ℝ²         p = {(t, 0) : t ∈ ℝ}

  e₂ axis
  │
  │   *  ← (1,1) in E, no f-value on p
  │
──┼───────────────────▶ e₁ axis
  │   ←  p = ℝ·e₁  →
  │   f(t,0) = 3t

One extension: g(x₁, x₂) = 3x₁  (ignores x₂ component)
  g(1,0) = 3 = f(1,0)  ✓
  g(0,1) = 0           (free choice, norm preserved)
  ‖g‖ = 3 = ‖f‖        ✓

Point in $p$	$f$ value	$g$ value (extension)
$(1, 0)$	$3$	$3$
$(2, 0)$	$6$	$6$
$(-1, 0)$	$-3$	$-3$
$(0, 1) \notin p$	—	$0$ (chosen)
$(1, 1) \notin p$	—	$3$ (chosen)

The extension $g(x_1, x_2) = 3x_1$ has $\|g\| = 3 = \|f\|$, confirming the norm is not inflated.

Proof Sketch

1. Seminorm domination. Let $p(x) = \|f\| \cdot \|x\|$ be a seminorm on $E$ dominating $f$ on $p$.
2. One-dimensional extension. For any $x_0 \notin p$, extend $f$ to $p + \mathbb{R} x_0$ by choosing $g(x_0)$ so that $g \le p$ everywhere. Algebraic manipulation shows a valid choice exists.
3. Zorn's lemma (or transfinite induction). Among all extensions dominated by $p$, take a maximal one. Maximality forces the domain to be all of $E$.
4. Norm equality. $\|g\| \le \|f\|$ by domination; $\|g\| \ge \|f\|$ because $g$ agrees with $f$ on $p$.

Connections

• 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 → — the inner product form of the Hahn–Banach bound in Hilbert spaces reduces to Cauchy–Schwarz.
• Riesz Representation TheoremRiesz Representation Theorem$$\phi \in H^* \Rightarrow \exists!\, u \in H : \phi(v) = \langle u, v \rangle$$Every bounded linear functional on a Hilbert space is inner product with a unique vectorRead more → — in Hilbert spaces, Hahn–Banach is superseded by the Riesz theorem, which identifies the extending functional with an inner product.
• Spectral Radius FormulaSpectral Radius Formula$$r(a) = \lim_{n\to\infty} \|a^n\|^{1/n}$$The spectral radius equals the limit of the nth root of the operator norm of the nth power (Gelfand's formula)Read more → — dual space techniques from Hahn–Banach underpin the analytic function proof of the Gelfand formula.
• Heine–Borel TheoremHeine–Borel Theorem$$K \subseteq \mathbb{R}^n \;\text{compact} \iff K \;\text{closed and bounded}$$In ℝⁿ, a subset is compact if and only if it is closed and boundedRead more → — compactness and weak-* compactness (Banach–Alaoglu, related to Hahn–Banach) parallel the finite-dimensional Heine–Borel picture.

import Mathlib.Analysis.Normed.Module.HahnBanach

/-- **Hahn–Banach theorem** (real normed space, norm-preserving extension).
    Direct alias of `exists_extension_norm_eq` in Mathlib. -/
theorem hahn_banach_extension (E : Type*) [SeminormedAddCommGroup E] [NormedSpace ℝ E]
    (p : Subspace ℝ E) (f : StrongDual ℝ p) :
    ∃ g : StrongDual ℝ E, (∀ x : p, g x = f x) ∧ ‖g‖ = ‖f‖ :=
  exists_extension_norm_eq p f