author  wenzelm 
Fri, 22 Oct 1999 20:14:31 +0200  
changeset 7917  5e5b9813cce7 
parent 7808  fd019ac3485f 
child 7927  b50446a33c16 
permissions  rwrr 
7566  1 
(* Title: HOL/Real/HahnBanach/Subspace.thy 
2 
ID: $Id$ 

3 
Author: Gertrud Bauer, TU Munich 

4 
*) 

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

5 

7808  6 

7 
header {* Subspaces *}; 

8 

7917  9 
theory Subspace = VectorSpace:; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

10 

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

11 

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

13 

7917  14 
text {* A nonempty subset $U$ of a vector space $V$ is a 
15 
\emph{subspace} of $V$, iff $U$ is closed under addition and 

16 
scalar multiplication. *}; 

17 

18 
constdefs 

19 
is_subspace :: "['a::{minus, plus} set, 'a set] => bool" 

20 
"is_subspace U V == U ~= {} & U <= V 

21 
& (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)"; 

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

22 

7566  23 
lemma subspaceI [intro]: 
7917  24 
"[ <0>:U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
25 
ALL x:U. ALL a. a <*> x : U ] 

7808  26 
==> is_subspace U V"; 
7917  27 
proof (unfold is_subspace_def, intro conjI); 
28 
assume "<0>:U"; thus "U ~= {}"; by fast; 

29 
qed (simp+); 

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

30 

7917  31 
lemma subspace_not_empty [intro!!]: "is_subspace U V ==> U ~= {}"; 
32 
by (unfold is_subspace_def) simp; 

7566  33 

34 
lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V"; 

7656  35 
by (unfold is_subspace_def) simp; 
7566  36 

7808  37 
lemma subspace_subsetD [simp, intro!!]: 
38 
"[ is_subspace U V; x:U ]==> x:V"; 

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

39 
by (unfold is_subspace_def) force; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

40 

7808  41 
lemma subspace_add_closed [simp, intro!!]: 
7917  42 
"[ is_subspace U V; x: U; y: U ] ==> x + y : U"; 
7656  43 
by (unfold is_subspace_def) simp; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

44 

7808  45 
lemma subspace_mult_closed [simp, intro!!]: 
7917  46 
"[ is_subspace U V; x: U ] ==> a <*> x: U"; 
7808  47 
by (unfold is_subspace_def) simp; 
48 

49 
lemma subspace_diff_closed [simp, intro!!]: 

7917  50 
"[ is_subspace U V; is_vectorspace V; x: U; y: U ] 
51 
==> x  y: U"; 

52 
by (simp! add: diff_eq1 negate_eq1); 

53 

54 
text {* Similar as for linear spaces, the existence of the 

55 
zero element in every subspace follws from the nonemptyness 

56 
of the subspace and vector space laws.*}; 

57 

58 
lemma zero_in_subspace [intro !!]: 

59 
"[ is_subspace U V; is_vectorspace V ] ==> <0>:U"; 

60 
proof ; 

61 
assume "is_subspace U V" and v: "is_vectorspace V"; 

62 
have "U ~= {}"; ..; 

63 
hence "EX x. x:U"; by force; 

64 
thus ?thesis; 

65 
proof; 

66 
fix x; assume u: "x:U"; 

67 
hence "x:V"; by (simp!); 

68 
with v; have "<0> = x  x"; by (simp!); 

69 
also; have "... : U"; by (rule subspace_diff_closed); 

70 
finally; show ?thesis; .; 

71 
qed; 

72 
qed; 

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

73 

7808  74 
lemma subspace_neg_closed [simp, intro!!]: 
7917  75 
"[ is_subspace U V; is_vectorspace V; x: U ] ==>  x: U"; 
76 
by (simp add: negate_eq1); 

77 

78 
text_raw {* \medskip *}; 

79 
text {* Further derived laws: Every subspace is a vector space. *}; 

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

80 

7808  81 
lemma subspace_vs [intro!!]: 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

82 
"[ is_subspace U V; is_vectorspace V ] ==> is_vectorspace U"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

83 
proof ; 
7656  84 
assume "is_subspace U V" "is_vectorspace V"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

85 
show ?thesis; 
7566  86 
proof; 
87 
show "<0>:U"; ..; 

7917  88 
show "ALL x:U. ALL a. a <*> x : U"; by (simp!); 
89 
show "ALL x:U. ALL y:U. x + y : U"; by (simp!); 

90 
show "ALL x:U.  x = 1r <*> x"; by (simp! add: negate_eq1); 

