[proofplan]
This is a foundational theorem of functional analysis, stated here in its real-normed-vector-space norm-preserving form. We do not reproduce the full proof; we recall the standard two-stage strategy — extension by one dimension, then transfinite extension via Zorn's lemma — and cite standard references.
[/proofplan]
[step:State the result as a quoted functional analysis theorem]
Let $(L, \|\cdot\|)$ be a normed vector space over $\mathbb{R}$, let $L_0 \subseteq L$ be a linear subspace, and let
\begin{align*}
f : L_0 &\to \mathbb{R}
\end{align*}
be a bounded linear functional with norm $\|f\|_{L_0^*} := \sup\{|f(x)| : x \in L_0, \, \|x\| \le 1\}$. The theorem asserts the existence of a bounded linear functional
\begin{align*}
\tilde f : L &\to \mathbb{R}
\end{align*}
such that $\tilde f|_{L_0} = f$ and $\|\tilde f\|_{L^*} = \|f\|_{L_0^*}$, i.e., the extension preserves the norm.
This is the Hahn–Banach extension theorem in its norm-preserving form for real normed spaces. It is a standard black box from functional analysis; we use it here as a quoted result.
[/step]
[step:Outline the standard proof technique]
The standard proof proceeds in two stages.
**(1) One-dimensional extension.** Fix $x_0 \in L \setminus L_0$, and consider the subspace $L_1 := L_0 + \mathbb{R} x_0$. To extend $f$ to a bounded linear functional $f_1 : L_1 \to \mathbb{R}$ with the same norm, one must choose a real number $c := f_1(x_0)$ such that
\begin{align*}
|f(y) + tc| \le \|f\|_{L_0^*} \, \|y + t x_0\| \qquad \text{for all } y \in L_0, \ t \in \mathbb{R}.
\end{align*}
Dividing by $|t|$ (the case $t = 0$ is the original bound on $f$) reduces the existence of such $c$ to showing
\begin{align*}
\sup_{y' \in L_0} \big( -f(y') - \|f\|_{L_0^*}\,\|y' + x_0\| \big) \le \inf_{y \in L_0} \big( -f(y) + \|f\|_{L_0^*}\,\|y + x_0\| \big),
\end{align*}
which is the inequality $f(y) - f(y') \le \|f\|_{L_0^*}(\|y + x_0\| + \|y' + x_0\|)$ for all $y, y' \in L_0$. The latter follows from the triangle inequality applied to $f(y - y') = f((y + x_0) - (y' + x_0))$ together with the norm bound on $f$. Any $c$ in the (non-empty) interval determined by these sup and inf works.
**(2) Maximal extension via Zorn's lemma.** Order the set of all norm-preserving extensions of $f$ to subspaces between $L_0$ and $L$ by inclusion of graphs. Every chain has an upper bound (the union of the graphs is again a norm-preserving extension on the union of the domains). By Zorn's lemma, a maximal element $\tilde f$ exists. Its domain $\tilde L$ must equal $L$: otherwise, picking $x_0 \in L \setminus \tilde L$ and applying the one-dimensional extension would produce a strictly larger norm-preserving extension, contradicting maximality.
For the complete proof, see Rudin, *Functional Analysis*, Chapter 3 (Hahn–Banach theorems), or Brezis, *Functional Analysis, Sobolev Spaces and Partial Differential Equations*, Chapter 1 (the analytic and geometric forms of Hahn–Banach).
[/step]
[step:Discuss the role of the axiom of choice and the use of Hahn–Banach in this course]
**Why Zorn's lemma is needed.** When $L_0$ has finite codimension in $L$, finitely many one-dimensional extensions suffice to reach $L$, and the construction is constructive — no choice principle is required. When $L_0$ has infinite codimension, however, the construction must extend through transfinitely many one-dimensional steps, and some form of the axiom of choice is unavoidable. Zorn's lemma is the most natural form for this argument: it directly gives the maximal element whose domain must, by maximality, equal $L$. The same argument can be phrased using transfinite induction or the well-ordering theorem; all three forms are equivalent given the rest of ZF set theory.
**The norm-preserving condition.** Without the norm-preserving requirement, the existence of an extension is automatic: any linear functional on $L_0$ extends to a linear functional on $L$ by choosing a complementary subspace. The depth of Hahn–Banach lies in preserving the operator norm, which the one-dimensional step achieves via the sup-inf inequality and which Zorn's lemma propagates to the global extension.
**Generalisations and applications.** The version stated here is the analytic Hahn–Banach theorem for real normed spaces. Standard generalisations include: (i) complex normed spaces, where one extends a complex-linear functional by extending its real part and recovering the imaginary part via $f(ix) = i f(x)$; (ii) the dominated extension form, in which $\|f\|_{L_0^*} \, \|x\|$ is replaced by an arbitrary sublinear functional $p(x)$; (iii) the geometric Hahn–Banach theorem, which separates disjoint convex sets by a closed hyperplane.
**Use in this course.** In the present chapter, Hahn–Banach is invoked exactly once: to extend the identification of $L^2$-Cauchy sequences in $\Delta\Omega^p(M)$ to bounded linear functionals on the closed subspace $\Delta\Omega^p(M) \subseteq \widetilde{\Omega}^p$, which is needed for the closedness step in the Hodge Decomposition proof. The norm-preserving form is essential there: without it, the extended functional might have a larger norm than its restriction, breaking the contradiction argument used to derive the Poincaré-type bound.
[/step]
