src/HOL/Real/HahnBanach/HahnBanach.thy
author wenzelm
Fri Oct 22 20:14:31 1999 +0200 (1999-10-22)
changeset 7917 5e5b9813cce7
parent 7808 fd019ac3485f
child 7927 b50446a33c16
permissions -rw-r--r--
HahnBanach update by Gertrud Bauer;
wenzelm@7566
     1
(*  Title:      HOL/Real/HahnBanach/HahnBanach.thy
wenzelm@7566
     2
    ID:         $Id$
wenzelm@7917
     3
    Author:     Gertrud Baueer, TU Munich
wenzelm@7566
     4
*)
wenzelm@7535
     5
wenzelm@7917
     6
header {* The Hahn-Banach Theorem *};
wenzelm@7656
     7
wenzelm@7917
     8
theory HahnBanach
wenzelm@7917
     9
     = HahnBanachSupLemmas + HahnBanachExtLemmas + ZornLemma:;
wenzelm@7535
    10
wenzelm@7808
    11
text {*
wenzelm@7917
    12
  We present the proof of two different versions of the Hahn-Banach 
wenzelm@7917
    13
  Theorem, closely following \cite{Heuser:1986}.
wenzelm@7808
    14
*};
wenzelm@7535
    15
wenzelm@7917
    16
subsection {* The case of general linear spaces *};
wenzelm@7656
    17
wenzelm@7917
    18
text  {* Every linearform $f$ on a subspace $F$ of $E$, which is 
wenzelm@7917
    19
 bounded by some  quasinorm $q$ on $E$, can be extended 
wenzelm@7917
    20
 to a function on $E$ in a norm preseving way. *};
wenzelm@7535
    21
wenzelm@7917
    22
theorem HahnBanach: 
wenzelm@7808
    23
  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; 
wenzelm@7808
    24
  is_linearform F f; ALL x:F. f x <= p x |]
wenzelm@7535
    25
  ==> EX h. is_linearform E h
wenzelm@7535
    26
          & (ALL x:F. h x = f x)
wenzelm@7535
    27
          & (ALL x:E. h x <= p x)";
wenzelm@7535
    28
proof -;
wenzelm@7808
    29
  assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p"
wenzelm@7808
    30
         "is_linearform F f" "ALL x:F. f x <= p x";
wenzelm@7656
    31
  
wenzelm@7917
    32
  txt{* We define $M$ to be the set of all linear extensions 
wenzelm@7917
    33
  of $f$ to superspaces of $F$, which are bounded by $p$. *};
wenzelm@7917
    34
wenzelm@7656
    35
  def M == "norm_pres_extensions E p F f";
wenzelm@7917
    36
  
wenzelm@7917
    37
  txt{* We show that $M$ is non-empty: *};
wenzelm@7535
    38
 
wenzelm@7656
    39
  have aM: "graph F f : norm_pres_extensions E p F f";
wenzelm@7656
    40
  proof (rule norm_pres_extensionI2);
wenzelm@7917
    41
    have "is_vectorspace F"; ..;
wenzelm@7917
    42
    thus "is_subspace F F"; ..;
wenzelm@7566
    43
  qed (blast!)+;
wenzelm@7535
    44
wenzelm@7917
    45
  subsubsect {* Existence of a limit function of the norm preserving
wenzelm@7917
    46
  extensions *}; 
wenzelm@7535
    47
wenzelm@7917
    48
  txt {* For every non-empty chain of norm preserving functions
wenzelm@7917
    49
  the union of all functions in the chain is again a norm preserving
wenzelm@7917
    50
  function. (The union is an upper bound for all elements. 
wenzelm@7917
    51
  It is even the least upper bound, because every upper bound of $M$
wenzelm@7917
    52
  is also an upper bound for $\cup\; c$.) *};
wenzelm@7917
    53
wenzelm@7917
    54
  have "!! c. [| c : chain M; EX x. x:c |] ==> Union c : M";  
wenzelm@7535
    55
  proof -;
wenzelm@7917
    56
    fix c; assume "c:chain M" "EX x. x:c";
wenzelm@7917
    57
    show "Union c : M";
wenzelm@7535
    58
wenzelm@7656
    59
    proof (unfold M_def, rule norm_pres_extensionI);
wenzelm@7535
    60
      show "EX (H::'a set) h::'a => real. graph H h = Union c
wenzelm@7535
    61
              & is_linearform H h 
wenzelm@7535
    62
              & is_subspace H E 
