author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44887  7ca82df6e951 
child 47445  69e96e5500df 
permissions  rwrr 
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
30729
diff
changeset

1 
(* Title: HOL/Hahn_Banach/Subspace.thy 
7566  2 
Author: Gertrud Bauer, TU Munich 
3 
*) 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

4 

9035  5 
header {* Subspaces *} 
7808  6 

27612  7 
theory Subspace 
44190  8 
imports Vector_Space "~~/src/HOL/Library/Set_Algebras" 
27612  9 
begin 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

10 

9035  11 
subsection {* Definition *} 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

12 

10687  13 
text {* 
14 
A nonempty subset @{text U} of a vector space @{text V} is a 

15 
\emph{subspace} of @{text V}, iff @{text U} is closed under addition 

16 
and scalar multiplication. 

17 
*} 

7917  18 

29234  19 
locale subspace = 
20 
fixes U :: "'a\<Colon>{minus, plus, zero, uminus} set" and V 

13515  21 
assumes non_empty [iff, intro]: "U \<noteq> {}" 
22 
and subset [iff]: "U \<subseteq> V" 

23 
and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U" 

24 
and mult_closed [iff]: "x \<in> U \<Longrightarrow> a \<cdot> x \<in> U" 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

25 

21210  26 
notation (symbols) 
19736  27 
subspace (infix "\<unlhd>" 50) 
14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset

28 

19736  29 
declare vectorspace.intro [intro?] subspace.intro [intro?] 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

30 

13515  31 
lemma subspace_subset [elim]: "U \<unlhd> V \<Longrightarrow> U \<subseteq> V" 
32 
by (rule subspace.subset) 

7566  33 

13515  34 
lemma (in subspace) subsetD [iff]: "x \<in> U \<Longrightarrow> x \<in> V" 
35 
using subset by blast 

7566  36 

13515  37 
lemma subspaceD [elim]: "U \<unlhd> V \<Longrightarrow> x \<in> U \<Longrightarrow> x \<in> V" 
38 
by (rule subspace.subsetD) 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

39 

13515  40 
lemma rev_subspaceD [elim?]: "x \<in> U \<Longrightarrow> U \<unlhd> V \<Longrightarrow> x \<in> V" 
41 
by (rule subspace.subsetD) 

42 

13547  43 
lemma (in subspace) diff_closed [iff]: 
27611  44 
assumes "vectorspace V" 
27612  45 
assumes x: "x \<in> U" and y: "y \<in> U" 
46 
shows "x  y \<in> U" 

27611  47 
proof  
29234  48 
interpret vectorspace V by fact 
27612  49 
from x y show ?thesis by (simp add: diff_eq1 negate_eq1) 
27611  50 
qed 
7917  51 

13515  52 
text {* 
53 
\medskip Similar as for linear spaces, the existence of the zero 

54 
element in every subspace follows from the nonemptiness of the 

55 
carrier set and by vector space laws. 

56 
*} 

57 

13547  58 
lemma (in subspace) zero [intro]: 
27611  59 
assumes "vectorspace V" 
13547  60 
shows "0 \<in> U" 
10687  61 
proof  
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29252
diff
changeset

62 
interpret V: vectorspace V by fact 
29234  63 
have "U \<noteq> {}" by (rule non_empty) 
13515  64 
then obtain x where x: "x \<in> U" by blast 
27612  65 
then have "x \<in> V" .. then have "0 = x  x" by simp 
29234  66 
also from `vectorspace V` x x have "\<dots> \<in> U" by (rule diff_closed) 
13515  67 
finally show ?thesis . 
9035  68 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

69 

13547  70 
lemma (in subspace) neg_closed [iff]: 
27611  71 
assumes "vectorspace V" 
27612  72 
assumes x: "x \<in> U" 
73 
shows " x \<in> U" 

27611  74 
proof  
29234  75 
interpret vectorspace V by fact 
27612  76 
from x show ?thesis by (simp add: negate_eq1) 
27611  77 
qed 
13515  78 

