src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 50883 1421884baf5b
parent 50882 a382bf90867e
child 50884 2b21b4e2d7cb
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 17:30:36 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 14 17:53:37 2013 +0100
     1.3 @@ -239,6 +239,82 @@
     1.4  
     1.5  end
     1.6  
     1.7 +class first_countable_topology = topological_space +
     1.8 +  assumes first_countable_basis:
     1.9 +    "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
    1.10 +
    1.11 +lemma (in first_countable_topology) countable_basis_at_decseq:
    1.12 +  obtains A :: "nat \<Rightarrow> 'a set" where
    1.13 +    "\<And>i. open (A i)" "\<And>i. x \<in> (A i)"
    1.14 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
    1.15 +proof atomize_elim
    1.16 +  from first_countable_basis[of x] obtain A
    1.17 +    where "countable A"
    1.18 +    and nhds: "\<And>a. a \<in> A \<Longrightarrow> open a" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a"
    1.19 +    and incl: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"  by auto
    1.20 +  then have "A \<noteq> {}" by auto
    1.21 +  with `countable A` have r: "A = range (from_nat_into A)" by auto
    1.22 +  def F \<equiv> "\<lambda>n. \<Inter>i\<le>n. from_nat_into A i"
    1.23 +  show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and>
    1.24 +      (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially)"
    1.25 +  proof (safe intro!: exI[of _ F])
    1.26 +    fix i
    1.27 +    show "open (F i)" using nhds(1) r by (auto simp: F_def intro!: open_INT)
    1.28 +    show "x \<in> F i" using nhds(2) r by (auto simp: F_def)
    1.29 +  next
    1.30 +    fix S assume "open S" "x \<in> S"
    1.31 +    from incl[OF this] obtain i where "F i \<subseteq> S"
    1.32 +      by (subst (asm) r) (auto simp: F_def)
    1.33 +    moreover have "\<And>j. i \<le> j \<Longrightarrow> F j \<subseteq> F i"
    1.34 +      by (auto simp: F_def)
    1.35 +    ultimately show "eventually (\<lambda>i. F i \<subseteq> S) sequentially"
    1.36 +      by (auto simp: eventually_sequentially)
    1.37 +  qed
    1.38 +qed
    1.39 +
    1.40 +lemma (in first_countable_topology) first_countable_basisE:
    1.41 +  obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
    1.42 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
    1.43 +  using first_countable_basis[of x]
    1.44 +  by atomize_elim auto
    1.45 +
    1.46 +instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
    1.47 +proof
    1.48 +  fix x :: "'a \<times> 'b"
    1.49 +  from first_countable_basisE[of "fst x"] guess A :: "'a set set" . note A = this
    1.50 +  from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this
    1.51 +  show "\<exists>A::('a\<times>'b) set set. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
    1.52 +  proof (intro exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
    1.53 +    fix a b assume x: "a \<in> A" "b \<in> B"
    1.54 +    with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" "open (a \<times> b)"
    1.55 +      unfolding mem_Times_iff by (auto intro: open_Times)
    1.56 +  next
    1.57 +    fix S assume "open S" "x \<in> S"
    1.58 +    from open_prod_elim[OF this] guess a' b' .
    1.59 +    moreover with A(4)[of a'] B(4)[of b']
    1.60 +    obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto
    1.61 +    ultimately show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
    1.62 +      by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
    1.63 +  qed (simp add: A B)
    1.64 +qed
    1.65 +
    1.66 +instance metric_space \<subseteq> first_countable_topology
    1.67 +proof
    1.68 +  fix x :: 'a
    1.69 +  show "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
    1.70 +  proof (intro exI, safe)
    1.71 +    fix S assume "open S" "x \<in> S"
    1.72 +    then obtain r where "0 < r" "{y. dist x y < r} \<subseteq> S"
    1.73 +      by (auto simp: open_dist dist_commute subset_eq)
    1.74 +    moreover from reals_Archimedean[OF `0 < r`] guess n ..
    1.75 +    moreover
    1.76 +    then have "{y. dist x y < inverse (Suc n)} \<subseteq> {y. dist x y < r}"
    1.77 +      by (auto simp: inverse_eq_divide)
    1.78 +    ultimately show "\<exists>a\<in>range (\<lambda>n. {y. dist x y < inverse (Suc n)}). a \<subseteq> S"
    1.79 +      by auto
    1.80 +  qed (auto intro: open_ball)
    1.81 +qed
    1.82 +
    1.83  class second_countable_topology = topological_space +
    1.84    assumes ex_countable_basis:
    1.85      "\<exists>B::'a::topological_space set set. countable B \<and> topological_basis B"
    1.86 @@ -257,6 +333,18 @@
    1.87      by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod)
    1.88  qed
    1.89  
    1.90 +instance second_countable_topology \<subseteq> first_countable_topology
    1.91 +proof
    1.92 +  fix x :: 'a
    1.93 +  def B \<equiv> "SOME B::'a set set. countable B \<and> topological_basis B"
    1.94 +  then have B: "countable B" "topological_basis B"
    1.95 +    using countable_basis is_basis
    1.96 +    by (auto simp: countable_basis is_basis)
    1.97 +  then show "\<exists>A. countable A \<and> (\<forall>a\<in>A. x \<in> a \<and> open a) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S))"
    1.98 +    by (intro exI[of _ "{b\<in>B. x \<in> b}"])
    1.99 +       (fastforce simp: topological_space_class.topological_basis_def)
   1.100 +qed
   1.101 +
   1.102  subsection {* Polish spaces *}
   1.103  
   1.104  text {* Textbooks define Polish spaces as completely metrizable.
   1.105 @@ -1350,33 +1438,38 @@
   1.106  text{* Another limit point characterization. *}
   1.107  
   1.108  lemma islimpt_sequential:
   1.109 -  fixes x :: "'a::metric_space"
   1.110 -  shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)"
   1.111 +  fixes x :: "'a::first_countable_topology"
   1.112 +  shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f ---> x) sequentially)"
   1.113      (is "?lhs = ?rhs")
   1.114  proof
   1.115    assume ?lhs
   1.116 -  then obtain f where f:"\<forall>y. y>0 \<longrightarrow> f y \<in> S \<and> f y \<noteq> x \<and> dist (f y) x < y"
   1.117 -    unfolding islimpt_approachable
   1.118 -    using choice[of "\<lambda>e y. e>0 \<longrightarrow> y\<in>S \<and> y\<noteq>x \<and> dist y x < e"] by auto
   1.119 -  let ?I = "\<lambda>n. inverse (real (Suc n))"
   1.120 -  have "\<forall>n. f (?I n) \<in> S - {x}" using f by simp
   1.121 -  moreover have "(\<lambda>n. f (?I n)) ----> x"
   1.122 -  proof (rule metric_tendsto_imp_tendsto)
   1.123 -    show "?I ----> 0"
   1.124 -      by (rule LIMSEQ_inverse_real_of_nat)
   1.125 -    show "eventually (\<lambda>n. dist (f (?I n)) x \<le> dist (?I n) 0) sequentially"
   1.126 -      by (simp add: norm_conv_dist [symmetric] less_imp_le f)
   1.127 +  from countable_basis_at_decseq[of x] guess A . note A = this
   1.128 +  def f \<equiv> "\<lambda>n. SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
   1.129 +  { fix n
   1.130 +    from `?lhs` have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
   1.131 +      unfolding islimpt_def using A(1,2)[of n] by auto
   1.132 +    then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
   1.133 +      unfolding f_def by (rule someI_ex)
   1.134 +    then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto }
   1.135 +  then have "\<forall>n. f n \<in> S - {x}" by auto
   1.136 +  moreover have "(\<lambda>n. f n) ----> x"
   1.137 +  proof (rule topological_tendstoI)
   1.138 +    fix S assume "open S" "x \<in> S"
   1.139 +    from A(3)[OF this] `\<And>n. f n \<in> A n`
   1.140 +    show "eventually (\<lambda>x. f x \<in> S) sequentially" by (auto elim!: eventually_elim1)
   1.141    qed
   1.142    ultimately show ?rhs by fast
   1.143  next
   1.144    assume ?rhs
   1.145 -  then obtain f::"nat\<Rightarrow>'a"  where f:"(\<forall>n. f n \<in> S - {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f n) x < e)" unfolding LIMSEQ_def by auto
   1.146 -  { fix e::real assume "e>0"
   1.147 -    then obtain N where "dist (f N) x < e" using f(2) by auto
   1.148 -    moreover have "f N\<in>S" "f N \<noteq> x" using f(1) by auto
   1.149 -    ultimately have "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" by auto
   1.150 -  }
   1.151 -  thus ?lhs unfolding islimpt_approachable by auto
   1.152 +  then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x" by auto
   1.153 +  show ?lhs
   1.154 +    unfolding islimpt_def
   1.155 +  proof safe
   1.156 +    fix T assume "open T" "x \<in> T"
   1.157 +    from lim[THEN topological_tendstoD, OF this] f
   1.158 +    show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
   1.159 +      unfolding eventually_sequentially by auto
   1.160 +  qed
   1.161  qed
   1.162  
   1.163  lemma Lim_inv: (* TODO: delete *)
   1.164 @@ -1626,7 +1719,7 @@
   1.165  text{* Useful lemmas on closure and set of possible sequential limits.*}
   1.166  
   1.167  lemma closure_sequential:
   1.168 -  fixes l :: "'a::metric_space"
   1.169 +  fixes l :: "'a::first_countable_topology"
   1.170    shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
   1.171  proof
   1.172    assume "?lhs" moreover
   1.173 @@ -1643,7 +1736,7 @@
   1.174  qed
   1.175  
   1.176  lemma closed_sequential_limits:
   1.177 -  fixes S :: "'a::metric_space set"
   1.178 +  fixes S :: "'a::first_countable_topology set"
   1.179    shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
   1.180    unfolding closed_limpt
   1.181    using closure_sequential [where 'a='a] closure_closed [where 'a='a] closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a]
   1.182 @@ -2778,74 +2871,37 @@
   1.183  subsubsection {* Complete the chain of compactness variants *}
   1.184  
   1.185  lemma islimpt_range_imp_convergent_subsequence:
   1.186 -  fixes f :: "nat \<Rightarrow> 'a::metric_space"
   1.187 -  assumes "l islimpt (range f)"
   1.188 +  fixes l :: "'a :: {t1_space, first_countable_topology}"
   1.189 +  assumes l: "l islimpt (range f)"
   1.190    shows "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
   1.191 -proof (intro exI conjI)
   1.192 -  have *: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. 0 < dist (f n) l \<and> dist (f n) l < e"
   1.193 -    using assms unfolding islimpt_def
   1.194 -    by (drule_tac x="ball l e" in spec)
   1.195 -       (auto simp add: zero_less_dist_iff dist_commute)
   1.196 -
   1.197 -  def t \<equiv> "\<lambda>e. LEAST n. 0 < dist (f n) l \<and> dist (f n) l < e"
   1.198 -  have f_t_neq: "\<And>e. 0 < e \<Longrightarrow> 0 < dist (f (t e)) l"
   1.199 -    unfolding t_def by (rule LeastI2_ex [OF * conjunct1])
   1.200 -  have f_t_closer: "\<And>e. 0 < e \<Longrightarrow> dist (f (t e)) l < e"
   1.201 -    unfolding t_def by (rule LeastI2_ex [OF * conjunct2])
   1.202 -  have t_le: "\<And>n e. 0 < dist (f n) l \<Longrightarrow> dist (f n) l < e \<Longrightarrow> t e \<le> n"
   1.203 -    unfolding t_def by (simp add: Least_le)
   1.204 -  have less_tD: "\<And>n e. n < t e \<Longrightarrow> 0 < dist (f n) l \<Longrightarrow> e \<le> dist (f n) l"
   1.205 -    unfolding t_def by (drule not_less_Least) simp
   1.206 -  have t_antimono: "\<And>e e'. 0 < e \<Longrightarrow> e \<le> e' \<Longrightarrow> t e' \<le> t e"
   1.207 -    apply (rule t_le)
   1.208 -    apply (erule f_t_neq)
   1.209 -    apply (erule (1) less_le_trans [OF f_t_closer])
   1.210 -    done
   1.211 -  have t_dist_f_neq: "\<And>n. 0 < dist (f n) l \<Longrightarrow> t (dist (f n) l) \<noteq> n"
   1.212 -    by (drule f_t_closer) auto
   1.213 -  have t_less: "\<And>e. 0 < e \<Longrightarrow> t e < t (dist (f (t e)) l)"
   1.214 -    apply (subst less_le)
   1.215 -    apply (rule conjI)
   1.216 -    apply (rule t_antimono)
   1.217 -    apply (erule f_t_neq)
   1.218 -    apply (erule f_t_closer [THEN less_imp_le])
   1.219 -    apply (rule t_dist_f_neq [symmetric])
   1.220 -    apply (erule f_t_neq)
   1.221 -    done
   1.222 -  have dist_f_t_less':
   1.223 -    "\<And>e e'. 0 < e \<Longrightarrow> 0 < e' \<Longrightarrow> t e \<le> t e' \<Longrightarrow> dist (f (t e')) l < e"
   1.224 -    apply (simp add: le_less)
   1.225 -    apply (erule disjE)
   1.226 -    apply (rule less_trans)
   1.227 -    apply (erule f_t_closer)
   1.228 -    apply (rule le_less_trans)
   1.229 -    apply (erule less_tD)
   1.230 -    apply (erule f_t_neq)
   1.231 -    apply (erule f_t_closer)
   1.232 -    apply (erule subst)
   1.233 -    apply (erule f_t_closer)
   1.234 -    done
   1.235 -
   1.236 -  def r \<equiv> "nat_rec (t 1) (\<lambda>_ x. t (dist (f x) l))"
   1.237 -  have r_simps: "r 0 = t 1" "\<And>n. r (Suc n) = t (dist (f (r n)) l)"
   1.238 -    unfolding r_def by simp_all
   1.239 -  have f_r_neq: "\<And>n. 0 < dist (f (r n)) l"
   1.240 -    by (induct_tac n) (simp_all add: r_simps f_t_neq)
   1.241 -
   1.242 -  show "subseq r"
   1.243 -    unfolding subseq_Suc_iff
   1.244 -    apply (rule allI)
   1.245 -    apply (case_tac n)
   1.246 -    apply (simp_all add: r_simps)
   1.247 -    apply (rule t_less, rule zero_less_one)
   1.248 -    apply (rule t_less, rule f_r_neq)
   1.249 -    done
   1.250 -  show "((f \<circ> r) ---> l) sequentially"
   1.251 -    unfolding LIMSEQ_def o_def
   1.252 -    apply (clarify, rename_tac e, rule_tac x="t e" in exI, clarify)
   1.253 -    apply (drule le_trans, rule seq_suble [OF `subseq r`])
   1.254 -    apply (case_tac n, simp_all add: r_simps dist_f_t_less' f_r_neq)
   1.255 -    done
   1.256 +proof -
   1.257 +  from first_countable_topology_class.countable_basis_at_decseq[of l] guess A . note A = this
   1.258 +
   1.259 +  def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> f j \<in> A (Suc n)"
   1.260 +  { fix n i
   1.261 +    have "\<exists>a. i < a \<and> f a \<in> A (Suc n)"
   1.262 +      by (rule l[THEN islimptE, of "A (Suc n) - (f ` {.. i} - {l})"])
   1.263 +         (auto simp: not_le[symmetric] finite_imp_closed A(1,2))
   1.264 +    then have "i < s n i" "f (s n i) \<in> A (Suc n)"
   1.265 +      unfolding s_def by (auto intro: someI2_ex) }
   1.266 +  note s = this
   1.267 +  def r \<equiv> "nat_rec (s 0 0) s"
   1.268 +  have "subseq r"
   1.269 +    by (auto simp: r_def s subseq_Suc_iff)
   1.270 +  moreover
   1.271 +  have "(\<lambda>n. f (r n)) ----> l"
   1.272 +  proof (rule topological_tendstoI)
   1.273 +    fix S assume "open S" "l \<in> S"
   1.274 +    with A(3) have "eventually (\<lambda>i. A i \<subseteq> S) sequentially" by auto
   1.275 +    moreover
   1.276 +    { fix i assume "Suc 0 \<le> i" then have "f (r i) \<in> A i"
   1.277 +        by (cases i) (simp_all add: r_def s) }
   1.278 +    then have "eventually (\<lambda>i. f (r i) \<in> A i) sequentially" by (auto simp: eventually_sequentially)
   1.279 +    ultimately show "eventually (\<lambda>i. f (r i) \<in> S) sequentially"
   1.280 +      by eventually_elim auto
   1.281 +  qed
   1.282 +  ultimately show "\<exists>r. subseq r \<and> (f \<circ> r) ----> l"
   1.283 +    by (auto simp: convergent_def comp_def)
   1.284  qed
   1.285  
   1.286  lemma finite_range_imp_infinite_repeats: