(* Title: HOL/Hahn_Banach/Hahn_Banach.thy
Author: Gertrud Bauer, TU Munich
*)
section \The Hahn-Banach Theorem\
theory Hahn_Banach
imports Hahn_Banach_Lemmas
begin
text \
We present the proof of two different versions of the Hahn-Banach Theorem,
closely following @{cite \\S36\ "Heuser:1986"}.
\
subsection \The Hahn-Banach Theorem for vector spaces\
paragraph \Hahn-Banach Theorem.\
text \
Let \F\ be a subspace of a real vector space \E\, let \p\ be a semi-norm on
\E\, and \f\ be a linear form defined on \F\ such that \f\ is bounded by
\p\, i.e. \\x \ F. f x \ p x\. Then \f\ can be extended to a linear form \h\
on \E\ such that \h\ is norm-preserving, i.e. \h\ is also bounded by \p\.
\
paragraph \Proof Sketch.\
text \
\<^enum> Define \M\ as the set of norm-preserving extensions of \f\ to subspaces of
\E\. The linear forms in \M\ are ordered by domain extension.
\<^enum> We show that every non-empty chain in \M\ has an upper bound in \M\.
\<^enum> With Zorn's Lemma we conclude that there is a maximal function \g\ in \M\.
\<^enum> The domain \H\ of \g\ is the whole space \E\, as shown by classical
contradiction:
\<^item> Assuming \g\ is not defined on whole \E\, it can still be extended in a
norm-preserving way to a super-space \H'\ of \H\.
\<^item> Thus \g\ can not be maximal. Contradiction!
\
theorem Hahn_Banach:
assumes E: "vectorspace E" and "subspace F E"
and "seminorm E p" and "linearform F f"
assumes fp: "\x \ F. f x \ p x"
shows "\h. linearform E h \ (\x \ F. h x = f x) \ (\x \ E. h x \ p x)"
\ \Let \E\ be a vector space, \F\ a subspace of \E\, \p\ a seminorm on \E\,\
\ \and \f\ a linear form on \F\ such that \f\ is bounded by \p\,\
\ \then \f\ can be extended to a linear form \h\ on \E\ in a norm-preserving way. \<^smallskip>\
proof -
interpret vectorspace E by fact
interpret subspace F E by fact
interpret seminorm E p by fact
interpret linearform F f by fact
define M where "M = norm_pres_extensions E p F f"
then have M: "M = \" by (simp only:)
from E have F: "vectorspace F" ..
note FE = \F \ E\
{
fix c assume cM: "c \ chains M" and ex: "\x. x \ c"
have "\c \ M"
\ \Show that every non-empty chain \c\ of \M\ has an upper bound in \M\:\
\ \\\c\ is greater than any element of the chain \c\, so it suffices to show \\c \ M\.\
unfolding M_def
proof (rule norm_pres_extensionI)
let ?H = "domain (\c)"
let ?h = "funct (\c)"
have a: "graph ?H ?h = \c"
proof (rule graph_domain_funct)
fix x y z assume "(x, y) \ \c" and "(x, z) \ \c"
with M_def cM show "z = y" by (rule sup_definite)
qed
moreover from M cM a have "linearform ?H ?h"
by (rule sup_lf)
moreover from a M cM ex FE E have "?H \ E"
by (rule sup_subE)
moreover from a M cM ex FE have "F \ ?H"
by (rule sup_supF)
moreover from a M cM ex have "graph F f \ graph ?H ?h"
by (rule sup_ext)
moreover from a M cM have "\x \ ?H. ?h x \ p x"
by (rule sup_norm_pres)
ultimately show "\H h. \c = graph H h
\ linearform H h
\ H \ E
\ F \ H
\ graph F f \ graph H h
\ (\x \ H. h x \ p x)" by blast
qed
}
then have "\g \ M. \x \ M. g \ x \ x = g"
\ \With Zorn's Lemma we can conclude that there is a maximal element in \M\. \<^smallskip>\
proof (rule Zorn's_Lemma)
\ \We show that \M\ is non-empty:\
show "graph F f \ M"
unfolding M_def
proof (rule norm_pres_extensionI2)
show "linearform F f" by fact
show "F \ E" by fact
from F show "F \ F" by (rule vectorspace.subspace_refl)
show "graph F f \ graph F f" ..
show "\x\F. f x \ p x" by fact
qed
qed
then obtain g where gM: "g \ M" and gx: "\x \ M. g \ x \ g = x"
by blast
from gM obtain H h where
g_rep: "g = graph H h"
and linearform: "linearform H h"
and HE: "H \ E" and FH: "F \ H"
and graphs: "graph F f \ graph H h"
and hp: "\x \ H. h x \ p x" unfolding M_def ..
\ \\g\ is a norm-preserving extension of \f\, in other words:\
\ \\g\ is the graph of some linear form \h\ defined on a subspace \H\ of \E\,\
\ \and \h\ is an extension of \f\ that is again bounded by \p\. \<^smallskip>\
from HE E have H: "vectorspace H"
by (rule subspace.vectorspace)
have HE_eq: "H = E"
\ \We show that \h\ is defined on whole \E\ by classical contradiction. \<^smallskip>\
proof (rule classical)
assume neq: "H \ E"
\ \Assume \h\ is not defined on whole \E\