wenzelm@7535
    63
              & is_subspace F H 
wenzelm@7917
    64
              & graph F f <= graph H h
wenzelm@7917
    65
              & (ALL x::'a:H. h x <= p x)";
wenzelm@7656
    66
      proof (intro exI conjI);
wenzelm@7535
    67
        let ?H = "domain (Union c)";
wenzelm@7656
    68
        let ?h = "funct (Union c)";
wenzelm@7656
    69
wenzelm@7917
    70
        show a [simp]: "graph ?H ?h = Union c"; 
wenzelm@7656
    71
        proof (rule graph_domain_funct);
wenzelm@7656
    72
          fix x y z; assume "(x, y) : Union c" "(x, z) : Union c";
wenzelm@7917
    73
          show "z = y"; by (rule sup_definite);
wenzelm@7656
    74
        qed;
wenzelm@7535
    75
            
wenzelm@7917
    76
        show "is_linearform ?H ?h"; 
wenzelm@7917
    77
          by (simp! add: sup_lf a);
wenzelm@7535
    78
wenzelm@7917
    79
        show "is_subspace ?H E"; 
wenzelm@7656
    80
          by (rule sup_subE, rule a) (simp!)+;
wenzelm@7656
    81
 
wenzelm@7917
    82
        show "is_subspace F ?H"; 
wenzelm@7656
    83
          by (rule sup_supF, rule a) (simp!)+;
wenzelm@7535
    84
wenzelm@7917
    85
        show "graph F f <= graph ?H ?h"; 
wenzelm@7656
    86
          by (rule sup_ext, rule a) (simp!)+;
wenzelm@7535
    87
wenzelm@7656
    88
        show "ALL x::'a:?H. ?h x <= p x"; 
wenzelm@7656
    89
          by (rule sup_norm_pres, rule a) (simp!)+;
wenzelm@7535
    90
      qed;
wenzelm@7535
    91
    qed;
wenzelm@7535
    92
  qed;
wenzelm@7656
    93
 
wenzelm@7917
    94
  txt {* According to Zorn's Lemma there exists 
wenzelm@7917
    95
  a maximal norm-preserving extension $g\in M$. *};
wenzelm@7535
    96
  
wenzelm@7535
    97
  with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x";
wenzelm@7566
    98
    by (simp! add: Zorn's_Lemma);
wenzelm@7656
    99
wenzelm@7535
   100
  thus ?thesis;
wenzelm@7535
   101
  proof;
wenzelm@7535
   102
    fix g; assume g: "g:M" "ALL x:M. g <= x --> g = x";
wenzelm@7535
   103
 
wenzelm@7917
   104
    have ex_Hh: 
wenzelm@7917
   105
      "EX H h. graph H h = g 
wenzelm@7917
   106
           & is_linearform H h 
wenzelm@7917
   107
           & is_subspace H E 
wenzelm@7917
   108
           & is_subspace F H
wenzelm@7917
   109
           & graph F f <= graph H h
wenzelm@7917
   110
           & (ALL x:H. h x <= p x) "; 
wenzelm@7656
   111
      by (simp! add: norm_pres_extension_D);
wenzelm@7535
   112
    thus ?thesis;
wenzelm@7917
   113
    proof (elim exE conjE, intro exI);
wenzelm@7656
   114
      fix H h; 
wenzelm@7808
   115
      assume "graph H h = g" "is_linearform (H::'a set) h" 
wenzelm@7808
   116
             "is_subspace H E" "is_subspace F H"
wenzelm@7917
   117
        and h_ext: "graph F f <= graph H h"
wenzelm@7917
   118
        and h_bound: "ALL x:H. h x <= p x";
wenzelm@7656
   119
wenzelm@7917
   120
      have h: "is_vectorspace H"; ..;
wenzelm@7917
   121
      have f: "is_vectorspace F"; ..;
wenzelm@7535
   122
wenzelm@7917
   123
subsubsect {* The domain of the limit function. *};
wenzelm@7656
   124
wenzelm@7808
   125
have eq: "H = E"; 
wenzelm@7808
   126
proof (rule classical);
wenzelm@7656
   127
wenzelm@7917
   128
txt {* Assume the domain of the supremum is not $E$. *};
wenzelm@7917
   129
;
wenzelm@7808
   130
  assume "H ~= E";
wenzelm@7917
   131
  have "H <= E"; ..;
wenzelm@7917
   132
  hence "H < E"; ..;
wenzelm@7917
   133
 
wenzelm@7917
   134
  txt{* Then there exists an element $x_0$ in 
wenzelm@7917
   135
  the difference of $E$ and $H$. *};
wenzelm@7656
   136
wenzelm@7917
   137
  hence "EX x0:E. x0~:H"; 
wenzelm@7917
   138
    by (rule set_less_imp_diff_not_empty);
wenzelm@7535
   139
wenzelm@7917
   140
  txt {* We get that $h$ can be extended  in a 
wenzelm@7917
   141
  norm-preserving way to some $H_0$. *};
wenzelm@7917
   142
;  
wenzelm@7917
   143
  hence "EX H0 h0. g <= graph H0 h0 & g ~= graph H0 h0 
wenzelm@7917
   144
                 & graph H0 h0 : M";
wenzelm@7917
   145
  proof;
wenzelm@7917
   146
    fix x0; assume "x0:E" "x0~:H";
wenzelm@7656
   147
wenzelm@7917
   148
    have x0: "x0 ~= <0>";
wenzelm@7917
   149
    proof (rule classical);
wenzelm@7917
   150
      presume "x0 = <0>";
wenzelm@7917
   151
      with h; have "x0:H"; by simp;
wenzelm@7917
   152
      thus ?thesis; by contradiction;
wenzelm@7917
   153
    qed blast;
wenzelm@7917
   154
wenzelm@7917
   155
    txt {* Define $H_0$ as the (direct) sum of H and the 
wenzelm@7917
   156
    linear closure of $x_0$.*};
wenzelm@7917
   157
wenzelm@7917
   158
    def H0 == "H + lin x0";
wenzelm@7535
   159
wenzelm@7917
   160
    from h; have xi: "EX xi. (ALL y:H. - p (y + x0) - h y <= xi)
wenzelm@7917
   161
                     & (ALL y:H. xi <= p (y + x0) - h y)";
wenzelm@7917
   162
    proof (rule ex_xi);
wenzelm@7917
   163
      fix u v; assume "u:H" "v:H";
wenzelm@7917
   164
      from h; have "h v - h u = h (v - u)";
wenzelm@7917
   165
         by (simp! add: linearform_diff_linear);
wenzelm@7917
   166
      also; from h_bound; have "... <= p (v - u)";
wenzelm@7917
   167
        by (simp!);
wenzelm@7917
   168
      also; have "v - u = x0 + - x0 + v + - u";
wenzelm@7917
   169
        by (simp! add: diff_eq1);
wenzelm@7917
   170
      also; have "... = v + x0 + - (u + x0)";
wenzelm@7917
   171
        by (simp!);
wenzelm@7917
   172
      also; have "... = (v + x0) - (u + x0)";
wenzelm@7917
   173
        by (simp! add: diff_eq1);
wenzelm@7917
   174
      also; have "p ... <= p (v + x0) + p (u + x0)";
wenzelm@7917
   175
         by (rule quasinorm_diff_triangle_ineq) (simp!)+;
wenzelm@7917
   176
      finally; have "h v - h u <= p (v + x0) + p (u + x0)"; .;
wenzelm@7808
   177
wenzelm@7917
   178
      thus "- p (u + x0) - h u <= p (v + x0) - h v";
wenzelm@7917
   179
        by (rule real_diff_ineq_swap);
wenzelm@7917
   180
    qed;
wenzelm@7917
   181
    hence "EX h0. g <= graph H0 h0 & g ~= graph H0 h0
wenzelm@7917
   182
               & graph H0 h0 : M"; 
wenzelm@7917
   183
    proof (elim exE, intro exI conjI);
wenzelm@7917
   184
      fix xi; 
wenzelm@7917
   185
      assume a: "(ALL y:H. - p (y + x0) - h y <= xi) 
wenzelm@7917
   186
               & (ALL y:H. xi <= p (y + x0) - h y)";
wenzelm@7917
   187
     
wenzelm@7917
   188
      txt {* Define $h_0$ as the linear extension of $h$ on $H_0$:*};  
wenzelm@7535
   189
wenzelm@7917
   190
      def h0 ==
wenzelm@7917
   191
          "\<lambda>x. let (y,a) = SOME (y, a). (x = y + a <*> x0 & y:H)
wenzelm@7917
   192
               in (h y) + a * xi";
wenzelm@7808
   193
wenzelm@7917
   194
      txt {* We get that the graph of $h_0$ extend that of
wenzelm@7917
   195
      $h$. *};
wenzelm@7917
   196
        
wenzelm@7917
   197
      have  "graph H h <= graph H0 h0"; 
wenzelm@7917
   198
      proof (rule graph_extI);
wenzelm@7917
   199
        fix t; assume "t:H"; 
wenzelm@7917
   200
        have "(SOME (y, a). t = y + a <*> x0 & y : H) = (t,0r)";
wenzelm@7917
   201
          by (rule decomp_H0_H, rule x0); 
wenzelm@7917
   202
        thus "h t = h0 t"; by (simp! add: Let_def);
wenzelm@7917
   203
      next;
wenzelm@7917
   204
        show "H <= H0";
wenzelm@7917
   205
        proof (rule subspace_subset);
wenzelm@7917
   206
	  show "is_subspace H H0";
wenzelm@7917
   207
          proof (unfold H0_def, rule subspace_vs_sum1);
wenzelm@7917
   208
       	    show "is_vectorspace H"; ..;
wenzelm@7917
   209
            show "is_vectorspace (lin x0)"; ..;
wenzelm@7566
   210
          qed;
wenzelm@7535
   211
        qed;
wenzelm@7808
   212
      qed;
wenzelm@7917
   213
      thus "g <= graph H0 h0"; by (simp!);
wenzelm@7808
   214
wenzelm@7917
   215
      txt {* Apparently $h_0$ is not equal to $h$. *};
wenzelm@7917
   216
wenzelm@7917
   217
      have "graph H h ~= graph H0 h0";
wenzelm@7917
   218
      proof;
wenzelm@7917
   219
        assume e: "graph H h = graph H0 h0";
wenzelm@7917
   220
        have "x0 : H0"; 
wenzelm@7917
   221
        proof (unfold H0_def, rule vs_sumI);
wenzelm@7917
   222
          show "x0 = <0> + x0"; by (simp!);
wenzelm@7917
   223
          from h; show "<0> : H"; ..;
wenzelm@7917
   224
          show "x0 : lin x0"; by (rule x_lin_x);
wenzelm@7917
   225
        qed;
wenzelm@7917
   226
        hence "(x0, h0 x0) : graph H0 h0"; ..;
wenzelm@7917
   227
        with e; have "(x0, h0 x0) : graph H h"; by simp;
wenzelm@7917
   228
        hence "x0 : H"; ..;
wenzelm@7917
   229
        thus False; by contradiction;
wenzelm@7917
   230
      qed;
wenzelm@7917
   231
      thus "g ~= graph H0 h0"; by (simp!);
wenzelm@7917
   232
wenzelm@7917
   233
      txt {* Furthermore  $h_0$ is a norm preserving extension 
wenzelm@7917
   234
     of $f$. *};
wenzelm@7917
   235
wenzelm@7917
   236
      have "graph H0 h0 : norm_pres_extensions E p F f";
wenzelm@7917
   237
      proof (rule norm_pres_extensionI2);
wenzelm@7917
   238
wenzelm@7917
   239
        show "is_linearform H0 h0";
wenzelm@7917
   240
          by (rule h0_lf, rule x0) (simp!)+;
wenzelm@7917
   241
wenzelm@7917
   242
        show "is_subspace H0 E";
wenzelm@7917
   243
          by (unfold H0_def, rule vs_sum_subspace, 
wenzelm@7917
   244
             rule lin_subspace);
wenzelm@7917
   245
wenzelm@7917
   246
        have "is_subspace F H"; .;
wenzelm@7917
   247
        also; from h lin_vs; 
wenzelm@7917
   248
	have [fold H0_def]: "is_subspace H (H + lin x0)"; ..;
wenzelm@7917
   249
        finally (subspace_trans [OF _ h]); 
wenzelm@7917
   250
	show f_h0: "is_subspace F H0"; .; (*** 
wenzelm@7917
   251
        backwards:
wenzelm@7917
   252
        show f_h0: "is_subspace F H0"; .;
wenzelm@7917
   253
        proof (rule subspace_trans [of F H H0]);
wenzelm@7917
   254
          from h lin_vs; 
wenzelm@7917
   255
          have "is_subspace H (H + lin x0)"; ..;
wenzelm@7917
   256
          thus "is_subspace H H0"; by (unfold H0_def);
wenzelm@7917
   257
        qed; ***)
wenzelm@7917
   258
wenzelm@7917
   259
        show "graph F f <= graph H0 h0";
wenzelm@7917
   260
        proof (rule graph_extI);
wenzelm@7917
   261
          fix x; assume "x:F";
wenzelm@7917
   262
          have "f x = h x"; ..;
wenzelm@7917
   263
          also; have " ... = h x + 0r * xi"; by simp;
wenzelm@7917
   264
          also; have "... = (let (y,a) = (x, 0r) in h y + a * xi)";
wenzelm@7917
   265
            by (simp add: Let_def);
wenzelm@7917
   266
          also; have 
wenzelm@7917
   267
            "(x, 0r) = (SOME (y, a). x = y + a <*> x0 & y : H)";
wenzelm@7917
   268
            by (rule decomp_H0_H [RS sym], rule x0) (simp!)+;
wenzelm@7917
   269
          also; have 
wenzelm@7917
   270
            "(let (y,a) = (SOME (y,a). x = y + a <*> x0 & y : H)
wenzelm@7917
   271
              in h y + a * xi) 
wenzelm@7917
   272
             = h0 x"; by (simp!);
wenzelm@7917
   273
          finally; show "f x = h0 x"; .;
wenzelm@7917
   274
        next;
wenzelm@7917
   275
          from f_h0; show "F <= H0"; ..;
wenzelm@7917
   276
        qed;
wenzelm@7917
   277
wenzelm@7917
   278
        show "ALL x:H0. h0 x <= p x";
wenzelm@7917
   279
          by (rule h0_norm_pres, rule x0) (assumption | (simp!))+;
wenzelm@7917
   280
      qed;
wenzelm@7917
   281
      thus "graph H0 h0 : M"; by (simp!);
wenzelm@7808
   282
    qed;
wenzelm@7917
   283
    thus ?thesis; ..;
wenzelm@7535
   284
  qed;
wenzelm@7917
   285
wenzelm@7917
   286
  txt {* We have shown, that $h$ can still be extended to 
wenzelm@7917
   287
  some $h_0$, in contradiction to the assumption that 
wenzelm@7917
   288
  $h$ is a maximal element. *};
wenzelm@7917
   289
wenzelm@7917
   290
  hence "EX x:M. g <= x & g ~= x"; 
wenzelm@7917
   291
    by (elim exE conjE, intro bexI conjI);
wenzelm@7917
   292
  hence "~ (ALL x:M. g <= x --> g = x)"; by simp;
wenzelm@7917
   293
  thus ?thesis; by contradiction;
wenzelm@7808
   294
qed; 
wenzelm@7808
   295
wenzelm@7917
   296
txt{* It follows $H = E$ and the thesis can be shown. *};
wenzelm@7917
   297
wenzelm@7808
   298
show "is_linearform E h & (ALL x:F. h x = f x) 
wenzelm@7808
   299
     & (ALL x:E. h x <= p x)";
wenzelm@7808
   300
proof (intro conjI); 
wenzelm@7808
   301
  from eq; show "is_linearform E h"; by (simp!);
wenzelm@7808
   302
  show "ALL x:F. h x = f x"; 
wenzelm@7808
   303
  proof (intro ballI, rule sym);
wenzelm@7808
   304
    fix x; assume "x:F"; show "f x = h x "; ..;
wenzelm@7808
   305
  qed;
wenzelm@7808
   306
  from eq; show "ALL x:E. h x <= p x"; by (force!);
wenzelm@7917
   307
qed;
wenzelm@7917
   308
wenzelm@7917
   309
qed;
wenzelm@7917
   310
qed;
wenzelm@7535
   311
qed;
wenzelm@7535
   312
wenzelm@7917
   313
wenzelm@7917
   314
wenzelm@7917
   315
subsection  {* An alternative formulation of the theorem *};
wenzelm@7656
   316
wenzelm@7917
   317
text {* The following alternative formulation of the 
wenzelm@7917
   318
Hahn-Banach Theorem uses the fact that for
wenzelm@7917
   319
real numbers the following inequations are equivalent:
wenzelm@7917
   320
\begin{matharray}{ll}
wenzelm@7917
   321
\forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\
wenzelm@7917
   322
\forall x\in H.\ap h\ap x\leq p\ap x\\
wenzelm@7917
   323
\end{matharray}
wenzelm@7917
   324
(This was shown in lemma $\idt{rabs{\dsh}ineq}$.) *};
wenzelm@7917
   325
wenzelm@7917
   326
theorem rabs_HahnBanach:
wenzelm@7808
   327
  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; 
wenzelm@7808
   328
  is_linearform F f; ALL x:F. rabs (f x) <= p x |]
