group compactness-eq-seq-compactness lemmas together
authorhoelzl
Thu Jan 17 12:26:54 2013 +0100 (2013-01-17)
changeset 50940a7c273a83d27
parent 50939 ae7cd20ed118
child 50941 3690724028b1
group compactness-eq-seq-compactness lemmas together
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 12:21:24 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 12:26:54 2013 +0100
     1.3 @@ -2992,6 +2992,122 @@
     1.4    thus ?thesis unfolding seq_compact_def by auto
     1.5  qed
     1.6  
     1.7 +subsubsection{* Total boundedness *}
     1.8 +
     1.9 +lemma cauchy_def:
    1.10 +  "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
    1.11 +unfolding Cauchy_def by blast
    1.12 +
    1.13 +fun helper_1::"('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where
    1.14 +  "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
    1.15 +declare helper_1.simps[simp del]
    1.16 +
    1.17 +lemma seq_compact_imp_totally_bounded:
    1.18 +  assumes "seq_compact s"
    1.19 +  shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))"
    1.20 +proof(rule, rule, rule ccontr)
    1.21 +  fix e::real assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k)"
    1.22 +  def x \<equiv> "helper_1 s e"
    1.23 +  { fix n
    1.24 +    have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
    1.25 +    proof(induct_tac rule:nat_less_induct)
    1.26 +      fix n  def Q \<equiv> "(\<lambda>y. y \<in> s \<and> (\<forall>m<n. \<not> dist (x m) y < e))"
    1.27 +      assume as:"\<forall>m<n. x m \<in> s \<and> (\<forall>ma<m. \<not> dist (x ma) (x m) < e)"
    1.28 +      have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)" using assm apply simp apply(erule_tac x="x ` {0 ..< n}" in allE) using as by auto
    1.29 +      then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)" unfolding subset_eq by auto
    1.30 +      have "Q (x n)" unfolding x_def and helper_1.simps[of s e n]
    1.31 +        apply(rule someI2[where a=z]) unfolding x_def[symmetric] and Q_def using z by auto
    1.32 +      thus "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)" unfolding Q_def by auto
    1.33 +    qed }
    1.34 +  hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)" by blast+
    1.35 +  then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially" using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto
    1.36 +  from this(3) have "Cauchy (x \<circ> r)" using LIMSEQ_imp_Cauchy by auto
    1.37 +  then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e" unfolding cauchy_def using `e>0` by auto
    1.38 +  show False
    1.39 +    using N[THEN spec[where x=N], THEN spec[where x="N+1"]]
    1.40 +    using r[unfolded subseq_def, THEN spec[where x=N], THEN spec[where x="N+1"]]
    1.41 +    using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] by auto
    1.42 +qed
    1.43 +
    1.44 +subsubsection{* Heine-Borel theorem *}
    1.45 +
    1.46 +text {* Following Burkill \& Burkill vol. 2. *}
    1.47 +
    1.48 +lemma heine_borel_lemma: fixes s::"'a::metric_space set"
    1.49 +  assumes "seq_compact s"  "s \<subseteq> (\<Union> t)"  "\<forall>b \<in> t. open b"
    1.50 +  shows "\<exists>e>0. \<forall>x \<in> s. \<exists>b \<in> t. ball x e \<subseteq> b"
    1.51 +proof(rule ccontr)
    1.52 +  assume "\<not> (\<exists>e>0. \<forall>x\<in>s. \<exists>b\<in>t. ball x e \<subseteq> b)"
    1.53 +  hence cont:"\<forall>e>0. \<exists>x\<in>s. \<forall>xa\<in>t. \<not> (ball x e \<subseteq> xa)" by auto
    1.54 +  { fix n::nat
    1.55 +    have "1 / real (n + 1) > 0" by auto
    1.56 +    hence "\<exists>x. x\<in>s \<and> (\<forall>xa\<in>t. \<not> (ball x (inverse (real (n+1))) \<subseteq> xa))" using cont unfolding Bex_def by auto }
    1.57 +  hence "\<forall>n::nat. \<exists>x. x \<in> s \<and> (\<forall>xa\<in>t. \<not> ball x (inverse (real (n + 1))) \<subseteq> xa)" by auto
    1.58 +  then obtain f where f:"\<forall>n::nat. f n \<in> s \<and> (\<forall>xa\<in>t. \<not> ball (f n) (inverse (real (n + 1))) \<subseteq> xa)"
    1.59 +    using choice[of "\<lambda>n::nat. \<lambda>x. x\<in>s \<and> (\<forall>xa\<in>t. \<not> ball x (inverse (real (n + 1))) \<subseteq> xa)"] by auto
    1.60 +
    1.61 +  then obtain l r where l:"l\<in>s" and r:"subseq r" and lr:"((f \<circ> r) ---> l) sequentially"
    1.62 +    using assms(1)[unfolded seq_compact_def, THEN spec[where x=f]] by auto
    1.63 +
    1.64 +  obtain b where "l\<in>b" "b\<in>t" using assms(2) and l by auto
    1.65 +  then obtain e where "e>0" and e:"\<forall>z. dist z l < e \<longrightarrow> z\<in>b"
    1.66 +    using assms(3)[THEN bspec[where x=b]] unfolding open_dist by auto
    1.67 +
    1.68 +  then obtain N1 where N1:"\<forall>n\<ge>N1. dist ((f \<circ> r) n) l < e / 2"
    1.69 +    using lr[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] by auto
    1.70 +
    1.71 +  obtain N2::nat where N2:"N2>0" "inverse (real N2) < e /2" using real_arch_inv[of "e/2"] and `e>0` by auto
    1.72 +  have N2':"inverse (real (r (N1 + N2) +1 )) < e/2"
    1.73 +    apply(rule order_less_trans) apply(rule less_imp_inverse_less) using N2
    1.74 +    using seq_suble[OF r, of "N1 + N2"] by auto
    1.75 +
    1.76 +  def x \<equiv> "(f (r (N1 + N2)))"
    1.77 +  have x:"\<not> ball x (inverse (real (r (N1 + N2) + 1))) \<subseteq> b" unfolding x_def
    1.78 +    using f[THEN spec[where x="r (N1 + N2)"]] using `b\<in>t` by auto
    1.79 +  have "\<exists>y\<in>ball x (inverse (real (r (N1 + N2) + 1))). y\<notin>b" apply(rule ccontr) using x by auto
    1.80 +  then obtain y where y:"y \<in> ball x (inverse (real (r (N1 + N2) + 1)))" "y \<notin> b" by auto
    1.81 +
    1.82 +  have "dist x l < e/2" using N1 unfolding x_def o_def by auto
    1.83 +  hence "dist y l < e" using y N2' using dist_triangle[of y l x]by (auto simp add:dist_commute)
    1.84 +
    1.85 +  thus False using e and `y\<notin>b` by auto
    1.86 +qed
    1.87 +
    1.88 +lemma seq_compact_imp_heine_borel:
    1.89 +  fixes s :: "'a :: metric_space set"
    1.90 +  shows "seq_compact s \<Longrightarrow> compact s"
    1.91 +  unfolding compact_eq_heine_borel
    1.92 +proof clarify
    1.93 +  fix f assume "seq_compact s" " \<forall>t\<in>f. open t" "s \<subseteq> \<Union>f"
    1.94 +  then obtain e::real where "e>0" and "\<forall>x\<in>s. \<exists>b\<in>f. ball x e \<subseteq> b" using heine_borel_lemma[of s f] by auto
    1.95 +  hence "\<forall>x\<in>s. \<exists>b. b\<in>f \<and> ball x e \<subseteq> b" by auto
    1.96 +  hence "\<exists>bb. \<forall>x\<in>s. bb x \<in>f \<and> ball x e \<subseteq> bb x" using bchoice[of s "\<lambda>x b. b\<in>f \<and> ball x e \<subseteq> b"] by auto
    1.97 +  then obtain  bb where bb:"\<forall>x\<in>s. (bb x) \<in> f \<and> ball x e \<subseteq> (bb x)" by blast
    1.98 +
    1.99 +  from `seq_compact s` have  "\<exists> k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k"
   1.100 +    using seq_compact_imp_totally_bounded[of s] `e>0` by auto
   1.101 +  then obtain k where k:"finite k" "k \<subseteq> s" "s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k" by auto
   1.102 +
   1.103 +  have "finite (bb ` k)" using k(1) by auto
   1.104 +  moreover
   1.105 +  { fix x assume "x\<in>s"
   1.106 +    hence "x\<in>\<Union>(\<lambda>x. ball x e) ` k" using k(3)  unfolding subset_eq by auto
   1.107 +    hence "\<exists>X\<in>bb ` k. x \<in> X" using bb k(2) by blast
   1.108 +    hence "x \<in> \<Union>(bb ` k)" using  Union_iff[of x "bb ` k"] by auto
   1.109 +  }
   1.110 +  ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f'" using bb k(2) by (rule_tac x="bb ` k" in exI) auto
   1.111 +qed
   1.112 +
   1.113 +lemma compact_eq_seq_compact_metric:
   1.114 +  "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
   1.115 +  using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
   1.116 +
   1.117 +lemma compact_def:
   1.118 +  "compact (S :: 'a::metric_space set) \<longleftrightarrow>
   1.119 +   (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow>
   1.120 +       (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f o r) ---> l) sequentially)) "
   1.121 +  unfolding compact_eq_seq_compact_metric seq_compact_def by auto
   1.122 +
   1.123  text {*
   1.124    A metric space (or topological vector space) is said to have the
   1.125    Heine-Borel property if every closed and bounded subset is compact.
   1.126 @@ -3214,10 +3330,6 @@
   1.127  
   1.128  subsubsection{* Completeness *}
   1.129  
   1.130 -lemma cauchy_def:
   1.131 -  "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
   1.132 -unfolding Cauchy_def by blast
   1.133 -
   1.134  definition
   1.135    complete :: "'a::metric_space set \<Rightarrow> bool" where
   1.136    "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f
   1.137 @@ -3344,108 +3456,6 @@
   1.138    shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
   1.139    by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
   1.140  
   1.141 -subsubsection{* Total boundedness *}
   1.142 -
   1.143 -fun helper_1::"('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where
   1.144 -  "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
   1.145 -declare helper_1.simps[simp del]
   1.146 -
   1.147 -lemma seq_compact_imp_totally_bounded:
   1.148 -  assumes "seq_compact s"
   1.149 -  shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))"
   1.150 -proof(rule, rule, rule ccontr)
   1.151 -  fix e::real assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k)"
   1.152 -  def x \<equiv> "helper_1 s e"
   1.153 -  { fix n
   1.154 -    have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
   1.155 -    proof(induct_tac rule:nat_less_induct)
   1.156 -      fix n  def Q \<equiv> "(\<lambda>y. y \<in> s \<and> (\<forall>m<n. \<not> dist (x m) y < e))"
   1.157 -      assume as:"\<forall>m<n. x m \<in> s \<and> (\<forall>ma<m. \<not> dist (x ma) (x m) < e)"
   1.158 -      have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)" using assm apply simp apply(erule_tac x="x ` {0 ..< n}" in allE) using as by auto
   1.159 -      then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)" unfolding subset_eq by auto
   1.160 -      have "Q (x n)" unfolding x_def and helper_1.simps[of s e n]
   1.161 -        apply(rule someI2[where a=z]) unfolding x_def[symmetric] and Q_def using z by auto
   1.162 -      thus "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)" unfolding Q_def by auto
   1.163 -    qed }
   1.164 -  hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)" by blast+
   1.165 -  then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially" using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto
   1.166 -  from this(3) have "Cauchy (x \<circ> r)" using LIMSEQ_imp_Cauchy by auto
   1.167 -  then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e" unfolding cauchy_def using `e>0` by auto
   1.168 -  show False
   1.169 -    using N[THEN spec[where x=N], THEN spec[where x="N+1"]]
   1.170 -    using r[unfolded subseq_def, THEN spec[where x=N], THEN spec[where x="N+1"]]
   1.171 -    using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] by auto
   1.172 -qed
   1.173 -
   1.174 -subsubsection{* Heine-Borel theorem *}
   1.175 -
   1.176 -text {* Following Burkill \& Burkill vol. 2. *}
   1.177 -
   1.178 -lemma heine_borel_lemma: fixes s::"'a::metric_space set"
   1.179 -  assumes "seq_compact s"  "s \<subseteq> (\<Union> t)"  "\<forall>b \<in> t. open b"
   1.180 -  shows "\<exists>e>0. \<forall>x \<in> s. \<exists>b \<in> t. ball x e \<subseteq> b"
   1.181 -proof(rule ccontr)
   1.182 -  assume "\<not> (\<exists>e>0. \<forall>x\<in>s. \<exists>b\<in>t. ball x e \<subseteq> b)"
   1.183 -  hence cont:"\<forall>e>0. \<exists>x\<in>s. \<forall>xa\<in>t. \<not> (ball x e \<subseteq> xa)" by auto
   1.184 -  { fix n::nat
   1.185 -    have "1 / real (n + 1) > 0" by auto
   1.186 -    hence "\<exists>x. x\<in>s \<and> (\<forall>xa\<in>t. \<not> (ball x (inverse (real (n+1))) \<subseteq> xa))" using cont unfolding Bex_def by auto }
   1.187 -  hence "\<forall>n::nat. \<exists>x. x \<in> s \<and> (\<forall>xa\<in>t. \<not> ball x (inverse (real (n + 1))) \<subseteq> xa)" by auto
   1.188 -  then obtain f where f:"\<forall>n::nat. f n \<in> s \<and> (\<forall>xa\<in>t. \<not> ball (f n) (inverse (real (n + 1))) \<subseteq> xa)"
   1.189 -    using choice[of "\<lambda>n::nat. \<lambda>x. x\<in>s \<and> (\<forall>xa\<in>t. \<not> ball x (inverse (real (n + 1))) \<subseteq> xa)"] by auto
   1.190 -
   1.191 -  then obtain l r where l:"l\<in>s" and r:"subseq r" and lr:"((f \<circ> r) ---> l) sequentially"
   1.192 -    using assms(1)[unfolded seq_compact_def, THEN spec[where x=f]] by auto
   1.193 -
   1.194 -  obtain b where "l\<in>b" "b\<in>t" using assms(2) and l by auto
   1.195 -  then obtain e where "e>0" and e:"\<forall>z. dist z l < e \<longrightarrow> z\<in>b"
   1.196 -    using assms(3)[THEN bspec[where x=b]] unfolding open_dist by auto
   1.197 -
   1.198 -  then obtain N1 where N1:"\<forall>n\<ge>N1. dist ((f \<circ> r) n) l < e / 2"
   1.199 -    using lr[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] by auto
   1.200 -
   1.201 -  obtain N2::nat where N2:"N2>0" "inverse (real N2) < e /2" using real_arch_inv[of "e/2"] and `e>0` by auto
   1.202 -  have N2':"inverse (real (r (N1 + N2) +1 )) < e/2"
   1.203 -    apply(rule order_less_trans) apply(rule less_imp_inverse_less) using N2
   1.204 -    using seq_suble[OF r, of "N1 + N2"] by auto
   1.205 -
   1.206 -  def x \<equiv> "(f (r (N1 + N2)))"
   1.207 -  have x:"\<not> ball x (inverse (real (r (N1 + N2) + 1))) \<subseteq> b" unfolding x_def
   1.208 -    using f[THEN spec[where x="r (N1 + N2)"]] using `b\<in>t` by auto
   1.209 -  have "\<exists>y\<in>ball x (inverse (real (r (N1 + N2) + 1))). y\<notin>b" apply(rule ccontr) using x by auto
   1.210 -  then obtain y where y:"y \<in> ball x (inverse (real (r (N1 + N2) + 1)))" "y \<notin> b" by auto
   1.211 -
   1.212 -  have "dist x l < e/2" using N1 unfolding x_def o_def by auto
   1.213 -  hence "dist y l < e" using y N2' using dist_triangle[of y l x]by (auto simp add:dist_commute)
   1.214 -
   1.215 -  thus False using e and `y\<notin>b` by auto
   1.216 -qed
   1.217 -
   1.218 -lemma seq_compact_imp_heine_borel:
   1.219 -  fixes s :: "'a :: metric_space set"
   1.220 -  shows "seq_compact s \<Longrightarrow> compact s"
   1.221 -  unfolding compact_eq_heine_borel
   1.222 -proof clarify
   1.223 -  fix f assume "seq_compact s" " \<forall>t\<in>f. open t" "s \<subseteq> \<Union>f"
   1.224 -  then obtain e::real where "e>0" and "\<forall>x\<in>s. \<exists>b\<in>f. ball x e \<subseteq> b" using heine_borel_lemma[of s f] by auto
   1.225 -  hence "\<forall>x\<in>s. \<exists>b. b\<in>f \<and> ball x e \<subseteq> b" by auto
   1.226 -  hence "\<exists>bb. \<forall>x\<in>s. bb x \<in>f \<and> ball x e \<subseteq> bb x" using bchoice[of s "\<lambda>x b. b\<in>f \<and> ball x e \<subseteq> b"] by auto
   1.227 -  then obtain  bb where bb:"\<forall>x\<in>s. (bb x) \<in> f \<and> ball x e \<subseteq> (bb x)" by blast
   1.228 -
   1.229 -  from `seq_compact s` have  "\<exists> k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k"
   1.230 -    using seq_compact_imp_totally_bounded[of s] `e>0` by auto
   1.231 -  then obtain k where k:"finite k" "k \<subseteq> s" "s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k" by auto
   1.232 -
   1.233 -  have "finite (bb ` k)" using k(1) by auto
   1.234 -  moreover
   1.235 -  { fix x assume "x\<in>s"
   1.236 -    hence "x\<in>\<Union>(\<lambda>x. ball x e) ` k" using k(3)  unfolding subset_eq by auto
   1.237 -    hence "\<exists>X\<in>bb ` k. x \<in> X" using bb k(2) by blast
   1.238 -    hence "x \<in> \<Union>(bb ` k)" using  Union_iff[of x "bb ` k"] by auto
   1.239 -  }
   1.240 -  ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f'" using bb k(2) by (rule_tac x="bb ` k" in exI) auto
   1.241 -qed
   1.242 -
   1.243  subsubsection {* Complete the chain of compactness variants *}
   1.244  
   1.245  primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where
   1.246 @@ -3514,16 +3524,6 @@
   1.247  
   1.248  text {* Hence express everything as an equivalence. *}
   1.249  
   1.250 -lemma compact_eq_seq_compact_metric:
   1.251 -  "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
   1.252 -  using compact_imp_seq_compact seq_compact_imp_heine_borel by blast
   1.253 -
   1.254 -lemma compact_def:
   1.255 -  "compact (S :: 'a::metric_space set) \<longleftrightarrow>
   1.256 -   (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow>
   1.257 -       (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f o r) ---> l) sequentially)) "
   1.258 -  unfolding compact_eq_seq_compact_metric seq_compact_def by auto
   1.259 -
   1.260  lemma compact_eq_bolzano_weierstrass:
   1.261    fixes s :: "'a::metric_space set"
   1.262    shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" (is "?lhs = ?rhs")