src/HOL/Real/HahnBanach/HahnBanach.thy
author bauerg
Mon Jul 17 13:58:18 2000 +0200 (2000-07-17)
changeset 9374 153853af318b
parent 9261 879e0f0cd047
child 9379 21cfeae6659d
permissions -rw-r--r--
- xsymbols for
\<noteq> \<notin> \<in> \<exists> \<forall>
\<and> \<inter> \<union> \<Union>
- vector space type of {plus, minus, zero}, overload 0 in vector space
- syntax |.| and ||.||
bauerg@9374
     1
(*  Title:      HOL/Real/HahnBanach/HahnBanach.thy
bauerg@9374
     2
    ID:         $Id$
bauerg@9374
     3
    Author:     Gertrud Bauer, TU Munich
bauerg@9374
     4
*)
bauerg@9374
     5
bauerg@9374
     6
header {* The Hahn-Banach Theorem *}
bauerg@9374
     7
bauerg@9374
     8
theory HahnBanach = HahnBanachLemmas: 
bauerg@9374
     9
bauerg@9374
    10
text {*
bauerg@9374
    11
  We present the proof of two different versions of the Hahn-Banach 
bauerg@9374
    12
  Theorem, closely following \cite[\S36]{Heuser:1986}.
bauerg@9374
    13
*}
bauerg@9374
    14
bauerg@9374
    15
subsection {* The Hahn-Banach Theorem for vector spaces *}
bauerg@9374
    16
bauerg@9374
    17
text {*
bauerg@9374
    18
{\bf Hahn-Banach Theorem.}\quad
bauerg@9374
    19
  Let $F$ be a subspace of a real vector space $E$, let $p$ be a semi-norm on
bauerg@9374
    20
  $E$, and $f$ be a linear form defined on $F$ such that $f$ is bounded by
bauerg@9374
    21
  $p$, i.e. $\All {x\in F} f\ap x \leq p\ap x$.  Then $f$ can be extended to
bauerg@9374
    22
  a linear form $h$ on $E$ such that $h$ is norm-preserving, i.e. $h$ is also
bauerg@9374
    23
  bounded by $p$.
bauerg@9374
    24
bauerg@9374
    25
\bigskip
bauerg@9374
    26
{\bf Proof Sketch.}
bauerg@9374
    27
\begin{enumerate}
bauerg@9374
    28
\item Define $M$ as the set of norm-preserving extensions of $f$ to subspaces
bauerg@9374
    29
  of $E$. The linear forms in $M$ are ordered by domain extension.
bauerg@9374
    30
\item We show that every non-empty chain in $M$ has an upper bound in $M$.
bauerg@9374
    31
\item With Zorn's Lemma we conclude that there is a maximal function $g$ in
bauerg@9374
    32
  $M$.
bauerg@9374
    33
\item The domain $H$ of $g$ is the whole space $E$, as shown by classical
bauerg@9374
    34
  contradiction:
bauerg@9374
    35
\begin{itemize}
bauerg@9374
    36
\item Assuming $g$ is not defined on whole $E$, it can still be extended in a
bauerg@9374
    37
  norm-preserving way to a super-space $H'$ of $H$.
bauerg@9374
    38
\item Thus $g$ can not be maximal. Contradiction!
bauerg@9374
    39
\end{itemize}
bauerg@9374
    40
\end{enumerate}
bauerg@9374
    41
\bigskip
bauerg@9374
    42
*}
bauerg@9374
    43
bauerg@9374
    44
(*
bauerg@9374
    45
text {* {\bf Theorem.} Let $f$ be a linear form defined on a subspace 
bauerg@9374
    46
 $F$ of a real vector space $E$, such that $f$ is bounded by a seminorm 
bauerg@9374
    47
 $p$. 
bauerg@9374
    48
bauerg@9374
    49
 Then $f$ can be extended  to a linear form $h$  on $E$ that is again
bauerg@9374
    50
 bounded by $p$.
bauerg@9374
    51
bauerg@9374
    52
 \bigskip{\bf Proof Outline.}
bauerg@9374
    53
 First we define the set $M$ of all norm-preserving extensions of $f$.
bauerg@9374
    54
 We show that every chain in $M$ has an upper bound in $M$.
bauerg@9374
    55
 With Zorn's lemma we can conclude that $M$ has a maximal element $g$.
bauerg@9374
    56
 We further show by contradiction that the domain $H$ of $g$ is the whole
bauerg@9374
    57
 vector space $E$. 
bauerg@9374
    58
 If $H \neq E$, then $g$ can be extended in 
bauerg@9374
    59
 a norm-preserving way to a greater vector space $H_0$. 
bauerg@9374
    60
 So $g$ cannot be maximal in $M$.
bauerg@9374
    61
 \bigskip
bauerg@9374
    62
*}
bauerg@9374
    63
*)
bauerg@8084
    64