wenzelm@7808
   329
  ==> EX g. is_linearform E g
wenzelm@7808
   330
          & (ALL x:F. g x = f x)
wenzelm@7808
   331
          & (ALL x:E. rabs (g x) <= p x)";
wenzelm@7535
   332
proof -; 
wenzelm@7808
   333
  assume e: "is_vectorspace E" "is_subspace F E" "is_quasinorm E p" 
wenzelm@7808
   334
            "is_linearform F f"  "ALL x:F. rabs (f x) <= p x";
wenzelm@7917
   335
  have "ALL x:F. f x <= p x"; 
wenzelm@7917
   336
    by (rule rabs_ineq_iff [RS iffD1]);
wenzelm@7808
   337
  hence "EX g. is_linearform E g & (ALL x:F. g x = f x) 
wenzelm@7808
   338
              & (ALL x:E. g x <= p x)";
wenzelm@7917
   339
    by (simp! only: HahnBanach);
wenzelm@7535
   340
  thus ?thesis;
wenzelm@7535
   341
  proof (elim exE conjE);
wenzelm@7808
   342
    fix g; assume "is_linearform E g" "ALL x:F. g x = f x" 
wenzelm@7808
   343
                  "ALL x:E. g x <= p x";
wenzelm@7535
   344
    show ?thesis;
