src/HOL/Real/HahnBanach/Subspace.thy
 author wenzelm Tue Jul 15 19:39:37 2008 +0200 (2008-07-15) changeset 27612 d3eb431db035 parent 27611 2c01c0bdb385 child 29234 60f7fb56f8cd permissions -rw-r--r--
modernized specifications and proofs;
tuned document;
1 (*  Title:      HOL/Real/HahnBanach/Subspace.thy
2     ID:         $Id$
3     Author:     Gertrud Bauer, TU Munich
4 *)
8 theory Subspace
9 imports VectorSpace
10 begin
12 subsection {* Definition *}
14 text {*
15   A non-empty subset @{text U} of a vector space @{text V} is a
16   \emph{subspace} of @{text V}, iff @{text U} is closed under addition
17   and scalar multiplication.
18 *}
20 locale subspace = var U + var V +
21   constrains U :: "'a\<Colon>{minus, plus, zero, uminus} set"
22   assumes non_empty [iff, intro]: "U \<noteq> {}"
23     and subset [iff]: "U \<subseteq> V"
24     and add_closed [iff]: "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
25     and mult_closed [iff]: "x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
27 notation (symbols)
28   subspace  (infix "\<unlhd>" 50)
30 declare vectorspace.intro [intro?] subspace.intro [intro?]
32 lemma subspace_subset [elim]: "U \<unlhd> V \<Longrightarrow> U \<subseteq> V"
33   by (rule subspace.subset)
35 lemma (in subspace) subsetD [iff]: "x \<in> U \<Longrightarrow> x \<in> V"
36   using subset by blast
38 lemma subspaceD [elim]: "U \<unlhd> V \<Longrightarrow> x \<in> U \<Longrightarrow> x \<in> V"
39   by (rule subspace.subsetD)
41 lemma rev_subspaceD [elim?]: "x \<in> U \<Longrightarrow> U \<unlhd> V \<Longrightarrow> x \<in> V"
42   by (rule subspace.subsetD)
44 lemma (in subspace) diff_closed [iff]:
45   assumes "vectorspace V"
46   assumes x: "x \<in> U" and y: "y \<in> U"
47   shows "x - y \<in> U"
48 proof -
49   interpret vectorspace [V] by fact
50   from x y show ?thesis by (simp add: diff_eq1 negate_eq1)
51 qed
53 text {*
54   \medskip Similar as for linear spaces, the existence of the zero
55   element in every subspace follows from the non-emptiness of the
56   carrier set and by vector space laws.
57 *}
59 lemma (in subspace) zero [intro]:
60   assumes "vectorspace V"
61   shows "0 \<in> U"
62 proof -
63   interpret vectorspace [V] by fact
64   have "U \<noteq> {}" by (rule U_V.non_empty)
65   then obtain x where x: "x \<in> U" by blast
66   then have "x \<in> V" .. then have "0 = x - x" by simp
67   also from vectorspace V x x have "\<dots> \<in> U" by (rule U_V.diff_closed)
68   finally show ?thesis .
69 qed
71 lemma (in subspace) neg_closed [iff]:
72   assumes "vectorspace V"
73   assumes x: "x \<in> U"
74   shows "- x \<in> U"
75 proof -
76   interpret vectorspace [V] by fact
77   from x show ?thesis by (simp add: negate_eq1)
78 qed
80 text {* \medskip Further derived laws: every subspace is a vector space. *}
82 lemma (in subspace) vectorspace [iff]:
83   assumes "vectorspace V"
84   shows "vectorspace U"
85 proof -
86   interpret vectorspace [V] by fact
87   show ?thesis
88   proof
89     show "U \<noteq> {}" ..
90     fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"
91     fix a b :: real
92     from x y show "x + y \<in> U" by simp
93     from x show "a \<cdot> x \<in> U" by simp
94     from x y z show "(x + y) + z = x + (y + z)" by (simp add: add_ac)
95     from x y show "x + y = y + x" by (simp add: add_ac)
96     from x show "x - x = 0" by simp
97     from x show "0 + x = x" by simp
98     from x y show "a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y" by (simp add: distrib)
99     from x show "(a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" by (simp add: distrib)
100     from x show "(a * b) \<cdot> x = a \<cdot> b \<cdot> x" by (simp add: mult_assoc)
101     from x show "1 \<cdot> x = x" by simp
102     from x show "- x = - 1 \<cdot> x" by (simp add: negate_eq1)
103     from x y show "x - y = x + - y" by (simp add: diff_eq1)
104   qed
105 qed
108 text {* The subspace relation is reflexive. *}
110 lemma (in vectorspace) subspace_refl [intro]: "V \<unlhd> V"
111 proof
112   show "V \<noteq> {}" ..
113   show "V \<subseteq> V" ..
114   fix x y assume x: "x \<in> V" and y: "y \<in> V"
115   fix a :: real
116   from x y show "x + y \<in> V" by simp
117   from x show "a \<cdot> x \<in> V" by simp
118 qed
120 text {* The subspace relation is transitive. *}
122 lemma (in vectorspace) subspace_trans [trans]:
123   "U \<unlhd> V \<Longrightarrow> V \<unlhd> W \<Longrightarrow> U \<unlhd> W"
124 proof
125   assume uv: "U \<unlhd> V" and vw: "V \<unlhd> W"
126   from uv show "U \<noteq> {}" by (rule subspace.non_empty)
127   show "U \<subseteq> W"
128   proof -
129     from uv have "U \<subseteq> V" by (rule subspace.subset)
130     also from vw have "V \<subseteq> W" by (rule subspace.subset)
131     finally show ?thesis .
132   qed
133   fix x y assume x: "x \<in> U" and y: "y \<in> U"
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)
136 qed
139 subsection {* Linear closure *}
141 text {*
142   The \emph{linear closure} of a vector @{text x} is the set of all
143   scalar multiples of @{text x}.
144 *}
146 definition
147   lin :: "('a::{minus, plus, zero}) \<Rightarrow> 'a set" where
148   "lin x = {a \<cdot> x | a. True}"
150 lemma linI [intro]: "y = a \<cdot> x \<Longrightarrow> y \<in> lin x"
151   unfolding lin_def by blast
153 lemma linI' [iff]: "a \<cdot> x \<in> lin x"
154   unfolding lin_def by blast
156 lemma linE [elim]: "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C"
157   unfolding lin_def by blast
160 text {* Every vector is contained in its linear closure. *}
162 lemma (in vectorspace) x_lin_x [iff]: "x \<in> V \<Longrightarrow> x \<in> lin x"
163 proof -
164   assume "x \<in> V"
165   then have "x = 1 \<cdot> x" by simp
166   also have "\<dots> \<in> lin x" ..
167   finally show ?thesis .
168 qed
170 lemma (in vectorspace) "0_lin_x" [iff]: "x \<in> V \<Longrightarrow> 0 \<in> lin x"
171 proof
172   assume "x \<in> V"
173   then show "0 = 0 \<cdot> x" by simp
174 qed
176 text {* Any linear closure is a subspace. *}
178 lemma (in vectorspace) lin_subspace [intro]:
179   "x \<in> V \<Longrightarrow> lin x \<unlhd> V"
180 proof
181   assume x: "x \<in> V"
182   then show "lin x \<noteq> {}" by (auto simp add: x_lin_x)
183   show "lin x \<subseteq> V"
184   proof
185     fix x' assume "x' \<in> lin x"
186     then obtain a where "x' = a \<cdot> x" ..
187     with x show "x' \<in> V" by simp
188   qed
189   fix x' x'' assume x': "x' \<in> lin x" and x'': "x'' \<in> lin x"
190   show "x' + x'' \<in> lin x"
191   proof -
192     from x' obtain a' where "x' = a' \<cdot> x" ..
193     moreover from x'' obtain a'' where "x'' = a'' \<cdot> x" ..
194     ultimately have "x' + x'' = (a' + a'') \<cdot> x"
195       using x by (simp add: distrib)
196     also have "\<dots> \<in> lin x" ..
197     finally show ?thesis .
198   qed
199   fix a :: real
200   show "a \<cdot> x' \<in> lin x"
201   proof -
202     from x' obtain a' where "x' = a' \<cdot> x" ..
203     with x have "a \<cdot> x' = (a * a') \<cdot> x" by (simp add: mult_assoc)
204     also have "\<dots> \<in> lin x" ..
205     finally show ?thesis .
206   qed
207 qed
210 text {* Any linear closure is a vector space. *}
212 lemma (in vectorspace) lin_vectorspace [intro]:
213   assumes "x \<in> V"
214   shows "vectorspace (lin x)"
215 proof -
216   from x \<in> V have "subspace (lin x) V"
217     by (rule lin_subspace)
218   from this and vectorspace_axioms show ?thesis
219     by (rule subspace.vectorspace)
220 qed
223 subsection {* Sum of two vectorspaces *}
225 text {*
226   The \emph{sum} of two vectorspaces @{text U} and @{text V} is the
227   set of all sums of elements from @{text U} and @{text V}.
228 *}
230 instantiation "fun" :: (type, type) plus
231 begin
233 definition
234   sum_def: "plus_fun U V = {u + v | u v. u \<in> U \<and> v \<in> V}"  (* FIXME not fully general!? *)
236 instance ..
238 end
240 lemma sumE [elim]:
241     "x \<in> U + V \<Longrightarrow> (\<And>u v. x = u + v \<Longrightarrow> u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> C) \<Longrightarrow> C"
242   unfolding sum_def by blast
244 lemma sumI [intro]:
245     "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> x = u + v \<Longrightarrow> x \<in> U + V"
246   unfolding sum_def by blast
248 lemma sumI' [intro]:
249     "u \<in> U \<Longrightarrow> v \<in> V \<Longrightarrow> u + v \<in> U + V"
250   unfolding sum_def by blast
252 text {* @{text U} is a subspace of @{text "U + V"}. *}
254 lemma subspace_sum1 [iff]:
255   assumes "vectorspace U" "vectorspace V"
256   shows "U \<unlhd> U + V"
257 proof -
258   interpret vectorspace [U] by fact
259   interpret vectorspace [V] by fact
260   show ?thesis
261   proof
262     show "U \<noteq> {}" ..
263     show "U \<subseteq> U + V"
264     proof
265       fix x assume x: "x \<in> U"
266       moreover have "0 \<in> V" ..
267       ultimately have "x + 0 \<in> U + V" ..
268       with x show "x \<in> U + V" by simp
269     qed
270     fix x y assume x: "x \<in> U" and "y \<in> U"
271     then show "x + y \<in> U" by simp
272     from x show "\<And>a. a \<cdot> x \<in> U" by simp
273   qed
274 qed
276 text {* The sum of two subspaces is again a subspace. *}
278 lemma sum_subspace [intro?]:
279   assumes "subspace U E" "vectorspace E" "subspace V E"
280   shows "U + V \<unlhd> E"
281 proof -
282   interpret subspace [U E] by fact
283   interpret vectorspace [E] by fact
284   interpret subspace [V E] by fact
285   show ?thesis
286   proof
287     have "0 \<in> U + V"
288     proof
289       show "0 \<in> U" using vectorspace E ..
290       show "0 \<in> V" using vectorspace E ..
291       show "(0::'a) = 0 + 0" by simp
292     qed
293     then show "U + V \<noteq> {}" by blast
294     show "U + V \<subseteq> E"
295     proof
296       fix x assume "x \<in> U + V"
297       then obtain u v where "x = u + v" and
298 	"u \<in> U" and "v \<in> V" ..
299       then show "x \<in> E" by simp
300     qed
301     fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V"
302     show "x + y \<in> U + V"
303     proof -
304       from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" ..
305       moreover
306       from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" ..
307       ultimately
308       have "ux + uy \<in> U"
309 	and "vx + vy \<in> V"
310 	and "x + y = (ux + uy) + (vx + vy)"
312       then show ?thesis ..
313     qed
314     fix a show "a \<cdot> x \<in> U + V"
315     proof -
316       from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" ..
317       then have "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V"
318 	and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib)
319       then show ?thesis ..
320     qed
321   qed
322 qed
324 text{* The sum of two subspaces is a vectorspace. *}
326 lemma sum_vs [intro?]:
327     "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)"
328   by (rule subspace.vectorspace) (rule sum_subspace)
331 subsection {* Direct sums *}
333 text {*
334   The sum of @{text U} and @{text V} is called \emph{direct}, iff the
335   zero element is the only common element of @{text U} and @{text
336   V}. For every element @{text x} of the direct sum of @{text U} and
337   @{text V} the decomposition in @{text "x = u + v"} with
338   @{text "u \<in> U"} and @{text "v \<in> V"} is unique.
339 *}
341 lemma decomp:
342   assumes "vectorspace E" "subspace U E" "subspace V E"
343   assumes direct: "U \<inter> V = {0}"
344     and u1: "u1 \<in> U" and u2: "u2 \<in> U"
345     and v1: "v1 \<in> V" and v2: "v2 \<in> V"
346     and sum: "u1 + v1 = u2 + v2"
347   shows "u1 = u2 \<and> v1 = v2"
348 proof -
349   interpret vectorspace [E] by fact
350   interpret subspace [U E] by fact
351   interpret subspace [V E] by fact
352   show ?thesis
353   proof
354     have U: "vectorspace U"  (* FIXME: use interpret *)
355       using subspace U E vectorspace E by (rule subspace.vectorspace)
356     have V: "vectorspace V"
357       using subspace V E vectorspace E by (rule subspace.vectorspace)
358     from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
360     from u1 u2 have u: "u1 - u2 \<in> U"
361       by (rule vectorspace.diff_closed [OF U])
362     with eq have v': "v2 - v1 \<in> U" by (simp only:)
363     from v2 v1 have v: "v2 - v1 \<in> V"
364       by (rule vectorspace.diff_closed [OF V])
365     with eq have u': " u1 - u2 \<in> V" by (simp only:)
367     show "u1 = u2"
369       from u1 show "u1 \<in> E" ..
370       from u2 show "u2 \<in> E" ..
371       from u u' and direct show "u1 - u2 = 0" by blast
372     qed
373     show "v1 = v2"
375       from v1 show "v1 \<in> E" ..
376       from v2 show "v2 \<in> E" ..
377       from v v' and direct show "v2 - v1 = 0" by blast
378     qed
379   qed
380 qed
382 text {*
383   An application of the previous lemma will be used in the proof of
384   the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
385   element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a
386   vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"}
387   the components @{text "y \<in> H"} and @{text a} are uniquely
388   determined.
389 *}
391 lemma decomp_H':
392   assumes "vectorspace E" "subspace H E"
393   assumes y1: "y1 \<in> H" and y2: "y2 \<in> H"
394     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
395     and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
396   shows "y1 = y2 \<and> a1 = a2"
397 proof -
398   interpret vectorspace [E] by fact
399   interpret subspace [H E] by fact
400   show ?thesis
401   proof
402     have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
403     proof (rule decomp)
404       show "a1 \<cdot> x' \<in> lin x'" ..
405       show "a2 \<cdot> x' \<in> lin x'" ..
406       show "H \<inter> lin x' = {0}"
407       proof
408 	show "H \<inter> lin x' \<subseteq> {0}"
409 	proof
410           fix x assume x: "x \<in> H \<inter> lin x'"
411           then obtain a where xx': "x = a \<cdot> x'"
412             by blast
413           have "x = 0"
414           proof cases
415             assume "a = 0"
416             with xx' and x' show ?thesis by simp
417           next
418             assume a: "a \<noteq> 0"
419             from x have "x \<in> H" ..
420             with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp
421             with a and x' have "x' \<in> H" by (simp add: mult_assoc2)
422             with x' \<notin> H show ?thesis by contradiction
423           qed
424           then show "x \<in> {0}" ..
425 	qed
426 	show "{0} \<subseteq> H \<inter> lin x'"
427 	proof -
428           have "0 \<in> H" using vectorspace E ..
429           moreover have "0 \<in> lin x'" using x' \<in> E ..
430           ultimately show ?thesis by blast
431 	qed
432       qed
433       show "lin x' \<unlhd> E" using x' \<in> E ..
434     qed (rule vectorspace E, rule subspace H E, rule y1, rule y2, rule eq)
435     then show "y1 = y2" ..
436     from c have "a1 \<cdot> x' = a2 \<cdot> x'" ..
437     with x' show "a1 = a2" by (simp add: mult_right_cancel)
438   qed
439 qed
441 text {*
442   Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a
443   vectorspace @{text H} and the linear closure of @{text x'} the
444   components @{text "y \<in> H"} and @{text a} are unique, it follows from
445   @{text "y \<in> H"} that @{text "a = 0"}.
446 *}
448 lemma decomp_H'_H:
449   assumes "vectorspace E" "subspace H E"
450   assumes t: "t \<in> H"
451     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
452   shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
453 proof -
454   interpret vectorspace [E] by fact
455   interpret subspace [H E] by fact
456   show ?thesis
457   proof (rule, simp_all only: split_paired_all split_conv)
458     from t x' show "t = t + 0 \<cdot> x' \<and> t \<in> H" by simp
459     fix y and a assume ya: "t = y + a \<cdot> x' \<and> y \<in> H"
460     have "y = t \<and> a = 0"
461     proof (rule decomp_H')
462       from ya x' show "y + a \<cdot> x' = t + 0 \<cdot> x'" by simp
463       from ya show "y \<in> H" ..
464     qed (rule vectorspace E, rule subspace H E, rule t, (rule x')+)
465     with t x' show "(y, a) = (y + a \<cdot> x', 0)" by simp
466   qed
467 qed
469 text {*
470   The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"}
471   are unique, so the function @{text h'} defined by
472   @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite.
473 *}
475 lemma h'_definite:
476   fixes H
477   assumes h'_def:
478     "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
479                 in (h y) + a * xi)"
480     and x: "x = y + a \<cdot> x'"
481   assumes "vectorspace E" "subspace H E"
482   assumes y: "y \<in> H"
483     and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
484   shows "h' x = h y + a * xi"
485 proof -
486   interpret vectorspace [E] by fact
487   interpret subspace [H E] by fact
488   from x y x' have "x \<in> H + lin x'" by auto
489   have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
490   proof (rule ex_ex1I)
491     from x y show "\<exists>p. ?P p" by blast
492     fix p q assume p: "?P p" and q: "?P q"
493     show "p = q"
494     proof -
495       from p have xp: "x = fst p + snd p \<cdot> x' \<and> fst p \<in> H"
496         by (cases p) simp
497       from q have xq: "x = fst q + snd q \<cdot> x' \<and> fst q \<in> H"
498         by (cases q) simp
499       have "fst p = fst q \<and> snd p = snd q"
500       proof (rule decomp_H')
501         from xp show "fst p \<in> H" ..
502         from xq show "fst q \<in> H" ..
503         from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'"
504           by simp
505       qed (rule vectorspace E, rule subspace H E, (rule x')+)
506       then show ?thesis by (cases p, cases q) simp
507     qed
508   qed
509   then have eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)"
510     by (rule some1_equality) (simp add: x y)
511   with h'_def show "h' x = h y + a * xi" by (simp add: Let_def)
512 qed
514 end