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