bauerg@9256
    65
theorem HahnBanach:
bauerg@9374
    66
  "[| is_vectorspace E; is_subspace F E; is_seminorm E p;
bauerg@9374
    67
  is_linearform F f; \<forall>x \<in> F. f x \<le> p x |] 
bauerg@9374
    68
  ==> \<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"   
bauerg@9256
    69
    -- {* Let $E$ be a vector space, $F$ a subspace of $E$, $p$ a seminorm on $E$, *}
bauerg@9256
    70
    -- {* and $f$ a linear form on $F$ such that $f$ is bounded by $p$, *}
bauerg@9256
    71
    -- {* then $f$ can be extended to a linear form $h$ on $E$ in a norm-preserving way. \skp *}
wenzelm@9035
    72
proof -
bauerg@8084
    73
  assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
bauerg@9374
    74
   and "is_linearform F f" "\<forall>x \<in> F. f x \<le> p x"
bauerg@9256
    75
  -- {* Assume the context of the theorem. \skp *}
wenzelm@9035
    76
  def M == "norm_pres_extensions E p F f"
bauerg@9256
    77
  -- {* Define $M$ as the set of all norm-preserving extensions of $F$. \skp *}
wenzelm@9035
    78
  {
bauerg@9374
    79
    fix c assume "c \<in> chain M" "\<exists>x. x \<in> c"
bauerg@9374
    80
    have "\<Union> c \<in> M"
bauerg@9374
    81
    -- {* Show that every non-empty chain $c$ of $M$ has an upper bound in $M$: *}
bauerg@9374
    82
    -- {* $\Union c$ is greater than any element of the chain $c$, so it suffices to show $\Union c \in M$. *}
wenzelm@9035
    83
    proof (unfold M_def, rule norm_pres_extensionI)
bauerg@9374
    84
      show "\<exists>H h. graph H h = \<Union> c
bauerg@9374
    85
              \<and> is_linearform H h 
bauerg@9374
    86
              \<and> is_subspace H E 
bauerg@9374
    87
              \<and> is_subspace F H 
bauerg@9374
    88
              \<and> graph F f \<subseteq> graph H h
bauerg@9374
    89
              \<and> (\<forall>x \<in> H. h x \<le> p x)"
wenzelm@9035
    90
      proof (intro exI conjI)
bauerg@9374
    91
        let ?H = "domain (\<Union> c)"
bauerg@9374
    92
        let ?h = "funct (\<Union> c)"
bauerg@8084
    93
bauerg@9374
    94
        show a: "graph ?H ?h = \<Union> c" 
wenzelm@9035
    95
        proof (rule graph_domain_funct)
bauerg@9374
    96
          fix x y z assume "(x, y) \<in> \<Union> c" "(x, z) \<in> \<Union> c"
wenzelm@9035
    97
          show "z = y" by (rule sup_definite)
wenzelm@9035
    98
        qed
wenzelm@9035
    99
        show "is_linearform ?H ?h" 
wenzelm@9035
   100
          by (simp! add: sup_lf a)
bauerg@9374
   101
        show "is_subspace ?H E" 
bauerg@9374
   102
          by (rule sup_subE, rule a) (simp!)+
wenzelm@9035
   103
        show "is_subspace F ?H" 
bauerg@9374
   104
          by (rule sup_supF, rule a) (simp!)+
bauerg@9374
   105
        show "graph F f \<subseteq> graph ?H ?h" 
bauerg@9374
   106
          by (rule sup_ext, rule a) (simp!)+
bauerg@9374
   107
        show "\<forall>x \<in> ?H. ?h x \<le> p x" 
bauerg@9374
   108
          by (rule sup_norm_pres, rule a) (simp!)+
wenzelm@9035
   109
      qed
wenzelm@9035
   110
    qed
bauerg@9256
   111
wenzelm@9035
   112
  }
bauerg@9374
   113
  hence "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x --> g = x" 