wenzelm@7917
   345
    proof (intro exI conjI);
wenzelm@7566
   346
      from e; show "ALL x:E. rabs (g x) <= p x"; 
wenzelm@7917
   347
        by (simp! add: rabs_ineq_iff [OF subspace_refl]);
wenzelm@7535
   348
    qed;
wenzelm@7535
   349
  qed;
wenzelm@7535
   350
qed;
wenzelm@7535
   351
wenzelm@7535
   352
wenzelm@7917
   353
subsection {* The Hahn-Banach Theorem for normed spaces *};
wenzelm@7656
   354
wenzelm@7917
   355
text  {* Every continous linear function $f$ on a subspace of $E$, 
wenzelm@7917
   356
  can be extended to a continous function on $E$ with the same 
wenzelm@7917
   357
  function norm. *};
wenzelm@7656
   358
wenzelm@7917
   359
theorem norm_HahnBanach:
wenzelm@7917
   360
  "[| is_normed_vectorspace E norm; is_subspace F E; 
wenzelm@7917
   361
  is_linearform F f; is_continous F norm f |] 
wenzelm@7535
   362
  ==> EX g. is_linearform E g
wenzelm@7535
   363
         & is_continous E norm g 
wenzelm@7535
   364
         & (ALL x:F. g x = f x) 
