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