4441 unfolding Bseq_eq_bounded using f by (force intro: bounded_subset) |
4441 unfolding Bseq_eq_bounded using f by (force intro: bounded_subset) |
4442 with r show "\<exists>l r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l" |
4442 with r show "\<exists>l r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l" |
4443 using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def) |
4443 using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def) |
4444 qed |
4444 qed |
4445 |
4445 |
4446 lemma compact_lemma: |
4446 lemma compact_lemma_general: |
4447 fixes f :: "nat \<Rightarrow> 'a::euclidean_space" |
4447 fixes f :: "nat \<Rightarrow> 'a" |
4448 assumes "bounded (range f)" |
4448 fixes proj::"'a \<Rightarrow> 'b \<Rightarrow> 'c::heine_borel" (infixl "proj" 60) |
4449 shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r. |
4449 fixes unproj:: "('b \<Rightarrow> 'c) \<Rightarrow> 'a" |
4450 subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)" |
4450 assumes finite_basis: "finite basis" |
|
4451 assumes bounded_proj: "\<And>k. k \<in> basis \<Longrightarrow> bounded ((\<lambda>x. x proj k) ` range f)" |
|
4452 assumes proj_unproj: "\<And>e k. k \<in> basis \<Longrightarrow> (unproj e) proj k = e k" |
|
4453 assumes unproj_proj: "\<And>x. unproj (\<lambda>k. x proj k) = x" |
|
4454 shows "\<forall>d\<subseteq>basis. \<exists>l::'a. \<exists> r. |
|
4455 subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)" |
4451 proof safe |
4456 proof safe |
4452 fix d :: "'a set" |
4457 fix d :: "'b set" |
4453 assume d: "d \<subseteq> Basis" |
4458 assume d: "d \<subseteq> basis" |
4454 with finite_Basis have "finite d" |
4459 with finite_basis have "finite d" |
4455 by (blast intro: finite_subset) |
4460 by (blast intro: finite_subset) |
4456 from this d show "\<exists>l::'a. \<exists>r. subseq r \<and> |
4461 from this d show "\<exists>l::'a. \<exists>r. subseq r \<and> |
4457 (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)" |
4462 (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)" |
4458 proof (induct d) |
4463 proof (induct d) |
4459 case empty |
4464 case empty |
4460 then show ?case |
4465 then show ?case |
4461 unfolding subseq_def by auto |
4466 unfolding subseq_def by auto |
4462 next |
4467 next |
4463 case (insert k d) |
4468 case (insert k d) |
4464 have k[intro]: "k \<in> Basis" |
4469 have k[intro]: "k \<in> basis" |
4465 using insert by auto |
4470 using insert by auto |
4466 have s': "bounded ((\<lambda>x. x \<bullet> k) ` range f)" |
4471 have s': "bounded ((\<lambda>x. x proj k) ` range f)" |
4467 using \<open>bounded (range f)\<close> |
4472 using k |
4468 by (auto intro!: bounded_linear_image bounded_linear_inner_left) |
4473 by (rule bounded_proj) |
4469 obtain l1::"'a" and r1 where r1: "subseq r1" |
4474 obtain l1::"'a" and r1 where r1: "subseq r1" |
4470 and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially" |
4475 and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially" |
4471 using insert(3) using insert(4) by auto |
4476 using insert(3) using insert(4) by auto |
4472 have f': "\<forall>n. f (r1 n) \<bullet> k \<in> (\<lambda>x. x \<bullet> k) ` range f" |
4477 have f': "\<forall>n. f (r1 n) proj k \<in> (\<lambda>x. x proj k) ` range f" |
4473 by simp |
4478 by simp |
4474 have "bounded (range (\<lambda>i. f (r1 i) \<bullet> k))" |
4479 have "bounded (range (\<lambda>i. f (r1 i) proj k))" |
4475 by (metis (lifting) bounded_subset f' image_subsetI s') |
4480 by (metis (lifting) bounded_subset f' image_subsetI s') |
4476 then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) \<longlongrightarrow> l2) sequentially" |
4481 then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) proj k) \<longlongrightarrow> l2) sequentially" |
4477 using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) \<bullet> k"] |
4482 using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) proj k"] |
4478 by (auto simp: o_def) |
4483 by (auto simp: o_def) |
4479 def r \<equiv> "r1 \<circ> r2" |
4484 def r \<equiv> "r1 \<circ> r2" |
4480 have r:"subseq r" |
4485 have r:"subseq r" |
4481 using r1 and r2 unfolding r_def o_def subseq_def by auto |
4486 using r1 and r2 unfolding r_def o_def subseq_def by auto |
4482 moreover |
4487 moreover |
4483 def l \<equiv> "(\<Sum>i\<in>Basis. (if i = k then l2 else l1\<bullet>i) *\<^sub>R i)::'a" |
4488 def l \<equiv> "unproj (\<lambda>i. if i = k then l2 else l1 proj i)::'a" |
4484 { |
4489 { |
4485 fix e::real |
4490 fix e::real |
4486 assume "e > 0" |
4491 assume "e > 0" |
4487 from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially" |
4492 from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially" |
4488 by blast |
4493 by blast |
4489 from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) \<bullet> k) l2 < e) sequentially" |
4494 from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) proj k) l2 < e) sequentially" |
4490 by (rule tendstoD) |
4495 by (rule tendstoD) |
4491 from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) \<bullet> i) (l1 \<bullet> i) < e) sequentially" |
4496 from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e) sequentially" |
4492 by (rule eventually_subseq) |
4497 by (rule eventually_subseq) |
4493 have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially" |
4498 have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) proj i) (l proj i) < e) sequentially" |
4494 using N1' N2 |
4499 using N1' N2 |
4495 by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def) |
4500 by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def proj_unproj) |
4496 } |
4501 } |
4497 ultimately show ?case by auto |
4502 ultimately show ?case by auto |
4498 qed |
4503 qed |
4499 qed |
4504 qed |
|
4505 |
|
4506 lemma compact_lemma: |
|
4507 fixes f :: "nat \<Rightarrow> 'a::euclidean_space" |
|
4508 assumes "bounded (range f)" |
|
4509 shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r. |
|
4510 subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)" |
|
4511 by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"]) |
|
4512 (auto intro!: assms bounded_linear_inner_left bounded_linear_image |
|
4513 simp: euclidean_representation) |
4500 |
4514 |
4501 instance euclidean_space \<subseteq> heine_borel |
4515 instance euclidean_space \<subseteq> heine_borel |
4502 proof |
4516 proof |
4503 fix f :: "nat \<Rightarrow> 'a" |
4517 fix f :: "nat \<Rightarrow> 'a" |
4504 assume f: "bounded (range f)" |
4518 assume f: "bounded (range f)" |