src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
 author wenzelm Mon Nov 02 11:43:02 2015 +0100 (2015-11-02) changeset 61540 f92bf6674699 parent 61539 a29295dac1ca child 61879 e4f9d8f094fe permissions -rw-r--r--
tuned document;
 wenzelm@31795  1 (* Title: HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy  wenzelm@7917  2  Author: Gertrud Bauer, TU Munich  wenzelm@7917  3 *)  wenzelm@7917  4 wenzelm@58889  5 section \Extending non-maximal functions\  wenzelm@7917  6 wenzelm@31795  7 theory Hahn_Banach_Ext_Lemmas  wenzelm@31795  8 imports Function_Norm  wenzelm@27612  9 begin  wenzelm@7917  10 wenzelm@58744  11 text \  wenzelm@61540  12  In this section the following context is presumed. Let \E\ be a real  wenzelm@61540  13  vector space with a seminorm \q\ on \E\. \F\ is a subspace of \E\ and \f\  wenzelm@61540  14  a linear function on \F\. We consider a subspace \H\ of \E\ that is a  wenzelm@61540  15  superspace of \F\ and a linear form \h\ on \H\. \H\ is a not equal to \E\  wenzelm@61540  16  and \x\<^sub>0\ is an element in \E - H\. \H\ is extended to the direct sum \H'  wenzelm@61540  17  = H + lin x\<^sub>0\, so for any \x \ H'\ the decomposition of \x = y + a \ x\  wenzelm@61540  18  with \y \ H\ is unique. \h'\ is defined on \H'\ by \h' x = h y + a \ \\  wenzelm@61540  19  for a certain \\\.  wenzelm@7917  20 wenzelm@61540  21  Subsequently we show some properties of this extension \h'\ of \h\.  wenzelm@7917  22 wenzelm@61486  23  \<^medskip>  wenzelm@61540  24  This lemma will be used to show the existence of a linear extension of \f\  wenzelm@61540  25  (see page \pageref{ex-xi-use}). It is a consequence of the completeness of  wenzelm@61540  26  \\\. To show  wenzelm@10687  27  \begin{center}  wenzelm@10687  28  \begin{tabular}{l}  wenzelm@61539  29  \\\. \y \ F. a y \ \ \ \ \ b y\  wenzelm@10687  30  \end{tabular}  wenzelm@10687  31  \end{center}  wenzelm@61540  32  \<^noindent> it suffices to show that  wenzelm@10687  33  \begin{center}  wenzelm@10687  34  \begin{tabular}{l}  wenzelm@61539  35  \\u \ F. \v \ F. a u \ b v\  wenzelm@10687  36  \end{tabular}  wenzelm@10687  37  \end{center}  wenzelm@58744  38 \  wenzelm@7917  39 wenzelm@10687  40 lemma ex_xi:  ballarin@27611  41  assumes "vectorspace F"  wenzelm@13515  42  assumes r: "\u v. u \ F \ v \ F \ a u \ b v"  wenzelm@13515  43  shows "\xi::real. \y \ F. a y \ xi \ xi \ b y"  wenzelm@10007  44 proof -  ballarin@29234  45  interpret vectorspace F by fact  wenzelm@58744  46  txt \From the completeness of the reals follows:  wenzelm@61539  47  The set \S = {a u. u \ F}\ has a supremum, if it is  wenzelm@58744  48  non-empty and has an upper bound.\  wenzelm@7917  49 wenzelm@13515  50  let ?S = "{a u | u. u \ F}"  wenzelm@13515  51  have "\xi. lub ?S xi"  wenzelm@13515  52  proof (rule real_complete)  wenzelm@13515  53  have "a 0 \ ?S" by blast  wenzelm@13515  54  then show "\X. X \ ?S" ..  wenzelm@13515  55  have "\y \ ?S. y \ b 0"  wenzelm@13515  56  proof  wenzelm@13515  57  fix y assume y: "y \ ?S"  wenzelm@13515  58  then obtain u where u: "u \ F" and y: "y = a u" by blast  wenzelm@13515  59  from u and zero have "a u \ b 0" by (rule r)  wenzelm@13515  60  with y show "y \ b 0" by (simp only:)  wenzelm@10007  61  qed  wenzelm@13515  62  then show "\u. \y \ ?S. y \ u" ..  wenzelm@10007  63  qed  wenzelm@13515  64  then obtain xi where xi: "lub ?S xi" ..  wenzelm@13515  65  {  wenzelm@13515  66  fix y assume "y \ F"  wenzelm@13515  67  then have "a y \ ?S" by blast  wenzelm@13515  68  with xi have "a y \ xi" by (rule lub.upper)  wenzelm@60458  69  }  wenzelm@60458  70  moreover {  wenzelm@13515  71  fix y assume y: "y \ F"  wenzelm@13515  72  from xi have "xi \ b y"  wenzelm@13515  73  proof (rule lub.least)  wenzelm@13515  74  fix au assume "au \ ?S"  wenzelm@13515  75  then obtain u where u: "u \ F" and au: "au = a u" by blast  wenzelm@13515  76  from u y have "a u \ b y" by (rule r)  wenzelm@13515  77  with au show "au \ b y" by (simp only:)  wenzelm@10007  78  qed  wenzelm@60458  79  }  wenzelm@60458  80  ultimately show "\xi. \y \ F. a y \ xi \ xi \ b y" by blast  wenzelm@10007  81 qed  wenzelm@7917  82 wenzelm@58744  83 text \  wenzelm@61486  84  \<^medskip>  wenzelm@61540  85  The function \h'\ is defined as a \h' x = h y + a \ \\ where  wenzelm@61540  86  \x = y + a \ \\ is a linear extension of \h\ to \H'\.  wenzelm@58744  87 \  wenzelm@7917  88 wenzelm@10687  89 lemma h'_lf:  wenzelm@13515  90  assumes h'_def: "h' \ \x. let (y, a) =  wenzelm@13515  91  SOME (y, a). x = y + a \ x0 \ y \ H in h y + a * xi"  krauss@47445  92  and H'_def: "H' \ H + lin x0"  wenzelm@13515  93  and HE: "H \ E"  ballarin@27611  94  assumes "linearform H h"  wenzelm@13515  95  assumes x0: "x0 \ H" "x0 \ E" "x0 \ 0"  ballarin@27611  96  assumes E: "vectorspace E"  wenzelm@13515  97  shows "linearform H' h'"  ballarin@27611  98 proof -  ballarin@29234  99  interpret linearform H h by fact  ballarin@29234  100  interpret vectorspace E by fact  wenzelm@27612  101  show ?thesis  wenzelm@27612  102  proof  wenzelm@58744  103  note E = \vectorspace E\  ballarin@27611  104  have H': "vectorspace H'"  ballarin@27611  105  proof (unfold H'_def)  wenzelm@58744  106  from \x0 \ E\  ballarin@27611  107  have "lin x0 \ E" ..  krauss@47445  108  with HE show "vectorspace (H + lin x0)" using E ..  ballarin@27611  109  qed  ballarin@27611  110  {  ballarin@27611  111  fix x1 x2 assume x1: "x1 \ H'" and x2: "x2 \ H'"  ballarin@27611  112  show "h' (x1 + x2) = h' x1 + h' x2"  ballarin@27611  113  proof -  wenzelm@32960  114  from H' x1 x2 have "x1 + x2 \ H'"  ballarin@27611  115  by (rule vectorspace.add_closed)  wenzelm@32960  116  with x1 x2 obtain y y1 y2 a a1 a2 where  ballarin@27611  117  x1x2: "x1 + x2 = y + a \ x0" and y: "y \ H"  wenzelm@13515  118  and x1_rep: "x1 = y1 + a1 \ x0" and y1: "y1 \ H"  wenzelm@13515  119  and x2_rep: "x2 = y2 + a2 \ x0" and y2: "y2 \ H"  wenzelm@27612  120  unfolding H'_def sum_def lin_def by blast  wenzelm@32960  121   wenzelm@32960  122  have ya: "y1 + y2 = y \ a1 + a2 = a" using E HE _ y x0  wenzelm@58999  123  proof (rule decomp_H') text_raw \\label{decomp-H-use}\  ballarin@27611  124  from HE y1 y2 show "y1 + y2 \ H"  ballarin@27611  125  by (rule subspace.add_closed)  ballarin@27611  126  from x0 and HE y y1 y2  ballarin@27611  127  have "x0 \ E" "y \ E" "y1 \ E" "y2 \ E" by auto  ballarin@27611  128  with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \ x0 = x1 + x2"  ballarin@27611  129  by (simp add: add_ac add_mult_distrib2)  ballarin@27611  130  also note x1x2  ballarin@27611  131  finally show "(y1 + y2) + (a1 + a2) \ x0 = y + a \ x0" .  wenzelm@32960  132  qed  wenzelm@32960  133   wenzelm@32960  134  from h'_def x1x2 E HE y x0  wenzelm@32960  135  have "h' (x1 + x2) = h y + a * xi"  ballarin@27611  136  by (rule h'_definite)  wenzelm@32960  137  also have "\ = h (y1 + y2) + (a1 + a2) * xi"  ballarin@27611  138  by (simp only: ya)  wenzelm@32960  139  also from y1 y2 have "h (y1 + y2) = h y1 + h y2"  ballarin@27611  140  by simp  wenzelm@32960  141  also have "\ + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)"  webertj@49962  142  by (simp add: distrib_right)  wenzelm@32960  143  also from h'_def x1_rep E HE y1 x0  wenzelm@32960  144  have "h y1 + a1 * xi = h' x1"  ballarin@27611  145  by (rule h'_definite [symmetric])  wenzelm@32960  146  also from h'_def x2_rep E HE y2 x0  wenzelm@32960  147  have "h y2 + a2 * xi = h' x2"  ballarin@27611  148  by (rule h'_definite [symmetric])  wenzelm@32960  149  finally show ?thesis .  wenzelm@10007  150  qed  ballarin@27611  151  next  ballarin@27611  152  fix x1 c assume x1: "x1 \ H'"  ballarin@27611  153  show "h' (c \ x1) = c * (h' x1)"  ballarin@27611  154  proof -  wenzelm@32960  155  from H' x1 have ax1: "c \ x1 \ H'"  ballarin@27611  156  by (rule vectorspace.mult_closed)  wenzelm@32960  157  with x1 obtain y a y1 a1 where  wenzelm@27612  158  cx1_rep: "c \ x1 = y + a \ x0" and y: "y \ H"  wenzelm@13515  159  and x1_rep: "x1 = y1 + a1 \ x0" and y1: "y1 \ H"  wenzelm@27612  160  unfolding H'_def sum_def lin_def by blast  wenzelm@32960  161   wenzelm@32960  162  have ya: "c \ y1 = y \ c * a1 = a" using E HE _ y x0  wenzelm@32960  163  proof (rule decomp_H')  ballarin@27611  164  from HE y1 show "c \ y1 \ H"  ballarin@27611  165  by (rule subspace.mult_closed)  ballarin@27611  166  from x0 and HE y y1  ballarin@27611  167  have "x0 \ E" "y \ E" "y1 \ E" by auto  ballarin@27611  168  with x1_rep have "c \ y1 + (c * a1) \ x0 = c \ x1"  ballarin@27611  169  by (simp add: mult_assoc add_mult_distrib1)  ballarin@27611  170  also note cx1_rep  ballarin@27611  171  finally show "c \ y1 + (c * a1) \ x0 = y + a \ x0" .  wenzelm@32960  172  qed  wenzelm@32960  173   wenzelm@32960  174  from h'_def cx1_rep E HE y x0 have "h' (c \ x1) = h y + a * xi"  ballarin@27611  175  by (rule h'_definite)  wenzelm@32960  176  also have "\ = h (c \ y1) + (c * a1) * xi"  ballarin@27611  177  by (simp only: ya)  wenzelm@32960  178  also from y1 have "h (c \ y1) = c * h y1"  ballarin@27611  179  by simp  wenzelm@32960  180  also have "\ + (c * a1) * xi = c * (h y1 + a1 * xi)"  webertj@49962  181  by (simp only: distrib_left)  wenzelm@32960  182  also from h'_def x1_rep E HE y1 x0 have "h y1 + a1 * xi = h' x1"  ballarin@27611  183  by (rule h'_definite [symmetric])  wenzelm@32960  184  finally show ?thesis .  wenzelm@10007  185  qed  ballarin@27611  186  }  ballarin@27611  187  qed  wenzelm@10007  188 qed  wenzelm@7917  189 wenzelm@61486  190 text \  wenzelm@61486  191  \<^medskip>  wenzelm@61540  192  The linear extension \h'\ of \h\ is bounded by the seminorm \p\.  wenzelm@61540  193 \  wenzelm@7917  194 bauerg@9374  195 lemma h'_norm_pres:  wenzelm@13515  196  assumes h'_def: "h' \ \x. let (y, a) =  wenzelm@13515  197  SOME (y, a). x = y + a \ x0 \ y \ H in h y + a * xi"  krauss@47445  198  and H'_def: "H' \ H + lin x0"  wenzelm@13515  199  and x0: "x0 \ H" "x0 \ E" "x0 \ 0"  ballarin@27611  200  assumes E: "vectorspace E" and HE: "subspace H E"  ballarin@27611  201  and "seminorm E p" and "linearform H h"  wenzelm@13515  202  assumes a: "\y \ H. h y \ p y"  wenzelm@13515  203  and a': "\y \ H. - p (y + x0) - h y \ xi \ xi \ p (y + x0) - h y"  wenzelm@13515  204  shows "\x \ H'. h' x \ p x"  ballarin@27611  205 proof -  ballarin@29234  206  interpret vectorspace E by fact  ballarin@29234  207  interpret subspace H E by fact  ballarin@29234  208  interpret seminorm E p by fact  ballarin@29234  209  interpret linearform H h by fact  wenzelm@27612  210  show ?thesis  wenzelm@27612  211  proof  ballarin@27611  212  fix x assume x': "x \ H'"  ballarin@27611  213  show "h' x \ p x"  ballarin@27611  214  proof -  ballarin@27611  215  from a' have a1: "\ya \ H. - p (ya + x0) - h ya \ xi"  wenzelm@32960  216  and a2: "\ya \ H. xi \ p (ya + x0) - h ya" by auto  ballarin@27611  217  from x' obtain y a where  wenzelm@27612  218  x_rep: "x = y + a \ x0" and y: "y \ H"  wenzelm@32960  219  unfolding H'_def sum_def lin_def by blast  ballarin@27611  220  from y have y': "y \ E" ..  ballarin@27611  221  from y have ay: "inverse a \ y \ H" by simp  ballarin@27611  222   ballarin@27611  223  from h'_def x_rep E HE y x0 have "h' x = h y + a * xi"  wenzelm@32960  224  by (rule h'_definite)  ballarin@27611  225  also have "\ \ p (y + a \ x0)"  ballarin@27611  226  proof (rule linorder_cases)  wenzelm@32960  227  assume z: "a = 0"  wenzelm@32960  228  then have "h y + a * xi = h y" by simp  wenzelm@32960  229  also from a y have "\ \ p y" ..  wenzelm@32960  230  also from x0 y' z have "p y = p (y + a \ x0)" by simp  wenzelm@32960  231  finally show ?thesis .  ballarin@27611  232  next  wenzelm@61539  233  txt \In the case \a < 0\, we use \a\<^sub>1\  wenzelm@61539  234  with \ya\ taken as \y / a\:\  wenzelm@32960  235  assume lz: "a < 0" then have nz: "a \ 0" by simp  wenzelm@32960  236  from a1 ay  wenzelm@32960  237  have "- p (inverse a \ y + x0) - h (inverse a \ y) \ xi" ..  wenzelm@32960  238  with lz have "a * xi \  wenzelm@13515  239  a * (- p (inverse a \ y + x0) - h (inverse a \ y))"  ballarin@27611  240  by (simp add: mult_left_mono_neg order_less_imp_le)  wenzelm@32960  241   wenzelm@32960  242  also have "\ =  wenzelm@13515  243  - a * (p (inverse a \ y + x0)) - a * (h (inverse a \ y))"  wenzelm@32960  244  by (simp add: right_diff_distrib)  wenzelm@32960  245  also from lz x0 y' have "- a * (p (inverse a \ y + x0)) =  wenzelm@13515  246  p (a \ (inverse a \ y + x0))"  ballarin@27611  247  by (simp add: abs_homogenous)  wenzelm@32960  248  also from nz x0 y' have "\ = p (y + a \ x0)"  ballarin@27611  249  by (simp add: add_mult_distrib1 mult_assoc [symmetric])  wenzelm@32960  250  also from nz y have "a * (h (inverse a \ y)) = h y"  ballarin@27611  251  by simp  wenzelm@32960  252  finally have "a * xi \ p (y + a \ x0) - h y" .  wenzelm@32960  253  then show ?thesis by simp  ballarin@27611  254  next  wenzelm@61539  255  txt \In the case \a > 0\, we use \a\<^sub>2\  wenzelm@61539  256  with \ya\ taken as \y / a\:\  wenzelm@32960  257  assume gz: "0 < a" then have nz: "a \ 0" by simp  wenzelm@32960  258  from a2 ay  wenzelm@32960  259  have "xi \ p (inverse a \ y + x0) - h (inverse a \ y)" ..  wenzelm@32960  260  with gz have "a * xi \  wenzelm@13515  261  a * (p (inverse a \ y + x0) - h (inverse a \ y))"  ballarin@27611  262  by simp  wenzelm@32960  263  also have "\ = a * p (inverse a \ y + x0) - a * h (inverse a \ y)"  wenzelm@32960  264  by (simp add: right_diff_distrib)  wenzelm@32960  265  also from gz x0 y'  wenzelm@32960  266  have "a * p (inverse a \ y + x0) = p (a \ (inverse a \ y + x0))"  ballarin@27611  267  by (simp add: abs_homogenous)  wenzelm@32960  268  also from nz x0 y' have "\ = p (y + a \ x0)"  ballarin@27611  269  by (simp add: add_mult_distrib1 mult_assoc [symmetric])  wenzelm@32960  270  also from nz y have "a * h (inverse a \ y) = h y"  ballarin@27611  271  by simp  wenzelm@32960  272  finally have "a * xi \ p (y + a \ x0) - h y" .  wenzelm@32960  273  then show ?thesis by simp  ballarin@27611  274  qed  ballarin@27611  275  also from x_rep have "\ = p x" by (simp only:)  ballarin@27611  276  finally show ?thesis .  wenzelm@10007  277  qed  wenzelm@10007  278  qed  wenzelm@13515  279 qed  wenzelm@7917  280 wenzelm@10007  281 end