author | berghofe |
Fri, 01 Jul 2005 13:54:12 +0200 | |
changeset 16633 | 208ebc9311f2 |
parent 16417 | 9bc16273c2d4 |
child 23378 | 1d138d6bb461 |
permissions | -rw-r--r-- |
7917 | 1 |
(* Title: HOL/Real/HahnBanach/HahnBanachExtLemmas.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gertrud Bauer, TU Munich |
|
4 |
*) |
|
5 |
||
10007 | 6 |
header {* Extending non-maximal functions *} |
7917 | 7 |
|
16417 | 8 |
theory HahnBanachExtLemmas imports FunctionNorm begin |
7917 | 9 |
|
10687 | 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 |
|
13515 | 20 |
unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y + |
21 |
a \<cdot> \<xi>"} for a certain @{text \<xi>}. |
|
7917 | 22 |
|
10687 | 23 |
Subsequently we show some properties of this extension @{text h'} of |
24 |
@{text h}. |
|
7917 | 25 |
|
13515 | 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 |
|
10687 | 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 |
*} |
|
7917 | 41 |
|
10687 | 42 |
lemma ex_xi: |
13515 | 43 |
includes 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" |
|
10007 | 46 |
proof - |
7917 | 47 |
txt {* From the completeness of the reals follows: |
13515 | 48 |
The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is |
49 |
non-empty and has an upper bound. *} |
|
7917 | 50 |
|
13515 | 51 |
let ?S = "{a u | u. u \<in> F}" |
52 |
have "\<exists>xi. lub ?S xi" |
|
53 |
proof (rule real_complete) |
|
54 |
have "a 0 \<in> ?S" by blast |
|
55 |
then show "\<exists>X. X \<in> ?S" .. |
|
56 |
have "\<forall>y \<in> ?S. y \<le> b 0" |
|
57 |
proof |
|
58 |
fix y assume y: "y \<in> ?S" |
|
59 |
then obtain u where u: "u \<in> F" and y: "y = a u" by blast |
|
60 |
from u and zero have "a u \<le> b 0" by (rule r) |
|
61 |
with y show "y \<le> b 0" by (simp only:) |
|
10007 | 62 |
qed |
13515 | 63 |
then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" .. |
10007 | 64 |
qed |
13515 | 65 |
then obtain xi where xi: "lub ?S xi" .. |
66 |
{ |
|
67 |
fix y assume "y \<in> F" |
|
68 |
then have "a y \<in> ?S" by blast |
|
69 |
with xi have "a y \<le> xi" by (rule lub.upper) |
|
70 |
} moreover { |
|
71 |
fix y assume y: "y \<in> F" |
|
72 |
from xi have "xi \<le> b y" |
|
73 |
proof (rule lub.least) |
|
74 |
fix au assume "au \<in> ?S" |
|
75 |
then obtain u where u: "u \<in> F" and au: "au = a u" by blast |
|
76 |
from u y have "a u \<le> b y" by (rule r) |
|
77 |
with au show "au \<le> b y" by (simp only:) |
|
10007 | 78 |
qed |
13515 | 79 |
} ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast |
10007 | 80 |
qed |
7917 | 81 |
|
10687 | 82 |
text {* |
13515 | 83 |
\medskip The function @{text h'} is defined as a @{text "h' x = h y |
84 |
+ a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of |
|
85 |
@{text h} to @{text H'}. |
|
86 |
*} |
|
7917 | 87 |
|
10687 | 88 |
lemma h'_lf: |
13515 | 89 |
includes var H + var h + var E |
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" |
|
10687 | 92 |
and H'_def: "H' \<equiv> H + lin x0" |
13515 | 93 |
and HE: "H \<unlhd> E" |
94 |
includes linearform H h |
|
95 |
assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" |
|
96 |
includes vectorspace E |
|
97 |
shows "linearform H' h'" |
|
98 |
proof |
|
99 |
have H': "vectorspace H'" |
|
100 |
proof (unfold H'_def) |
|
101 |
have "x0 \<in> E" . |
|
102 |
then have "lin x0 \<unlhd> E" .. |
|
103 |
with HE show "vectorspace (H + lin x0)" .. |
|
10687 | 104 |
qed |
13515 | 105 |
{ |
10687 | 106 |
fix x1 x2 assume x1: "x1 \<in> H'" and x2: "x2 \<in> H'" |
13515 | 107 |
show "h' (x1 + x2) = h' x1 + h' x2" |
108 |
proof - |
|
109 |
from H' x1 x2 have "x1 + x2 \<in> H'" |
|
110 |
by (rule vectorspace.add_closed) |
|
111 |
with x1 x2 obtain y y1 y2 a a1 a2 where |
|
112 |
x1x2: "x1 + x2 = y + a \<cdot> x0" and y: "y \<in> H" |
|
113 |
and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H" |
|
114 |
and x2_rep: "x2 = y2 + a2 \<cdot> x0" and y2: "y2 \<in> H" |
|
115 |
by (unfold H'_def sum_def lin_def) blast |
|
7917 | 116 |
|
13515 | 117 |
have ya: "y1 + y2 = y \<and> a1 + a2 = a" using _ HE _ y x0 |
118 |
proof (rule decomp_H') txt_raw {* \label{decomp-H-use} *} |
|
119 |
from HE y1 y2 show "y1 + y2 \<in> H" |
|
120 |
by (rule subspace.add_closed) |
|
121 |
from x0 and HE y y1 y2 |
|
122 |
have "x0 \<in> E" "y \<in> E" "y1 \<in> E" "y2 \<in> E" by auto |
|
123 |
with x1_rep x2_rep have "(y1 + y2) + (a1 + a2) \<cdot> x0 = x1 + x2" |
|
124 |
by (simp add: add_ac add_mult_distrib2) |
|
125 |
also note x1x2 |
|
126 |
finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" . |
|
10007 | 127 |
qed |
7917 | 128 |
|
13515 | 129 |
from h'_def x1x2 _ HE y x0 |
10007 | 130 |
have "h' (x1 + x2) = h y + a * xi" |
10687 | 131 |
by (rule h'_definite) |
13515 | 132 |
also have "\<dots> = h (y1 + y2) + (a1 + a2) * xi" |
133 |
by (simp only: ya) |
|
134 |
also from y1 y2 have "h (y1 + y2) = h y1 + h y2" |
|
10007 | 135 |
by simp |
13515 | 136 |
also have "\<dots> + (a1 + a2) * xi = (h y1 + a1 * xi) + (h y2 + a2 * xi)" |
14334 | 137 |
by (simp add: left_distrib) |
13515 | 138 |
also from h'_def x1_rep _ HE y1 x0 |
139 |
have "h y1 + a1 * xi = h' x1" |
|
10007 | 140 |
by (rule h'_definite [symmetric]) |
13515 | 141 |
also from h'_def x2_rep _ HE y2 x0 |
142 |
have "h y2 + a2 * xi = h' x2" |
|
10007 | 143 |
by (rule h'_definite [symmetric]) |
144 |
finally show ?thesis . |
|
145 |
qed |
|
10687 | 146 |
next |
13515 | 147 |
fix x1 c assume x1: "x1 \<in> H'" |
148 |
show "h' (c \<cdot> x1) = c * (h' x1)" |
|
149 |
proof - |
|
150 |
from H' x1 have ax1: "c \<cdot> x1 \<in> H'" |
|
151 |
by (rule vectorspace.mult_closed) |
|
152 |
with x1 obtain y a y1 a1 where |
|
153 |
cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H" |
|
154 |
and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H" |
|
155 |
by (unfold H'_def sum_def lin_def) blast |
|
7917 | 156 |
|
13515 | 157 |
have ya: "c \<cdot> y1 = y \<and> c * a1 = a" using _ HE _ y x0 |
10687 | 158 |
proof (rule decomp_H') |
13515 | 159 |
from HE y1 show "c \<cdot> y1 \<in> H" |
160 |
by (rule subspace.mult_closed) |
|
161 |
from x0 and HE y y1 |
|
162 |
have "x0 \<in> E" "y \<in> E" "y1 \<in> E" by auto |
|
163 |
with x1_rep have "c \<cdot> y1 + (c * a1) \<cdot> x0 = c \<cdot> x1" |
|
164 |
by (simp add: mult_assoc add_mult_distrib1) |
|
165 |
also note cx1_rep |
|
166 |
finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" . |
|
10007 | 167 |
qed |
7917 | 168 |
|
13515 | 169 |
from h'_def cx1_rep _ HE y x0 have "h' (c \<cdot> x1) = h y + a * xi" |
10687 | 170 |
by (rule h'_definite) |
13515 | 171 |
also have "\<dots> = h (c \<cdot> y1) + (c * a1) * xi" |
172 |
by (simp only: ya) |
|
173 |
also from y1 have "h (c \<cdot> y1) = c * h y1" |
|
174 |
by simp |
|
175 |
also have "\<dots> + (c * a1) * xi = c * (h y1 + a1 * xi)" |
|
14334 | 176 |
by (simp only: right_distrib) |
13515 | 177 |
also from h'_def x1_rep _ HE y1 x0 have "h y1 + a1 * xi = h' x1" |
10007 | 178 |
by (rule h'_definite [symmetric]) |
179 |
finally show ?thesis . |
|
180 |
qed |
|
13515 | 181 |
} |
10007 | 182 |
qed |
7917 | 183 |
|
10687 | 184 |
text {* \medskip The linear extension @{text h'} of @{text h} |
13515 | 185 |
is bounded by the seminorm @{text p}. *} |
7917 | 186 |
|
9374 | 187 |
lemma h'_norm_pres: |
13515 | 188 |
includes var H + var h + var E |
189 |
assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) = |
|
190 |
SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi" |
|
10687 | 191 |
and H'_def: "H' \<equiv> H + lin x0" |
13515 | 192 |
and x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0" |
13547 | 193 |
includes vectorspace E + subspace H E + seminorm E p + linearform H h |
13515 | 194 |
assumes a: "\<forall>y \<in> H. h y \<le> p y" |
195 |
and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y" |
|
196 |
shows "\<forall>x \<in> H'. h' x \<le> p x" |
|
197 |
proof |
|
198 |
fix x assume x': "x \<in> H'" |
|
199 |
show "h' x \<le> p x" |
|
200 |
proof - |
|
201 |
from a' have a1: "\<forall>ya \<in> H. - p (ya + x0) - h ya \<le> xi" |
|
202 |
and a2: "\<forall>ya \<in> H. xi \<le> p (ya + x0) - h ya" by auto |
|
203 |
from x' obtain y a where |
|
204 |
x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H" |
|
205 |
by (unfold H'_def sum_def lin_def) blast |
|
206 |
from y have y': "y \<in> E" .. |
|
207 |
from y have ay: "inverse a \<cdot> y \<in> H" by simp |
|
208 |
||
209 |
from h'_def x_rep _ _ y x0 have "h' x = h y + a * xi" |
|
10007 | 210 |
by (rule h'_definite) |
13515 | 211 |
also have "\<dots> \<le> p (y + a \<cdot> x0)" |
10007 | 212 |
proof (rule linorder_cases) |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
213 |
assume z: "a = 0" |
13515 | 214 |
then have "h y + a * xi = h y" by simp |
215 |
also from a y have "\<dots> \<le> p y" .. |
|
216 |
also from x0 y' z have "p y = p (y + a \<cdot> x0)" by simp |
|
217 |
finally show ?thesis . |
|
10007 | 218 |
next |
13515 | 219 |
txt {* In the case @{text "a < 0"}, we use @{text "a\<^sub>1"} |
220 |
with @{text ya} taken as @{text "y / a"}: *} |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
221 |
assume lz: "a < 0" hence nz: "a \<noteq> 0" by simp |
13515 | 222 |
from a1 ay |
223 |
have "- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y) \<le> xi" .. |
|
224 |
with lz have "a * xi \<le> |
|
225 |
a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))" |
|
14710 | 226 |
by (simp add: mult_left_mono_neg order_less_imp_le) |
227 |
||
13515 | 228 |
also have "\<dots> = |
229 |
- a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))" |
|
14711 | 230 |
by (simp add: right_diff_distrib) |
13515 | 231 |
also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) = |
232 |
p (a \<cdot> (inverse a \<cdot> y + x0))" |
|
15229 | 233 |
by (simp add: abs_homogenous) |
13515 | 234 |
also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)" |
235 |
by (simp add: add_mult_distrib1 mult_assoc [symmetric]) |
|
236 |
also from nz y have "a * (h (inverse a \<cdot> y)) = h y" |
|
237 |
by simp |
|
10687 | 238 |
finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" . |
13515 | 239 |
then show ?thesis by simp |
240 |
next |
|
10687 | 241 |
txt {* In the case @{text "a > 0"}, we use @{text "a\<^sub>2"} |
242 |
with @{text ya} taken as @{text "y / a"}: *} |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11701
diff
changeset
|
243 |
assume gz: "0 < a" hence nz: "a \<noteq> 0" by simp |
13515 | 244 |
from a2 ay |
245 |
have "xi \<le> p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y)" .. |
|
246 |
with gz have "a * xi \<le> |
|
247 |
a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))" |
|
14710 | 248 |
by simp |
10606 | 249 |
also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)" |
14711 | 250 |
by (simp add: right_diff_distrib) |
13515 | 251 |
also from gz x0 y' |
10606 | 252 |
have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))" |
15229 | 253 |
by (simp add: abs_homogenous) |
13515 | 254 |
also from nz x0 y' have "\<dots> = p (y + a \<cdot> x0)" |
255 |
by (simp add: add_mult_distrib1 mult_assoc [symmetric]) |
|
256 |
also from nz y have "a * h (inverse a \<cdot> y) = h y" |
|
257 |
by simp |
|
10687 | 258 |
finally have "a * xi \<le> p (y + a \<cdot> x0) - h y" . |
13515 | 259 |
then show ?thesis by simp |
10007 | 260 |
qed |
13515 | 261 |
also from x_rep have "\<dots> = p x" by (simp only:) |
10007 | 262 |
finally show ?thesis . |
263 |
qed |
|
13515 | 264 |
qed |
7917 | 265 |
|
10007 | 266 |
end |