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