author | wenzelm |
Wed, 29 Sep 1999 16:41:52 +0200 | |
changeset 7656 | 2f18c0ffc348 |
parent 7567 | 62384a807775 |
child 7808 | fd019ac3485f |
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 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
6 |
theory Subspace = LinearSpace:; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
7 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
8 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
9 |
section {* subspaces *}; |
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 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
12 |
is_subspace :: "['a set, 'a set] => bool" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
13 |
"is_subspace U V == <0>:U & U <= V |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
14 |
& (ALL x:U. ALL y:U. ALL a. x [+] y : U |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
15 |
& a [*] x : U)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
16 |
|
7566 | 17 |
lemma subspaceI [intro]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
18 |
"[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); ALL x:U. ALL a. a [*] x : U |] |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
19 |
\ ==> is_subspace U V"; |
7656 | 20 |
by (unfold is_subspace_def) simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
21 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
22 |
lemma "is_subspace U V ==> U ~= {}"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
23 |
by (unfold is_subspace_def) force; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
24 |
|
7566 | 25 |
lemma zero_in_subspace [intro !!]: "is_subspace U V ==> <0>:U"; |
7656 | 26 |
by (unfold is_subspace_def) simp;; |
7566 | 27 |
|
28 |
lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V"; |
|
7656 | 29 |
by (unfold is_subspace_def) simp; |
7566 | 30 |
|
31 |
lemma subspace_subsetD [simp, intro!!]: "[| is_subspace U V; x:U |]==> x:V"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
32 |
by (unfold is_subspace_def) force; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
33 |
|
7566 | 34 |
lemma subspace_add_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U"; |
7656 | 35 |
by (unfold is_subspace_def) simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
36 |
|
7566 | 37 |
lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U"; |
7656 | 38 |
by (unfold is_subspace_def) simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
39 |
|
7566 | 40 |
lemma subspace_diff_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U"; |
7656 | 41 |
by (unfold diff_def negate_def) simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
42 |
|
7566 | 43 |
lemma subspace_neg_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> [-] x: U"; |
7656 | 44 |
by (unfold negate_def) simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
45 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
46 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
47 |
theorem subspace_vs [intro!!]: |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
48 |
"[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
49 |
proof -; |
7656 | 50 |
assume "is_subspace U V" "is_vectorspace V"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
51 |
show ?thesis; |
7566 | 52 |
proof; |
53 |
show "<0>:U"; ..; |
|
54 |
show "ALL x:U. ALL a. a [*] x : U"; by (simp!); |
|
55 |
show "ALL x:U. ALL y:U. x [+] y : U"; by (simp!); |
|
56 |
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
|
57 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
58 |
|
7566 | 59 |
lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V"; |
60 |
proof; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
61 |
assume "is_vectorspace V"; |
7566 | 62 |
show "<0> : V"; ..; |
63 |
show "V <= V"; ..; |
|
64 |
show "ALL x:V. ALL y:V. x [+] y : V"; by (simp!); |
|
65 |
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
|
66 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
67 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
68 |
lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W"; |
7566 | 69 |
proof; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
70 |
assume "is_subspace U V" "is_subspace V W"; |
7566 | 71 |
show "<0> : U"; ..; |
7656 | 72 |
|
7566 | 73 |
have "U <= V"; ..; |
74 |
also; have "V <= W"; ..; |
|
75 |
finally; show "U <= W"; .; |
|
7656 | 76 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
77 |
show "ALL x:U. ALL y:U. x [+] y : U"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
78 |
proof (intro ballI); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
79 |
fix x y; assume "x:U" "y:U"; |
7566 | 80 |
show "x [+] y : U"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
81 |
qed; |
7656 | 82 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
83 |
show "ALL x:U. ALL a. a [*] x : U"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
84 |
proof (intro ballI allI); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
85 |
fix x a; assume "x:U"; |
7566 | 86 |
show "a [*] x : U"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
87 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
88 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
89 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
90 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
91 |
section {* linear closure *}; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
92 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
93 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
94 |
lin :: "'a => 'a set" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
95 |
"lin x == {y. ? a. y = a [*] x}"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
96 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
97 |
lemma linD: "x : lin v = (? a::real. x = a [*] v)"; |
7566 | 98 |
by (unfold lin_def) force; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
99 |
|
7656 | 100 |
lemma linI [intro!!]: "a [*] x0 : lin x0"; |
101 |
by (unfold lin_def) force; |
|
102 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
103 |
lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
104 |
proof (unfold lin_def, intro CollectI exI); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
105 |
assume "is_vectorspace V" "x:V"; |
7566 | 106 |
show "x = 1r [*] x"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
107 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
108 |
|
7566 | 109 |
lemma lin_subspace [intro!!]: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V"; |
110 |
proof; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
111 |
assume "is_vectorspace V" "x:V"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
112 |
show "<0> : lin x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
113 |
proof (unfold lin_def, intro CollectI exI); |
7566 | 114 |
show "<0> = 0r [*] x"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
115 |
qed; |
7566 | 116 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
117 |
show "lin x <= V"; |
7566 | 118 |
proof (unfold lin_def, intro subsetI, elim CollectE exE); |
119 |
fix xa a; assume "xa = a [*] x"; |
|
120 |
show "xa:V"; by (simp!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
121 |
qed; |
7566 | 122 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
123 |
show "ALL x1 : lin x. ALL x2 : lin x. x1 [+] x2 : lin x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
124 |
proof (intro ballI); |
7566 | 125 |
fix x1 x2; assume "x1 : lin x" "x2 : lin x"; |
126 |
thus "x1 [+] x2 : lin x"; |
|
7567 | 127 |
proof (unfold lin_def, elim CollectE exE, intro CollectI exI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
128 |
fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x"; |
7566 | 129 |
show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2); |
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; |
7566 | 132 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
133 |
show "ALL xa:lin x. ALL a. a [*] xa : lin x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
134 |
proof (intro ballI allI); |
7566 | 135 |
fix x1 a; assume "x1 : lin x"; |
136 |
thus "a [*] x1 : lin x"; |
|
7567 | 137 |
proof (unfold lin_def, elim CollectE exE, intro CollectI exI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
138 |
fix a1; assume "x1 = a1 [*] x"; |
7566 | 139 |
show "a [*] x1 = (a * a1) [*] x"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
140 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
141 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
142 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
143 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
144 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
145 |
lemma lin_vs [intro!!]: "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
146 |
proof (rule subspace_vs); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
147 |
assume "is_vectorspace V" "x:V"; |
7566 | 148 |
show "is_subspace (lin x) V"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
149 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
150 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
151 |
section {* sum of two vectorspaces *}; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
152 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
153 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
154 |
vectorspace_sum :: "['a set, 'a set] => 'a set" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
155 |
"vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
156 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
157 |
lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)"; |
7656 | 158 |
by (unfold vectorspace_sum_def) simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
159 |
|
7566 | 160 |
lemmas vs_sumE = vs_sumD [RS iffD1, elimify]; |
161 |
||
162 |
lemma vs_sumI [intro!!]: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
163 |
by (unfold vectorspace_sum_def, intro CollectI bexI); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
164 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
165 |
lemma subspace_vs_sum1 [intro!!]: |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
166 |
"[| is_vectorspace U; is_vectorspace V |] ==> is_subspace U (vectorspace_sum U V)"; |
7566 | 167 |
proof; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
168 |
assume "is_vectorspace U" "is_vectorspace V"; |
7566 | 169 |
show "<0> : U"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
170 |
show "U <= vectorspace_sum U V"; |
7566 | 171 |
proof (intro subsetI vs_sumI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
172 |
fix x; assume "x:U"; |
7566 | 173 |
show "x = x [+] <0>"; by (simp!); |
174 |
show "<0> : V"; by (simp!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
175 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
176 |
show "ALL x:U. ALL y:U. x [+] y : U"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
177 |
proof (intro ballI); |
7566 | 178 |
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
|
179 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
180 |
show "ALL x:U. ALL a. a [*] x : U"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
181 |
proof (intro ballI allI); |
7566 | 182 |
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
|
183 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
184 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
185 |
|
7566 | 186 |
lemma vs_sum_subspace [intro!!]: |
187 |
"[| is_subspace U E; is_subspace V E; is_vectorspace E |] |
|
188 |
==> is_subspace (vectorspace_sum U V) E"; |
|
189 |
proof; |
|
190 |
assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
191 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
192 |
show "<0> : vectorspace_sum U V"; |
7566 | 193 |
proof (intro vs_sumI); |
194 |
show "<0> : U"; ..; |
|
195 |
show "<0> : V"; ..; |
|
7656 | 196 |
show "(<0>::'a) = <0> [+] <0>"; by (simp!); |
7566 | 197 |
qed; |
198 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
199 |
show "vectorspace_sum U V <= E"; |
7566 | 200 |
proof (intro subsetI, elim vs_sumE bexE); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
201 |
fix x u v; assume "u : U" "v : V" "x = u [+] v"; |
7566 | 202 |
show "x:E"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
203 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
204 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
205 |
show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V"; |
7566 | 206 |
proof (intro ballI); |
207 |
fix x y; assume "x:vectorspace_sum U V" "y:vectorspace_sum U V"; |
|
208 |
thus "x [+] y : vectorspace_sum U V"; |
|
209 |
proof (elim vs_sumE bexE, intro vs_sumI); |
|
210 |
fix ux vx uy vy; |
|
211 |
assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy"; |
|
212 |
show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by (simp!); |
|
213 |
qed (simp!)+; |
|
214 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
215 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
216 |
show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V"; |
7566 | 217 |
proof (intro ballI allI); |
218 |
fix x a; assume "x:vectorspace_sum U V"; |
|
219 |
thus "a [*] x : vectorspace_sum U V"; |
|
220 |
proof (elim vs_sumE bexE, intro vs_sumI); |
|
221 |
fix a x u v; assume "u : U" "v : V" "x = u [+] v"; |
|
222 |
show "a [*] x = (a [*] u) [+] (a [*] v)"; by (simp! add: vs_add_mult_distrib1); |
|
223 |
qed (simp!)+; |
|
224 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
225 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
226 |
|
7566 | 227 |
lemma vs_sum_vs [intro!!]: |
228 |
"[| is_subspace U E; is_subspace V E; is_vectorspace E |] |
|
229 |
==> is_vectorspace (vectorspace_sum U V)"; |
|
230 |
proof (rule subspace_vs); |
|
231 |
assume "is_subspace U E" "is_subspace V E" "is_vectorspace E"; |
|
232 |
show "is_subspace (vectorspace_sum U V) E"; ..; |
|
233 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
234 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
235 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
236 |
section {* special case: direct sum of a vectorspace and a linear closure of a vector *}; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
237 |
|
7656 | 238 |
lemma decomp: "[| is_vectorspace E; is_subspace U E; is_subspace V E; U Int V = {<0>}; |
239 |
u1:U; u2:U; v1:V; v2:V; u1 [+] v1 = u2 [+] v2 |] |
|
240 |
==> u1 = u2 & v1 = v2"; |
|
241 |
proof; |
|
242 |
assume "is_vectorspace E" "is_subspace U E" "is_subspace V E" "U Int V = {<0>}" |
|
243 |
"u1:U" "u2:U" "v1:V" "v2:V" "u1 [+] v1 = u2 [+] v2"; |
|
244 |
have eq: "u1 [-] u2 = v2 [-] v1"; by (simp! add: vs_add_diff_swap); |
|
245 |
have u: "u1 [-] u2 : U"; by (simp!); with eq; have v': "v2 [-] v1 : U"; by simp; |
|
246 |
have v: "v2 [-] v1 : V"; by (simp!); with eq; have u': "u1 [-] u2 : V"; by simp; |
|
247 |
||
248 |
show "u1 = u2"; |
|
249 |
proof (rule vs_add_minus_eq); |
|
250 |
show "u1 [-] u2 = <0>"; by (rule Int_singletonD [OF _ u u']); |
|
251 |
qed (rule); |
|
252 |
||
253 |
show "v1 = v2"; |
|
254 |
proof (rule vs_add_minus_eq [RS sym]); |
|
255 |
show "v2 [-] v1 = <0>"; by (rule Int_singletonD [OF _ v' v]); |
|
256 |
qed (rule); |
|
257 |
qed; |
|
258 |
||
7566 | 259 |
lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
260 |
x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |] |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
261 |
==> y1 = y2 & a1 = a2"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
262 |
proof; |
7656 | 263 |
assume "is_vectorspace E" and h: "is_subspace H E" |
264 |
and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
265 |
"y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
266 |
|
7656 | 267 |
have c: "y1 = y2 & a1 [*] x0 = a2 [*] x0"; |
268 |
proof (rule decomp); |
|
269 |
show "a1 [*] x0 : lin x0"; ..; |
|
270 |
show "a2 [*] x0 : lin x0"; ..; |
|
271 |
show "H Int (lin x0) = {<0>}"; |
|
272 |
proof; |
|
273 |
show "H Int lin x0 <= {<0>}"; |
|
274 |
proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]); |
|
275 |
fix x; assume "x:H" "x:lin x0"; |
|
276 |
thus "x = <0>"; |
|
277 |
proof (unfold lin_def, elim CollectE exE); |
|
278 |
fix a; assume "x = a [*] x0"; |
|
279 |
show ?thesis; |
|
280 |
proof (rule case_split [of "a = 0r"]); |
|
281 |
assume "a = 0r"; show ?thesis; by (simp!); |
|
282 |
next; |
|
283 |
assume "a ~= 0r"; |
|
284 |
from h; have "(rinv a) [*] a [*] x0 : H"; by (rule subspace_mult_closed) (simp!); |
|
285 |
also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!); |
|
286 |
finally; have "x0 : H"; .; |
|
287 |
thus ?thesis; by contradiction; |
|
288 |
qed; |
|
289 |
qed; |
|
290 |
qed; |
|
291 |
show "{<0>} <= H Int lin x0"; |
|
292 |
proof (intro subsetI, elim singletonE, intro IntI, simp+); |
|
293 |
show "<0> : H"; ..; |
|
294 |
from lin_vs; show "<0> : lin x0"; ..; |
|
295 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
296 |
qed; |
7656 | 297 |
show "is_subspace (lin x0) E"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
298 |
qed; |
7656 | 299 |
|
300 |
from c; show "y1 = y2"; by simp; |
|
301 |
||
302 |
show "a1 = a2"; |
|
303 |
proof (rule vs_mult_right_cancel [RS iffD1]); |
|
304 |
from c; show "a1 [*] x0 = a2 [*] x0"; by simp; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
305 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
306 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
307 |
|
7566 | 308 |
lemma decomp1: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
309 |
"[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |] |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
310 |
==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
311 |
proof (rule, unfold split_paired_all); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
312 |
assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>"; |
7566 | 313 |
have h: "is_vectorspace H"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
314 |
fix y a; presume t1: "t = y [+] a [*] x0" and "y : H"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
315 |
have "y = t & a = 0r"; |
7656 | 316 |
by (rule decomp4) (assumption | (simp!))+; |
7566 | 317 |
thus "(y, a) = (t, 0r)"; by (simp!); |
318 |
qed (simp!)+; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
319 |
|
7566 | 320 |
lemma decomp3: |
321 |
"[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) |
|
322 |
in (h y) + a * xi); |
|
323 |
x = y [+] a [*] x0; |
|
324 |
is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |] |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
325 |
==> h0 x = h y + a * xi"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
326 |
proof -; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
327 |
assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) |
7656 | 328 |
in (h y) + a * xi)" |
329 |
"x = y [+] a [*] x0" |
|
330 |
"is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
331 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
332 |
have "x : vectorspace_sum H (lin x0)"; |
7566 | 333 |
by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
334 |
have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; |
7656 | 335 |
proof%%; |
7566 | 336 |
show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; |
337 |
by (force!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
338 |
next; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
339 |
fix xa ya; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
340 |
assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
341 |
"(%(y,a). x = y [+] a [*] x0 & y : H) ya"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
342 |
show "xa = ya"; ; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
343 |
proof -; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
344 |
show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; |
7566 | 345 |
by (rule Pair_fst_snd_eq [RS iffD2]); |
346 |
have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by (force!); |
|
347 |
have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by (force!); |
|
7656 | 348 |
from x y; show "fst xa = fst ya & snd xa = snd ya"; by (elim conjE) (rule decomp4, (simp!)+); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
349 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
350 |
qed; |
7656 | 351 |
hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; by (rule select1_equality) (force!); |
352 |
thus "h0 x = h y + a * xi"; by (simp! add: Let_def); |
|
7566 | 353 |
qed; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
354 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
355 |
end; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
356 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
357 |