wenzelm@7917
   365
         & function_norm E norm g = function_norm F norm f";
wenzelm@7535
   366
proof -;
wenzelm@7917
   367
  assume e_norm: "is_normed_vectorspace E norm";
wenzelm@7917
   368
  assume f: "is_subspace F E" "is_linearform F f";
wenzelm@7917
   369
  assume f_cont: "is_continous F norm f";
wenzelm@7566
   370
  have e: "is_vectorspace E"; ..;
wenzelm@7917
   371
  with _; have f_norm: "is_normed_vectorspace F norm"; ..;
wenzelm@7656
   372
wenzelm@7917
   373
  txt{* We define the function $p$ on $E$ as follows:
wenzelm@7917
   374
  \begin{matharray}{l}
wenzelm@7917
   375
  p\ap x = \fnorm f * \norm x\\
wenzelm@7917
   376
  % p\ap x = \fnorm f * \fnorm x.\\
wenzelm@7917
   377
  \end{matharray}
wenzelm@7917
   378
  *};
wenzelm@7917
   379
wenzelm@7917
   380
  def p == "\<lambda>x. function_norm F norm f * norm x";
wenzelm@7535
   381
  
wenzelm@7917
   382
  txt{* $p$ is a quasinorm on $E$: *};
wenzelm@7535
   383