10687  79 
text {* \medskip Further derived laws: every subspace is a vector space. *} 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

80 

13547  81 
lemma (in subspace) vectorspace [iff]: 
27611  82 
assumes "vectorspace V" 
13547  83 
shows "vectorspace U" 
27611  84 
proof  
29234  85 
interpret vectorspace V by fact 
27612  86 
show ?thesis 
87 
proof 

27611  88 
show "U \<noteq> {}" .. 
89 
fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U" 

90 
fix a b :: real 

91 
from x y show "x + y \<in> U" by simp 

92 
from x show "a \<cdot> x \<in> U" by simp 

93 
from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac) 

94 
from x y show "x + y = y + x" by (simp add: add_ac) 

95 
from x show "x  x = 0" by simp 

96 
from x show "0 + x = x" by simp 

97 
from x y show "a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y" by (simp add: distrib) 

98 
from x show "(a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" by (simp add: distrib) 

99 
from x show "(a * b) \<cdot> x = a \<cdot> b \<cdot> x" by (simp add: mult_assoc) 

100 
from x show "1 \<cdot> x = x" by simp 

101 
from x show " x =  1 \<cdot> x" by (simp add: negate_eq1) 

102 
from x y show "x  y = x +  y" by (simp add: diff_eq1) 

103 
qed 

9035  104 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

105 

13515  106 

9035  107 
text {* The subspace relation is reflexive. *} 
7917  108 

13515  109 
lemma (in vectorspace) subspace_refl [intro]: "V \<unlhd> V" 
10687  110 
proof 
13515  111 
show "V \<noteq> {}" .. 
10687  112 
show "V \<subseteq> V" .. 
44887  113 
next 
13515  114 
fix x y assume x: "x \<in> V" and y: "y \<in> V" 
115 
fix a :: real 

116 
from x y show "x + y \<in> V" by simp 

117 
from x show "a \<cdot> x \<in> V" by simp 

9035  118 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

119 

9035  120 
text {* The subspace relation is transitive. *} 
7917  121 

13515  122 
lemma (in vectorspace) subspace_trans [trans]: 
123 
"U \<unlhd> V \<Longrightarrow> V \<unlhd> W \<Longrightarrow> U \<unlhd> W" 

10687  124 
proof 
13515  125 
assume uv: "U \<unlhd> V" and vw: "V \<unlhd> W" 
126 
from uv show "U \<noteq> {}" by (rule subspace.non_empty) 

127 
show "U \<subseteq> W" 

128 
proof  

129 
from uv have "U \<subseteq> V" by (rule subspace.subset) 

130 
also from vw have "V \<subseteq> W" by (rule subspace.subset) 

131 
finally show ?thesis . 

9035  132 
qed 
13515  133 
fix x y assume x: "x \<in> U" and y: "y \<in> U" 
134 
from uv and x y show "x + y \<in> U" by (rule subspace.add_closed) 

135 
from uv and x show "\<And>a. a \<cdot> x \<in> U" by (rule subspace.mult_closed) 

9035  136 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

137 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

138 

9035  139 
subsection {* Linear closure *} 
7808  140 

10687  141 
text {* 
142 
The \emph{linear closure} of a vector @{text x} is the set of all 

143 
scalar multiples of @{text x}. 

144 
*} 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

145 

44887  146 
definition lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set" 
147 
where "lin x = {a \<cdot> x  a. True}" 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

148 

13515  149 
lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x" 
27612  150 
unfolding lin_def by blast 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

151 

13515  152 
lemma linI' [iff]: "a \<cdot> x \<in> lin x" 
27612  153 
unfolding lin_def by blast 
13515  154 

27612  155 
lemma linE [elim]: "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C" 
156 
unfolding lin_def by blast 

13515  157 

7656  158 

9035  159 
text {* Every vector is contained in its linear closure. *} 
7917  160 

13515  161 
lemma (in vectorspace) x_lin_x [iff]: "x \<in> V \<Longrightarrow> x \<in> lin x" 
162 
proof  

