# HG changeset patch # User huffman # Date 1244565536 25200 # Node ID d1b7f1f682ce86f1ea492157a3ec4e993682a78d # Parent f5bde0d3c3857b9fdb4c809b5608a8e610c7c157 new class heine_borel for lemma bounded_closed_imp_compact; instances for real, ^ diff -r f5bde0d3c385 -r d1b7f1f682ce src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Mon Jun 08 19:45:24 2009 -0700 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Tue Jun 09 09:38:56 2009 -0700 @@ -2220,6 +2220,30 @@ (\f. (\n::nat. f n \ S) \ (\l\S. \r. (\m n. m < n \ r m < r n) \ ((f o r) ---> l) sequentially))" +text {* + A metric space (or topological vector space) is said to have the + Heine-Borel property if every closed and bounded subset is compact. +*} + +class heine_borel = + assumes bounded_imp_convergent_subsequence: + "bounded s \ \n::nat. f n \ s + \ \l r. (\m n. m < n --> r m < r n) \ ((f \ r) ---> l) sequentially" + +lemma bounded_closed_imp_compact: + fixes s::"'a::heine_borel set" + assumes "bounded s" and "closed s" shows "compact s" +proof (unfold compact_def, clarify) + fix f :: "nat \ 'a" assume f: "\n. f n \ s" + obtain l r where r: "\m n. m < n \ r m < r n" and l: "((f \ r) ---> l) sequentially" + using bounded_imp_convergent_subsequence [OF `bounded s` `\n. f n \ s`] by auto + from f have fr: "\n. (f \ r) n \ s" by simp + have "l \ s" using `closed s` fr l + unfolding closed_sequential_limits by blast + show "\l\s. \r. (\m n. m < n \ r m < r n) \ ((f \ r) ---> l) sequentially" + using `l \ s` r l by blast +qed + lemma monotone_bigger: fixes r::"nat\nat" assumes "\m n::nat. m < n --> r m < r n" shows "n \ r n" @@ -2231,6 +2255,12 @@ ultimately show "Suc n \ r (Suc n)" by auto qed +lemma eventually_subsequence: + assumes r: "\m n. m < n \ r m < r n" + shows "eventually P sequentially \ eventually (\n. P (r n)) sequentially" +unfolding eventually_sequentially +by (metis monotone_bigger [OF r] le_trans) + lemma lim_subsequence: fixes l :: "'a::metric_space" (* TODO: generalize *) shows "\m n. m < n \ r m < r n \ (s ---> l) sequentially \ ((s o r) ---> l) sequentially" @@ -2276,87 +2306,97 @@ unfolding abs_minus_cancel by(rule_tac x="-l" in exI)auto lemma compact_real_lemma: - assumes "\n::nat. abs(s n) \ b" - shows "\l r. (\m n::nat. m < n --> r m < r n) \ - (\e>0::real. \N. \n\N. (abs(s (r n) - l) < e))" + assumes "\n::nat. abs(s n) \ b" + shows "\(l::real) r. (\m n::nat. m < n --> r m < r n) \ ((s \ r) ---> l) sequentially" proof- obtain r where r:"\m n::nat. m < n \ r m < r n" "(\m n. m \ n \ s (r m) \ s (r n)) \ (\m n. m \ n \ s (r n) \ s (r m))" using seq_monosub[of s] by (auto simp add: subseq_def monoseq_def) - thus ?thesis using convergent_bounded_monotone[of "s o r" b] and assms by auto -qed + thus ?thesis using convergent_bounded_monotone[of "s o r" b] and assms + unfolding tendsto_iff dist_norm eventually_sequentially by auto +qed + +instance real :: heine_borel +proof + fix s :: "real set" and f :: "nat \ real" + assume s: "bounded s" and f: "\n. f n \ s" + then obtain b where b: "\n. abs (f n) \ b" + unfolding bounded_iff by auto + obtain l :: real and r :: "nat \ nat" where + r: "\m n. m < n \ r m < r n" and l: "((f \ r) ---> l) sequentially" + using compact_real_lemma [OF b] by auto + thus "\l r. (\m n. m < n \ r m < r n) \ ((f \ r) ---> l) sequentially" + by auto +qed + +lemma bounded_component: "bounded s \ bounded ((\x. x $ i) ` s)" +unfolding bounded_def +apply clarify +apply (rule_tac x="x $ i" in exI) +apply (rule_tac x="e" in exI) +apply clarify +apply (rule order_trans [OF dist_nth_le], simp) +done lemma compact_lemma: - assumes "bounded s" and "\n. (x::nat \real^'a::finite) n \ s" + fixes f :: "nat \ 'a::heine_borel ^ 'n::finite" + assumes "bounded s" and "\n. f n \ s" shows "\d. - \l::(real^'a::finite). \ r. (\n m::nat. m < n --> r m < r n) \ - (\e>0. \N. \n\N. \i\d. \x (r n) $ i - l $ i\ < e)" -proof- - obtain b where b:"\x\s. norm x \ b" using assms(1)[unfolded bounded_iff] by auto - { { fix i::'a - { fix n::nat - have "\x n $ i\ \ b" using b[THEN bspec[where x="x n"]] and component_le_norm[of "x n" i] and assms(2)[THEN spec[where x=n]] by auto } - hence "\n. \x n $ i\ \ b" by auto - } note b' = this - - fix d::"'a set" have "finite d" by simp - hence "\l::(real^'a). \ r. (\n m::nat. m < n --> r m < r n) \ - (\e>0. \N. \n\N. \i\d. \x (r n) $ i - l $ i\ < e)" - proof(induct d) case empty thus ?case by auto - next case (insert k d) - obtain l1::"real^'a" and r1 where r1:"\n m::nat. m < n \ r1 m < r1 n" and lr1:"\e>0. \N. \n\N. \i\d. \x (r1 n) $ i - l1 $ i\ < e" - using insert(3) by auto - obtain l2 r2 where r2:"\m n::nat. m < n \ r2 m < r2 n" and lr2:"\e>0. \N. \n\N. \(x \ r1) (r2 n) $ k - l2\ < e" - using b'[of k] and compact_real_lemma[of "\i. ((x \ r1) i)$k" b] by auto - def r \ "r1 \ r2" have r:"\m n. m < n \ r m < r n" unfolding r_def o_def using r1 and r2 by auto - moreover - def l \ "(\ i. if i = k then l2 else l1$i)::real^'a" - { fix e::real assume "e>0" - from lr1 obtain N1 where N1:"\n\N1. \i\d. \x (r1 n) $ i - l1 $ i\ < e" using `e>0` by blast - from lr2 obtain N2 where N2:"\n\N2. \(x \ r1) (r2 n) $ k - l2\ < e" using `e>0` by blast - { fix n assume n:"n\ N1 + N2" - fix i assume i:"i\(insert k d)" - hence "\x (r n) $ i - l $ i\ < e" - using N2[THEN spec[where x="n"]] and n - using N1[THEN spec[where x="r2 n"]] and n - using monotone_bigger[OF r] and i - unfolding l_def and r_def - using monotone_bigger[OF r2, of n] by auto } - hence "\N. \n\N. \i\(insert k d). \x (r n) $ i - l $ i\ < e" by blast } - ultimately show ?case by auto - qed } - thus ?thesis by auto -qed - -lemma bounded_closed_imp_compact: fixes s::"(real^'a::finite) set" - assumes "bounded s" and "closed s" - shows "compact s" -proof- - let ?d = "UNIV::'a set" - { fix f assume as:"\n::nat. f n \ s" - obtain l::"real^'a" and r where r:"\n m::nat. m < n \ r m < r n" - and lr:"\e>0. \N. \n\N. \i\?d. \f (r n) $ i - l $ i\ < e" - using compact_lemma[OF assms(1) as, THEN spec[where x="?d"]] by auto + \l r. (\n m::nat. m < n --> r m < r n) \ + (\e>0. eventually (\n. \i\d. dist (f (r n) $ i) (l $ i) < e) sequentially)" +proof + fix d::"'n set" have "finite d" by simp + thus "\l::'a ^ 'n. \r. (\n m::nat. m < n --> r m < r n) \ + (\e>0. eventually (\n. \i\d. dist (f (r n) $ i) (l $ i) < e) sequentially)" + proof(induct d) case empty thus ?case by auto + next case (insert k d) + have s': "bounded ((\x. x $ k) ` s)" using `bounded s` by (rule bounded_component) + obtain l1::"'a^'n" and r1 where r1:"\n m::nat. m < n \ r1 m < r1 n" and lr1:"\e>0. eventually (\n. \i\d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially" + using insert(3) by auto + have f': "\n. f (r1 n) $ k \ (\x. x $ k) ` s" using `\n. f n \ s` by simp + obtain l2 r2 where r2:"\m n::nat. m < n \ r2 m < r2 n" and lr2:"((\i. f (r1 (r2 i)) $ k) ---> l2) sequentially" + using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto + def r \ "r1 \ r2" have r:"\m n. m < n \ r m < r n" unfolding r_def o_def using r1 and r2 by auto + moreover + def l \ "(\ i. if i = k then l2 else l1$i)::'a^'n" { fix e::real assume "e>0" - hence "0 < e / (real_of_nat (card ?d))" using zero_less_card_finite using divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto - then obtain N::nat where N:"\n\N. \i\?d. \f (r n) $ i - l $ i\ < e / (real_of_nat (card ?d))" using lr[THEN spec[where x="e / (real_of_nat (card ?d))"]] by blast - { fix n assume n:"n\N" - hence "finite ?d" "?d \ {}" by auto - moreover - { fix i assume i:"i \ ?d" - hence "\((f \ r) n - l) $ i\ < e / real_of_nat (card ?d)" using `n\N` using N[THEN spec[where x=n]] - by auto } - ultimately have "(\i \ ?d. \((f \ r) n - l) $ i\) - < (\i \ ?d. e / real_of_nat (card ?d))" - using setsum_strict_mono[of "?d" "\i. \((f \ r) n - l) $ i\" "\i. e / (real_of_nat (card ?d))"] by auto - hence "(\i \ ?d. \((f \ r) n - l) $ i\) < e" unfolding setsum_constant by auto - hence "dist ((f \ r) n) l < e" unfolding dist_norm using norm_le_l1[of "(f \ r) n - l"] by auto } - hence "\N. \n\N. dist ((f \ r) n) l < e" by auto } - hence *:"((f \ r) ---> l) sequentially" unfolding Lim_sequentially by auto - moreover have "l\s" - using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="f \ r"], THEN spec[where x=l]] and * and as by auto - ultimately have "\l\s. \r. (\m n. m < n \ r m < r n) \ ((f \ r) ---> l) sequentially" using r by auto } - thus ?thesis unfolding compact_def by auto + from lr1 `e>0` have N1:"eventually (\n. \i\d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially" by blast + from lr2 `e>0` have N2:"eventually (\n. dist (f (r1 (r2 n)) $ k) l2 < e) sequentially" by (rule tendstoD) + from r2 N1 have N1': "eventually (\n. \i\d. dist (f (r1 (r2 n)) $ i) (l1 $ i) < e) sequentially" + by (rule eventually_subsequence) + have "eventually (\n. \i\(insert k d). dist (f (r n) $ i) (l $ i) < e) sequentially" + using N1' N2 by (rule eventually_elim2, simp add: l_def r_def) + } + ultimately show ?case by auto + qed +qed + +instance "^" :: (heine_borel, finite) heine_borel +proof + fix s :: "('a ^ 'b) set" and f :: "nat \ 'a ^ 'b" + assume s: "bounded s" and f: "\n. f n \ s" + then obtain l r where r: "\n m::nat. m < n --> r m < r n" + and l: "\e>0. eventually (\n. \i\UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially" + using compact_lemma [OF s f] by blast + let ?d = "UNIV::'b set" + { fix e::real assume "e>0" + hence "0 < e / (real_of_nat (card ?d))" + using zero_less_card_finite using divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto + with l have "eventually (\n. \i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))) sequentially" + by simp + moreover + { fix n assume n: "\i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))" + have "dist (f (r n)) l \ (\i\?d. dist (f (r n) $ i) (l $ i))" + unfolding dist_vector_def using zero_le_dist by (rule setL2_le_setsum) + also have "\ < (\i\?d. e / (real_of_nat (card ?d)))" + by (rule setsum_strict_mono) (simp_all add: n) + finally have "dist (f (r n)) l < e" by simp + } + ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" + by (rule eventually_elim1) + } + hence *:"((f \ r) ---> l) sequentially" unfolding o_def tendsto_iff by simp + with r show "\l r. (\m n. m < n \ r m < r n) \ ((f \ r) ---> l) sequentially" by auto qed subsection{* Completeness. *}