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