163 
assume "x \<in> V" 

27612  164 
then have "x = 1 \<cdot> x" by simp 
13515  165 
also have "\<dots> \<in> lin x" .. 
166 
finally show ?thesis . 

167 
qed 

168 

169 
lemma (in vectorspace) "0_lin_x" [iff]: "x \<in> V \<Longrightarrow> 0 \<in> lin x" 

170 
proof 

171 
assume "x \<in> V" 

27612  172 
then show "0 = 0 \<cdot> x" by simp 
13515  173 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

174 

9035  175 
text {* Any linear closure is a subspace. *} 
7917  176 

13515  177 
lemma (in vectorspace) lin_subspace [intro]: 
44887  178 
assumes x: "x \<in> V" 
179 
shows "lin x \<unlhd> V" 

9035  180 
proof 
44887  181 
from x show "lin x \<noteq> {}" by auto 
182 
next 

10687  183 
show "lin x \<subseteq> V" 
13515  184 
proof 
185 
fix x' assume "x' \<in> lin x" 

186 
then obtain a where "x' = a \<cdot> x" .. 

187 
with x show "x' \<in> V" by simp 

9035  188 
qed 
44887  189 
next 
13515  190 
fix x' x'' assume x': "x' \<in> lin x" and x'': "x'' \<in> lin x" 
191 
show "x' + x'' \<in> lin x" 

192 
proof  

193 
from x' obtain a' where "x' = a' \<cdot> x" .. 

194 
moreover from x'' obtain a'' where "x'' = a'' \<cdot> x" .. 

195 
ultimately have "x' + x'' = (a' + a'') \<cdot> x" 

196 
using x by (simp add: distrib) 

197 
also have "\<dots> \<in> lin x" .. 

198 
finally show ?thesis . 

9035  199 
qed 
13515  200 
fix a :: real 
201 
show "a \<cdot> x' \<in> lin x" 

202 
proof  

203 
from x' obtain a' where "x' = a' \<cdot> x" .. 

204 
with x have "a \<cdot> x' = (a * a') \<cdot> x" by (simp add: mult_assoc) 

205 
also have "\<dots> \<in> lin x" .. 

206 
finally show ?thesis . 

10687  207 
qed 
9035  208 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

209 

13515  210 

9035  211 
text {* Any linear closure is a vector space. *} 
7917  212 

13515  213 
lemma (in vectorspace) lin_vectorspace [intro]: 
23378  214 
assumes "x \<in> V" 
215 
shows "vectorspace (lin x)" 

216 
proof  

217 
from `x \<in> V` have "subspace (lin x) V" 

218 
by (rule lin_subspace) 

26199  219 
from this and vectorspace_axioms show ?thesis 
23378  220 
by (rule subspace.vectorspace) 
221 
qed 

7808  222 

223 

9035  224 
subsection {* Sum of two vectorspaces *} 
7808  225 

10687  226 
text {* 
227 
The \emph{sum} of two vectorspaces @{text U} and @{text V} is the 

228 
set of all sums of elements from @{text U} and @{text V}. 

229 
*} 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

230 

44190  231 
lemma sum_def: "U \<oplus> V = {u + v  u v. u \<in> U \<and> v \<in> V}" 
232 
unfolding set_plus_def by auto 

7917  233 

13515  234 
lemma sumE [elim]: 
44190  235 
"x \<in> U \<oplus> V \<Longrightarrow> (\<And>u v. x = u + v \<Longrightarrow> u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> C) \<Longrightarrow> C" 
27612  236 
unfolding sum_def by blast 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

237 

13515  238 
lemma sumI [intro]: 
44190  239 
"u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U \<oplus> V" 
27612  240 
unfolding sum_def by blast 
7566  241 

13515  242 
lemma sumI' [intro]: 
44190  243 
"u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U \<oplus> V" 
27612  244 
unfolding sum_def by blast 
7917  245 

44190  246 
text {* @{text U} is a subspace of @{text "U \<oplus> V"}. *} 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

247 

13515  248 
lemma subspace_sum1 [iff]: 
27611  249 
assumes "vectorspace U" "vectorspace V" 
44190  250 
shows "U \<unlhd> U \<oplus> V" 
27611  251 
proof  
29234  252 
interpret vectorspace U by fact 
253 
interpret vectorspace V by fact 

27612  254 
show ?thesis 
255 
proof 

27611  256 
show "U \<noteq> {}" .. 
44190  257 
show "U \<subseteq> U \<oplus> V" 
27611  258 
proof 
259 
fix x assume x: "x \<in> U" 

260 
moreover have "0 \<in> V" .. 

44190  261 
ultimately have "x + 0 \<in> U \<oplus> V" .. 
262 
with x show "x \<in> U \<oplus> V" by simp 

27611  263 
qed 
264 
fix x y assume x: "x \<in> U" and "y \<in> U" 

27612  265 
then show "x + y \<in> U" by simp 
27611  266 
from x show "\<And>a. a \<cdot> x \<in> U" by simp 
9035  267 
qed 
268 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

269 

13515  270 
text {* The sum of two subspaces is again a subspace. *} 
7917  271 

13515  272 
lemma sum_subspace [intro?]: 
27611  273 
assumes "subspace U E" "vectorspace E" "subspace V E" 
44190  274 
shows "U \<oplus> V \<unlhd> E" 
27611  275 
proof  
29234  276 
interpret subspace U E by fact 
277 
interpret vectorspace E by fact 

278 
interpret subspace V E by fact 

27612  279 
show ?thesis 
280 
proof 

44190  281 
have "0 \<in> U \<oplus> V" 
27611  282 
proof 
283 
show "0 \<in> U" using `vectorspace E` .. 

284 
show "0 \<in> V" using `vectorspace E` .. 

285 
show "(0::'a) = 0 + 0" by simp 

286 
qed 

44190  287 
then show "U \<oplus> V \<noteq> {}" by blast 
288 
show "U \<oplus> V \<subseteq> E" 

27611  289 
proof 
44190  290 
fix x assume "x \<in> U \<oplus> V" 
27611  291 
then obtain u v where "x = u + v" and 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

292 
"u \<in> U" and "v \<in> V" .. 
27611  293 
then show "x \<in> E" by simp 
294 
qed 

44887  295 
next 
44190  296 
fix x y assume x: "x \<in> U \<oplus> V" and y: "y \<in> U \<oplus> V" 
297 
show "x + y \<in> U \<oplus> V" 

27611  298 
proof  
299 
from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" .. 

300 
moreover 

301 
from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" .. 

302 
ultimately 

303 
have "ux + uy \<in> U" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

304 
and "vx + vy \<in> V" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

305 
and "x + y = (ux + uy) + (vx + vy)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

306 
using x y by (simp_all add: add_ac) 
27612  307 
then show ?thesis .. 
27611  308 
qed 
44190  309 
fix a show "a \<cdot> x \<in> U \<oplus> V" 
27611  310 
proof  
311 
from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" .. 

27612  312 
then have "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

313 
and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib) 
27612  314 
then show ?thesis .. 
27611  315 
qed 
9035  316 
qed 
317 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

318 

9035  319 
text{* The sum of two subspaces is a vectorspace. *} 
7917  320 

13515  321 
lemma sum_vs [intro?]: 
44190  322 
"U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U \<oplus> V)" 
13547  323 
by (rule subspace.vectorspace) (rule sum_subspace) 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

324 

7808  325 

9035  326 
subsection {* Direct sums *} 
7808  327 

10687  328 
text {* 
329 
The sum of @{text U} and @{text V} is called \emph{direct}, iff the 

330 
zero element is the only common element of @{text U} and @{text 

331 
V}. For every element @{text x} of the direct sum of @{text U} and 

332 
@{text V} the decomposition in @{text "x = u + v"} with 

333 
@{text "u \<in> U"} and @{text "v \<in> V"} is unique. 

334 
*} 

7808  335 

