51 by (auto simp add: Cart_eq) |
51 by (auto simp add: Cart_eq) |
52 |
52 |
53 lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g" |
53 lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g" |
54 by (simp add: Cart_eq) |
54 by (simp add: Cart_eq) |
55 |
55 |
56 end |
56 |
|
57 subsection {* Group operations and class instances *} |
|
58 |
|
59 instantiation cart :: (zero,finite) zero |
|
60 begin |
|
61 definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)" |
|
62 instance .. |
|
63 end |
|
64 |
|
65 instantiation cart :: (plus,finite) plus |
|
66 begin |
|
67 definition vector_add_def : "op + \<equiv> (\<lambda> x y. (\<chi> i. (x$i) + (y$i)))" |
|
68 instance .. |
|
69 end |
|
70 |
|
71 instantiation cart :: (minus,finite) minus |
|
72 begin |
|
73 definition vector_minus_def : "op - \<equiv> (\<lambda> x y. (\<chi> i. (x$i) - (y$i)))" |
|
74 instance .. |
|
75 end |
|
76 |
|
77 instantiation cart :: (uminus,finite) uminus |
|
78 begin |
|
79 definition vector_uminus_def : "uminus \<equiv> (\<lambda> x. (\<chi> i. - (x$i)))" |
|
80 instance .. |
|
81 end |
|
82 |
|
83 lemma zero_index [simp]: "0 $ i = 0" |
|
84 unfolding vector_zero_def by simp |
|
85 |
|
86 lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i" |
|
87 unfolding vector_add_def by simp |
|
88 |
|
89 lemma vector_minus_component [simp]: "(x - y)$i = x$i - y$i" |
|
90 unfolding vector_minus_def by simp |
|
91 |
|
92 lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)" |
|
93 unfolding vector_uminus_def by simp |
|
94 |
|
95 instance cart :: (semigroup_add, finite) semigroup_add |
|
96 by default (simp add: Cart_eq add_assoc) |
|
97 |
|
98 instance cart :: (ab_semigroup_add, finite) ab_semigroup_add |
|
99 by default (simp add: Cart_eq add_commute) |
|
100 |
|
101 instance cart :: (monoid_add, finite) monoid_add |
|
102 by default (simp_all add: Cart_eq) |
|
103 |
|
104 instance cart :: (comm_monoid_add, finite) comm_monoid_add |
|
105 by default (simp add: Cart_eq) |
|
106 |
|
107 instance cart :: (cancel_semigroup_add, finite) cancel_semigroup_add |
|
108 by default (simp_all add: Cart_eq) |
|
109 |
|
110 instance cart :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add |
|
111 by default (simp add: Cart_eq) |
|
112 |
|
113 instance cart :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. |
|
114 |
|
115 instance cart :: (group_add, finite) group_add |
|
116 by default (simp_all add: Cart_eq diff_minus) |
|
117 |
|
118 instance cart :: (ab_group_add, finite) ab_group_add |
|
119 by default (simp_all add: Cart_eq) |
|
120 |
|
121 |
|
122 subsection {* Real vector space *} |
|
123 |
|
124 instantiation cart :: (real_vector, finite) real_vector |
|
125 begin |
|
126 |
|
127 definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))" |
|
128 |
|
129 lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)" |
|
130 unfolding vector_scaleR_def by simp |
|
131 |
|
132 instance |
|
133 by default (simp_all add: Cart_eq scaleR_left_distrib scaleR_right_distrib) |
|
134 |
|
135 end |
|
136 |
|
137 |
|
138 subsection {* Topological space *} |
|
139 |
|
140 instantiation cart :: (topological_space, finite) topological_space |
|
141 begin |
|
142 |
|
143 definition open_vector_def: |
|
144 "open (S :: ('a ^ 'b) set) \<longleftrightarrow> |
|
145 (\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and> |
|
146 (\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))" |
|
147 |
|
148 instance proof |
|
149 show "open (UNIV :: ('a ^ 'b) set)" |
|
150 unfolding open_vector_def by auto |
|
151 next |
|
152 fix S T :: "('a ^ 'b) set" |
|
153 assume "open S" "open T" thus "open (S \<inter> T)" |
|
154 unfolding open_vector_def |
|
155 apply clarify |
|
156 apply (drule (1) bspec)+ |
|
157 apply (clarify, rename_tac Sa Ta) |
|
158 apply (rule_tac x="\<lambda>i. Sa i \<inter> Ta i" in exI) |
|
159 apply (simp add: open_Int) |
|
160 done |
|
161 next |
|
162 fix K :: "('a ^ 'b) set set" |
|
163 assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)" |
|
164 unfolding open_vector_def |
|
165 apply clarify |
|
166 apply (drule (1) bspec) |
|
167 apply (drule (1) bspec) |
|
168 apply clarify |
|
169 apply (rule_tac x=A in exI) |
|
170 apply fast |
|
171 done |
|
172 qed |
|
173 |
|
174 end |
|
175 |
|
176 lemma open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}" |
|
177 unfolding open_vector_def by auto |
|
178 |
|
179 lemma open_vimage_Cart_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)" |
|
180 unfolding open_vector_def |
|
181 apply clarify |
|
182 apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp) |
|
183 done |
|
184 |
|
185 lemma closed_vimage_Cart_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)" |
|
186 unfolding closed_open vimage_Compl [symmetric] |
|
187 by (rule open_vimage_Cart_nth) |
|
188 |
|
189 lemma closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}" |
|
190 proof - |
|
191 have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto |
|
192 thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}" |
|
193 by (simp add: closed_INT closed_vimage_Cart_nth) |
|
194 qed |
|
195 |
|
196 lemma tendsto_Cart_nth [tendsto_intros]: |
|
197 assumes "((\<lambda>x. f x) ---> a) net" |
|
198 shows "((\<lambda>x. f x $ i) ---> a $ i) net" |
|
199 proof (rule topological_tendstoI) |
|
200 fix S assume "open S" "a $ i \<in> S" |
|
201 then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)" |
|
202 by (simp_all add: open_vimage_Cart_nth) |
|
203 with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net" |
|
204 by (rule topological_tendstoD) |
|
205 then show "eventually (\<lambda>x. f x $ i \<in> S) net" |
|
206 by simp |
|
207 qed |
|
208 |
|
209 lemma eventually_Ball_finite: (* TODO: move *) |
|
210 assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net" |
|
211 shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net" |
|
212 using assms by (induct set: finite, simp, simp add: eventually_conj) |
|
213 |
|
214 lemma eventually_all_finite: (* TODO: move *) |
|
215 fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool" |
|
216 assumes "\<And>y. eventually (\<lambda>x. P x y) net" |
|
217 shows "eventually (\<lambda>x. \<forall>y. P x y) net" |
|
218 using eventually_Ball_finite [of UNIV P] assms by simp |
|
219 |
|
220 lemma tendsto_vector: |
|
221 assumes "\<And>i. ((\<lambda>x. f x $ i) ---> a $ i) net" |
|
222 shows "((\<lambda>x. f x) ---> a) net" |
|
223 proof (rule topological_tendstoI) |
|
224 fix S assume "open S" and "a \<in> S" |
|
225 then obtain A where A: "\<And>i. open (A i)" "\<And>i. a $ i \<in> A i" |
|
226 and S: "\<And>y. \<forall>i. y $ i \<in> A i \<Longrightarrow> y \<in> S" |
|
227 unfolding open_vector_def by metis |
|
228 have "\<And>i. eventually (\<lambda>x. f x $ i \<in> A i) net" |
|
229 using assms A by (rule topological_tendstoD) |
|
230 hence "eventually (\<lambda>x. \<forall>i. f x $ i \<in> A i) net" |
|
231 by (rule eventually_all_finite) |
|
232 thus "eventually (\<lambda>x. f x \<in> S) net" |
|
233 by (rule eventually_elim1, simp add: S) |
|
234 qed |
|
235 |
|
236 lemma tendsto_Cart_lambda [tendsto_intros]: |
|
237 assumes "\<And>i. ((\<lambda>x. f x i) ---> a i) net" |
|
238 shows "((\<lambda>x. \<chi> i. f x i) ---> (\<chi> i. a i)) net" |
|
239 using assms by (simp add: tendsto_vector) |
|
240 |
|
241 |
|
242 subsection {* Metric *} |
|
243 |
|
244 (* TODO: move somewhere else *) |
|
245 lemma finite_choice: "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)" |
|
246 apply (induct set: finite, simp_all) |
|
247 apply (clarify, rename_tac y) |
|
248 apply (rule_tac x="f(x:=y)" in exI, simp) |
|
249 done |
|
250 |
|
251 instantiation cart :: (metric_space, finite) metric_space |
|
252 begin |
|
253 |
|
254 definition dist_vector_def: |
|
255 "dist x y = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV" |
|
256 |
|
257 lemma dist_nth_le: "dist (x $ i) (y $ i) \<le> dist x y" |
|
258 unfolding dist_vector_def |
|
259 by (rule member_le_setL2) simp_all |
|
260 |
|
261 instance proof |
|
262 fix x y :: "'a ^ 'b" |
|
263 show "dist x y = 0 \<longleftrightarrow> x = y" |
|
264 unfolding dist_vector_def |
|
265 by (simp add: setL2_eq_0_iff Cart_eq) |
|
266 next |
|
267 fix x y z :: "'a ^ 'b" |
|
268 show "dist x y \<le> dist x z + dist y z" |
|
269 unfolding dist_vector_def |
|
270 apply (rule order_trans [OF _ setL2_triangle_ineq]) |
|
271 apply (simp add: setL2_mono dist_triangle2) |
|
272 done |
|
273 next |
|
274 (* FIXME: long proof! *) |
|
275 fix S :: "('a ^ 'b) set" |
|
276 show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" |
|
277 unfolding open_vector_def open_dist |
|
278 apply safe |
|
279 apply (drule (1) bspec) |
|
280 apply clarify |
|
281 apply (subgoal_tac "\<exists>e>0. \<forall>i y. dist y (x$i) < e \<longrightarrow> y \<in> A i") |
|
282 apply clarify |
|
283 apply (rule_tac x=e in exI, clarify) |
|
284 apply (drule spec, erule mp, clarify) |
|
285 apply (drule spec, drule spec, erule mp) |
|
286 apply (erule le_less_trans [OF dist_nth_le]) |
|
287 apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>e>0. \<forall>y. dist y (x$i) < e \<longrightarrow> y \<in> A i") |
|
288 apply (drule finite_choice [OF finite], clarify) |
|
289 apply (rule_tac x="Min (range f)" in exI, simp) |
|
290 apply clarify |
|
291 apply (drule_tac x=i in spec, clarify) |
|
292 apply (erule (1) bspec) |
|
293 apply (drule (1) bspec, clarify) |
|
294 apply (subgoal_tac "\<exists>r. (\<forall>i::'b. 0 < r i) \<and> e = setL2 r UNIV") |
|
295 apply clarify |
|
296 apply (rule_tac x="\<lambda>i. {y. dist y (x$i) < r i}" in exI) |
|
297 apply (rule conjI) |
|
298 apply clarify |
|
299 apply (rule conjI) |
|
300 apply (clarify, rename_tac y) |
|
301 apply (rule_tac x="r i - dist y (x$i)" in exI, rule conjI, simp) |
|
302 apply clarify |
|
303 apply (simp only: less_diff_eq) |
|
304 apply (erule le_less_trans [OF dist_triangle]) |
|
305 apply simp |
|
306 apply clarify |
|
307 apply (drule spec, erule mp) |
|
308 apply (simp add: dist_vector_def setL2_strict_mono) |
|
309 apply (rule_tac x="\<lambda>i. e / sqrt (of_nat CARD('b))" in exI) |
|
310 apply (simp add: divide_pos_pos setL2_constant) |
|
311 done |
|
312 qed |
|
313 |
|
314 end |
|
315 |
|
316 lemma LIMSEQ_Cart_nth: |
|
317 "(X ----> a) \<Longrightarrow> (\<lambda>n. X n $ i) ----> a $ i" |
|
318 unfolding LIMSEQ_conv_tendsto by (rule tendsto_Cart_nth) |
|
319 |
|
320 lemma LIM_Cart_nth: |
|
321 "(f -- x --> y) \<Longrightarrow> (\<lambda>x. f x $ i) -- x --> y $ i" |
|
322 unfolding LIM_conv_tendsto by (rule tendsto_Cart_nth) |
|
323 |
|
324 lemma Cauchy_Cart_nth: |
|
325 "Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)" |
|
326 unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le]) |
|
327 |
|
328 lemma LIMSEQ_vector: |
|
329 assumes "\<And>i. (\<lambda>n. X n $ i) ----> (a $ i)" |
|
330 shows "X ----> a" |
|
331 using assms unfolding LIMSEQ_conv_tendsto by (rule tendsto_vector) |
|
332 |
|
333 lemma Cauchy_vector: |
|
334 fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n" |
|
335 assumes X: "\<And>i. Cauchy (\<lambda>n. X n $ i)" |
|
336 shows "Cauchy (\<lambda>n. X n)" |
|
337 proof (rule metric_CauchyI) |
|
338 fix r :: real assume "0 < r" |
|
339 then have "0 < r / of_nat CARD('n)" (is "0 < ?s") |
|
340 by (simp add: divide_pos_pos) |
|
341 def N \<equiv> "\<lambda>i. LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s" |
|
342 def M \<equiv> "Max (range N)" |
|
343 have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s" |
|
344 using X `0 < ?s` by (rule metric_CauchyD) |
|
345 hence "\<And>i. \<forall>m\<ge>N i. \<forall>n\<ge>N i. dist (X m $ i) (X n $ i) < ?s" |
|
346 unfolding N_def by (rule LeastI_ex) |
|
347 hence M: "\<And>i. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < ?s" |
|
348 unfolding M_def by simp |
|
349 { |
|
350 fix m n :: nat |
|
351 assume "M \<le> m" "M \<le> n" |
|
352 have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV" |
|
353 unfolding dist_vector_def .. |
|
354 also have "\<dots> \<le> setsum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV" |
|
355 by (rule setL2_le_setsum [OF zero_le_dist]) |
|
356 also have "\<dots> < setsum (\<lambda>i::'n. ?s) UNIV" |
|
357 by (rule setsum_strict_mono, simp_all add: M `M \<le> m` `M \<le> n`) |
|
358 also have "\<dots> = r" |
|
359 by simp |
|
360 finally have "dist (X m) (X n) < r" . |
|
361 } |
|
362 hence "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" |
|
363 by simp |
|
364 then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" .. |
|
365 qed |
|
366 |
|
367 instance cart :: (complete_space, finite) complete_space |
|
368 proof |
|
369 fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X" |
|
370 have "\<And>i. (\<lambda>n. X n $ i) ----> lim (\<lambda>n. X n $ i)" |
|
371 using Cauchy_Cart_nth [OF `Cauchy X`] |
|
372 by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) |
|
373 hence "X ----> Cart_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))" |
|
374 by (simp add: LIMSEQ_vector) |
|
375 then show "convergent X" |
|
376 by (rule convergentI) |
|
377 qed |
|
378 |
|
379 |
|
380 subsection {* Normed vector space *} |
|
381 |
|
382 instantiation cart :: (real_normed_vector, finite) real_normed_vector |
|
383 begin |
|
384 |
|
385 definition norm_vector_def: |
|
386 "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV" |
|
387 |
|
388 definition vector_sgn_def: |
|
389 "sgn (x::'a^'b) = scaleR (inverse (norm x)) x" |
|
390 |
|
391 instance proof |
|
392 fix a :: real and x y :: "'a ^ 'b" |
|
393 show "0 \<le> norm x" |
|
394 unfolding norm_vector_def |
|
395 by (rule setL2_nonneg) |
|
396 show "norm x = 0 \<longleftrightarrow> x = 0" |
|
397 unfolding norm_vector_def |
|
398 by (simp add: setL2_eq_0_iff Cart_eq) |
|
399 show "norm (x + y) \<le> norm x + norm y" |
|
400 unfolding norm_vector_def |
|
401 apply (rule order_trans [OF _ setL2_triangle_ineq]) |
|
402 apply (simp add: setL2_mono norm_triangle_ineq) |
|
403 done |
|
404 show "norm (scaleR a x) = \<bar>a\<bar> * norm x" |
|
405 unfolding norm_vector_def |
|
406 by (simp add: setL2_right_distrib) |
|
407 show "sgn x = scaleR (inverse (norm x)) x" |
|
408 by (rule vector_sgn_def) |
|
409 show "dist x y = norm (x - y)" |
|
410 unfolding dist_vector_def norm_vector_def |
|
411 by (simp add: dist_norm) |
|
412 qed |
|
413 |
|
414 end |
|
415 |
|
416 lemma norm_nth_le: "norm (x $ i) \<le> norm x" |
|
417 unfolding norm_vector_def |
|
418 by (rule member_le_setL2) simp_all |
|
419 |
|
420 interpretation Cart_nth: bounded_linear "\<lambda>x. x $ i" |
|
421 apply default |
|
422 apply (rule vector_add_component) |
|
423 apply (rule vector_scaleR_component) |
|
424 apply (rule_tac x="1" in exI, simp add: norm_nth_le) |
|
425 done |
|
426 |
|
427 instance cart :: (banach, finite) banach .. |
|
428 |
|
429 |
|
430 subsection {* Inner product space *} |
|
431 |
|
432 instantiation cart :: (real_inner, finite) real_inner |
|
433 begin |
|
434 |
|
435 definition inner_vector_def: |
|
436 "inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) UNIV" |
|
437 |
|
438 instance proof |
|
439 fix r :: real and x y z :: "'a ^ 'b" |
|
440 show "inner x y = inner y x" |
|
441 unfolding inner_vector_def |
|
442 by (simp add: inner_commute) |
|
443 show "inner (x + y) z = inner x z + inner y z" |
|
444 unfolding inner_vector_def |
|
445 by (simp add: inner_add_left setsum_addf) |
|
446 show "inner (scaleR r x) y = r * inner x y" |
|
447 unfolding inner_vector_def |
|
448 by (simp add: setsum_right_distrib) |
|
449 show "0 \<le> inner x x" |
|
450 unfolding inner_vector_def |
|
451 by (simp add: setsum_nonneg) |
|
452 show "inner x x = 0 \<longleftrightarrow> x = 0" |
|
453 unfolding inner_vector_def |
|
454 by (simp add: Cart_eq setsum_nonneg_eq_0_iff) |
|
455 show "norm x = sqrt (inner x x)" |
|
456 unfolding inner_vector_def norm_vector_def setL2_def |
|
457 by (simp add: power2_norm_eq_inner) |
|
458 qed |
|
459 |
|
460 end |
|
461 |
|
462 end |