src/HOL/Hahn_Banach/Hahn_Banach.thy
changeset 61540 f92bf6674699
parent 61539 a29295dac1ca
child 61543 de44d4fa5ef0
equal deleted inserted replaced
61539:a29295dac1ca 61540:f92bf6674699
     7 theory Hahn_Banach
     7 theory Hahn_Banach
     8 imports Hahn_Banach_Lemmas
     8 imports Hahn_Banach_Lemmas
     9 begin
     9 begin
    10 
    10 
    11 text \<open>
    11 text \<open>
    12   We present the proof of two different versions of the Hahn-Banach
    12   We present the proof of two different versions of the Hahn-Banach Theorem,
    13   Theorem, closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
    13   closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
    14 \<close>
    14 \<close>
       
    15 
    15 
    16 
    16 subsection \<open>The Hahn-Banach Theorem for vector spaces\<close>
    17 subsection \<open>The Hahn-Banach Theorem for vector spaces\<close>
    17 
    18 
    18 paragraph \<open>Hahn-Banach Theorem.\<close>
    19 paragraph \<open>Hahn-Banach Theorem.\<close>
    19 text \<open>
    20 text \<open>
    20   Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm on \<open>E\<close>, and \<open>f\<close> be a linear form defined on
    21   Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm
    21   \<open>F\<close> such that \<open>f\<close> is bounded by \<open>p\<close>, i.e. \<open>\<forall>x \<in>
    22   on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded
    22   F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear form \<open>h\<close>
    23   by \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear
    23   on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is
    24   form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded
    24   also bounded by \<open>p\<close>.
    25   by \<open>p\<close>. \<close>
    25 \<close>
       
    26 
    26 
    27 paragraph \<open>Proof Sketch.\<close>
    27 paragraph \<open>Proof Sketch.\<close>
    28 text \<open>
    28 text \<open>
    29   \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of
    29   \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces
    30   \<open>f\<close> to subspaces of \<open>E\<close>. The linear forms in \<open>M\<close>
    30   of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.
    31   are ordered by domain extension.
    31 
    32 
    32   \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>.
    33   \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper
    33 
    34   bound in \<open>M\<close>.
    34   \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in
    35 
    35   \<open>M\<close>.
    36   \<^enum> With Zorn's Lemma we conclude that there is a maximal function
    36 
    37   \<open>g\<close> in \<open>M\<close>.
    37   \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical
    38 
    38   contradiction:
    39   \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical contradiction:
    39 
    40 
    40     \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in
    41     \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can
    41     a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
    42     still be extended in a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
       
    43 
    42 
    44     \<^item> Thus \<open>g\<close> can not be maximal. Contradiction!
    43     \<^item> Thus \<open>g\<close> can not be maximal. Contradiction!
    45 \<close>
    44 \<close>
    46 
    45 
    47 theorem Hahn_Banach:
    46 theorem Hahn_Banach:
   151       qed
   150       qed
   152 
   151 
   153       obtain xi where
   152       obtain xi where
   154         xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
   153         xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
   155           \<and> xi \<le> p (y + x') - h y"
   154           \<and> xi \<le> p (y + x') - h y"
   156         -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequations; this will\<close>
   155         -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequality; this will\<close>
   157         -- \<open>be used to establish that \<open>h'\<close> is a norm-preserving extension of \<open>h\<close>.
   156         -- \<open>be used to establish that \<open>h'\<close> is a norm-preserving extension of \<open>h\<close>.
   158            \label{ex-xi-use}\<^smallskip>\<close>
   157            \label{ex-xi-use}\<^smallskip>\<close>
   159       proof -
   158       proof -
   160         from H have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
   159         from H have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
   161             \<and> xi \<le> p (y + x') - h y"
   160             \<and> xi \<le> p (y + x') - h y"
   290 
   289 
   291 subsection \<open>Alternative formulation\<close>
   290 subsection \<open>Alternative formulation\<close>
   292 
   291 
   293 text \<open>
   292 text \<open>
   294   The following alternative formulation of the Hahn-Banach
   293   The following alternative formulation of the Hahn-Banach
   295   Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear
   294   Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form
   296   form \<open>f\<close> and a seminorm \<open>p\<close> the following inequations
   295   \<open>f\<close> and a seminorm \<open>p\<close> the following inequality are
   297   are equivalent:\footnote{This was shown in lemma @{thm [source]
   296   equivalent:\footnote{This was shown in lemma @{thm [source] abs_ineq_iff}
   298   abs_ineq_iff} (see page \pageref{abs-ineq-iff}).}
   297   (see page \pageref{abs-ineq-iff}).}
   299   \begin{center}
   298   \begin{center}
   300   \begin{tabular}{lll}
   299   \begin{tabular}{lll}
   301   \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
   300   \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
   302   \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
   301   \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
   303   \end{tabular}
   302   \end{tabular}
   334 
   333 
   335 
   334 
   336 subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>
   335 subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>
   337 
   336 
   338 text \<open>
   337 text \<open>
   339   Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a
   338   Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>,
   340   norm space \<open>E\<close>, can be extended to a continuous linear form
   339   can be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> =
   341   \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = \<parallel>g\<parallel>\<close>.
   340   \<parallel>g\<parallel>\<close>.
   342 \<close>
   341 \<close>
   343 
   342 
   344 theorem norm_Hahn_Banach:
   343 theorem norm_Hahn_Banach:
   345   fixes V and norm ("\<parallel>_\<parallel>")
   344   fixes V and norm ("\<parallel>_\<parallel>")
   346   fixes B defines "\<And>V f. B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
   345   fixes B defines "\<And>V f. B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
   418       unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
   417       unfolding p_def by (rule normed_vectorspace_with_fn_norm.fn_norm_le_cong
   419         [OF normed_vectorspace_with_fn_norm.intro,
   418         [OF normed_vectorspace_with_fn_norm.intro,
   420          OF F_norm, folded B_def fn_norm_def])
   419          OF F_norm, folded B_def fn_norm_def])
   421   qed
   420   qed
   422 
   421 
   423   txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded
   422   txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we
   424     by \<open>p\<close> we can apply the Hahn-Banach Theorem for real vector
   423     can apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be
   425     spaces. So \<open>f\<close> can be extended in a norm-preserving way to
   424     extended in a norm-preserving way to some function \<open>g\<close> on the whole
   426     some function \<open>g\<close> on the whole vector space \<open>E\<close>.\<close>
   425     vector space \<open>E\<close>.\<close>
   427 
   426 
   428   with E FE linearform q obtain g where
   427   with E FE linearform q obtain g where
   429       linearformE: "linearform E g"
   428       linearformE: "linearform E g"
   430     and a: "\<forall>x \<in> F. g x = f x"
   429     and a: "\<forall>x \<in> F. g x = f x"
   431     and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
   430     and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
   443   txt \<open>To complete the proof, we show that \<open>\<parallel>g\<parallel> = \<parallel>f\<parallel>\<close>.\<close>
   442   txt \<open>To complete the proof, we show that \<open>\<parallel>g\<parallel> = \<parallel>f\<parallel>\<close>.\<close>
   444 
   443 
   445   have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
   444   have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
   446   proof (rule order_antisym)
   445   proof (rule order_antisym)
   447     txt \<open>
   446     txt \<open>
   448       First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>.  The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the smallest \<open>c \<in> \<real>\<close> such that
   447       First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>. The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the
       
   448       smallest \<open>c \<in> \<real>\<close> such that
   449       \begin{center}
   449       \begin{center}
   450       \begin{tabular}{l}
   450       \begin{tabular}{l}
   451       \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
   451       \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
   452       \end{tabular}
   452       \end{tabular}
   453       \end{center}
   453       \end{center}
   454       \noindent Furthermore holds
   454       \<^noindent> Furthermore holds
   455       \begin{center}
   455       \begin{center}
   456       \begin{tabular}{l}
   456       \begin{tabular}{l}
   457       \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
   457       \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
   458       \end{tabular}
   458       \end{tabular}
   459       \end{center}
   459       \end{center}
   460 \<close>
   460     \<close>
   461 
   461 
   462     from g_cont _ ge_zero
   462     from g_cont _ ge_zero
   463     show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
   463     show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
   464     proof
   464     proof
   465       fix x assume "x \<in> E"
   465       fix x assume "x \<in> E"