10687  336 
lemma decomp: 
27611  337 
assumes "vectorspace E" "subspace U E" "subspace V E" 
13515  338 
assumes direct: "U \<inter> V = {0}" 
339 
and u1: "u1 \<in> U" and u2: "u2 \<in> U" 

340 
and v1: "v1 \<in> V" and v2: "v2 \<in> V" 

341 
and sum: "u1 + v1 = u2 + v2" 

342 
shows "u1 = u2 \<and> v1 = v2" 

27611  343 
proof  
29234  344 
interpret vectorspace E by fact 
345 
interpret subspace U E by fact 

346 
interpret subspace V E by fact 

27612  347 
show ?thesis 
348 
proof 

27611  349 
have U: "vectorspace U" (* FIXME: use interpret *) 
350 
using `subspace U E` `vectorspace E` by (rule subspace.vectorspace) 

351 
have V: "vectorspace V" 

352 
using `subspace V E` `vectorspace E` by (rule subspace.vectorspace) 

353 
from u1 u2 v1 v2 and sum have eq: "u1  u2 = v2  v1" 

354 
by (simp add: add_diff_swap) 

355 
from u1 u2 have u: "u1  u2 \<in> U" 

356 
by (rule vectorspace.diff_closed [OF U]) 

357 
with eq have v': "v2  v1 \<in> U" by (simp only:) 

358 
from v2 v1 have v: "v2  v1 \<in> V" 

359 
by (rule vectorspace.diff_closed [OF V]) 

360 
with eq have u': " u1  u2 \<in> V" by (simp only:) 

361 

362 
show "u1 = u2" 

363 
proof (rule add_minus_eq) 

364 
from u1 show "u1 \<in> E" .. 

365 
from u2 show "u2 \<in> E" .. 

366 
from u u' and direct show "u1  u2 = 0" by blast 

367 
qed 

368 
show "v1 = v2" 

369 
proof (rule add_minus_eq [symmetric]) 

370 
from v1 show "v1 \<in> E" .. 

371 
from v2 show "v2 \<in> E" .. 

372 
from v v' and direct show "v2  v1 = 0" by blast 

373 
qed 

9035  374 
qed 
375 
qed 

7656  376 

10687  377 
text {* 
378 
An application of the previous lemma will be used in the proof of 

379 
the HahnBanach Theorem (see page \pageref{decompHuse}): for any 

380 
element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a 

381 
vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"} 

382 
the components @{text "y \<in> H"} and @{text a} are uniquely 

383 
determined. 

384 
*} 

7917  385 

10687  386 
lemma decomp_H': 
27611  387 
assumes "vectorspace E" "subspace H E" 
13515  388 
assumes y1: "y1 \<in> H" and y2: "y2 \<in> H" 
389 
and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" 

390 
and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'" 

391 
shows "y1 = y2 \<and> a1 = a2" 

27611  392 
proof  
29234  393 
interpret vectorspace E by fact 
394 
interpret subspace H E by fact 

27612  395 
show ?thesis 
396 
proof 

27611  397 
have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'" 
398 
proof (rule decomp) 

399 
show "a1 \<cdot> x' \<in> lin x'" .. 

400 
show "a2 \<cdot> x' \<in> lin x'" .. 

401 
show "H \<inter> lin x' = {0}" 

13515  402 
proof 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

403 
show "H \<inter> lin x' \<subseteq> {0}" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

404 
proof 
27611  405 
fix x assume x: "x \<in> H \<inter> lin x'" 
406 
then obtain a where xx': "x = a \<cdot> x'" 

407 
by blast 

408 
have "x = 0" 

409 
proof cases 

410 
assume "a = 0" 

411 
with xx' and x' show ?thesis by simp 

412 
next 

413 
assume a: "a \<noteq> 0" 

414 
from x have "x \<in> H" .. 

415 
with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp 

416 
with a and x' have "x' \<in> H" by (simp add: mult_assoc2) 

417 
with `x' \<notin> H` show ?thesis by contradiction 

418 
qed 