bauerg@9374
   114
  -- {* With Zorn's Lemma we can conclude that there is a maximal element in $M$.\skp *}
wenzelm@9035
   115
  proof (rule Zorn's_Lemma)
bauerg@9374
   116
    -- {* We show that $M$ is non-empty: *}
bauerg@9374
   117
    have "graph F f \<in> norm_pres_extensions E p F f"
wenzelm@9035
   118
    proof (rule norm_pres_extensionI2)
wenzelm@9035
   119
      have "is_vectorspace F" ..
wenzelm@9035
   120
      thus "is_subspace F F" ..
wenzelm@9035
   121
    qed (blast!)+ 
bauerg@9374
   122
    thus "graph F f \<in> M" by (simp!)
wenzelm@9035
   123
  qed
wenzelm@9035
   124
  thus ?thesis
wenzelm@9035
   125
  proof
bauerg@9374
   126
    fix g assume "g \<in> M" "\<forall>x \<in> M. g \<subseteq> x --> g = x"
bauerg@9256
   127
    -- {* We consider such a maximal element $g \in M$. \skp *}
wenzelm@9035
   128
    show ?thesis
wenzelm@8109
   129
      obtain H h where "graph H h = g" "is_linearform H h" 
bauerg@9374
   130
        "is_subspace H E" "is_subspace F H" "graph F f \<subseteq> graph H h" 
bauerg@9374
   131
        "\<forall>x \<in> H. h x \<le> p x" 
bauerg@9374
   132
        -- {* $g$ is a norm-preserving extension of $f$, in other words: *}
bauerg@9374
   133
        -- {* $g$ is the graph of some linear form $h$ defined on a subspace $H$ of $E$, *}
bauerg@9374
   134
        -- {* and $h$ is an extension of $f$ that is again bounded by $p$. \skp *}
wenzelm@9035
   135
      proof -
bauerg@9374
   136
        have "\<exists> H h. graph H h = g \<and> is_linearform H h 
bauerg@9374
   137
          \<and> is_subspace H E \<and> is_subspace F H
bauerg@9374
   138
          \<and> graph F f \<subseteq> graph H h
bauerg@9374
   139
          \<and> (\<forall>x \<in> H. h x \<le> p x)" by (simp! add: norm_pres_extension_D)
wenzelm@9035
   140
        thus ?thesis by (elim exE conjE) rule
wenzelm@9035
   141
      qed
wenzelm@9035
   142
      have h: "is_vectorspace H" ..
bauerg@9256
   143
      have "H = E"
bauerg@9256
   144
      -- {* We show that $h$ is defined on whole $E$ by classical contradiction. \skp *} 
wenzelm@9035
   145
      proof (rule classical)
bauerg@9374
   146
        assume "H \<noteq> E"
bauerg@9256
   147
        -- {* Assume $h$ is not defined on whole $E$. Then show that $h$ can be extended *}
bauerg@9256
   148
        -- {* in a norm-preserving way to a function $h'$ with the graph $g'$. \skp *}
bauerg@9374
   149
        have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'" 
bauerg@9374
   150
          obtain x' where "x' \<in> E" "x' \<notin> H" 
bauerg@9374
   151
          -- {* Pick $x' \in E \setminus H$. \skp *}
wenzelm@9035
   152
          proof -
bauerg@9374
   153
            have "\<exists>x' \<in> E. x' \<notin> H"
wenzelm@9035
   154
            proof (rule set_less_imp_diff_not_empty)
bauerg@9374
   155
              have "H \<subseteq> E" ..
bauerg@9374
   156
              thus "H \<subset> E" ..
wenzelm@9035
   157
            qed
wenzelm@9035
   158
            thus ?thesis by blast
wenzelm@9035
   159
          qed
bauerg@9374
   160
          have x': "x' \<noteq> 0"
wenzelm@9035
   161
          proof (rule classical)
bauerg@9374
   162
            presume "x' = 0"
bauerg@9374
   163
            with h have "x' \<in> H" by simp
wenzelm@9035
   164
            thus ?thesis by contradiction
wenzelm@9035
   165
          qed blast
bauerg@9256
   166
          def H' == "H + lin x'"
bauerg@9256
   167
          -- {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *}
wenzelm@9035
   168
          show ?thesis
bauerg@9374
   169
            obtain xi where "\<forall>y \<in> H. - p (y + x') - h y \<le> xi 
bauerg@9374
   170
                              \<and> xi \<le> p (y + x') - h y" 
bauerg@9374
   171
            -- {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
bauerg@9374
   172
            -- {* be used to establish that $h'$ is a norm-preserving extension of $h$. 
bauerg@9374
   173
               \label{ex-xi-use}\skp *}
bauerg@9261
   174
bauerg@9261
   175
            proof -
bauerg@9374
   176
	      from h have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y <= xi 
bauerg@9374
   177
                              \<and> xi <= p (y + x') - h y" 
bauerg@9261
   178
              proof (rule ex_xi)
bauerg@9374
   179
                fix u v assume "u \<in> H" "v \<in> H"
bauerg@9261
   180
                from h have "h v - h u = h (v - u)"
bauerg@9261
   181
                  by (simp! add: linearform_diff)
bauerg@9261
   182
                also have "... <= p (v - u)"
bauerg@9261
   183
                  by (simp!)
bauerg@9261
   184
                also have "v - u = x' + - x' + v + - u"
bauerg@9261
   185
                  by (simp! add: diff_eq1)
bauerg@9261
   186
                also have "... = v + x' + - (u + x')"
bauerg@9261
   187
                  by (simp!)
bauerg@9261
   188
                also have "... = (v + x') - (u + x')"
bauerg@9261
   189
                  by (simp! add: diff_eq1)
bauerg@9261
   190
                also have "p ... <= p (v + x') + p (u + x')"
bauerg@9261
   191
                  by (rule seminorm_diff_subadditive) (simp!)+
bauerg@9261
   192
                finally have "h v - h u <= p (v + x') + p (u + x')" .
bauerg@9261
   193
bauerg@9261
   194
                thus "- p (u + x') - h u <= p (v + x') - h v" 
bauerg@9261
   195
                  by (rule real_diff_ineq_swap)
bauerg@9261
   196
              qed
bauerg@9261
   197
              thus ?thesis by rule rule
bauerg@9261
   198
            qed
bauerg@9261
   199
bauerg@9374
   200
            def h' == "\<lambda>x. let (y,a) = SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H
wenzelm@9035
   201
                           in (h y) + a * xi"
bauerg@9256
   202
            -- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *}
wenzelm@9035
   203
            show ?thesis
wenzelm@9035
   204
            proof
bauerg@9374
   205
              show "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'" 
bauerg@9374
   206
              -- {* Show that $h'$ is an extension of $h$ \dots \skp *}
bauerg@9374
   207
              proof
bauerg@9374
   208
		show "g \<subseteq> graph H' h'"
wenzelm@9035
   209
		proof -
bauerg@9374
   210
		  have  "graph H h \<subseteq> graph H' h'"
wenzelm@9035
   211
                  proof (rule graph_extI)
bauerg@9374
   212
		    fix t assume "t \<in> H" 
bauerg@9374
   213
		    have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H)
bauerg@9374
   214
                         = (t, #0)"
bauerg@9374
   215
		      by (rule decomp_H'_H) (assumption+, rule x');
bauerg@9256
   216
		    thus "h t = h' t" by (simp! add: Let_def)
wenzelm@9035
   217
		  next
bauerg@9374
   218
		    show "H \<subseteq> H'"
wenzelm@9035
   219
		    proof (rule subspace_subset)
bauerg@9256
   220
		      show "is_subspace H H'"
bauerg@9256
   221
		      proof (unfold H'_def, rule subspace_vs_sum1)
wenzelm@9035
   222
			show "is_vectorspace H" ..
bauerg@9256
   223
			show "is_vectorspace (lin x')" ..
wenzelm@9035
   224
		      qed
wenzelm@9035
   225
		    qed
wenzelm@9035
   226
		  qed 
wenzelm@9035
   227
		  thus ?thesis by (simp!)
wenzelm@9035
   228
		qed
bauerg@9374
   229
                show "g \<noteq> graph H' h'"
wenzelm@9035
   230
		proof -
bauerg@9374
   231
		  have "graph H h \<noteq> graph H' h'"
wenzelm@9035
   232
		  proof
bauerg@9256
   233
		    assume e: "graph H h = graph H' h'"
bauerg@9374
   234
		    have "x' \<in> H'" 
bauerg@9256
   235
		    proof (unfold H'_def, rule vs_sumI)
bauerg@9374
   236
		      show "x' = 0 + x'" by (simp!)
bauerg@9374
   237
		      from h show "0 \<in> H" ..
bauerg@9374
   238
		      show "x' \<in> lin x'" by (rule x_lin_x)
wenzelm@9035
   239
		    qed
bauerg@9374
   240
		    hence "(x', h' x') \<in> graph H' h'" ..
bauerg@9374
   241
		    with e have "(x', h' x') \<in> graph H h" by simp
bauerg@9374
   242
		    hence "x' \<in> H" ..
wenzelm@9035
   243
		    thus False by contradiction
wenzelm@9035
   244
		  qed
wenzelm@9035
   245
		  thus ?thesis by (simp!)
wenzelm@9035
   246
		qed
wenzelm@9035
   247
              qed
bauerg@9374
   248
	      show "graph H' h' \<in> M" 
bauerg@9374
   249
              -- {* and $h'$ is norm-preserving. \skp *} 
bauerg@9256
   250
              proof -
bauerg@9374
   251
		have "graph H' h' \<in> norm_pres_extensions E p F f"
wenzelm@9035
   252
		proof (rule norm_pres_extensionI2)
bauerg@9256
   253
		  show "is_linearform H' h'"
bauerg@9374
   254
		    by (rule h'_lf) (simp! add: x')+
bauerg@9374
   255
                  show "is_subspace H' E" 
bauerg@9256
   256
		    by (unfold H'_def) (rule vs_sum_subspace [OF _ lin_subspace])
wenzelm@9035
   257
		  have "is_subspace F H" .
wenzelm@9035
   258
		  also from h lin_vs 
bauerg@9256
   259
		  have [fold H'_def]: "is_subspace H (H + lin x')" ..
wenzelm@9035
   260
		  finally (subspace_trans [OF _ h]) 
bauerg@9256
   261
		  show f_h': "is_subspace F H'" .
bauerg@8084
   262
		
bauerg@9374
   263
		  show "graph F f \<subseteq> graph H' h'"
wenzelm@9035
   264
		  proof (rule graph_extI)
bauerg@9374
   265
		    fix x assume "x \<in> F"
wenzelm@9035
   266
		    have "f x = h x" ..
wenzelm@9035
   267
		    also have " ... = h x + #0 * xi" by simp
wenzelm@9035
   268
		    also have "... = (let (y,a) = (x, #0) in h y + a * xi)"
wenzelm@9035
   269
		      by (simp add: Let_def)
wenzelm@9035
   270
		    also have 
bauerg@9374
   271
		      "(x, #0) = (SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H)"
bauerg@9374
   272
		      proof (rule decomp_H'_H [RS sym]) qed (simp! add: x')+
wenzelm@9035
   273
		    also have 
bauerg@9374
   274
		      "(let (y,a) = (SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H)
bauerg@8084
   275
                        in h y + a * xi) 
bauerg@9256
   276
                      = h' x" by (simp!)
bauerg@9256
   277
		    finally show "f x = h' x" .
wenzelm@9035
   278
		  next
bauerg@9374
   279
		    from f_h' show "F \<subseteq> H'" ..
wenzelm@9035
   280
		  qed
bauerg@8084
   281
		
bauerg@9374
   282
		  show "\<forall>x \<in> H'. h' x \<le> p x"
bauerg@9374
   283
		    by (rule h'_norm_pres) (assumption+, rule x')
wenzelm@9035
   284
		qed
bauerg@9374
   285
		thus "graph H' h' \<in> M" by (simp!)
wenzelm@9035
   286
	      qed
wenzelm@9035
   287
            qed
wenzelm@9035
   288
          qed
wenzelm@9035
   289
        qed
bauerg@9374
   290
        hence "\<not> (\<forall>x \<in> M. g \<subseteq> x --> g = x)" by simp
bauerg@9256
   291
        -- {* So the graph $g$ of $h$ cannot be maximal. Contradiction! \skp *}
bauerg@9256
   292
        thus "H = E" by contradiction
bauerg@9256
   293
      qed
bauerg@9374
   294
      thus "\<exists>h. is_linearform E h \<and> (\<forall>x \<in> F. h x = f x) 
bauerg@9374
   295
          \<and> (\<forall>x \<in> E. h x \<le> p x)" 
wenzelm@9035
   296
      proof (intro exI conjI)
wenzelm@9035
   297
        assume eq: "H = E"
wenzelm@9035
   298
	from eq show "is_linearform E h" by (simp!)
bauerg@9374
   299
	show "\<forall>x \<in> F. h x = f x" 
wenzelm@9035
   300
	proof (intro ballI, rule sym)
bauerg@9374
   301
	  fix x assume "x \<in> F" show "f x = h x " ..
wenzelm@9035
   302
	qed
bauerg@9374
   303
	from eq show "\<forall>x \<in> E. h x \<le> p x" by (force!)
wenzelm@9035
   304
      qed
wenzelm@9035
   305
    qed
wenzelm@9035
   306
  qed
bauerg@9374
   307
qed 
bauerg@9374
   308
bauerg@9374
   309
bauerg@9374
   310
bauerg@9374
   311
subsection  {* Alternative formulation *}
bauerg@9374
   312
bauerg@9374
   313
text {* The following alternative formulation of the Hahn-Banach
bauerg@9374
   314
Theorem\label{abs-HahnBanach} uses the fact that for a real linear form
bauerg@9374
   315
$f$ and a seminorm $p$ the
bauerg@9374
   316
following inequations are equivalent:\footnote{This was shown in lemma
bauerg@9374
   317
$\idt{abs{\dsh}ineq{\dsh}iff}$ (see page \pageref{abs-ineq-iff}).}
bauerg@9374
   318
\begin{matharray}{ll}
bauerg@9374
   319
\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\
bauerg@9374
   320
\forall x\in H.\ap h\ap x\leq p\ap x\\
bauerg@9374
   321
\end{matharray}
bauerg@9374
   322
*}
bauerg@9374
   323
bauerg@9374
   324
theorem abs_HahnBanach:
bauerg@9374
   325
  "[| is_vectorspace E; is_subspace F E; is_linearform F f; 
bauerg@9374
   326
  is_seminorm E p; \<forall>x \<in> F. |f x| <= p x |]
bauerg@9374
   327
  ==> \<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x)
bauerg@9374
   328
   \<and> (\<forall>x \<in> E. |g x| <= p x)"
bauerg@9374
   329
proof -
bauerg@9374
   330
  assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
bauerg@9374
   331
    "is_linearform F f"  "\<forall>x \<in> F. |f x| <= p x"
bauerg@9374
   332
  have "\<forall>x \<in> F. f x <= p x"  by (rule abs_ineq_iff [RS iffD1])
bauerg@9374
   333
  hence "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x) 
bauerg@9374
   334
              \<and> (\<forall>x \<in> E. g x <= p x)"
bauerg@9374
   335
    by (simp! only: HahnBanach)
bauerg@9374
   336
  thus ?thesis 
bauerg@9374
   337
  proof (elim exE conjE)
bauerg@9374
   338
    fix g assume "is_linearform E g" "\<forall>x \<in> F. g x = f x" 
bauerg@9374
   339
                  "\<forall>x \<in> E. g x <= p x"
bauerg@9374
   340
    hence "\<forall>x \<in> E. |g x| <= p x"
bauerg@9374
   341
      by (simp! add: abs_ineq_iff [OF subspace_refl])
bauerg@9374
   342
    thus ?thesis by (intro exI conjI)
bauerg@9374
   343
  qed
bauerg@9374
   344
qed
bauerg@9374
   345
bauerg@9374
   346
subsection {* The Hahn-Banach Theorem for normed spaces *}
bauerg@9374
   347
bauerg@9374
   348
text {* Every continuous linear form $f$ on a subspace $F$ of a
bauerg@9374
   349
norm space $E$, can be extended to a continuous linear form $g$ on
bauerg@9374
   350
$E$ such that $\fnorm{f} = \fnorm {g}$. *}
bauerg@9374
   351
bauerg@9374
   352
theorem norm_HahnBanach:
bauerg@9374
   353
  "[| is_normed_vectorspace E norm; is_subspace F E; 
bauerg@9374
   354
  is_linearform F f; is_continuous F norm f |] 
bauerg@9374
   355
  ==> \<exists>g. is_linearform E g
bauerg@9374
   356
         \<and> is_continuous E norm g 
bauerg@9374
   357
         \<and> (\<forall>x \<in> F. g x = f x) 
bauerg@9374
   358
         \<and> \<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
bauerg@9374
   359
proof -
bauerg@9374
   360
  assume e_norm: "is_normed_vectorspace E norm"
bauerg@9374
   361
  assume f: "is_subspace F E" "is_linearform F f"
bauerg@9374
   362
  assume f_cont: "is_continuous F norm f"
bauerg@9374
   363
  have e: "is_vectorspace E" ..
bauerg@9374
   364
  hence f_norm: "is_normed_vectorspace F norm" ..
bauerg@9374
   365
bauerg@9374
   366
  txt{* We define a function $p$ on $E$ as follows:
bauerg@9374
   367
  \begin{matharray}{l}
bauerg@9374
   368
  p \: x = \fnorm f \cdot \norm x\\
bauerg@9374
   369
  \end{matharray}
bauerg@9374
   370
  *}
bauerg@9374
   371
bauerg@9374
   372
  def p == "\<lambda>x. \<parallel>f\<parallel>F,norm * norm x"
bauerg@9374
   373
  
bauerg@9374
   374
  txt{* $p$ is a seminorm on $E$: *}
bauerg@9374
   375
bauerg@9374
   376
  have q: "is_seminorm E p"
bauerg@9374
   377
  proof
bauerg@9374
   378
    fix x y a assume "x \<in> E" "y \<in> E"
bauerg@9374
   379
bauerg@9374
   380
    txt{* $p$ is positive definite: *}
bauerg@9374
   381
bauerg@9374
   382
    show "#0 <= p x"
bauerg@9374
   383
    proof (unfold p_def, rule real_le_mult_order1a) thm fnorm_ge_zero
bauerg@9374
   384
      from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
bauerg@9374
   385
      show "#0 <= norm x" ..
bauerg@9374
   386
    qed
bauerg@9374
   387
bauerg@9374
   388
    txt{* $p$ is absolutely homogenous: *}
bauerg@9374
   389
bauerg@9374
   390
    show "p (a \<cdot> x) = |a| * p x"
bauerg@9374
   391
    proof - 
bauerg@9374
   392
      have "p (a \<cdot> x) = \<parallel>f\<parallel>F,norm * norm (a \<cdot> x)"
bauerg@9374
   393
        by (simp!)
bauerg@9374
   394
      also have "norm (a \<cdot> x) = |a| * norm x" 
bauerg@9374
   395
        by (rule normed_vs_norm_abs_homogenous)
bauerg@9374
   396
      also have "\<parallel>f\<parallel>F,norm * ( |a| * norm x ) 
bauerg@9374
   397
        = |a| * (\<parallel>f\<parallel>F,norm * norm x)"
bauerg@9374
   398
        by (simp! only: real_mult_left_commute)
bauerg@9374
   399
      also have "... = |a| * p x" by (simp!)
bauerg@9374
   400
      finally show ?thesis .
bauerg@9374
   401
    qed
bauerg@9374
   402
bauerg@9374
   403
    txt{* Furthermore, $p$ is subadditive: *}
bauerg@9374
   404
bauerg@9374
   405
    show "p (x + y) <= p x + p y"
bauerg@9374
   406
    proof -
bauerg@9374
   407
      have "p (x + y) = \<parallel>f\<parallel>F,norm * norm (x + y)"
bauerg@9374
   408
        by (simp!)
bauerg@9374
   409
      also 
bauerg@9374
   410
      have "... <= \<parallel>f\<parallel>F,norm * (norm x + norm y)"
bauerg@9374
   411
      proof (rule real_mult_le_le_mono1a)
bauerg@9374
   412
        from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
bauerg@9374
   413
        show "norm (x + y) <= norm x + norm y" ..
bauerg@9374
   414
      qed
bauerg@9374
   415
      also have "... = \<parallel>f\<parallel>F,norm * norm x 
bauerg@9374
   416
                        + \<parallel>f\<parallel>F,norm * norm y"
bauerg@9374
   417
        by (simp! only: real_add_mult_distrib2)
bauerg@9374
   418
      finally show ?thesis by (simp!)
bauerg@9374
   419
    qed
bauerg@9374
   420
  qed
bauerg@9374
   421
bauerg@9374
   422
  txt{* $f$ is bounded by $p$. *} 
bauerg@9374
   423
bauerg@9374
   424
  have "\<forall>x \<in> F. |f x| <= p x"
bauerg@9374
   425
  proof
bauerg@9374
   426
    fix x assume "x \<in> F"
bauerg@9374
   427
     from f_norm show "|f x| <= p x" 
bauerg@9374
   428
       by (simp! add: norm_fx_le_norm_f_norm_x)
bauerg@9374
   429
  qed
bauerg@9374
   430
bauerg@9374
   431
  txt{* Using the fact that $p$ is a seminorm and 
bauerg@9374
   432
  $f$ is bounded by $p$ we can apply the Hahn-Banach Theorem 
bauerg@9374
   433
  for real vector spaces. 
bauerg@9374
   434
  So $f$ can be extended in a norm-preserving way to some function
bauerg@9374
   435
  $g$ on the whole vector space $E$. *}
bauerg@9374
   436
bauerg@9374
   437
  with e f q 
bauerg@9374
   438
  have "\<exists>g. is_linearform E g \<and> (\<forall>x \<in> F. g x = f x) 
bauerg@9374
   439
            \<and> (\<forall>x \<in> E. |g x| <= p x)"
bauerg@9374
   440
    by (simp! add: abs_HahnBanach)
bauerg@9374
   441
bauerg@9374
   442
  thus ?thesis
bauerg@9374
   443
  proof (elim exE conjE) 
bauerg@9374
   444
    fix g
bauerg@9374
   445
    assume "is_linearform E g" and a: "\<forall>x \<in> F. g x = f x" 
bauerg@9374
   446
       and b: "\<forall>x \<in> E. |g x| <= p x"
bauerg@9374
   447
bauerg@9374
   448
    show "\<exists>g. is_linearform E g 
bauerg@9374
   449
            \<and> is_continuous E norm g 
bauerg@9374
   450
            \<and> (\<forall>x \<in> F. g x = f x) 
bauerg@9374
   451
            \<and> \<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
bauerg@9374
   452
    proof (intro exI conjI)
bauerg@9374
   453
bauerg@9374
   454
    txt{* We furthermore have to show that 
bauerg@9374
   455
    $g$ is also continuous: *}
bauerg@9374
   456
bauerg@9374
   457
      show g_cont: "is_continuous E norm g"
bauerg@9374
   458
      proof
bauerg@9374
   459
        fix x assume "x \<in> E"
bauerg@9374
   460
        with b show "|g x| <= \<parallel>f\<parallel>F,norm * norm x"
bauerg@9374
   461
          by (simp add: p_def) 
bauerg@9374
   462
      qed 
bauerg@9374
   463
bauerg@9374
   464
      txt {* To complete the proof, we show that 
bauerg@9374
   465
      $\fnorm g = \fnorm f$. \label{order_antisym} *}
bauerg@9374
   466
bauerg@9374
   467
      show "\<parallel>g\<parallel>E,norm = \<parallel>f\<parallel>F,norm"
bauerg@9374
   468
        (is "?L = ?R")
bauerg@9374
   469
      proof (rule order_antisym)
bauerg@9374
   470
bauerg@9374
   471
        txt{* First we show $\fnorm g \leq \fnorm f$.  The function norm
bauerg@9374
   472
        $\fnorm g$ is defined as the smallest $c\in\bbbR$ such that
bauerg@9374
   473
        \begin{matharray}{l}
bauerg@9374
   474
        \All {x\in E} {|g\ap x| \leq c \cdot \norm x}
bauerg@9374
   475
        \end{matharray}
bauerg@9374
   476
        Furthermore holds
bauerg@9374
   477
        \begin{matharray}{l}
bauerg@9374
   478
        \All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x}
bauerg@9374
   479
        \end{matharray}
bauerg@9374
   480
        *}
bauerg@9374
   481
 
bauerg@9374
   482
        have "\<forall>x \<in> E. |g x| <= \<parallel>f\<parallel>F,norm * norm x"
bauerg@9374
   483
        proof
bauerg@9374
   484
          fix x assume "x \<in> E" 
bauerg@9374
   485
          show "|g x| <= \<parallel>f\<parallel>F,norm * norm x"
bauerg@9374
   486
            by (simp!)
bauerg@9374
   487
        qed
bauerg@9374
   488
bauerg@9374
   489
        with g_cont e_norm show "?L <= ?R"
bauerg@9374
   490
        proof (rule fnorm_le_ub)
bauerg@9374
   491
          from f_cont f_norm show "#0 <= \<parallel>f\<parallel>F,norm" ..
bauerg@9374
   492
        qed
bauerg@9374
   493
bauerg@9374
   494
        txt{* The other direction is achieved by a similar 
bauerg@9374
   495
        argument. *}
bauerg@9374
   496
bauerg@9374
   497
        have "\<forall>x \<in> F. |f x| <= \<parallel>g\<parallel>E,norm * norm x"
bauerg@9374
   498
        proof
bauerg@9374
   499
          fix x assume "x \<in> F" 
bauerg@9374
   500
          from a have "g x = f x" ..
bauerg@9374
   501
          hence "|f x| = |g x|" by simp
bauerg@9374
   502
          also from g_cont
bauerg@9374
   503
          have "... <= \<parallel>g\<parallel>E,norm * norm x"
bauerg@9374
   504
          proof (rule norm_fx_le_norm_f_norm_x)
bauerg@9374
   505
            show "x \<in> E" ..
bauerg@9374
   506
          qed
bauerg@9374
   507
          finally show "|f x| <= \<parallel>g\<parallel>E,norm * norm x" .
bauerg@9374
   508
        qed 
bauerg@9374
   509
        thus "?R <= ?L" 
bauerg@9374
   510
        proof (rule fnorm_le_ub [OF f_cont f_norm])
bauerg@9374
   511
          from g_cont show "#0 <= \<parallel>g\<parallel>E,norm" ..
bauerg@9374
   512
        qed
bauerg@9374
   513
      qed
bauerg@9374
   514
    qed
bauerg@9374
   515
  qed
bauerg@9374
   516
qed
bauerg@9374
   517
wenzelm@9035
   518
end