91 
show "ALL x:U. ALL y:U. x  y = x +  y"; 

92 
by (simp! add: diff_eq1); 

7566  93 
qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

95 

7917  96 
text {* The subspace relation is reflexive. *}; 
97 

7566  98 
lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V"; 
99 
proof; 

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

100 
assume "is_vectorspace V"; 
7566  101 
show "<0> : V"; ..; 
102 
show "V <= V"; ..; 

7917  103 
show "ALL x:V. ALL y:V. x + y : V"; by (simp!); 
104 
show "ALL x:V. ALL a. a <*> x : V"; by (simp!); 

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

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

106 

7917  107 
text {* The subspace relation is transitive. *}; 
108 

7808  109 
lemma subspace_trans: 
7917  110 
"[ is_subspace U V; is_vectorspace V; is_subspace V W ] 
111 
==> is_subspace U W"; 

7566  112 
proof; 
7917  113 
assume "is_subspace U V" "is_subspace V W" "is_vectorspace V"; 
7566  114 
show "<0> : U"; ..; 
7656  115 

7566  116 
have "U <= V"; ..; 
117 
also; have "V <= W"; ..; 

118 
finally; show "U <= W"; .; 

7656  119 

7917  120 
show "ALL x:U. ALL y:U. x + y : U"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

121 
proof (intro ballI); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

122 
fix x y; assume "x:U" "y:U"; 
7917  123 
show "x + y : U"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

124 
qed; 
7656  125 

7917  126 
show "ALL x:U. ALL a. a <*> x : U"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

127 
proof (intro ballI allI); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

128 
fix x a; assume "x:U"; 
7917  129 
show "a <*> x : U"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

132 

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

133 

7808  134 

135 
subsection {* Linear closure *}; 

136 

7917  137 
text {* The \emph{linear closure} of a vector $x$ is the set of all 
138 
multiples of $x$. *}; 

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

139 

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

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

141 
lin :: "'a => 'a set" 
7917  142 
"lin x == {y. EX a. y = a <*> x}"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

143 

7917  144 
lemma linD: "x : lin v = (EX a::real. x = a <*> v)"; 
7566  145 
by (unfold lin_def) force; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

146 

7917  147 
lemma linI [intro!!]: "a <*> x0 : lin x0"; 
7656  148 
by (unfold lin_def) force; 
149 

7917  150 
text {* Every vector is contained in its linear closure. *}; 
151 

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

152 
lemma x_lin_x: "[ is_vectorspace V; x:V ] ==> x:lin x"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

153 
proof (unfold lin_def, intro CollectI exI); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

154 
assume "is_vectorspace V" "x:V"; 
7917  155 
show "x = 1r <*> x"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

157 

7917  158 
text {* Any linear closure is a subspace. *}; 
159 

7808  160 
lemma lin_subspace [intro!!]: 
161 
"[ is_vectorspace V; x:V ] ==> is_subspace (lin x) V"; 

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

163 
assume "is_vectorspace V" "x:V"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

164 
show "<0> : lin x"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

165 
proof (unfold lin_def, intro CollectI exI); 
7917  166 
show "<0> = 0r <*> x"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

167 
qed; 
7566  168 

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

169 
show "lin x <= V"; 
7566  170 
proof (unfold lin_def, intro subsetI, elim CollectE exE); 
7917  171 
fix xa a; assume "xa = a <*> x"; 
7566  172 
show "xa:V"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

173 
qed; 
7566  174 

7917  175 
show "ALL x1 : lin x. ALL x2 : lin x. x1 + x2 : lin x"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

176 
proof (intro ballI); 
7566  177 
fix x1 x2; assume "x1 : lin x" "x2 : lin x"; 
7917  178 
thus "x1 + x2 : lin x"; 
7567  179 
proof (unfold lin_def, elim CollectE exE, intro CollectI exI); 
7917  180 
fix a1 a2; assume "x1 = a1 <*> x" "x2 = a2 <*> x"; 
181 
show "x1 + x2 = (a1 + a2) <*> x"; 

7808  182 
by (simp! add: vs_add_mult_distrib2); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

184 
qed; 
7566  185 

7917  186 
show "ALL xa:lin x. ALL a. a <*> xa : lin x"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

187 
proof (intro ballI allI); 
7566  188 
fix x1 a; assume "x1 : lin x"; 
7917  189 
thus "a <*> x1 : lin x"; 
7567  190 
proof (unfold lin_def, elim CollectE exE, intro CollectI exI); 
7917  191 
fix a1; assume "x1 = a1 <*> x"; 
192 
show "a <*> x1 = (a * a1) <*> x"; by (simp!); 

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

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

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

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