27612  419 
then show "x \<in> {0}" .. 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

420 
qed 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

421 
show "{0} \<subseteq> H \<inter> lin x'" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

422 
proof  
27611  423 
have "0 \<in> H" using `vectorspace E` .. 
424 
moreover have "0 \<in> lin x'" using `x' \<in> E` .. 

425 
ultimately show ?thesis by blast 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31795
diff
changeset

426 
qed 
9035  427 
qed 
27611  428 
show "lin x' \<unlhd> E" using `x' \<in> E` .. 
429 
qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq) 

27612  430 
then show "y1 = y2" .. 
27611  431 
from c have "a1 \<cdot> x' = a2 \<cdot> x'" .. 
432 
with x' show "a1 = a2" by (simp add: mult_right_cancel) 

433 
qed 

9035  434 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

435 

10687  436 
text {* 
437 
Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a 

438 
vectorspace @{text H} and the linear closure of @{text x'} the 

439 
components @{text "y \<in> H"} and @{text a} are unique, it follows from 

440 
@{text "y \<in> H"} that @{text "a = 0"}. 

441 
*} 

7917  442 

10687  443 
lemma decomp_H'_H: 
27611  444 
assumes "vectorspace E" "subspace H E" 
13515  445 
assumes t: "t \<in> H" 
446 
and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" 

447 
shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)" 

27611  448 
proof  
29234  449 
interpret vectorspace E by fact 
450 
interpret subspace H E by fact 

27612  451 
show ?thesis 
452 
proof (rule, simp_all only: split_paired_all split_conv) 

27611  453 
from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp 
454 
fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H" 

455 
have "y = t \<and> a = 0" 

456 
proof (rule decomp_H') 

457 
from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp 

458 
from ya show "y \<in> H" .. 

459 
qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+) 

460 
with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp 

461 
qed 

13515  462 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

463 

10687  464 
text {* 
465 
The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"} 

466 
are unique, so the function @{text h'} defined by 

467 
@{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite. 

468 
*} 

7917  469 

9374  470 
lemma h'_definite: 
27611  471 
fixes H 
13515  472 
assumes h'_def: 
44887  473 
"h' \<equiv> \<lambda>x. 
474 
let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H) 

475 
in (h y) + a * xi" 

13515  476 
and x: "x = y + a \<cdot> x'" 
27611  477 
assumes "vectorspace E" "subspace H E" 
13515  478 
assumes y: "y \<in> H" 
479 
and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" 

480 
shows "h' x = h y + a * xi" 

10687  481 
proof  
29234  482 
interpret vectorspace E by fact 
483 
interpret subspace H E by fact 

44190  484 
from x y x' have "x \<in> H \<oplus> lin x'" by auto 
13515  485 
have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p") 
18689
a50587cd8414
prefer ex1I over ex_ex1I in singlestep reasoning;
wenzelm
parents:
16417
diff
changeset

486 
proof (rule ex_ex1I) 
13515  487 
from x y show "\<exists>p. ?P p" by blast 
488 
fix p q assume p: "?P p" and q: "?P q" 

489 
show "p = q" 

9035  490 
proof  
13515  491 
from p have xp: "x = fst p + snd p \<cdot> x' \<and> fst p \<in> H" 
492 
by (cases p) simp 

493 
from q have xq: "x = fst q + snd q \<cdot> x' \<and> fst q \<in> H" 

494 
by (cases q) simp 

495 
have "fst p = fst q \<and> snd p = snd q" 

496 
proof (rule decomp_H') 

497 
from xp show "fst p \<in> H" .. 

498 
from xq show "fst q \<in> H" .. 

499 
from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'" 

500 
by simp 

23378  501 
qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+) 
27612  502 
then show ?thesis by (cases p, cases q) simp 
9035  503 
qed 
504 
qed 

27612  505 
then have eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" 
13515  506 
by (rule some1_equality) (simp add: x y) 
507 
with h'_def show "h' x = h y + a * xi" by (simp add: Let_def) 

9035  508 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

509 

10687  510 
end 