wenzelm@7535
   384
  have q: "is_quasinorm E p";
wenzelm@7535
   385
  proof;
wenzelm@7535
   386
    fix x y a; assume "x:E" "y:E";
wenzelm@7535
   387
wenzelm@7917
   388
    txt{* $p$ is positive definite: *};
wenzelm@7917
   389
wenzelm@7535
   390
    show "0r <= p x";
wenzelm@7535
   391
    proof (unfold p_def, rule real_le_mult_order);
wenzelm@7917
   392
      from _ f_norm; show "0r <= function_norm F norm f"; ..;
wenzelm@7566
   393
      show "0r <= norm x"; ..;
wenzelm@7535
   394
    qed;
wenzelm@7535
   395
wenzelm@7917
   396
    txt{* $p$ is multiplicative: *};
wenzelm@7917
   397
wenzelm@7917
   398
    show "p (a <*> x) = rabs a * p x";
wenzelm@7535
   399
    proof -; 
wenzelm@7917
   400
      have "p (a <*> x) = function_norm F norm f * norm (a <*> x)";
wenzelm@7808
   401
        by (simp!);
wenzelm@7917
   402
      also; have "norm (a <*> x) = rabs a * norm x"; 
wenzelm@7808
   403
        by (rule normed_vs_norm_mult_distrib);
