7917
|
1 |
(* Title: HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
|
|
2 |
Author: Gertrud Bauer, TU Munich
|
|
3 |
*)
|
|
4 |
|
10007
|
5 |
header {* Extending non-maximal functions *}
|
7917
|
6 |
|
27612
|
7 |
theory HahnBanachExtLemmas
|
|
8 |
imports FunctionNorm
|
|
9 |
begin
|
7917
|
10 |
|
10687
|
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
|
13515
|
21 |
unique. @{text h'} is defined on @{text H'} by @{text "h' x = h y +
|
|
22 |
a \<cdot> \<xi>"} for a certain @{text \<xi>}.
|
7917
|
23 |
|
10687
|
24 |
Subsequently we show some properties of this extension @{text h'} of
|
|
25 |
@{text h}.
|
7917
|
26 |
|
13515
|
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
|
10687
|
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 |
*}
|
7917
|
42 |
|
10687
|
43 |
lemma ex_xi:
|
27611
|
44 |
assumes "vectorspace F"
|
13515
|
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"
|
10007
|
47 |
proof -
|
29234
|
48 |
interpret vectorspace F by fact
|
7917
|
49 |
txt {* From the completeness of the reals follows:
|
13515
|
50 |
The set @{text "S = {a u. u \<in> F}"} has a supremum, if it is
|
|
51 |
non-empty and has an upper bound. *}
|
7917
|
52 |
|
13515
|
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:)
|
10007
|
64 |
qed
|
13515
|
65 |
then show "\<exists>u. \<forall>y \<in> ?S. y \<le> u" ..
|
10007
|
66 |
qed
|
13515
|
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:)
|
10007
|
80 |
qed
|
13515
|
81 |
} ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
|
10007
|
82 |
qed
|
7917
|
83 |
|
10687
|
84 |
text {*
|
13515
|
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 |
*}
|
7917
|
89 |
|
10687
|
90 |
lemma h'_lf:
|
13515
|
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"
|
10687
|
93 |
and H'_def: "H' \<equiv> H + lin x0"
|
13515
|
94 |
and HE: "H \<unlhd> E"
|
27611
|
95 |
assumes "linearform H h"
|
13515
|
96 |
assumes x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"
|
27611
|
97 |
assumes E: "vectorspace E"
|
13515
|
98 |
shows "linearform H' h'"
|
27611
|
99 |
proof -
|
29234
|
100 |
interpret linearform H h by fact
|
|
101 |
interpret vectorspace E by fact
|
27612
|
102 |
show ?thesis
|
|
103 |
proof
|
27611
|
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"
|
13515
|
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"
|
27612
|
121 |
unfolding H'_def sum_def lin_def by blast
|
27611
|
122 |
|
|
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"
|
|
130 |
by (simp add: add_ac add_mult_distrib2)
|
|
131 |
also note x1x2
|
|
132 |
finally show "(y1 + y2) + (a1 + a2) \<cdot> x0 = y + a \<cdot> x0" .
|
|
133 |
qed
|
|
134 |
|
|
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: left_distrib)
|
|
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 .
|
10007
|
151 |
qed
|
27611
|
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
|
27612
|
159 |
cx1_rep: "c \<cdot> x1 = y + a \<cdot> x0" and y: "y \<in> H"
|
13515
|
160 |
and x1_rep: "x1 = y1 + a1 \<cdot> x0" and y1: "y1 \<in> H"
|
27612
|
161 |
unfolding H'_def sum_def lin_def by blast
|
27611
|
162 |
|
|
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"
|
|
170 |
by (simp add: mult_assoc add_mult_distrib1)
|
|
171 |
also note cx1_rep
|
|
172 |
finally show "c \<cdot> y1 + (c * a1) \<cdot> x0 = y + a \<cdot> x0" .
|
|
173 |
qed
|
|
174 |
|
|
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: right_distrib)
|
|
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 .
|
10007
|
186 |
qed
|
27611
|
187 |
}
|
|
188 |
qed
|
10007
|
189 |
qed
|
7917
|
190 |
|
10687
|
191 |
text {* \medskip The linear extension @{text h'} of @{text h}
|
13515
|
192 |
is bounded by the seminorm @{text p}. *}
|
7917
|
193 |
|
9374
|
194 |
lemma h'_norm_pres:
|
13515
|
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"
|
10687
|
197 |
and H'_def: "H' \<equiv> H + lin x0"
|
13515
|
198 |
and x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"
|
27611
|
199 |
assumes E: "vectorspace E" and HE: "subspace H E"
|
|
200 |
and "seminorm E p" and "linearform H h"
|
13515
|
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"
|
27611
|
204 |
proof -
|
29234
|
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
|
27612
|
209 |
show ?thesis
|
|
210 |
proof
|
27611
|
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
|
27612
|
217 |
x_rep: "x = y + a \<cdot> x0" and y: "y \<in> H"
|
|
218 |
unfolding H'_def sum_def lin_def by blast
|
27611
|
219 |
from y have y': "y \<in> E" ..
|
|
220 |
from y have ay: "inverse a \<cdot> y \<in> H" by simp
|
|
221 |
|
|
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"}: *}
|
27612
|
234 |
assume lz: "a < 0" then have nz: "a \<noteq> 0" by simp
|
27611
|
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>
|
13515
|
238 |
a * (- p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
|
27611
|
239 |
by (simp add: mult_left_mono_neg order_less_imp_le)
|
|
240 |
|
|
241 |
also have "\<dots> =
|
13515
|
242 |
- a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
|
27611
|
243 |
by (simp add: right_diff_distrib)
|
|
244 |
also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
|
13515
|
245 |
p (a \<cdot> (inverse a \<cdot> y + x0))"
|
27611
|
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"}: *}
|
27612
|
256 |
assume gz: "0 < a" then have nz: "a \<noteq> 0" by simp
|
27611
|
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>
|
13515
|
260 |
a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
|
27611
|
261 |
by simp
|
27612
|
262 |
also have "\<dots> = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
|
27611
|
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 .
|
10007
|
276 |
qed
|
|
277 |
qed
|
13515
|
278 |
qed
|
7917
|
279 |
|
10007
|
280 |
end
|