author | wenzelm |
Fri, 22 Oct 1999 20:14:31 +0200 | |
changeset 7917 | 5e5b9813cce7 |
parent 7808 | fd019ac3485f |
child 7927 | b50446a33c16 |
permissions | -rw-r--r-- |
7566 | 1 |
(* Title: HOL/Real/HahnBanach/Subspace.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gertrud Bauer, TU Munich |
|
4 |
*) |
|
7535
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
10 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
11 |
|
7917 | 12 |
subsection {* Definition *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
13 |
|
7917 | 14 |
text {* A non-empty 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
39 |
by (unfold is_subspace_def) force; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 non-emptyness |
|
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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
80 |
|
7808 | 81 |
lemma subspace_vs [intro!!]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
82 |
"[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U"; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
94 |
qed; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
105 |
qed; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
121 |
proof (intro ballI); |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
127 |
proof (intro ballI allI); |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
130 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
131 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
132 |
|
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
139 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
140 |
constdefs |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
153 |
proof (unfold lin_def, intro CollectI exI); |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
156 |
qed; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
163 |
assume "is_vectorspace V" "x:V"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
164 |
show "<0> : lin x"; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
167 |
qed; |
7566 | 168 |
|
7535
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
183 |
qed; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
193 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
194 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
195 |
qed; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
201 |
proof (rule subspace_vs); |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
204 |
qed; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
236 |
|
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
256 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
257 |
qed; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
277 |
qed; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
301 |
qed; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
312 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
313 |
|
7808 | 314 |
|
7917 | 315 |
subsection {* Direct sums *}; |
7808 | 316 |
|
7535
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
360 |
==> y1 = y2 & a1 = a2"; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
396 |
qed; |
7656 | 397 |
show "is_subspace (lin x0) E"; ..; |
7535
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
405 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
406 |
qed; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
436 |
==> h0 x = h y + a * xi"; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
449 |
next; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
453 |
show "xa = ya"; ; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
454 |
proof -; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
463 |
qed; |
599d3414b51d
The Hahn-Banach 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 Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
469 |
|
7808 | 470 |
end; |