wenzelm@7917
   404
      also; have "function_norm F norm f * (rabs a * norm x) 
wenzelm@7917
   405
        = rabs a * (function_norm F norm f * norm x)";
wenzelm@7566
   406
        by (simp! only: real_mult_left_commute);
wenzelm@7917
   407
      also; have "... = rabs a * p x"; by (simp!);
wenzelm@7535
   408
      finally; show ?thesis; .;
wenzelm@7535
   409
    qed;
wenzelm@7535
   410
wenzelm@7917
   411
    txt{* Furthermore $p$ obeys the triangle inequation: *};
wenzelm@7917
   412
wenzelm@7917
   413
    show "p (x + y) <= p x + p y";
wenzelm@7535
   414
    proof -;
wenzelm@7917
   415
      have "p (x + y) = function_norm F norm f * norm (x + y)";
wenzelm@7808
   416
        by (simp!);
wenzelm@7917
   417
      also; 
wenzelm@7917
   418
      have "... <= function_norm F norm f * (norm x + norm y)";
wenzelm@7535
   419
      proof (rule real_mult_le_le_mono1);
wenzelm@7917
   420
        from _ f_norm; show "0r <= function_norm F norm f"; ..;
wenzelm@7917
   421
        show "norm (x + y) <= norm x + norm y"; ..;
wenzelm@7535
   422
      qed;
wenzelm@7917
   423
      also; have "... = function_norm F norm f * norm x 
wenzelm@7917
   424
                        + function_norm F norm f * norm y";
wenzelm@7566
   425
        by (simp! only: real_add_mult_distrib2);
wenzelm@7566
   426
      finally; show ?thesis; by (simp!);
wenzelm@7535
   427
    qed;
wenzelm@7535
   428
  qed;
wenzelm@7917
   429
wenzelm@7917
   430
  txt{* $f$ is bounded by $p$. *}; 
wenzelm@7917
   431
wenzelm@7535
   432
  have "ALL x:F. rabs (f x) <= p x";
wenzelm@7535
   433
  proof;
wenzelm@7535
   434
    fix x; assume "x:F";
wenzelm@7917
   435
     from f_norm; show "rabs (f x) <= p x"; 
wenzelm@7808
   436
       by (simp! add: norm_fx_le_norm_f_norm_x);
wenzelm@7535
   437
  qed;
wenzelm@7535
   438
wenzelm@7917
   439
  txt{* Using the facts that $p$ is a quasinorm and 
wenzelm@7917
   440
  $f$ is bounded we can apply the Hahn-Banach Theorem for real
wenzelm@7917
   441
  vector spaces. 
wenzelm@7917
   442
  So $f$ can be extended in a norm preserving way to some function
wenzelm@7917
   443
  $g$ on the whole vector space $E$. *};
wenzelm@7535
   444
wenzelm@7917
   445
  with e f q; 
wenzelm@7917
   446
  have "EX g. is_linearform E g & (ALL x:F. g x = f x) 
wenzelm@7917
   447
            & (ALL x:E. rabs (g x) <= p x)";
wenzelm@7917
   448
    by (simp! add: rabs_HahnBanach);
wenzelm@7917
   449
wenzelm@7917
   450
  thus ?thesis;
wenzelm@7917
   451
  proof (elim exE conjE); 
wenzelm@7535
   452
    fix g;
wenzelm@7808
   453
    assume "is_linearform E g" and a: "ALL x:F. g x = f x" 
wenzelm@7808
   454
       and "ALL x:E. rabs (g x) <= p x";
wenzelm@7917
   455
