1 (* Title: HOL/Hahn_Banach/Subspace.thy |
1 (* Title: HOL/Hahn_Banach/Subspace.thy |
2 Author: Gertrud Bauer, TU Munich |
2 Author: Gertrud Bauer, TU Munich |
3 *) |
3 *) |
4 |
4 |
5 header {* Subspaces *} |
5 header \<open>Subspaces\<close> |
6 |
6 |
7 theory Subspace |
7 theory Subspace |
8 imports Vector_Space "~~/src/HOL/Library/Set_Algebras" |
8 imports Vector_Space "~~/src/HOL/Library/Set_Algebras" |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Definition *} |
11 subsection \<open>Definition\<close> |
12 |
12 |
13 text {* |
13 text \<open> |
14 A non-empty subset @{text U} of a vector space @{text V} is a |
14 A non-empty subset @{text U} of a vector space @{text V} is a |
15 \emph{subspace} of @{text V}, iff @{text U} is closed under addition |
15 \emph{subspace} of @{text V}, iff @{text U} is closed under addition |
16 and scalar multiplication. |
16 and scalar multiplication. |
17 *} |
17 \<close> |
18 |
18 |
19 locale subspace = |
19 locale subspace = |
20 fixes U :: "'a\<Colon>{minus, plus, zero, uminus} set" and V |
20 fixes U :: "'a\<Colon>{minus, plus, zero, uminus} set" and V |
21 assumes non_empty [iff, intro]: "U \<noteq> {}" |
21 assumes non_empty [iff, intro]: "U \<noteq> {}" |
22 and subset [iff]: "U \<subseteq> V" |
22 and subset [iff]: "U \<subseteq> V" |
47 proof - |
47 proof - |
48 interpret vectorspace V by fact |
48 interpret vectorspace V by fact |
49 from x y show ?thesis by (simp add: diff_eq1 negate_eq1) |
49 from x y show ?thesis by (simp add: diff_eq1 negate_eq1) |
50 qed |
50 qed |
51 |
51 |
52 text {* |
52 text \<open> |
53 \medskip Similar as for linear spaces, the existence of the zero |
53 \medskip Similar as for linear spaces, the existence of the zero |
54 element in every subspace follows from the non-emptiness of the |
54 element in every subspace follows from the non-emptiness of the |
55 carrier set and by vector space laws. |
55 carrier set and by vector space laws. |
56 *} |
56 \<close> |
57 |
57 |
58 lemma (in subspace) zero [intro]: |
58 lemma (in subspace) zero [intro]: |
59 assumes "vectorspace V" |
59 assumes "vectorspace V" |
60 shows "0 \<in> U" |
60 shows "0 \<in> U" |
61 proof - |
61 proof - |
62 interpret V: vectorspace V by fact |
62 interpret V: vectorspace V by fact |
63 have "U \<noteq> {}" by (rule non_empty) |
63 have "U \<noteq> {}" by (rule non_empty) |
64 then obtain x where x: "x \<in> U" by blast |
64 then obtain x where x: "x \<in> U" by blast |
65 then have "x \<in> V" .. then have "0 = x - x" by simp |
65 then have "x \<in> V" .. then have "0 = x - x" by simp |
66 also from `vectorspace V` x x have "\<dots> \<in> U" by (rule diff_closed) |
66 also from \<open>vectorspace V\<close> x x have "\<dots> \<in> U" by (rule diff_closed) |
67 finally show ?thesis . |
67 finally show ?thesis . |
68 qed |
68 qed |
69 |
69 |
70 lemma (in subspace) neg_closed [iff]: |
70 lemma (in subspace) neg_closed [iff]: |
71 assumes "vectorspace V" |
71 assumes "vectorspace V" |
74 proof - |
74 proof - |
75 interpret vectorspace V by fact |
75 interpret vectorspace V by fact |
76 from x show ?thesis by (simp add: negate_eq1) |
76 from x show ?thesis by (simp add: negate_eq1) |
77 qed |
77 qed |
78 |
78 |
79 text {* \medskip Further derived laws: every subspace is a vector space. *} |
79 text \<open>\medskip Further derived laws: every subspace is a vector space.\<close> |
80 |
80 |
81 lemma (in subspace) vectorspace [iff]: |
81 lemma (in subspace) vectorspace [iff]: |
82 assumes "vectorspace V" |
82 assumes "vectorspace V" |
83 shows "vectorspace U" |
83 shows "vectorspace U" |
84 proof - |
84 proof - |
115 fix a :: real |
115 fix a :: real |
116 from x y show "x + y \<in> V" by simp |
116 from x y show "x + y \<in> V" by simp |
117 from x show "a \<cdot> x \<in> V" by simp |
117 from x show "a \<cdot> x \<in> V" by simp |
118 qed |
118 qed |
119 |
119 |
120 text {* The subspace relation is transitive. *} |
120 text \<open>The subspace relation is transitive.\<close> |
121 |
121 |
122 lemma (in vectorspace) subspace_trans [trans]: |
122 lemma (in vectorspace) subspace_trans [trans]: |
123 "U \<unlhd> V \<Longrightarrow> V \<unlhd> W \<Longrightarrow> U \<unlhd> W" |
123 "U \<unlhd> V \<Longrightarrow> V \<unlhd> W \<Longrightarrow> U \<unlhd> W" |
124 proof |
124 proof |
125 assume uv: "U \<unlhd> V" and vw: "V \<unlhd> W" |
125 assume uv: "U \<unlhd> V" and vw: "V \<unlhd> W" |
134 from uv and x y show "x + y \<in> U" by (rule subspace.add_closed) |
134 from uv and x y show "x + y \<in> U" by (rule subspace.add_closed) |
135 from uv and x show "\<And>a. a \<cdot> x \<in> U" by (rule subspace.mult_closed) |
135 from uv and x show "\<And>a. a \<cdot> x \<in> U" by (rule subspace.mult_closed) |
136 qed |
136 qed |
137 |
137 |
138 |
138 |
139 subsection {* Linear closure *} |
139 subsection \<open>Linear closure\<close> |
140 |
140 |
141 text {* |
141 text \<open> |
142 The \emph{linear closure} of a vector @{text x} is the set of all |
142 The \emph{linear closure} of a vector @{text x} is the set of all |
143 scalar multiples of @{text x}. |
143 scalar multiples of @{text x}. |
144 *} |
144 \<close> |
145 |
145 |
146 definition lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set" |
146 definition lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set" |
147 where "lin x = {a \<cdot> x | a. True}" |
147 where "lin x = {a \<cdot> x | a. True}" |
148 |
148 |
149 lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x" |
149 lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x" |
154 |
154 |
155 lemma linE [elim]: "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C" |
155 lemma linE [elim]: "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C" |
156 unfolding lin_def by blast |
156 unfolding lin_def by blast |
157 |
157 |
158 |
158 |
159 text {* Every vector is contained in its linear closure. *} |
159 text \<open>Every vector is contained in its linear closure.\<close> |
160 |
160 |
161 lemma (in vectorspace) x_lin_x [iff]: "x \<in> V \<Longrightarrow> x \<in> lin x" |
161 lemma (in vectorspace) x_lin_x [iff]: "x \<in> V \<Longrightarrow> x \<in> lin x" |
162 proof - |
162 proof - |
163 assume "x \<in> V" |
163 assume "x \<in> V" |
164 then have "x = 1 \<cdot> x" by simp |
164 then have "x = 1 \<cdot> x" by simp |
206 finally show ?thesis . |
206 finally show ?thesis . |
207 qed |
207 qed |
208 qed |
208 qed |
209 |
209 |
210 |
210 |
211 text {* Any linear closure is a vector space. *} |
211 text \<open>Any linear closure is a vector space.\<close> |
212 |
212 |
213 lemma (in vectorspace) lin_vectorspace [intro]: |
213 lemma (in vectorspace) lin_vectorspace [intro]: |
214 assumes "x \<in> V" |
214 assumes "x \<in> V" |
215 shows "vectorspace (lin x)" |
215 shows "vectorspace (lin x)" |
216 proof - |
216 proof - |
217 from `x \<in> V` have "subspace (lin x) V" |
217 from \<open>x \<in> V\<close> have "subspace (lin x) V" |
218 by (rule lin_subspace) |
218 by (rule lin_subspace) |
219 from this and vectorspace_axioms show ?thesis |
219 from this and vectorspace_axioms show ?thesis |
220 by (rule subspace.vectorspace) |
220 by (rule subspace.vectorspace) |
221 qed |
221 qed |
222 |
222 |
223 |
223 |
224 subsection {* Sum of two vectorspaces *} |
224 subsection \<open>Sum of two vectorspaces\<close> |
225 |
225 |
226 text {* |
226 text \<open> |
227 The \emph{sum} of two vectorspaces @{text U} and @{text V} is the |
227 The \emph{sum} of two vectorspaces @{text U} and @{text V} is the |
228 set of all sums of elements from @{text U} and @{text V}. |
228 set of all sums of elements from @{text U} and @{text V}. |
229 *} |
229 \<close> |
230 |
230 |
231 lemma sum_def: "U + V = {u + v | u v. u \<in> U \<and> v \<in> V}" |
231 lemma sum_def: "U + V = {u + v | u v. u \<in> U \<and> v \<in> V}" |
232 unfolding set_plus_def by auto |
232 unfolding set_plus_def by auto |
233 |
233 |
234 lemma sumE [elim]: |
234 lemma sumE [elim]: |
241 |
241 |
242 lemma sumI' [intro]: |
242 lemma sumI' [intro]: |
243 "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V" |
243 "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V" |
244 unfolding sum_def by blast |
244 unfolding sum_def by blast |
245 |
245 |
246 text {* @{text U} is a subspace of @{text "U + V"}. *} |
246 text \<open>@{text U} is a subspace of @{text "U + V"}.\<close> |
247 |
247 |
248 lemma subspace_sum1 [iff]: |
248 lemma subspace_sum1 [iff]: |
249 assumes "vectorspace U" "vectorspace V" |
249 assumes "vectorspace U" "vectorspace V" |
250 shows "U \<unlhd> U + V" |
250 shows "U \<unlhd> U + V" |
251 proof - |
251 proof - |
265 then show "x + y \<in> U" by simp |
265 then show "x + y \<in> U" by simp |
266 from x show "\<And>a. a \<cdot> x \<in> U" by simp |
266 from x show "\<And>a. a \<cdot> x \<in> U" by simp |
267 qed |
267 qed |
268 qed |
268 qed |
269 |
269 |
270 text {* The sum of two subspaces is again a subspace. *} |
270 text \<open>The sum of two subspaces is again a subspace.\<close> |
271 |
271 |
272 lemma sum_subspace [intro?]: |
272 lemma sum_subspace [intro?]: |
273 assumes "subspace U E" "vectorspace E" "subspace V E" |
273 assumes "subspace U E" "vectorspace E" "subspace V E" |
274 shows "U + V \<unlhd> E" |
274 shows "U + V \<unlhd> E" |
275 proof - |
275 proof - |
278 interpret subspace V E by fact |
278 interpret subspace V E by fact |
279 show ?thesis |
279 show ?thesis |
280 proof |
280 proof |
281 have "0 \<in> U + V" |
281 have "0 \<in> U + V" |
282 proof |
282 proof |
283 show "0 \<in> U" using `vectorspace E` .. |
283 show "0 \<in> U" using \<open>vectorspace E\<close> .. |
284 show "0 \<in> V" using `vectorspace E` .. |
284 show "0 \<in> V" using \<open>vectorspace E\<close> .. |
285 show "(0::'a) = 0 + 0" by simp |
285 show "(0::'a) = 0 + 0" by simp |
286 qed |
286 qed |
287 then show "U + V \<noteq> {}" by blast |
287 then show "U + V \<noteq> {}" by blast |
288 show "U + V \<subseteq> E" |
288 show "U + V \<subseteq> E" |
289 proof |
289 proof |
314 then show ?thesis .. |
314 then show ?thesis .. |
315 qed |
315 qed |
316 qed |
316 qed |
317 qed |
317 qed |
318 |
318 |
319 text{* The sum of two subspaces is a vectorspace. *} |
319 text\<open>The sum of two subspaces is a vectorspace.\<close> |
320 |
320 |
321 lemma sum_vs [intro?]: |
321 lemma sum_vs [intro?]: |
322 "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)" |
322 "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)" |
323 by (rule subspace.vectorspace) (rule sum_subspace) |
323 by (rule subspace.vectorspace) (rule sum_subspace) |
324 |
324 |
325 |
325 |
326 subsection {* Direct sums *} |
326 subsection \<open>Direct sums\<close> |
327 |
327 |
328 text {* |
328 text \<open> |
329 The sum of @{text U} and @{text V} is called \emph{direct}, iff the |
329 The sum of @{text U} and @{text V} is called \emph{direct}, iff the |
330 zero element is the only common element of @{text U} and @{text |
330 zero element is the only common element of @{text U} and @{text |
331 V}. For every element @{text x} of the direct sum of @{text U} and |
331 V}. For every element @{text x} of the direct sum of @{text U} and |
332 @{text V} the decomposition in @{text "x = u + v"} with |
332 @{text V} the decomposition in @{text "x = u + v"} with |
333 @{text "u \<in> U"} and @{text "v \<in> V"} is unique. |
333 @{text "u \<in> U"} and @{text "v \<in> V"} is unique. |
334 *} |
334 \<close> |
335 |
335 |
336 lemma decomp: |
336 lemma decomp: |
337 assumes "vectorspace E" "subspace U E" "subspace V E" |
337 assumes "vectorspace E" "subspace U E" "subspace V E" |
338 assumes direct: "U \<inter> V = {0}" |
338 assumes direct: "U \<inter> V = {0}" |
339 and u1: "u1 \<in> U" and u2: "u2 \<in> U" |
339 and u1: "u1 \<in> U" and u2: "u2 \<in> U" |
345 interpret subspace U E by fact |
345 interpret subspace U E by fact |
346 interpret subspace V E by fact |
346 interpret subspace V E by fact |
347 show ?thesis |
347 show ?thesis |
348 proof |
348 proof |
349 have U: "vectorspace U" (* FIXME: use interpret *) |
349 have U: "vectorspace U" (* FIXME: use interpret *) |
350 using `subspace U E` `vectorspace E` by (rule subspace.vectorspace) |
350 using \<open>subspace U E\<close> \<open>vectorspace E\<close> by (rule subspace.vectorspace) |
351 have V: "vectorspace V" |
351 have V: "vectorspace V" |
352 using `subspace V E` `vectorspace E` by (rule subspace.vectorspace) |
352 using \<open>subspace V E\<close> \<open>vectorspace E\<close> by (rule subspace.vectorspace) |
353 from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1" |
353 from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1" |
354 by (simp add: add_diff_swap) |
354 by (simp add: add_diff_swap) |
355 from u1 u2 have u: "u1 - u2 \<in> U" |
355 from u1 u2 have u: "u1 - u2 \<in> U" |
356 by (rule vectorspace.diff_closed [OF U]) |
356 by (rule vectorspace.diff_closed [OF U]) |
357 with eq have v': "v2 - v1 \<in> U" by (simp only:) |
357 with eq have v': "v2 - v1 \<in> U" by (simp only:) |
372 from v v' and direct show "v2 - v1 = 0" by blast |
372 from v v' and direct show "v2 - v1 = 0" by blast |
373 qed |
373 qed |
374 qed |
374 qed |
375 qed |
375 qed |
376 |
376 |
377 text {* |
377 text \<open> |
378 An application of the previous lemma will be used in the proof of |
378 An application of the previous lemma will be used in the proof of |
379 the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any |
379 the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any |
380 element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a |
380 element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a |
381 vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"} |
381 vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"} |
382 the components @{text "y \<in> H"} and @{text a} are uniquely |
382 the components @{text "y \<in> H"} and @{text a} are uniquely |
383 determined. |
383 determined. |
384 *} |
384 \<close> |
385 |
385 |
386 lemma decomp_H': |
386 lemma decomp_H': |
387 assumes "vectorspace E" "subspace H E" |
387 assumes "vectorspace E" "subspace H E" |
388 assumes y1: "y1 \<in> H" and y2: "y2 \<in> H" |
388 assumes y1: "y1 \<in> H" and y2: "y2 \<in> H" |
389 and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" |
389 and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" |
412 next |
412 next |
413 assume a: "a \<noteq> 0" |
413 assume a: "a \<noteq> 0" |
414 from x have "x \<in> H" .. |
414 from x have "x \<in> H" .. |
415 with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp |
415 with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp |
416 with a and x' have "x' \<in> H" by (simp add: mult_assoc2) |
416 with a and x' have "x' \<in> H" by (simp add: mult_assoc2) |
417 with `x' \<notin> H` show ?thesis by contradiction |
417 with \<open>x' \<notin> H\<close> show ?thesis by contradiction |
418 qed |
418 qed |
419 then show "x \<in> {0}" .. |
419 then show "x \<in> {0}" .. |
420 qed |
420 qed |
421 show "{0} \<subseteq> H \<inter> lin x'" |
421 show "{0} \<subseteq> H \<inter> lin x'" |
422 proof - |
422 proof - |
423 have "0 \<in> H" using `vectorspace E` .. |
423 have "0 \<in> H" using \<open>vectorspace E\<close> .. |
424 moreover have "0 \<in> lin x'" using `x' \<in> E` .. |
424 moreover have "0 \<in> lin x'" using \<open>x' \<in> E\<close> .. |
425 ultimately show ?thesis by blast |
425 ultimately show ?thesis by blast |
426 qed |
426 qed |
427 qed |
427 qed |
428 show "lin x' \<unlhd> E" using `x' \<in> E` .. |
428 show "lin x' \<unlhd> E" using \<open>x' \<in> E\<close> .. |
429 qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq) |
429 qed (rule \<open>vectorspace E\<close>, rule \<open>subspace H E\<close>, rule y1, rule y2, rule eq) |
430 then show "y1 = y2" .. |
430 then show "y1 = y2" .. |
431 from c have "a1 \<cdot> x' = a2 \<cdot> x'" .. |
431 from c have "a1 \<cdot> x' = a2 \<cdot> x'" .. |
432 with x' show "a1 = a2" by (simp add: mult_right_cancel) |
432 with x' show "a1 = a2" by (simp add: mult_right_cancel) |
433 qed |
433 qed |
434 qed |
434 qed |
435 |
435 |
436 text {* |
436 text \<open> |
437 Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a |
437 Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a |
438 vectorspace @{text H} and the linear closure of @{text x'} the |
438 vectorspace @{text H} and the linear closure of @{text x'} the |
439 components @{text "y \<in> H"} and @{text a} are unique, it follows from |
439 components @{text "y \<in> H"} and @{text a} are unique, it follows from |
440 @{text "y \<in> H"} that @{text "a = 0"}. |
440 @{text "y \<in> H"} that @{text "a = 0"}. |
441 *} |
441 \<close> |
442 |
442 |
443 lemma decomp_H'_H: |
443 lemma decomp_H'_H: |
444 assumes "vectorspace E" "subspace H E" |
444 assumes "vectorspace E" "subspace H E" |
445 assumes t: "t \<in> H" |
445 assumes t: "t \<in> H" |
446 and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" |
446 and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" |
454 fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H" |
454 fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H" |
455 have "y = t \<and> a = 0" |
455 have "y = t \<and> a = 0" |
456 proof (rule decomp_H') |
456 proof (rule decomp_H') |
457 from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp |
457 from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp |
458 from ya show "y \<in> H" .. |
458 from ya show "y \<in> H" .. |
459 qed (rule `vectorspace E`, rule `subspace H E`, rule t, (rule x')+) |
459 qed (rule \<open>vectorspace E\<close>, rule \<open>subspace H E\<close>, rule t, (rule x')+) |
460 with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp |
460 with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp |
461 qed |
461 qed |
462 qed |
462 qed |
463 |
463 |
464 text {* |
464 text \<open> |
465 The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"} |
465 The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"} |
466 are unique, so the function @{text h'} defined by |
466 are unique, so the function @{text h'} defined by |
467 @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite. |
467 @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite. |
468 *} |
468 \<close> |
469 |
469 |
470 lemma h'_definite: |
470 lemma h'_definite: |
471 fixes H |
471 fixes H |
472 assumes h'_def: |
472 assumes h'_def: |
473 "h' \<equiv> \<lambda>x. |
473 "h' \<equiv> \<lambda>x. |
496 proof (rule decomp_H') |
496 proof (rule decomp_H') |
497 from xp show "fst p \<in> H" .. |
497 from xp show "fst p \<in> H" .. |
498 from xq show "fst q \<in> H" .. |
498 from xq show "fst q \<in> H" .. |
499 from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'" |
499 from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'" |
500 by simp |
500 by simp |
501 qed (rule `vectorspace E`, rule `subspace H E`, (rule x')+) |
501 qed (rule \<open>vectorspace E\<close>, rule \<open>subspace H E\<close>, (rule x')+) |
502 then show ?thesis by (cases p, cases q) simp |
502 then show ?thesis by (cases p, cases q) simp |
503 qed |
503 qed |
504 qed |
504 qed |
505 then have eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" |
505 then have eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" |
506 by (rule some1_equality) (simp add: x y) |
506 by (rule some1_equality) (simp add: x y) |