author hoelzl Thu Jan 17 12:26:54 2013 +0100 (2013-01-17) changeset 50940 a7c273a83d27 parent 50939 ae7cd20ed118 child 50941 3690724028b1
group compactness-eq-seq-compactness lemmas together
```     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")
```