Editing Hahn–Banach theorem (section)

===Proof===

The [[#Hahn–Banach dominated extension theorem|Hahn–Banach theorem for real vector spaces]] ultimately follows from Helly's initial result for the special case where the linear functional is extended from <math>M</math> to a larger vector space in which <math>M</math> has [[codimension]] <math>1.</math>{{sfn|Narici|Beckenstein|2011|pp=177-220}}

{{Math theorem
| name = Lemma{{sfn|Narici|Beckenstein|2011|pp=177-183}}
| note = {{visible anchor|One–dimensional dominated extension theorem}}
| math_statement = Let <math>p : X \to \R</math> be a [[sublinear function]] on a real vector space <math>X,</math> let <math>f : M \to \R</math> a [[linear functional]] on a [[Proper subset|proper]] [[vector subspace]] <math>M \subsetneq X</math> such that <math>f \leq p</math> on <math>M</math> (meaning <math>f(m) \leq p(m)</math> for all <math>m \in M</math>), and let <math>x \in X</math> be a vector {{em|not}} in <math>M</math> (so <math>M \oplus \R x = \operatorname{span} \{M, x\}</math>). 
There exists a linear extension <math>F : M \oplus \R x \to \R</math> of <math>f</math> such that <math>F \leq p</math> on <math>M \oplus \R x.</math>
}}

{{Math proof|title=Proof{{sfn|Narici|Beckenstein|2011|pp=177-183}}|drop=hidden|proof=
Given any real number <math>b,</math> the map <math>F_b : M \oplus \R x \to \R</math> defined by <math>F_b(m + r x) = f(m) + r b</math> is always a linear extension of <math>f</math> to <math>M \oplus \R x</math><ref group=note>This definition means, for instance, that <math>F_b(x) = F_b(0 + 1 x) = f(0) + 1 b = b</math> and if <math>m \in M</math> then <math>F_b(m) = F_b(m + 0 x) = f(m) + 0 b = f(m).</math> In fact, if <math>G : M \oplus \R x \to \R</math> is any linear extension of <math>f</math> to <math>M \oplus \R x</math> then <math>G = F_b</math> for <math>b := G(x).</math> In other words, every linear extension of <math>f</math> to <math>M \oplus \R x</math> is of the form <math>F_b</math> for some (unique) <math>b.</math></ref> but it might not satisfy <math>F_b \leq p.</math> 
It will be shown that <math>b</math> can always be chosen so as to guarantee that <math>F_b \leq p,</math> which will complete the proof. 

If <math>m, n \in M</math> then 
<math display=block>f(m) - f(n) = f(m - n) \leq p(m - n) = p(m + x - x - n) \leq p(m + x) + p(- x - n)</math>
which implies
<math display=block>-p(-n - x) - f(n) ~\leq~ p(m + x) - f(m).</math>
<!--where importantly, the left hand side is independent of <math>m</math> and the right hand side is independent of <math>n.</math>--> 
So define
<math display=block>a = \sup_{n \in M}[-p(-n - x) - f(n)] \qquad \text{ and } \qquad c = \inf_{m \in M} [p(m + x) - f(m)]</math>
where <math>a \leq c</math> are real numbers. 
To guarantee <math>F_b \leq p,</math> it suffices that <math>a \leq b \leq c</math> (in fact, this is also necessary<ref group=note>Explicitly, for any real number <math>b \in \R,</math> <math>F_b \leq p</math> on <math>M \oplus \R x</math> if and only if <math>a \leq b \leq c.</math> Combined with the fact that <math>F_b(x) = b,</math> it follows that the dominated linear extension of <math>f</math> to <math>M \oplus \R x</math> is unique if and only if <math>a = c,</math> in which case this scalar will be the extension's values at <math>x.</math> Since every linear extension of <math>f</math> to <math>M \oplus \R x</math> is of the form <math>F_b</math> for some <math>b,</math> the bounds <math>a \leq b = F_b(x) \leq c</math> thus also limit the range of possible values (at <math>x</math>) that can be taken by any of <math>f</math>'s dominated linear extensions. Specifically, if <math>F : X \to \R</math> is any linear extension of <math>f</math> satisfying <math>F \leq p</math> then for every <math>x \in X \setminus M,</math> <math>\sup_{m \in M}[-p(-m - x) - f(m)] ~\leq~ F(x) ~\leq~ \inf_{m \in M} [p(m + x) - f(m)].</math></ref>) because then <math>b</math> satisfies "the decisive inequality"{{sfn|Narici|Beckenstein|2011|pp=177-183}}
<math display=block>-p(-n - x) - f(n) ~\leq~ b ~\leq~ p(m + x) - f(m) \qquad \text{ for all }\;  m, n \in M.</math>

To see that <math>f(m) + r b \leq p(m + r x)</math> follows,<ref group=note name="GeometricIllustration" /> assume <math>r \neq 0</math> and substitute <math>\tfrac{1}{r} m</math> in for both <math>m</math> and <math>n</math> to obtain
<math display=block>-p\left(- \tfrac{1}{r} m - x\right) - \tfrac{1}{r} f\left(m\right) ~\leq~ b ~\leq~ p\left(\tfrac{1}{r} m + x\right) - \tfrac{1}{r} f\left(m\right).</math> 
If <math>r > 0</math> (respectively, if <math>r < 0</math>) then the right (respectively, the left) hand side equals <math>\tfrac{1}{r} \left[p(m + r x) - f(m)\right]</math> so that multiplying by <math>r</math> gives <math>r b \leq p(m + r x) - f(m).</math> 
<!--<math display=block>-p\left(- \tfrac{1}{r} m - x\right) - f\left(\tfrac{1}{r} m\right) = -p\left(\left(- \tfrac{1}{r}\right) \left(m + rx\right)\right) - \tfrac{1}{r} f(m) = \tfrac{1}{r} \left[p(m + r x) - f(m)\right].</math> -->
<math>\blacksquare</math>
}}

This lemma remains true if <math>p : X \to \R</math> is merely a [[convex function]] instead of a sublinear function.{{Sfn|Schechter|1996|pp=318-319}}{{Sfn|Reed|Simon|1980|p=}} 

{{collapse top|title=Proof|left=true}}
Assume that <math>p</math> is convex, which means that <math>p(t y + (1 - t) z) \leq t p(y) + (1 - t) p(z)</math> for all <math>0 \leq t \leq 1</math> and <math>y, z \in X.</math> Let <math>M,</math> <math>f : M \to \R,</math> and <math>x \in X \setminus M</math> be as in [[Hahn–Banach theorem#One–dimensional dominated extension theorem|the lemma's statement]]. Given any <math>m, n \in M</math> and any positive real <math>r, s > 0,</math> the positive real numbers <math>t := \tfrac{s}{r + s}</math> and <math>\tfrac{r}{r + s} = 1 - t</math> sum to <math>1</math> so that the convexity of <math>p</math> on <math>X</math> guarantees
<math display=block>\begin{alignat}{9}
p\left(\tfrac{s}{r + s} m + \tfrac{r}{r + s} n\right) 
~&=~ p\big(\tfrac{s}{r + s} (m - r x) &&+ \tfrac{r}{r + s} (n + s x)\big) &&  \\
&\leq~ \tfrac{s}{r + s} \; p(m - r x) &&+ \tfrac{r}{r + s} \; p(n + s x)  && \\
\end{alignat}</math>
and hence
<math display=block>\begin{alignat}{9}
s f(m) + r f(n) 
~&=~ (r + s) \; f\left(\tfrac{s}{r + s} m + \tfrac{r}{r + s} n\right)   && \qquad \text{ by linearity of } f \\
&\leq~ (r + s) \; p\left(\tfrac{s}{r + s} m + \tfrac{r}{r + s} n\right) && \qquad f \leq p \text{ on } M \\
&\leq~ s p(m - r x) + r p(n + s x) \\
\end{alignat}</math>
thus proving that <math>- s p(m - r x) + s f(m) ~\leq~ r p(n + s x) - r f(n),</math> which after multiplying both sides by <math>\tfrac{1}{rs}</math> becomes 
<math display=block>\tfrac{1}{r} [- p(m - r x) + f(m)] ~\leq~ \tfrac{1}{s} [p(n + s x) - f(n)].</math> 
This implies that the values defined by 
<math display=block>a = \sup_{\stackrel{m \in M}{r > 0}} \tfrac{1}{r} [- p(m - r x) + f(m)] \qquad \text{ and } \qquad c = \inf_{\stackrel{n \in M}{s > 0}} \tfrac{1}{s} [p(n + s x) - f(n)]</math> 
are real numbers that satisfy <math>a \leq c.</math> As in the above proof of the [[Hahn–Banach theorem#One–dimensional dominated extension theorem|one–dimensional dominated extension theorem]] above, for any real <math>b \in \R</math> define <math>F_b : M \oplus \R x \to \R</math> by <math>F_b(m + r x) = f(m) + r b.</math> 
It can be verified that if <math>a \leq b \leq c</math> then <math>F_b \leq p</math> where <math>r b \leq p(m + r x) - f(m)</math> follows from <math>b \leq c</math> when <math>r > 0</math> (respectively, follows from <math>a \leq b</math> when <math>r < 0</math>).
<math>\blacksquare</math>
{{collapse bottom}}

The [[#One–dimensional dominated extension theorem|lemma above]] is the key step in deducing the dominated extension theorem from [[Zorn's lemma]]. 

{{Math proof|title=Proof of dominated extension theorem using [[Zorn's lemma]]|drop=hidden|proof=
The set of all possible dominated linear extensions of <math>f</math> are partially ordered by extension of each other, so there is a maximal extension <math>F.</math>  By the codimension-1 result, if <math>F</math> is not defined on all of <math>X,</math> then it can be further extended.  Thus <math>F</math> must be defined everywhere, as claimed. 
<math>\blacksquare</math>
}}

When <math>M</math> has countable codimension, then using induction and the lemma completes the proof of the Hahn–Banach theorem. The standard proof of the general case uses [[Zorn's lemma]] although the strictly weaker [[ultrafilter lemma]]{{sfn|Luxemburg|1962|p=}} (which is equivalent to the [[compactness theorem]] and to the [[Boolean prime ideal theorem]]) may be used instead. Hahn–Banach can also be proved using [[Tychonoff's theorem]] for [[Compact space|compact]] [[Hausdorff space]]s{{sfn|Łoś|Ryll-Nardzewski|1951|pp=233–237}} (which is also equivalent to the ultrafilter lemma)

The [[Mizar system|Mizar project]] has completely formalized and automatically checked the proof of the Hahn–Banach theorem in the HAHNBAN file.<ref>[http://mizar.uwb.edu.pl/JFM/Vol5/hahnban.html HAHNBAN file]</ref>