196 

7917  197 
text {* Any linear closure is a vector space. *}; 
198 

7808  199 
lemma lin_vs [intro!!]: 
200 
"[ is_vectorspace V; x:V ] ==> is_vectorspace (lin x)"; 

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

201 
proof (rule subspace_vs); 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

202 
assume "is_vectorspace V" "x:V"; 
7566  203 
show "is_subspace (lin x) V"; ..; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

205 

7808  206 

207 

208 
subsection {* Sum of two vectorspaces *}; 

209 

7917  210 
text {* The \emph{sum} of two vectorspaces $U$ and $V$ is the set of 
211 
all sums of elements from $U$ and $V$. *}; 

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

212 

7917  213 
instance set :: (plus) plus; by intro_classes; 
214 

215 
defs vs_sum_def: 

216 
"U + V == {x. EX u:U. EX v:V. x = u + v}"; 

217 

218 
(*** 

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

219 
constdefs 
7917  220 
vs_sum :: 
221 
"['a::{minus, plus} set, 'a set] => 'a set" (infixl "+" 65) 

222 
"vs_sum U V == {x. EX u:U. EX v:V. x = u + v}"; 

223 
***) 

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

224 

7917  225 
lemma vs_sumD: 
226 
"x: U + V = (EX u:U. EX v:V. x = u + v)"; 

227 
by (unfold vs_sum_def) simp; 

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

228 

7566  229 
lemmas vs_sumE = vs_sumD [RS iffD1, elimify]; 
230 

7808  231 
lemma vs_sumI [intro!!]: 
7917  232 
"[ x:U; y:V; t= x + y ] ==> t : U + V"; 
233 
by (unfold vs_sum_def, intro CollectI bexI); 

234 

235 
text{* $U$ is a subspace of $U + V$. *}; 

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

236 

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

237 
lemma subspace_vs_sum1 [intro!!]: 
7917  238 
"[ is_vectorspace U; is_vectorspace V ] 
239 
==> is_subspace U (U + V)"; 

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

241 
assume "is_vectorspace U" "is_vectorspace V"; 
7566  242 
show "<0> : U"; ..; 
7917  243 
show "U <= U + V"; 
7566  244 
proof (intro subsetI vs_sumI); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

245 
fix x; assume "x:U"; 
7917  246 
show "x = x + <0>"; by (simp!); 
7566  247 
show "<0> : V"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

248 
qed; 
7917  249 
show "ALL x:U. ALL y:U. x + y : U"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

250 
proof (intro ballI); 
7917  251 
fix x y; assume "x:U" "y:U"; show "x + y : U"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

252 
qed; 
7917  253 
show "ALL x:U. ALL a. a <*> x : U"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

254 
proof (intro ballI allI); 
7917  255 
fix x a; assume "x:U"; show "a <*> x : U"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

258 

7917  259 
text{* The sum of two subspaces is again a subspace.*}; 
260 

7566  261 
lemma vs_sum_subspace [intro!!]: 
262 
"[ is_subspace U E; is_subspace V E; is_vectorspace E ] 

7917  263 
==> is_subspace (U + V) E"; 
7566  264 
proof; 
7917  265 
assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"; 
266 
show "<0> : U + V"; 

7566  267 
proof (intro vs_sumI); 
268 
show "<0> : U"; ..; 

269 
show "<0> : V"; ..; 

7917  270 
show "(<0>::'a) = <0> + <0>"; by (simp!); 
7566  271 
qed; 
272 

7917  273 
show "U + V <= E"; 
7566  274 
proof (intro subsetI, elim vs_sumE bexE); 
7917  275 
fix x u v; assume "u : U" "v : V" "x = u + v"; 
7566  276 
show "x:E"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

278 

7917  279 
show "ALL x: U + V. ALL y: U + V. x + y : U + V"; 
7566  280 
proof (intro ballI); 
7917  281 
fix x y; assume "x : U + V" "y : U + V"; 
282 
thus "x + y : U + V"; 

7566  283 
proof (elim vs_sumE bexE, intro vs_sumI); 
284 
fix ux vx uy vy; 

7917  285 
assume "ux : U" "vx : V" "x = ux + vx" 
286 
and "uy : U" "vy : V" "y = uy + vy"; 

287 
show "x + y = (ux + uy) + (vx + vy)"; by (simp!); 

7566  288 
qed (simp!)+; 
289 
qed; 

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

290 