wenzelm@7917
   456
    show "EX g. is_linearform E g 
wenzelm@7917
   457
            & is_continous E norm g 
wenzelm@7917
   458
            & (ALL x:F. g x = f x) 
wenzelm@7917
   459
            & function_norm E norm g = function_norm F norm f";
wenzelm@7917
   460
    proof (intro exI conjI);
wenzelm@7917
   461
wenzelm@7917
   462
    txt{* To complete the proof, we show that this function
wenzelm@7917
   463
    $g$ is also continous and has the same function norm as
wenzelm@7917
   464
    $f$. *};
wenzelm@7917
   465
wenzelm@7917
   466
      show g_cont: "is_continous E norm g";
wenzelm@7917
   467
      proof;
wenzelm@7917
   468
        fix x; assume "x:E";
wenzelm@7917
   469
        show "rabs (g x) <= function_norm F norm f * norm x";
wenzelm@7917
   470
          by (rule bspec [of _ _ x], (simp!));
wenzelm@7917
   471
      qed; 
wenzelm@7917
   472
wenzelm@7917
   473
      show "function_norm E norm g = function_norm F norm f"
wenzelm@7917
   474
        (is "?L = ?R");
wenzelm@7917
   475
      proof (rule order_antisym);
wenzelm@7917
   476
wenzelm@7917
   477
        txt{* $\idt{function{\dsh}norm}\ap F\ap \idt{norm}\ap f$ is 
wenzelm@7917
   478
        a solution
wenzelm@7917
   479
        for the inequation 
wenzelm@7917
   480
        \begin{matharray}{l}
wenzelm@7917
   481
        \forall\ap x\in E.\ap |g\ap x| \leq c * \norm x.
wenzelm@7917
   482
        \end{matharray} *};
wenzelm@7917
   483
wenzelm@7917
   484
        have "ALL x:E. rabs (g x) <= function_norm F norm f * norm x";
wenzelm@7535
   485
        proof;
wenzelm@7535
   486
          fix x; assume "x:E"; 
wenzelm@7535
   487
          show "rabs (g x) <= function_norm F norm f * norm x";
wenzelm@7917
   488
            by (simp!);
wenzelm@7535
   489
        qed;
wenzelm@7917
   490
wenzelm@7917
   491
        txt{* Since
wenzelm@7917
   492
         $\idt{function{\dsh}norm}\ap E\ap \idt{norm}\ap g$
wenzelm@7917
   493
        is the smallest solution for this inequation, we have: *};
wenzelm@7917
   494
wenzelm@7917
   495
        with _ g_cont;
wenzelm@7917
   496
        show "?L <= ?R";
wenzelm@7917
   497
        proof (rule fnorm_le_ub);
wenzelm@7917
   498
          from f_cont f_norm; show "0r <= function_norm F norm f"; ..;
wenzelm@7917
   499
        qed;
wenzelm@7917
   500
wenzelm@7917
   501
        txt{* The other direction is achieved by a similar 
wenzelm@7917
   502
        argument. *};
wenzelm@7917
   503
wenzelm@7917
   504
        have "ALL x:F. rabs (f x) <= function_norm E norm g * norm x";
wenzelm@7535
   505
        proof;
wenzelm@7566
   506
          fix x; assume "x : F"; 
wenzelm@7566
   507
          from a; have "g x = f x"; ..;
wenzelm@7535
   508
          hence "rabs (f x) = rabs (g x)"; by simp;
wenzelm@7917
   509
          also; from _ _ g_cont; 
wenzelm@7917
   510
          have "... <= function_norm E norm g * norm x";
wenzelm@7917
   511
            by (rule norm_fx_le_norm_f_norm_x) (simp!)+;
wenzelm@7808
   512
          finally; 
wenzelm@7808
   513
          show "rabs (f x) <= function_norm E norm g * norm x"; .;
wenzelm@7535
   514
        qed;
wenzelm@7917
   515
  
wenzelm@7917
   516
        with f_norm f_cont; show "?R <= ?L"; 
wenzelm@7917
   517
        proof (rule fnorm_le_ub);
wenzelm@7917
   518
          from g_cont; show "0r <= function_norm E norm g"; ..;
wenzelm@7917
   519
        qed;
wenzelm@7535
   520
      qed;
wenzelm@7535
   521
    qed;
wenzelm@7535
   522
  qed;
wenzelm@7535
   523
qed;
wenzelm@7535
   524
wenzelm@7808
   525
end;