1 (* Title: HOL/Real/HahnBanach/Subspace.thy |
1 (* Title: HOL/Real/HahnBanach/Subspace.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Gertrud Bauer, TU Munich |
3 Author: Gertrud Bauer, TU Munich |
4 *) |
4 *) |
5 |
5 |
6 |
|
7 header {* Subspaces *} |
6 header {* Subspaces *} |
8 |
7 |
9 theory Subspace = VectorSpace: |
8 theory Subspace = VectorSpace: |
10 |
9 |
11 |
10 |
12 subsection {* Definition *} |
11 subsection {* Definition *} |
13 |
12 |
14 text {* A non-empty subset $U$ of a vector space $V$ is a |
13 text {* |
15 \emph{subspace} of $V$, iff $U$ is closed under addition and |
14 A non-empty subset @{text U} of a vector space @{text V} is a |
16 scalar multiplication. *} |
15 \emph{subspace} of @{text V}, iff @{text U} is closed under addition |
17 |
16 and scalar multiplication. |
18 constdefs |
17 *} |
19 is_subspace :: "['a::{plus, minus, zero} set, 'a set] => bool" |
18 |
20 "is_subspace U V == U \<noteq> {} \<and> U <= V |
19 constdefs |
21 \<and> (\<forall>x \<in> U. \<forall>y \<in> U. \<forall>a. x + y \<in> U \<and> a \<cdot> x\<in> U)" |
20 is_subspace :: "'a::{plus, minus, zero} set \<Rightarrow> 'a set \<Rightarrow> bool" |
22 |
21 "is_subspace U V \<equiv> U \<noteq> {} \<and> U \<subseteq> V |
23 lemma subspaceI [intro]: |
22 \<and> (\<forall>x \<in> U. \<forall>y \<in> U. \<forall>a. x + y \<in> U \<and> a \<cdot> x \<in> U)" |
24 "[| 0 \<in> U; U <= V; \<forall>x \<in> U. \<forall>y \<in> U. (x + y \<in> U); |
23 |
25 \<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U |] |
24 lemma subspaceI [intro]: |
26 ==> is_subspace U V" |
25 "0 \<in> U \<Longrightarrow> U \<subseteq> V \<Longrightarrow> \<forall>x \<in> U. \<forall>y \<in> U. (x + y \<in> U) \<Longrightarrow> |
27 proof (unfold is_subspace_def, intro conjI) |
26 \<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U |
|
27 \<Longrightarrow> is_subspace U V" |
|
28 proof (unfold is_subspace_def, intro conjI) |
28 assume "0 \<in> U" thus "U \<noteq> {}" by fast |
29 assume "0 \<in> U" thus "U \<noteq> {}" by fast |
29 qed (simp+) |
30 qed (simp+) |
30 |
31 |
31 lemma subspace_not_empty [intro?]: "is_subspace U V ==> U \<noteq> {}" |
32 lemma subspace_not_empty [intro?]: "is_subspace U V \<Longrightarrow> U \<noteq> {}" |
32 by (unfold is_subspace_def) simp |
33 by (unfold is_subspace_def) blast |
33 |
34 |
34 lemma subspace_subset [intro?]: "is_subspace U V ==> U <= V" |
35 lemma subspace_subset [intro?]: "is_subspace U V \<Longrightarrow> U \<subseteq> V" |
35 by (unfold is_subspace_def) simp |
36 by (unfold is_subspace_def) blast |
36 |
37 |
37 lemma subspace_subsetD [simp, intro?]: |
38 lemma subspace_subsetD [simp, intro?]: |
38 "[| is_subspace U V; x \<in> U |] ==> x \<in> V" |
39 "is_subspace U V \<Longrightarrow> x \<in> U \<Longrightarrow> x \<in> V" |
39 by (unfold is_subspace_def) force |
40 by (unfold is_subspace_def) blast |
40 |
41 |
41 lemma subspace_add_closed [simp, intro?]: |
42 lemma subspace_add_closed [simp, intro?]: |
42 "[| is_subspace U V; x \<in> U; y \<in> U |] ==> x + y \<in> U" |
43 "is_subspace U V \<Longrightarrow> x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U" |
43 by (unfold is_subspace_def) simp |
44 by (unfold is_subspace_def) blast |
44 |
45 |
45 lemma subspace_mult_closed [simp, intro?]: |
46 lemma subspace_mult_closed [simp, intro?]: |
46 "[| is_subspace U V; x \<in> U |] ==> a \<cdot> x \<in> U" |
47 "is_subspace U V \<Longrightarrow> x \<in> U \<Longrightarrow> a \<cdot> x \<in> U" |
47 by (unfold is_subspace_def) simp |
48 by (unfold is_subspace_def) blast |
48 |
49 |
49 lemma subspace_diff_closed [simp, intro?]: |
50 lemma subspace_diff_closed [simp, intro?]: |
50 "[| is_subspace U V; is_vectorspace V; x \<in> U; y \<in> U |] |
51 "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> x \<in> U \<Longrightarrow> y \<in> U |
51 ==> x - y \<in> U" |
52 \<Longrightarrow> x - y \<in> U" |
52 by (simp! add: diff_eq1 negate_eq1) |
53 by (simp add: diff_eq1 negate_eq1) |
53 |
54 |
54 text {* Similar as for linear spaces, the existence of the |
55 text {* Similar as for linear spaces, the existence of the |
55 zero element in every subspace follows from the non-emptiness |
56 zero element in every subspace follows from the non-emptiness |
56 of the carrier set and by vector space laws.*} |
57 of the carrier set and by vector space laws.*} |
57 |
58 |
58 lemma zero_in_subspace [intro?]: |
59 lemma zero_in_subspace [intro?]: |
59 "[| is_subspace U V; is_vectorspace V |] ==> 0 \<in> U" |
60 "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> 0 \<in> U" |
60 proof - |
61 proof - |
61 assume "is_subspace U V" and v: "is_vectorspace V" |
62 assume "is_subspace U V" and v: "is_vectorspace V" |
62 have "U \<noteq> {}" .. |
63 have "U \<noteq> {}" .. |
63 hence "\<exists>x. x \<in> U" by force |
64 hence "\<exists>x. x \<in> U" by blast |
64 thus ?thesis |
65 thus ?thesis |
65 proof |
66 proof |
66 fix x assume u: "x \<in> U" |
67 fix x assume u: "x \<in> U" |
67 hence "x \<in> V" by (simp!) |
68 hence "x \<in> V" by (simp!) |
68 with v have "0 = x - x" by (simp!) |
69 with v have "0 = x - x" by (simp!) |
69 also have "... \<in> U" by (rule subspace_diff_closed) |
70 also have "... \<in> U" by (rule subspace_diff_closed) |
70 finally show ?thesis . |
71 finally show ?thesis . |
71 qed |
72 qed |
72 qed |
73 qed |
73 |
74 |
74 lemma subspace_neg_closed [simp, intro?]: |
75 lemma subspace_neg_closed [simp, intro?]: |
75 "[| is_subspace U V; is_vectorspace V; x \<in> U |] ==> - x \<in> U" |
76 "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> x \<in> U \<Longrightarrow> - x \<in> U" |
76 by (simp add: negate_eq1) |
77 by (simp add: negate_eq1) |
77 |
78 |
78 text_raw {* \medskip *} |
79 text {* \medskip Further derived laws: every subspace is a vector space. *} |
79 text {* Further derived laws: every subspace is a vector space. *} |
|
80 |
80 |
81 lemma subspace_vs [intro?]: |
81 lemma subspace_vs [intro?]: |
82 "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U" |
82 "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> is_vectorspace U" |
83 proof - |
83 proof - |
84 assume "is_subspace U V" "is_vectorspace V" |
84 assume "is_subspace U V" "is_vectorspace V" |
85 show ?thesis |
85 show ?thesis |
86 proof |
86 proof |
87 show "0 \<in> U" .. |
87 show "0 \<in> U" .. |
88 show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" by (simp!) |
88 show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" by (simp!) |
89 show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" by (simp!) |
89 show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" by (simp!) |
90 show "\<forall>x \<in> U. - x = -#1 \<cdot> x" by (simp! add: negate_eq1) |
90 show "\<forall>x \<in> U. - x = -#1 \<cdot> x" by (simp! add: negate_eq1) |
91 show "\<forall>x \<in> U. \<forall>y \<in> U. x - y = x + - y" |
91 show "\<forall>x \<in> U. \<forall>y \<in> U. x - y = x + - y" |
92 by (simp! add: diff_eq1) |
92 by (simp! add: diff_eq1) |
93 qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+ |
93 qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+ |
94 qed |
94 qed |
95 |
95 |
96 text {* The subspace relation is reflexive. *} |
96 text {* The subspace relation is reflexive. *} |
97 |
97 |
98 lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V" |
98 lemma subspace_refl [intro]: "is_vectorspace V \<Longrightarrow> is_subspace V V" |
99 proof |
99 proof |
100 assume "is_vectorspace V" |
100 assume "is_vectorspace V" |
101 show "0 \<in> V" .. |
101 show "0 \<in> V" .. |
102 show "V <= V" .. |
102 show "V \<subseteq> V" .. |
103 show "\<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V" by (simp!) |
103 show "\<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V" by (simp!) |
104 show "\<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V" by (simp!) |
104 show "\<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V" by (simp!) |
105 qed |
105 qed |
106 |
106 |
107 text {* The subspace relation is transitive. *} |
107 text {* The subspace relation is transitive. *} |
108 |
108 |
109 lemma subspace_trans: |
109 lemma subspace_trans: |
110 "[| is_subspace U V; is_vectorspace V; is_subspace V W |] |
110 "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> is_subspace V W |
111 ==> is_subspace U W" |
111 \<Longrightarrow> is_subspace U W" |
112 proof |
112 proof |
113 assume "is_subspace U V" "is_subspace V W" "is_vectorspace V" |
113 assume "is_subspace U V" "is_subspace V W" "is_vectorspace V" |
114 show "0 \<in> U" .. |
114 show "0 \<in> U" .. |
115 |
115 |
116 have "U <= V" .. |
116 have "U \<subseteq> V" .. |
117 also have "V <= W" .. |
117 also have "V \<subseteq> W" .. |
118 finally show "U <= W" . |
118 finally show "U \<subseteq> W" . |
119 |
119 |
120 show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" |
120 show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" |
121 proof (intro ballI) |
121 proof (intro ballI) |
122 fix x y assume "x \<in> U" "y \<in> U" |
122 fix x y assume "x \<in> U" "y \<in> U" |
123 show "x + y \<in> U" by (simp!) |
123 show "x + y \<in> U" by (simp!) |
124 qed |
124 qed |
125 |
125 |
126 show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" |
126 show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" |
127 proof (intro ballI allI) |
127 proof (intro ballI allI) |
132 |
132 |
133 |
133 |
134 |
134 |
135 subsection {* Linear closure *} |
135 subsection {* Linear closure *} |
136 |
136 |
137 text {* The \emph{linear closure} of a vector $x$ is the set of all |
137 text {* |
138 scalar multiples of $x$. *} |
138 The \emph{linear closure} of a vector @{text x} is the set of all |
|
139 scalar multiples of @{text x}. |
|
140 *} |
139 |
141 |
140 constdefs |
142 constdefs |
141 lin :: "('a::{minus,plus,zero}) => 'a set" |
143 lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set" |
142 "lin x == {a \<cdot> x | a. True}" |
144 "lin x \<equiv> {a \<cdot> x | a. True}" |
143 |
145 |
144 lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)" |
146 lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)" |
145 by (unfold lin_def) fast |
147 by (unfold lin_def) fast |
146 |
148 |
147 lemma linI [intro?]: "a \<cdot> x0 \<in> lin x0" |
149 lemma linI [intro?]: "a \<cdot> x0 \<in> lin x0" |
148 by (unfold lin_def) fast |
150 by (unfold lin_def) fast |
149 |
151 |
150 text {* Every vector is contained in its linear closure. *} |
152 text {* Every vector is contained in its linear closure. *} |
151 |
153 |
152 lemma x_lin_x: "[| is_vectorspace V; x \<in> V |] ==> x \<in> lin x" |
154 lemma x_lin_x: "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x \<in> lin x" |
153 proof (unfold lin_def, intro CollectI exI conjI) |
155 proof (unfold lin_def, intro CollectI exI conjI) |
154 assume "is_vectorspace V" "x \<in> V" |
156 assume "is_vectorspace V" "x \<in> V" |
155 show "x = #1 \<cdot> x" by (simp!) |
157 show "x = #1 \<cdot> x" by (simp!) |
156 qed simp |
158 qed simp |
157 |
159 |
158 text {* Any linear closure is a subspace. *} |
160 text {* Any linear closure is a subspace. *} |
159 |
161 |
160 lemma lin_subspace [intro?]: |
162 lemma lin_subspace [intro?]: |
161 "[| is_vectorspace V; x \<in> V |] ==> is_subspace (lin x) V" |
163 "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> is_subspace (lin x) V" |
162 proof |
164 proof |
163 assume "is_vectorspace V" "x \<in> V" |
165 assume "is_vectorspace V" "x \<in> V" |
164 show "0 \<in> lin x" |
166 show "0 \<in> lin x" |
165 proof (unfold lin_def, intro CollectI exI conjI) |
167 proof (unfold lin_def, intro CollectI exI conjI) |
166 show "0 = (#0::real) \<cdot> x" by (simp!) |
168 show "0 = (#0::real) \<cdot> x" by (simp!) |
167 qed simp |
169 qed simp |
168 |
170 |
169 show "lin x <= V" |
171 show "lin x \<subseteq> V" |
170 proof (unfold lin_def, intro subsetI, elim CollectE exE conjE) |
172 proof (unfold lin_def, intro subsetI, elim CollectE exE conjE) |
171 fix xa a assume "xa = a \<cdot> x" |
173 fix xa a assume "xa = a \<cdot> x" |
172 show "xa \<in> V" by (simp!) |
174 show "xa \<in> V" by (simp!) |
173 qed |
175 qed |
174 |
176 |
175 show "\<forall>x1 \<in> lin x. \<forall>x2 \<in> lin x. x1 + x2 \<in> lin x" |
177 show "\<forall>x1 \<in> lin x. \<forall>x2 \<in> lin x. x1 + x2 \<in> lin x" |
176 proof (intro ballI) |
178 proof (intro ballI) |
177 fix x1 x2 assume "x1 \<in> lin x" "x2 \<in> lin x" |
179 fix x1 x2 assume "x1 \<in> lin x" "x2 \<in> lin x" |
178 thus "x1 + x2 \<in> lin x" |
180 thus "x1 + x2 \<in> lin x" |
179 proof (unfold lin_def, elim CollectE exE conjE, |
181 proof (unfold lin_def, elim CollectE exE conjE, |
180 intro CollectI exI conjI) |
182 intro CollectI exI conjI) |
181 fix a1 a2 assume "x1 = a1 \<cdot> x" "x2 = a2 \<cdot> x" |
183 fix a1 a2 assume "x1 = a1 \<cdot> x" "x2 = a2 \<cdot> x" |
182 show "x1 + x2 = (a1 + a2) \<cdot> x" |
184 show "x1 + x2 = (a1 + a2) \<cdot> x" |
183 by (simp! add: vs_add_mult_distrib2) |
185 by (simp! add: vs_add_mult_distrib2) |
184 qed simp |
186 qed simp |
185 qed |
187 qed |
186 |
188 |
187 show "\<forall>xa \<in> lin x. \<forall>a. a \<cdot> xa \<in> lin x" |
189 show "\<forall>xa \<in> lin x. \<forall>a. a \<cdot> xa \<in> lin x" |
188 proof (intro ballI allI) |
190 proof (intro ballI allI) |
189 fix x1 a assume "x1 \<in> lin x" |
191 fix x1 a assume "x1 \<in> lin x" |
190 thus "a \<cdot> x1 \<in> lin x" |
192 thus "a \<cdot> x1 \<in> lin x" |
191 proof (unfold lin_def, elim CollectE exE conjE, |
193 proof (unfold lin_def, elim CollectE exE conjE, |
192 intro CollectI exI conjI) |
194 intro CollectI exI conjI) |
193 fix a1 assume "x1 = a1 \<cdot> x" |
195 fix a1 assume "x1 = a1 \<cdot> x" |
194 show "a \<cdot> x1 = (a * a1) \<cdot> x" by (simp!) |
196 show "a \<cdot> x1 = (a * a1) \<cdot> x" by (simp!) |
195 qed simp |
197 qed simp |
196 qed |
198 qed |
197 qed |
199 qed |
198 |
200 |
199 text {* Any linear closure is a vector space. *} |
201 text {* Any linear closure is a vector space. *} |
200 |
202 |
201 lemma lin_vs [intro?]: |
203 lemma lin_vs [intro?]: |
202 "[| is_vectorspace V; x \<in> V |] ==> is_vectorspace (lin x)" |
204 "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> is_vectorspace (lin x)" |
203 proof (rule subspace_vs) |
205 proof (rule subspace_vs) |
204 assume "is_vectorspace V" "x \<in> V" |
206 assume "is_vectorspace V" "x \<in> V" |
205 show "is_subspace (lin x) V" .. |
207 show "is_subspace (lin x) V" .. |
206 qed |
208 qed |
207 |
209 |
208 |
210 |
209 |
211 |
210 subsection {* Sum of two vectorspaces *} |
212 subsection {* Sum of two vectorspaces *} |
211 |
213 |
212 text {* The \emph{sum} of two vectorspaces $U$ and $V$ is the set of |
214 text {* |
213 all sums of elements from $U$ and $V$. *} |
215 The \emph{sum} of two vectorspaces @{text U} and @{text V} is the |
|
216 set of all sums of elements from @{text U} and @{text V}. |
|
217 *} |
214 |
218 |
215 instance set :: (plus) plus .. |
219 instance set :: (plus) plus .. |
216 |
220 |
217 defs vs_sum_def: |
221 defs (overloaded) |
218 "U + V == {u + v | u v. u \<in> U \<and> v \<in> V}" (*** |
222 vs_sum_def: "U + V \<equiv> {u + v | u v. u \<in> U \<and> v \<in> V}" |
219 |
223 |
220 constdefs |
224 lemma vs_sumD: |
221 vs_sum :: |
|
222 "['a::{plus, minus, zero} set, 'a set] => 'a set" (infixl "+" 65) |
|
223 "vs_sum U V == {x. \<exists>u \<in> U. \<exists>v \<in> V. x = u + v}"; |
|
224 ***) |
|
225 |
|
226 lemma vs_sumD: |
|
227 "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)" |
225 "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)" |
228 by (unfold vs_sum_def) fast |
226 by (unfold vs_sum_def) fast |
229 |
227 |
230 lemmas vs_sumE = vs_sumD [THEN iffD1, elim_format, standard] |
228 lemmas vs_sumE = vs_sumD [THEN iffD1, elim_format, standard] |
231 |
229 |
232 lemma vs_sumI [intro?]: |
230 lemma vs_sumI [intro?]: |
233 "[| x \<in> U; y \<in> V; t= x + y |] ==> t \<in> U + V" |
231 "x \<in> U \<Longrightarrow> y \<in> V \<Longrightarrow> t = x + y \<Longrightarrow> t \<in> U + V" |
234 by (unfold vs_sum_def) fast |
232 by (unfold vs_sum_def) fast |
235 |
233 |
236 text{* $U$ is a subspace of $U + V$. *} |
234 text {* @{text U} is a subspace of @{text "U + V"}. *} |
237 |
235 |
238 lemma subspace_vs_sum1 [intro?]: |
236 lemma subspace_vs_sum1 [intro?]: |
239 "[| is_vectorspace U; is_vectorspace V |] |
237 "is_vectorspace U \<Longrightarrow> is_vectorspace V |
240 ==> is_subspace U (U + V)" |
238 \<Longrightarrow> is_subspace U (U + V)" |
241 proof |
239 proof |
242 assume "is_vectorspace U" "is_vectorspace V" |
240 assume "is_vectorspace U" "is_vectorspace V" |
243 show "0 \<in> U" .. |
241 show "0 \<in> U" .. |
244 show "U <= U + V" |
242 show "U \<subseteq> U + V" |
245 proof (intro subsetI vs_sumI) |
243 proof (intro subsetI vs_sumI) |
246 fix x assume "x \<in> U" |
244 fix x assume "x \<in> U" |
247 show "x = x + 0" by (simp!) |
245 show "x = x + 0" by (simp!) |
248 show "0 \<in> V" by (simp!) |
246 show "0 \<in> V" by (simp!) |
249 qed |
247 qed |
250 show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" |
248 show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" |
251 proof (intro ballI) |
249 proof (intro ballI) |
252 fix x y assume "x \<in> U" "y \<in> U" show "x + y \<in> U" by (simp!) |
250 fix x y assume "x \<in> U" "y \<in> U" show "x + y \<in> U" by (simp!) |
253 qed |
251 qed |
254 show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" |
252 show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" |
255 proof (intro ballI allI) |
253 proof (intro ballI allI) |
256 fix x a assume "x \<in> U" show "a \<cdot> x \<in> U" by (simp!) |
254 fix x a assume "x \<in> U" show "a \<cdot> x \<in> U" by (simp!) |
257 qed |
255 qed |
258 qed |
256 qed |
259 |
257 |
260 text{* The sum of two subspaces is again a subspace.*} |
258 text{* The sum of two subspaces is again a subspace.*} |
261 |
259 |
262 lemma vs_sum_subspace [intro?]: |
260 lemma vs_sum_subspace [intro?]: |
263 "[| is_subspace U E; is_subspace V E; is_vectorspace E |] |
261 "is_subspace U E \<Longrightarrow> is_subspace V E \<Longrightarrow> is_vectorspace E |
264 ==> is_subspace (U + V) E" |
262 \<Longrightarrow> is_subspace (U + V) E" |
265 proof |
263 proof |
266 assume "is_subspace U E" "is_subspace V E" "is_vectorspace E" |
264 assume "is_subspace U E" "is_subspace V E" "is_vectorspace E" |
267 show "0 \<in> U + V" |
265 show "0 \<in> U + V" |
268 proof (intro vs_sumI) |
266 proof (intro vs_sumI) |
269 show "0 \<in> U" .. |
267 show "0 \<in> U" .. |
270 show "0 \<in> V" .. |
268 show "0 \<in> V" .. |
271 show "(0::'a) = 0 + 0" by (simp!) |
269 show "(0::'a) = 0 + 0" by (simp!) |
272 qed |
270 qed |
273 |
271 |
274 show "U + V <= E" |
272 show "U + V \<subseteq> E" |
275 proof (intro subsetI, elim vs_sumE bexE) |
273 proof (intro subsetI, elim vs_sumE bexE) |
276 fix x u v assume "u \<in> U" "v \<in> V" "x = u + v" |
274 fix x u v assume "u \<in> U" "v \<in> V" "x = u + v" |
277 show "x \<in> E" by (simp!) |
275 show "x \<in> E" by (simp!) |
278 qed |
276 qed |
279 |
277 |
280 show "\<forall>x \<in> U + V. \<forall>y \<in> U + V. x + y \<in> U + V" |
278 show "\<forall>x \<in> U + V. \<forall>y \<in> U + V. x + y \<in> U + V" |
281 proof (intro ballI) |
279 proof (intro ballI) |
282 fix x y assume "x \<in> U + V" "y \<in> U + V" |
280 fix x y assume "x \<in> U + V" "y \<in> U + V" |
283 thus "x + y \<in> U + V" |
281 thus "x + y \<in> U + V" |
284 proof (elim vs_sumE bexE, intro vs_sumI) |
282 proof (elim vs_sumE bexE, intro vs_sumI) |
285 fix ux vx uy vy |
283 fix ux vx uy vy |
286 assume "ux \<in> U" "vx \<in> V" "x = ux + vx" |
284 assume "ux \<in> U" "vx \<in> V" "x = ux + vx" |
287 and "uy \<in> U" "vy \<in> V" "y = uy + vy" |
285 and "uy \<in> U" "vy \<in> V" "y = uy + vy" |
288 show "x + y = (ux + uy) + (vx + vy)" by (simp!) |
286 show "x + y = (ux + uy) + (vx + vy)" by (simp!) |
289 qed (simp!)+ |
287 qed (simp_all!) |
290 qed |
288 qed |
291 |
289 |
292 show "\<forall>x \<in> U + V. \<forall>a. a \<cdot> x \<in> U + V" |
290 show "\<forall>x \<in> U + V. \<forall>a. a \<cdot> x \<in> U + V" |
293 proof (intro ballI allI) |
291 proof (intro ballI allI) |
294 fix x a assume "x \<in> U + V" |
292 fix x a assume "x \<in> U + V" |
295 thus "a \<cdot> x \<in> U + V" |
293 thus "a \<cdot> x \<in> U + V" |
296 proof (elim vs_sumE bexE, intro vs_sumI) |
294 proof (elim vs_sumE bexE, intro vs_sumI) |
297 fix a x u v assume "u \<in> U" "v \<in> V" "x = u + v" |
295 fix a x u v assume "u \<in> U" "v \<in> V" "x = u + v" |
298 show "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" |
296 show "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" |
299 by (simp! add: vs_add_mult_distrib1) |
297 by (simp! add: vs_add_mult_distrib1) |
300 qed (simp!)+ |
298 qed (simp_all!) |
301 qed |
299 qed |
302 qed |
300 qed |
303 |
301 |
304 text{* The sum of two subspaces is a vectorspace. *} |
302 text{* The sum of two subspaces is a vectorspace. *} |
305 |
303 |
306 lemma vs_sum_vs [intro?]: |
304 lemma vs_sum_vs [intro?]: |
307 "[| is_subspace U E; is_subspace V E; is_vectorspace E |] |
305 "is_subspace U E \<Longrightarrow> is_subspace V E \<Longrightarrow> is_vectorspace E |
308 ==> is_vectorspace (U + V)" |
306 \<Longrightarrow> is_vectorspace (U + V)" |
309 proof (rule subspace_vs) |
307 proof (rule subspace_vs) |
310 assume "is_subspace U E" "is_subspace V E" "is_vectorspace E" |
308 assume "is_subspace U E" "is_subspace V E" "is_vectorspace E" |
311 show "is_subspace (U + V) E" .. |
309 show "is_subspace (U + V) E" .. |
312 qed |
310 qed |
313 |
311 |
314 |
312 |
315 |
313 |
316 subsection {* Direct sums *} |
314 subsection {* Direct sums *} |
317 |
315 |
318 |
316 |
319 text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero |
317 text {* |
320 element is the only common element of $U$ and $V$. For every element |
318 The sum of @{text U} and @{text V} is called \emph{direct}, iff the |
321 $x$ of the direct sum of $U$ and $V$ the decomposition in |
319 zero element is the only common element of @{text U} and @{text |
322 $x = u + v$ with $u \in U$ and $v \in V$ is unique.*} |
320 V}. For every element @{text x} of the direct sum of @{text U} and |
323 |
321 @{text V} the decomposition in @{text "x = u + v"} with |
324 lemma decomp: |
322 @{text "u \<in> U"} and @{text "v \<in> V"} is unique. |
325 "[| is_vectorspace E; is_subspace U E; is_subspace V E; |
323 *} |
326 U \<inter> V = {0}; u1 \<in> U; u2 \<in> U; v1 \<in> V; v2 \<in> V; u1 + v1 = u2 + v2 |] |
324 |
327 ==> u1 = u2 \<and> v1 = v2" |
325 lemma decomp: |
328 proof |
326 "is_vectorspace E \<Longrightarrow> is_subspace U E \<Longrightarrow> is_subspace V E \<Longrightarrow> |
329 assume "is_vectorspace E" "is_subspace U E" "is_subspace V E" |
327 U \<inter> V = {0} \<Longrightarrow> u1 \<in> U \<Longrightarrow> u2 \<in> U \<Longrightarrow> v1 \<in> V \<Longrightarrow> v2 \<in> V \<Longrightarrow> |
330 "U \<inter> V = {0}" "u1 \<in> U" "u2 \<in> U" "v1 \<in> V" "v2 \<in> V" |
328 u1 + v1 = u2 + v2 \<Longrightarrow> u1 = u2 \<and> v1 = v2" |
331 "u1 + v1 = u2 + v2" |
329 proof |
|
330 assume "is_vectorspace E" "is_subspace U E" "is_subspace V E" |
|
331 "U \<inter> V = {0}" "u1 \<in> U" "u2 \<in> U" "v1 \<in> V" "v2 \<in> V" |
|
332 "u1 + v1 = u2 + v2" |
332 have eq: "u1 - u2 = v2 - v1" by (simp! add: vs_add_diff_swap) |
333 have eq: "u1 - u2 = v2 - v1" by (simp! add: vs_add_diff_swap) |
333 have u: "u1 - u2 \<in> U" by (simp!) |
334 have u: "u1 - u2 \<in> U" by (simp!) |
334 with eq have v': "v2 - v1 \<in> U" by simp |
335 with eq have v': "v2 - v1 \<in> U" by simp |
335 have v: "v2 - v1 \<in> V" by (simp!) |
336 have v: "v2 - v1 \<in> V" by (simp!) |
336 with eq have u': "u1 - u2 \<in> V" by simp |
337 with eq have u': "u1 - u2 \<in> V" by simp |
337 |
338 |
338 show "u1 = u2" |
339 show "u1 = u2" |
339 proof (rule vs_add_minus_eq) |
340 proof (rule vs_add_minus_eq) |
340 show "u1 - u2 = 0" by (rule Int_singletonD [OF _ u u']) |
341 show "u1 - u2 = 0" by (rule Int_singletonD [OF _ u u']) |
341 show "u1 \<in> E" .. |
342 show "u1 \<in> E" .. |
342 show "u2 \<in> E" .. |
343 show "u2 \<in> E" .. |
343 qed |
344 qed |
344 |
345 |
345 show "v1 = v2" |
346 show "v1 = v2" |
348 show "v1 \<in> E" .. |
349 show "v1 \<in> E" .. |
349 show "v2 \<in> E" .. |
350 show "v2 \<in> E" .. |
350 qed |
351 qed |
351 qed |
352 qed |
352 |
353 |
353 text {* An application of the previous lemma will be used in the proof |
354 text {* |
354 of the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any |
355 An application of the previous lemma will be used in the proof of |
355 element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and |
356 the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any |
356 the linear closure of $x_0$ the components $y \in H$ and $a$ are |
357 element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a |
357 uniquely determined. *} |
358 vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"} |
358 |
359 the components @{text "y \<in> H"} and @{text a} are uniquely |
359 lemma decomp_H': |
360 determined. |
360 "[| is_vectorspace E; is_subspace H E; y1 \<in> H; y2 \<in> H; |
361 *} |
361 x' \<notin> H; x' \<in> E; x' \<noteq> 0; y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x' |] |
362 |
362 ==> y1 = y2 \<and> a1 = a2" |
363 lemma decomp_H': |
|
364 "is_vectorspace E \<Longrightarrow> is_subspace H E \<Longrightarrow> y1 \<in> H \<Longrightarrow> y2 \<in> H \<Longrightarrow> |
|
365 x' \<notin> H \<Longrightarrow> x' \<in> E \<Longrightarrow> x' \<noteq> 0 \<Longrightarrow> y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x' |
|
366 \<Longrightarrow> y1 = y2 \<and> a1 = a2" |
363 proof |
367 proof |
364 assume "is_vectorspace E" and h: "is_subspace H E" |
368 assume "is_vectorspace E" and h: "is_subspace H E" |
365 and "y1 \<in> H" "y2 \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" |
369 and "y1 \<in> H" "y2 \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" |
366 "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'" |
370 "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'" |
367 |
371 |
368 have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'" |
372 have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'" |
369 proof (rule decomp) |
373 proof (rule decomp) |
370 show "a1 \<cdot> x' \<in> lin x'" .. |
374 show "a1 \<cdot> x' \<in> lin x'" .. |
371 show "a2 \<cdot> x' \<in> lin x'" .. |
375 show "a2 \<cdot> x' \<in> lin x'" .. |
372 show "H \<inter> (lin x') = {0}" |
376 show "H \<inter> (lin x') = {0}" |
373 proof |
377 proof |
374 show "H \<inter> lin x' <= {0}" |
378 show "H \<inter> lin x' \<subseteq> {0}" |
375 proof (intro subsetI, elim IntE, rule singleton_iff [THEN iffD2]) |
379 proof (intro subsetI, elim IntE, rule singleton_iff [THEN iffD2]) |
376 fix x assume "x \<in> H" "x \<in> lin x'" |
380 fix x assume "x \<in> H" "x \<in> lin x'" |
377 thus "x = 0" |
381 thus "x = 0" |
378 proof (unfold lin_def, elim CollectE exE conjE) |
382 proof (unfold lin_def, elim CollectE exE conjE) |
379 fix a assume "x = a \<cdot> x'" |
383 fix a assume "x = a \<cdot> x'" |
380 show ?thesis |
384 show ?thesis |
381 proof cases |
385 proof cases |
382 assume "a = (#0::real)" show ?thesis by (simp!) |
386 assume "a = (#0::real)" show ?thesis by (simp!) |
383 next |
387 next |
384 assume "a \<noteq> (#0::real)" |
388 assume "a \<noteq> (#0::real)" |
385 from h have "inverse a \<cdot> a \<cdot> x' \<in> H" |
389 from h have "inverse a \<cdot> a \<cdot> x' \<in> H" |
386 by (rule subspace_mult_closed) (simp!) |
390 by (rule subspace_mult_closed) (simp!) |
387 also have "inverse a \<cdot> a \<cdot> x' = x'" by (simp!) |
391 also have "inverse a \<cdot> a \<cdot> x' = x'" by (simp!) |
388 finally have "x' \<in> H" . |
392 finally have "x' \<in> H" . |
389 thus ?thesis by contradiction |
393 thus ?thesis by contradiction |
390 qed |
394 qed |
391 qed |
395 qed |
392 qed |
396 qed |
393 show "{0} <= H \<inter> lin x'" |
397 show "{0} \<subseteq> H \<inter> lin x'" |
394 proof - |
398 proof - |
395 have "0 \<in> H \<inter> lin x'" |
399 have "0 \<in> H \<inter> lin x'" |
396 proof (rule IntI) |
400 proof (rule IntI) |
397 show "0 \<in> H" .. |
401 show "0 \<in> H" .. |
398 from lin_vs show "0 \<in> lin x'" .. |
402 from lin_vs show "0 \<in> lin x'" .. |
399 qed |
403 qed |
400 thus ?thesis by simp |
404 thus ?thesis by simp |
401 qed |
405 qed |
402 qed |
406 qed |
403 show "is_subspace (lin x') E" .. |
407 show "is_subspace (lin x') E" .. |
404 qed |
408 qed |
405 |
409 |
406 from c show "y1 = y2" by simp |
410 from c show "y1 = y2" by simp |
407 |
411 |
408 show "a1 = a2" |
412 show "a1 = a2" |
409 proof (rule vs_mult_right_cancel [THEN iffD1]) |
413 proof (rule vs_mult_right_cancel [THEN iffD1]) |
410 from c show "a1 \<cdot> x' = a2 \<cdot> x'" by simp |
414 from c show "a1 \<cdot> x' = a2 \<cdot> x'" by simp |
411 qed |
415 qed |
412 qed |
416 qed |
413 |
417 |
414 text {* Since for any element $y + a \mult x'$ of the direct sum |
418 text {* |
415 of a vectorspace $H$ and the linear closure of $x'$ the components |
419 Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a |
416 $y\in H$ and $a$ are unique, it follows from $y\in H$ that |
420 vectorspace @{text H} and the linear closure of @{text x'} the |
417 $a = 0$.*} |
421 components @{text "y \<in> H"} and @{text a} are unique, it follows from |
418 |
422 @{text "y \<in> H"} that @{text "a = 0"}. |
419 lemma decomp_H'_H: |
423 *} |
420 "[| is_vectorspace E; is_subspace H E; t \<in> H; x' \<notin> H; x' \<in> E; |
424 |
421 x' \<noteq> 0 |] |
425 lemma decomp_H'_H: |
422 ==> (SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, (#0::real))" |
426 "is_vectorspace E \<Longrightarrow> is_subspace H E \<Longrightarrow> t \<in> H \<Longrightarrow> x' \<notin> H \<Longrightarrow> x' \<in> E |
|
427 \<Longrightarrow> x' \<noteq> 0 |
|
428 \<Longrightarrow> (SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, (#0::real))" |
423 proof (rule, unfold split_tupled_all) |
429 proof (rule, unfold split_tupled_all) |
424 assume "is_vectorspace E" "is_subspace H E" "t \<in> H" "x' \<notin> H" "x' \<in> E" |
430 assume "is_vectorspace E" "is_subspace H E" "t \<in> H" "x' \<notin> H" "x' \<in> E" |
425 "x' \<noteq> 0" |
431 "x' \<noteq> 0" |
426 have h: "is_vectorspace H" .. |
432 have h: "is_vectorspace H" .. |
427 fix y a presume t1: "t = y + a \<cdot> x'" and "y \<in> H" |
433 fix y a presume t1: "t = y + a \<cdot> x'" and "y \<in> H" |
428 have "y = t \<and> a = (#0::real)" |
434 have "y = t \<and> a = (#0::real)" |
429 by (rule decomp_H') (assumption | (simp!))+ |
435 by (rule decomp_H') (auto!) |
430 thus "(y, a) = (t, (#0::real))" by (simp!) |
436 thus "(y, a) = (t, (#0::real))" by (simp!) |
431 qed (simp!)+ |
437 qed (simp_all!) |
432 |
438 |
433 text {* The components $y\in H$ and $a$ in $y \plus a \mult x'$ |
439 text {* |
434 are unique, so the function $h'$ defined by |
440 The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"} |
435 $h' (y \plus a \mult x') = h y + a \cdot \xi$ is definite. *} |
441 are unique, so the function @{text h'} defined by |
|
442 @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite. |
|
443 *} |
436 |
444 |
437 lemma h'_definite: |
445 lemma h'_definite: |
438 "[| h' == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H) |
446 "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H) |
439 in (h y) + a * xi); |
447 in (h y) + a * xi) \<Longrightarrow> |
440 x = y + a \<cdot> x'; is_vectorspace E; is_subspace H E; |
448 x = y + a \<cdot> x' \<Longrightarrow> is_vectorspace E \<Longrightarrow> is_subspace H E \<Longrightarrow> |
441 y \<in> H; x' \<notin> H; x' \<in> E; x' \<noteq> 0 |] |
449 y \<in> H \<Longrightarrow> x' \<notin> H \<Longrightarrow> x' \<in> E \<Longrightarrow> x' \<noteq> 0 |
442 ==> h' x = h y + a * xi" |
450 \<Longrightarrow> h' x = h y + a * xi" |
443 proof - |
451 proof - |
444 assume |
452 assume |
445 "h' == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H) |
453 "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H) |
446 in (h y) + a * xi)" |
454 in (h y) + a * xi)" |
447 "x = y + a \<cdot> x'" "is_vectorspace E" "is_subspace H E" |
455 "x = y + a \<cdot> x'" "is_vectorspace E" "is_subspace H E" |
448 "y \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" |
456 "y \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" |
449 have "x \<in> H + (lin x')" |
457 hence "x \<in> H + (lin x')" |
450 by (simp! add: vs_sum_def lin_def) force+ |
458 by (auto simp add: vs_sum_def lin_def) |
451 have "\<exists>! xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)" |
459 have "\<exists>! xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)" |
452 proof |
460 proof |
453 show "\<exists>xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)" |
461 show "\<exists>xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)" |
454 by (force!) |
462 by (blast!) |
455 next |
463 next |
456 fix xa ya |
464 fix xa ya |
457 assume "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) xa" |
465 assume "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) xa" |
458 "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) ya" |
466 "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) ya" |
459 show "xa = ya" |
467 show "xa = ya" |
460 proof - |
468 proof - |
461 show "fst xa = fst ya \<and> snd xa = snd ya ==> xa = ya" |
469 show "fst xa = fst ya \<and> snd xa = snd ya \<Longrightarrow> xa = ya" |
462 by (simp add: Pair_fst_snd_eq) |
470 by (simp add: Pair_fst_snd_eq) |
463 have x: "x = fst xa + snd xa \<cdot> x' \<and> fst xa \<in> H" |
471 have x: "x = fst xa + snd xa \<cdot> x' \<and> fst xa \<in> H" |
464 by (force!) |
472 by (auto!) |
465 have y: "x = fst ya + snd ya \<cdot> x' \<and> fst ya \<in> H" |
473 have y: "x = fst ya + snd ya \<cdot> x' \<and> fst ya \<in> H" |
466 by (force!) |
474 by (auto!) |
467 from x y show "fst xa = fst ya \<and> snd xa = snd ya" |
475 from x y show "fst xa = fst ya \<and> snd xa = snd ya" |
468 by (elim conjE) (rule decomp_H', (simp!)+) |
476 by (elim conjE) (rule decomp_H', (simp!)+) |
469 qed |
477 qed |
470 qed |
478 qed |
471 hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" |
479 hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" |
472 by (rule some1_equality) (force!) |
480 by (rule some1_equality) (blast!) |
473 thus "h' x = h y + a * xi" by (simp! add: Let_def) |
481 thus "h' x = h y + a * xi" by (simp! add: Let_def) |
474 qed |
482 qed |
475 |
483 |
476 end |
484 end |