7917  291 
show "ALL x: U + V. ALL a. a <*> x : U + V"; 
7566  292 
proof (intro ballI allI); 
7917  293 
fix x a; assume "x : U + V"; 
294 
thus "a <*> x : U + V"; 

7566  295 
proof (elim vs_sumE bexE, intro vs_sumI); 
7917  296 
fix a x u v; assume "u : U" "v : V" "x = u + v"; 
297 
show "a <*> x = (a <*> u) + (a <*> v)"; 

7808  298 
by (simp! add: vs_add_mult_distrib1); 
7566  299 
qed (simp!)+; 
300 
qed; 

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

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

302 

7917  303 
text{* The sum of two subspaces is a vectorspace. *}; 
304 

7566  305 
lemma vs_sum_vs [intro!!]: 
306 
"[ is_subspace U E; is_subspace V E; is_vectorspace E ] 

7917  307 
==> is_vectorspace (U + V)"; 
7566  308 
proof (rule subspace_vs); 
309 
assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"; 

7917  310 
show "is_subspace (U + V) E"; ..; 
7566  311 
qed; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

312 

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

313 

7808  314 

7917  315 
subsection {* Direct sums *}; 
7808  316 

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

317 

7917  318 
text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero 
319 
element is the only common element of $U$ and $V$. For every element 

320 
$x$ of the direct sum of $U$ and $V$ the decomposition in 

321 
$x = u + v$ with $u:U$ and $v:V$ is unique.*}; 

7808  322 

7917  323 
lemma decomp: 
324 
"[ is_vectorspace E; is_subspace U E; is_subspace V E; 

325 
U Int V = {<0>}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 ] 

7656  326 
==> u1 = u2 & v1 = v2"; 
327 
proof; 

7808  328 
assume "is_vectorspace E" "is_subspace U E" "is_subspace V E" 
329 
"U Int V = {<0>}" "u1:U" "u2:U" "v1:V" "v2:V" 

7917  330 
"u1 + v1 = u2 + v2"; 
331 
have eq: "u1  u2 = v2  v1"; by (simp! add: vs_add_diff_swap); 

332 
have u: "u1  u2 : U"; by (simp!); 

333 
with eq; have v': "v2  v1 : U"; by simp; 

334 
have v: "v2  v1 : V"; by (simp!); 

335 
with eq; have u': "u1  u2 : V"; by simp; 

7656  336 

337 
show "u1 = u2"; 

338 
proof (rule vs_add_minus_eq); 

7917  339 
show "u1  u2 = <0>"; by (rule Int_singletonD [OF _ u u']); 
340 
show "u1 : E"; ..; 

341 
show "u2 : E"; ..; 

342 
qed; 

7656  343 

344 
show "v1 = v2"; 

345 
proof (rule vs_add_minus_eq [RS sym]); 

7917  346 
show "v2  v1 = <0>"; by (rule Int_singletonD [OF _ v' v]); 
347 
show "v1 : E"; ..; 

348 
show "v2 : E"; ..; 

349 
qed; 

7656  350 
qed; 
351 

7917  352 
text {* An application of the previous lemma will be used in the 
353 
proof of the HahnBanach theorem: for an element $y + a \mult x_0$ 

354 
of the direct sum of a vectorspace $H$ and the linear closure of 

355 
$x_0$ the components $y:H$ and $a$ are unique. *}; 

356 

357 
lemma decomp_H0: 

358 
"[ is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 

359 
x0 ~: H; x0 : E; x0 ~= <0>; y1 + a1 <*> x0 = y2 + a2 <*> x0 ] 

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

360 
==> y1 = y2 & a1 = a2"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

361 
proof; 
7656  362 
assume "is_vectorspace E" and h: "is_subspace H E" 
363 
and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 

7917  364 
"y1 + a1 <*> x0 = y2 + a2 <*> x0"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

365 

7917  366 
have c: "y1 = y2 & a1 <*> x0 = a2 <*> x0"; 
7656  367 
proof (rule decomp); 
7917  368 
show "a1 <*> x0 : lin x0"; ..; 
369 
show "a2 <*> x0 : lin x0"; ..; 

7656  370 
show "H Int (lin x0) = {<0>}"; 
371 
proof; 

372 
show "H Int lin x0 <= {<0>}"; 

373 
proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]); 

374 
fix x; assume "x:H" "x:lin x0"; 

375 
thus "x = <0>"; 

376 
proof (unfold lin_def, elim CollectE exE); 

7917  377 
fix a; assume "x = a <*> x0"; 
7656  378 
show ?thesis; 
7917  379 
proof (rule case_split); 
7656  380 
assume "a = 0r"; show ?thesis; by (simp!); 
381 
next; 

382 
assume "a ~= 0r"; 

7917  383 
from h; have "rinv a <*> a <*> x0 : H"; 
7808  384 
by (rule subspace_mult_closed) (simp!); 
7917  385 
also; have "rinv a <*> a <*> x0 = x0"; by (simp!); 
7656  386 
finally; have "x0 : H"; .; 
387 
thus ?thesis; by contradiction; 

388 
qed; 

389 
qed; 

390 
qed; 

391 
show "{<0>} <= H Int lin x0"; 

392 
proof (intro subsetI, elim singletonE, intro IntI, simp+); 

393 
show "<0> : H"; ..; 

394 
from lin_vs; show "<0> : lin x0"; ..; 

395 
qed; 

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

396 
qed; 
7656  397 
show "is_subspace (lin x0) E"; ..; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

398 
qed; 
7656  399 

400 
from c; show "y1 = y2"; by simp; 

401 

402 
show "a1 = a2"; 

403 
proof (rule vs_mult_right_cancel [RS iffD1]); 

7917  404 
from c; show "a1 <*> x0 = a2 <*> x0"; by simp; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

407 

7917  408 
text {* Since for an element $y + a \mult x_0$ of the direct sum 
409 
of a vectorspace $H$ and the linear closure of $x_0$ the components 

410 
$y\in H$ and $a$ are unique, follows from $y\in H$ the fact that 

411 
$a = 0$.*}; 

412 

413 
lemma decomp_H0_H: 

414 
"[ is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; 

415 
x0 ~= <0> ] 

