author | fleuriot |
Thu, 01 Jun 2000 11:22:27 +0200 | |
changeset 9013 | 9dd0274f76af |
parent 8703 | 816d8f6513be |
child 9035 | 371f023d3dbd |
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" |
|
7978 | 20 |
"is_subspace U V == U ~= {} & U <= V |
8703 | 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]: |
8703 | 24 |
"[| 00 : 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); |
8703 | 28 |
assume "00 : U"; thus "U ~= {}"; by fast; |
7917 | 29 |
qed (simp+); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
30 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
31 |
lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}"; |
7917 | 32 |
by (unfold is_subspace_def) simp; |
7566 | 33 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
34 |
lemma subspace_subset [intro??]: "is_subspace U V ==> U <= V"; |
7656 | 35 |
by (unfold is_subspace_def) simp; |
7566 | 36 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
37 |
lemma subspace_subsetD [simp, intro??]: |
7978 | 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 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
41 |
lemma subspace_add_closed [simp, intro??]: |
7978 | 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 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
45 |
lemma subspace_mult_closed [simp, intro??]: |
8703 | 46 |
"[| is_subspace U V; x:U |] ==> a (*) x : U"; |
7808 | 47 |
by (unfold is_subspace_def) simp; |
48 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
49 |
lemma subspace_diff_closed [simp, intro??]: |
7978 | 50 |
"[| is_subspace U V; is_vectorspace V; x:U; y:U |] |
51 |
==> x - y : U"; |
|
7917 | 52 |
by (simp! add: diff_eq1 negate_eq1); |
53 |
||
54 |
text {* Similar as for linear spaces, the existence of the |
|
7978 | 55 |
zero element in every subspace follows from the non-emptiness |
56 |
of the carrier set and by vector space laws.*}; |
|
7917 | 57 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
58 |
lemma zero_in_subspace [intro??]: |
8703 | 59 |
"[| is_subspace U V; is_vectorspace V |] ==> 00 : U"; |
7917 | 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!); |
|
8703 | 68 |
with v; have "00 = x - x"; by (simp!); |
7917 | 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 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
74 |
lemma subspace_neg_closed [simp, intro??]: |
7978 | 75 |
"[| is_subspace U V; is_vectorspace V; x:U |] ==> - x : U"; |
7917 | 76 |
by (simp add: negate_eq1); |
77 |
||
78 |
text_raw {* \medskip *}; |
|
7978 | 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 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
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; |
8703 | 87 |
show "00 : U"; ..; |
88 |
show "ALL x:U. ALL a. a (*) x : U"; by (simp!); |
|
7917 | 89 |
show "ALL x:U. ALL y:U. x + y : U"; by (simp!); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8703
diff
changeset
|
90 |
show "ALL x:U. - x = -#1 (*) x"; by (simp! add: negate_eq1); |
7917 | 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"; |
8703 | 101 |
show "00 : V"; ..; |
7566 | 102 |
show "V <= V"; ..; |
7917 | 103 |
show "ALL x:V. ALL y:V. x + y : V"; by (simp!); |
8703 | 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"; |
8703 | 114 |
show "00 : 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 |
|
8703 | 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"; |
8703 | 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 |
||
7978 | 137 |
text {* The \emph{linear closure} of a vector $x$ is the set of all |
138 |
scalar 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" |
8703 | 142 |
"lin x == {a (*) x | a. True}"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
143 |
|
8703 | 144 |
lemma linD: "x : lin v = (EX a::real. x = a (*) v)"; |
7978 | 145 |
by (unfold lin_def) fast; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
146 |
|
8703 | 147 |
lemma linI [intro??]: "a (*) x0 : lin x0"; |
7978 | 148 |
by (unfold lin_def) fast; |
7656 | 149 |
|
7917 | 150 |
text {* Every vector is contained in its linear closure. *}; |
151 |
||
7978 | 152 |
lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x"; |
153 |
proof (unfold lin_def, intro CollectI exI conjI); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
154 |
assume "is_vectorspace V" "x:V"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8703
diff
changeset
|
155 |
show "x = #1 (*) x"; by (simp!); |
7978 | 156 |
qed simp; |
7535
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 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
160 |
lemma lin_subspace [intro??]: |
7808 | 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"; |
8703 | 164 |
show "00 : lin x"; |
7978 | 165 |
proof (unfold lin_def, intro CollectI exI conjI); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8703
diff
changeset
|
166 |
show "00 = (#0::real) (*) x"; by (simp!); |
7978 | 167 |
qed simp; |
7566 | 168 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
169 |
show "lin x <= V"; |
7978 | 170 |
proof (unfold lin_def, intro subsetI, elim CollectE exE conjE); |
8703 | 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"; |
7978 | 179 |
proof (unfold lin_def, elim CollectE exE conjE, |
180 |
intro CollectI exI conjI); |
|
8703 | 181 |
fix a1 a2; assume "x1 = a1 (*) x" "x2 = a2 (*) x"; |
182 |
show "x1 + x2 = (a1 + a2) (*) x"; |
|
7808 | 183 |
by (simp! add: vs_add_mult_distrib2); |
7978 | 184 |
qed simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
185 |
qed; |
7566 | 186 |
|
8703 | 187 |
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
|
188 |
proof (intro ballI allI); |
7566 | 189 |
fix x1 a; assume "x1 : lin x"; |
8703 | 190 |
thus "a (*) x1 : lin x"; |
7978 | 191 |
proof (unfold lin_def, elim CollectE exE conjE, |
192 |
intro CollectI exI conjI); |
|
8703 | 193 |
fix a1; assume "x1 = a1 (*) x"; |
194 |
show "a (*) x1 = (a * a1) (*) x"; by (simp!); |
|
7978 | 195 |
qed simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
196 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
197 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
198 |
|
7917 | 199 |
text {* Any linear closure is a vector space. *}; |
200 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
201 |
lemma lin_vs [intro??]: |
7808 | 202 |
"[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
203 |
proof (rule subspace_vs); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
204 |
assume "is_vectorspace V" "x:V"; |
7566 | 205 |
show "is_subspace (lin x) V"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
206 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
207 |
|
7808 | 208 |
|
209 |
||
210 |
subsection {* Sum of two vectorspaces *}; |
|
211 |
||
7917 | 212 |
text {* The \emph{sum} of two vectorspaces $U$ and $V$ is the set of |
213 |
all sums of elements from $U$ and $V$. *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
214 |
|
7917 | 215 |
instance set :: (plus) plus; by intro_classes; |
216 |
||
217 |
defs vs_sum_def: |
|
7978 | 218 |
"U + V == {u + v | u v. u:U & v:V}"; (*** |
7917 | 219 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
220 |
constdefs |
7917 | 221 |
vs_sum :: |
222 |
"['a::{minus, plus} set, 'a set] => 'a set" (infixl "+" 65) |
|
223 |
"vs_sum U V == {x. EX u:U. EX v:V. x = u + v}"; |
|
224 |
***) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
225 |
|
7917 | 226 |
lemma vs_sumD: |
227 |
"x: U + V = (EX u:U. EX v:V. x = u + v)"; |
|
7978 | 228 |
by (unfold vs_sum_def) fast; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
229 |
|
7566 | 230 |
lemmas vs_sumE = vs_sumD [RS iffD1, elimify]; |
231 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
232 |
lemma vs_sumI [intro??]: |
7917 | 233 |
"[| x:U; y:V; t= x + y |] ==> t : U + V"; |
7978 | 234 |
by (unfold vs_sum_def) fast; |
7917 | 235 |
|
236 |
text{* $U$ is a subspace of $U + V$. *}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
237 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
238 |
lemma subspace_vs_sum1 [intro??]: |
7917 | 239 |
"[| is_vectorspace U; is_vectorspace V |] |
240 |
==> is_subspace U (U + V)"; |
|
7566 | 241 |
proof; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
242 |
assume "is_vectorspace U" "is_vectorspace V"; |
8703 | 243 |
show "00 : U"; ..; |
7917 | 244 |
show "U <= U + V"; |
7566 | 245 |
proof (intro subsetI vs_sumI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
246 |
fix x; assume "x:U"; |
8703 | 247 |
show "x = x + 00"; by (simp!); |
248 |
show "00 : V"; by (simp!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
249 |
qed; |
7917 | 250 |
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
|
251 |
proof (intro ballI); |
7917 | 252 |
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
|
253 |
qed; |
8703 | 254 |
show "ALL x:U. ALL a. a (*) x : U"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
255 |
proof (intro ballI allI); |
8703 | 256 |
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
|
257 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
258 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
259 |
|
7917 | 260 |
text{* The sum of two subspaces is again a subspace.*}; |
261 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
262 |
lemma vs_sum_subspace [intro??]: |
7566 | 263 |
"[| is_subspace U E; is_subspace V E; is_vectorspace E |] |
7917 | 264 |
==> is_subspace (U + V) E"; |
7566 | 265 |
proof; |
7917 | 266 |
assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"; |
8703 | 267 |
show "00 : U + V"; |
7566 | 268 |
proof (intro vs_sumI); |
8703 | 269 |
show "00 : U"; ..; |
270 |
show "00 : V"; ..; |
|
271 |
show "(00::'a) = 00 + 00"; by (simp!); |
|
7566 | 272 |
qed; |
273 |
||
7917 | 274 |
show "U + V <= E"; |
7566 | 275 |
proof (intro subsetI, elim vs_sumE bexE); |
7917 | 276 |
fix x u v; assume "u : U" "v : V" "x = u + v"; |
7566 | 277 |
show "x:E"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
278 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
279 |
|
7917 | 280 |
show "ALL x: U + V. ALL y: U + V. x + y : U + V"; |
7566 | 281 |
proof (intro ballI); |
7917 | 282 |
fix x y; assume "x : U + V" "y : U + V"; |
283 |
thus "x + y : U + V"; |
|
7566 | 284 |
proof (elim vs_sumE bexE, intro vs_sumI); |
285 |
fix ux vx uy vy; |
|
7917 | 286 |
assume "ux : U" "vx : V" "x = ux + vx" |
287 |
and "uy : U" "vy : V" "y = uy + vy"; |
|
288 |
show "x + y = (ux + uy) + (vx + vy)"; by (simp!); |
|
7566 | 289 |
qed (simp!)+; |
290 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
291 |
|
8703 | 292 |
show "ALL x : U + V. ALL a. a (*) x : U + V"; |
7566 | 293 |
proof (intro ballI allI); |
7917 | 294 |
fix x a; assume "x : U + V"; |
8703 | 295 |
thus "a (*) x : U + V"; |
7566 | 296 |
proof (elim vs_sumE bexE, intro vs_sumI); |
7917 | 297 |
fix a x u v; assume "u : U" "v : V" "x = u + v"; |
8703 | 298 |
show "a (*) x = (a (*) u) + (a (*) v)"; |
7808 | 299 |
by (simp! add: vs_add_mult_distrib1); |
7566 | 300 |
qed (simp!)+; |
301 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
302 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
303 |
|
7917 | 304 |
text{* The sum of two subspaces is a vectorspace. *}; |
305 |
||
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset
|
306 |
lemma vs_sum_vs [intro??]: |
7566 | 307 |
"[| is_subspace U E; is_subspace V E; is_vectorspace E |] |
7917 | 308 |
==> is_vectorspace (U + V)"; |
7566 | 309 |
proof (rule subspace_vs); |
310 |
assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"; |
|
7917 | 311 |
show "is_subspace (U + V) E"; ..; |
7566 | 312 |
qed; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
313 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
314 |
|
7808 | 315 |
|
7917 | 316 |
subsection {* Direct sums *}; |
7808 | 317 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
318 |
|
7917 | 319 |
text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero |
320 |
element is the only common element of $U$ and $V$. For every element |
|
321 |
$x$ of the direct sum of $U$ and $V$ the decomposition in |
|
7927 | 322 |
$x = u + v$ with $u \in U$ and $v \in V$ is unique.*}; |
7808 | 323 |
|
7917 | 324 |
lemma decomp: |
325 |
"[| is_vectorspace E; is_subspace U E; is_subspace V E; |
|
8703 | 326 |
U Int V = {00}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |] |
7656 | 327 |
==> u1 = u2 & v1 = v2"; |
328 |
proof; |
|
7808 | 329 |
assume "is_vectorspace E" "is_subspace U E" "is_subspace V E" |
8703 | 330 |
"U Int V = {00}" "u1:U" "u2:U" "v1:V" "v2:V" |
7917 | 331 |
"u1 + v1 = u2 + v2"; |
332 |
have eq: "u1 - u2 = v2 - v1"; by (simp! add: vs_add_diff_swap); |
|
333 |
have u: "u1 - u2 : U"; by (simp!); |
|
334 |
with eq; have v': "v2 - v1 : U"; by simp; |
|
335 |
have v: "v2 - v1 : V"; by (simp!); |
|
336 |
with eq; have u': "u1 - u2 : V"; by simp; |
|
7656 | 337 |
|
338 |
show "u1 = u2"; |
|
339 |
proof (rule vs_add_minus_eq); |
|
8703 | 340 |
show "u1 - u2 = 00"; by (rule Int_singletonD [OF _ u u']); |
7917 | 341 |
show "u1 : E"; ..; |
342 |
show "u2 : E"; ..; |
|
343 |
qed; |
|
7656 | 344 |
|
345 |
show "v1 = v2"; |
|
346 |
proof (rule vs_add_minus_eq [RS sym]); |
|
8703 | 347 |
show "v2 - v1 = 00"; by (rule Int_singletonD [OF _ v' v]); |
7917 | 348 |
show "v1 : E"; ..; |
349 |
show "v2 : E"; ..; |
|
350 |
qed; |
|
7656 | 351 |
qed; |
352 |
||
7978 | 353 |
text {* An application of the previous lemma will be used in the proof |
354 |
of the Hahn-Banach Theorem (see page \pageref{decomp-H0-use}): for any |
|
355 |
element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and |
|
356 |
the linear closure of $x_0$ the components $y \in H$ and $a$ are |
|
357 |
uniquely determined. *}; |
|
7917 | 358 |
|
359 |
lemma decomp_H0: |
|
360 |
"[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; |
|
8703 | 361 |
x0 ~: H; x0 : E; x0 ~= 00; y1 + a1 (*) x0 = y2 + a2 (*) x0 |] |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
362 |
==> y1 = y2 & a1 = a2"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
363 |
proof; |
7656 | 364 |
assume "is_vectorspace E" and h: "is_subspace H E" |
8703 | 365 |
and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= 00" |
366 |
"y1 + a1 (*) x0 = y2 + a2 (*) x0"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
367 |
|
8703 | 368 |
have c: "y1 = y2 & a1 (*) x0 = a2 (*) x0"; |
7656 | 369 |
proof (rule decomp); |
8703 | 370 |
show "a1 (*) x0 : lin x0"; ..; |
371 |
show "a2 (*) x0 : lin x0"; ..; |
|
372 |
show "H Int (lin x0) = {00}"; |
|
7656 | 373 |
proof; |
8703 | 374 |
show "H Int lin x0 <= {00}"; |
7656 | 375 |
proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]); |
7978 | 376 |
fix x; assume "x:H" "x : lin x0"; |
8703 | 377 |
thus "x = 00"; |
7978 | 378 |
proof (unfold lin_def, elim CollectE exE conjE); |
8703 | 379 |
fix a; assume "x = a (*) x0"; |
7656 | 380 |
show ?thesis; |
8280 | 381 |
proof cases; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8703
diff
changeset
|
382 |
assume "a = (#0::real)"; show ?thesis; by (simp!); |
7656 | 383 |
next; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8703
diff
changeset
|
384 |
assume "a ~= (#0::real)"; |
8703 | 385 |
from h; have "rinv a (*) a (*) x0 : H"; |
7808 | 386 |
by (rule subspace_mult_closed) (simp!); |
8703 | 387 |
also; have "rinv a (*) a (*) x0 = x0"; by (simp!); |
7656 | 388 |
finally; have "x0 : H"; .; |
389 |
thus ?thesis; by contradiction; |
|
390 |
qed; |
|
391 |
qed; |
|
392 |
qed; |
|
8703 | 393 |
show "{00} <= H Int lin x0"; |
8169 | 394 |
proof -; |
8703 | 395 |
have "00: H Int lin x0"; |
8169 | 396 |
proof (rule IntI); |
8703 | 397 |
show "00:H"; ..; |
398 |
from lin_vs; show "00 : lin x0"; ..; |
|
8169 | 399 |
qed; |
400 |
thus ?thesis; by simp; |
|
7656 | 401 |
qed; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
402 |
qed; |
7656 | 403 |
show "is_subspace (lin x0) E"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
404 |
qed; |
7656 | 405 |
|
406 |
from c; show "y1 = y2"; by simp; |
|
407 |
||
408 |
show "a1 = a2"; |
|
409 |
proof (rule vs_mult_right_cancel [RS iffD1]); |
|
8703 | 410 |
from c; show "a1 (*) x0 = a2 (*) x0"; by simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
411 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
412 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
413 |
|
7978 | 414 |
text {* Since for any element $y + a \mult x_0$ of the direct sum |
7917 | 415 |
of a vectorspace $H$ and the linear closure of $x_0$ the components |
7978 | 416 |
$y\in H$ and $a$ are unique, it follows from $y\in H$ that |
7917 | 417 |
$a = 0$.*}; |
418 |
||
419 |
lemma decomp_H0_H: |
|
7978 | 420 |
"[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E; |
8703 | 421 |
x0 ~= 00 |] |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8703
diff
changeset
|
422 |
==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
423 |
proof (rule, unfold split_paired_all); |
7978 | 424 |
assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E" |
8703 | 425 |
"x0 ~= 00"; |
7566 | 426 |
have h: "is_vectorspace H"; ..; |
8703 | 427 |
fix y a; presume t1: "t = y + a (*) x0" and "y:H"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8703
diff
changeset
|
428 |
have "y = t & a = (#0::real)"; |
7917 | 429 |
by (rule decomp_H0) (assumption | (simp!))+; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8703
diff
changeset
|
430 |
thus "(y, a) = (t, (#0::real))"; by (simp!); |
7566 | 431 |
qed (simp!)+; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
432 |
|
7917 | 433 |
text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$ |
434 |
are unique, so the function $h_0$ defined by |
|
7927 | 435 |
$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *}; |
7917 | 436 |
|
437 |
lemma h0_definite: |
|
8703 | 438 |
"[| h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H) |
7566 | 439 |
in (h y) + a * xi); |
8703 | 440 |
x = y + a (*) x0; is_vectorspace E; is_subspace H E; |
441 |
y:H; x0 ~: H; x0:E; x0 ~= 00 |] |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
442 |
==> h0 x = h y + a * xi"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
443 |
proof -; |
7917 | 444 |
assume |
8703 | 445 |
"h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H) |
7917 | 446 |
in (h y) + a * xi)" |
8703 | 447 |
"x = y + a (*) x0" "is_vectorspace E" "is_subspace H E" |
448 |
"y:H" "x0 ~: H" "x0:E" "x0 ~= 00"; |
|
7917 | 449 |
have "x : H + (lin x0)"; |
450 |
by (simp! add: vs_sum_def lin_def) force+; |
|
8703 | 451 |
have "EX! xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)"; |
7917 | 452 |
proof; |
8703 | 453 |
show "EX xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)"; |
7566 | 454 |
by (force!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
455 |
next; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
456 |
fix xa ya; |
8703 | 457 |
assume "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) xa" |
458 |
"(\\<lambda>(y,a). x = y + a (*) x0 & y : H) ya"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
459 |
show "xa = ya"; ; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
460 |
proof -; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
461 |
show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; |
7566 | 462 |
by (rule Pair_fst_snd_eq [RS iffD2]); |
8703 | 463 |
have x: "x = fst xa + snd xa (*) x0 & fst xa : H"; |
7808 | 464 |
by (force!); |
8703 | 465 |
have y: "x = fst ya + snd ya (*) x0 & fst ya : H"; |
7808 | 466 |
by (force!); |
467 |
from x y; show "fst xa = fst ya & snd xa = snd ya"; |
|
7917 | 468 |
by (elim conjE) (rule decomp_H0, (simp!)+); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
469 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
470 |
qed; |
8703 | 471 |
hence eq: "(SOME (y, a). x = y + a (*) x0 & y:H) = (y, a)"; |
7808 | 472 |
by (rule select1_equality) (force!); |
7656 | 473 |
thus "h0 x = h y + a * xi"; by (simp! add: Let_def); |
7566 | 474 |
qed; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
475 |
|
7808 | 476 |
end; |