416 
==> (SOME (y, a). t = y + a <*> x0 & y : H) = (t, 0r)"; 

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

417 
proof (rule, unfold split_paired_all); 
7917  418 
assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" 
7808  419 
"x0 ~= <0>"; 
7566  420 
have h: "is_vectorspace H"; ..; 
7917  421 
fix y a; presume t1: "t = y + a <*> x0" and "y : H"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

422 
have "y = t & a = 0r"; 
7917  423 
by (rule decomp_H0) (assumption  (simp!))+; 
7566  424 
thus "(y, a) = (t, 0r)"; by (simp!); 
425 
qed (simp!)+; 

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

426 

7917  427 
text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$ 
428 
are unique, so the function $h_0$ defined by 

429 
$h_0 (y \plus a \mult x_0) = h y + a * xi$ is definite. *}; 

430 

431 
lemma h0_definite: 

432 
"[ h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H) 

7566  433 
in (h y) + a * xi); 
7917  434 
x = y + a <*> x0; is_vectorspace E; is_subspace H E; 
7808  435 
y:H; x0 ~: H; x0:E; x0 ~= <0> ] 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

436 
==> h0 x = h y + a * xi"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

437 
proof ; 
7917  438 
assume 
439 
"h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H) 

440 
in (h y) + a * xi)" 

441 
"x = y + a <*> x0" "is_vectorspace E" "is_subspace H E" 

442 
"y:H" "x0 ~: H" "x0:E" "x0 ~= <0>"; 

443 
have "x : H + (lin x0)"; 

444 
by (simp! add: vs_sum_def lin_def) force+; 

445 
have "EX! xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)"; 

446 
proof; 

447 
show "EX xa. ((%(y, a). x = y + a <*> x0 & y:H) xa)"; 

7566  448 
by (force!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

450 
fix xa ya; 
7917  451 
assume "(%(y,a). x = y + a <*> x0 & y : H) xa" 
452 
"(%(y,a). x = y + a <*> x0 & y : H) ya"; 

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

453 
show "xa = ya"; ; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

455 
show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
7566  456 
by (rule Pair_fst_snd_eq [RS iffD2]); 
7917  457 
have x: "x = (fst xa) + (snd xa) <*> x0 & (fst xa) : H"; 
7808  458 
by (force!); 
7917  459 
have y: "x = (fst ya) + (snd ya) <*> x0 & (fst ya) : H"; 
7808  460 
by (force!); 
461 
from x y; show "fst xa = fst ya & snd xa = snd ya"; 

7917  462 
by (elim conjE) (rule decomp_H0, (simp!)+); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

464 
qed; 
7917  465 
hence eq: "(SOME (y, a). (x = y + a <*> x0 & y:H)) = (y, a)"; 
7808  466 
by (rule select1_equality) (force!); 
7656  467 
thus "h0 x = h y + a * xi"; by (simp! add: Let_def); 
7566  468 
qed; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

469 

7808  470 
end; 