src/HOL/Real_Vector_Spaces.thy
changeset 57448 159e45728ceb
parent 57418 6ab1c7cb0b8d
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Jun 30 15:45:21 2014 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jun 30 15:45:25 2014 +0200
     1.3 @@ -1466,18 +1466,31 @@
     1.4  
     1.5  subsection {* Filters and Limits on Metric Space *}
     1.6  
     1.7 -lemma eventually_nhds_metric:
     1.8 -  fixes a :: "'a :: metric_space"
     1.9 -  shows "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)"
    1.10 -unfolding eventually_nhds open_dist
    1.11 -apply safe
    1.12 -apply fast
    1.13 -apply (rule_tac x="{x. dist x a < d}" in exI, simp)
    1.14 -apply clarsimp
    1.15 -apply (rule_tac x="d - dist x a" in exI, clarsimp)
    1.16 -apply (simp only: less_diff_eq)
    1.17 -apply (erule le_less_trans [OF dist_triangle])
    1.18 -done
    1.19 +lemma (in metric_space) nhds_metric: "nhds x = (INF e:{0 <..}. principal {y. dist y x < e})"
    1.20 +  unfolding nhds_def
    1.21 +proof (safe intro!: INF_eq)
    1.22 +  fix S assume "open S" "x \<in> S"
    1.23 +  then obtain e where "{y. dist y x < e} \<subseteq> S" "0 < e"
    1.24 +    by (auto simp: open_dist subset_eq)
    1.25 +  then show "\<exists>e\<in>{0<..}. principal {y. dist y x < e} \<le> principal S"
    1.26 +    by auto
    1.27 +qed (auto intro!: exI[of _ "{y. dist x y < e}" for e] open_ball simp: dist_commute)
    1.28 +
    1.29 +lemma (in metric_space) tendsto_iff:
    1.30 +  "(f ---> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
    1.31 +  unfolding nhds_metric filterlim_INF filterlim_principal by auto
    1.32 +
    1.33 +lemma (in metric_space) tendstoI: "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F) \<Longrightarrow> (f ---> l) F"
    1.34 +  by (auto simp: tendsto_iff)
    1.35 +
    1.36 +lemma (in metric_space) tendstoD: "(f ---> l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
    1.37 +  by (auto simp: tendsto_iff)
    1.38 +
    1.39 +lemma (in metric_space) eventually_nhds_metric:
    1.40 +  "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)"
    1.41 +  unfolding nhds_metric
    1.42 +  by (subst eventually_INF_base)
    1.43 +     (auto simp: eventually_principal Bex_def subset_eq intro: exI[of _ "min a b" for a b])
    1.44  
    1.45  lemma eventually_at:
    1.46    fixes a :: "'a :: metric_space"
    1.47 @@ -1493,34 +1506,6 @@
    1.48    apply auto
    1.49    done
    1.50  
    1.51 -lemma tendstoI:
    1.52 -  fixes l :: "'a :: metric_space"
    1.53 -  assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
    1.54 -  shows "(f ---> l) F"
    1.55 -  apply (rule topological_tendstoI)
    1.56 -  apply (simp add: open_dist)
    1.57 -  apply (drule (1) bspec, clarify)
    1.58 -  apply (drule assms)
    1.59 -  apply (erule eventually_elim1, simp)
    1.60 -  done
    1.61 -
    1.62 -lemma tendstoD:
    1.63 -  fixes l :: "'a :: metric_space"
    1.64 -  shows "(f ---> l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
    1.65 -  apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
    1.66 -  apply (clarsimp simp add: open_dist)
    1.67 -  apply (rule_tac x="e - dist x l" in exI, clarsimp)
    1.68 -  apply (simp only: less_diff_eq)
    1.69 -  apply (erule le_less_trans [OF dist_triangle])
    1.70 -  apply simp
    1.71 -  apply simp
    1.72 -  done
    1.73 -
    1.74 -lemma tendsto_iff:
    1.75 -  fixes l :: "'a :: metric_space"
    1.76 -  shows "(f ---> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
    1.77 -  using tendstoI tendstoD by fast
    1.78 -
    1.79  lemma metric_tendsto_imp_tendsto:
    1.80    fixes a :: "'a :: metric_space" and b :: "'b :: metric_space"
    1.81    assumes f: "(f ---> a) F"
    1.82 @@ -1786,49 +1771,31 @@
    1.83    fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
    1.84    assumes *: "\<And>X. filterlim X at_top sequentially \<Longrightarrow> (\<lambda>n. f (X n)) ----> y"
    1.85    shows "(f ---> y) at_top"
    1.86 -  unfolding filterlim_iff
    1.87 -proof safe
    1.88 -  fix P assume "eventually P (nhds y)"
    1.89 -  then have seq: "\<And>f. f ----> y \<Longrightarrow> eventually (\<lambda>x. P (f x)) at_top"
    1.90 -    unfolding eventually_nhds_iff_sequentially by simp
    1.91 -
    1.92 -  show "eventually (\<lambda>x. P (f x)) at_top"
    1.93 -  proof (rule ccontr)
    1.94 -    assume "\<not> eventually (\<lambda>x. P (f x)) at_top"
    1.95 -    then have "\<And>X. \<exists>x>X. \<not> P (f x)"
    1.96 -      unfolding eventually_at_top_dense by simp
    1.97 -    then obtain r where not_P: "\<And>x. \<not> P (f (r x))" and r: "\<And>x. x < r x"
    1.98 -      by metis
    1.99 -    
   1.100 -    def s \<equiv> "rec_nat (r 0) (\<lambda>_ x. r (x + 1))"
   1.101 -    then have [simp]: "s 0 = r 0" "\<And>n. s (Suc n) = r (s n + 1)"
   1.102 -      by auto
   1.103 -
   1.104 -    { fix n have "n < s n" using r
   1.105 -        by (induct n) (auto simp add: real_of_nat_Suc intro: less_trans add_strict_right_mono) }
   1.106 -    note s_subseq = this
   1.107 +proof -
   1.108 +  from nhds_countable[of y] guess A . note A = this
   1.109  
   1.110 -    have "mono s"
   1.111 -    proof (rule incseq_SucI)
   1.112 -      fix n show "s n \<le> s (Suc n)"
   1.113 -        using r[of "s n + 1"] by simp
   1.114 -    qed
   1.115 -
   1.116 -    have "filterlim s at_top sequentially"
   1.117 -      unfolding filterlim_at_top_gt[where c=0] eventually_sequentially
   1.118 -    proof (safe intro!: exI)
   1.119 -      fix Z :: real and n assume "0 < Z" "natceiling Z \<le> n"
   1.120 -      with real_natceiling_ge[of Z] `n < s n`
   1.121 -      show "Z \<le> s n"
   1.122 -        by auto
   1.123 -    qed
   1.124 -    moreover then have "eventually (\<lambda>x. P (f (s x))) sequentially"
   1.125 -      by (rule seq[OF *])
   1.126 -    then obtain n where "P (f (s n))"
   1.127 -      by (auto simp: eventually_sequentially)
   1.128 -    then show False
   1.129 -      using not_P by (cases n) auto
   1.130 +  have "\<forall>m. \<exists>k. \<forall>x\<ge>k. f x \<in> A m"
   1.131 +  proof (rule ccontr)
   1.132 +    assume "\<not> (\<forall>m. \<exists>k. \<forall>x\<ge>k. f x \<in> A m)"
   1.133 +    then obtain m where "\<And>k. \<exists>x\<ge>k. f x \<notin> A m"
   1.134 +      by auto
   1.135 +    then have "\<exists>X. \<forall>n. (f (X n) \<notin> A m) \<and> max n (X n) + 1 \<le> X (Suc n)"
   1.136 +      by (intro dependent_nat_choice) (auto simp del: max.bounded_iff)
   1.137 +    then obtain X where X: "\<And>n. f (X n) \<notin> A m" "\<And>n. max n (X n) + 1 \<le> X (Suc n)"
   1.138 +      by auto
   1.139 +    { fix n have "1 \<le> n \<longrightarrow> real n \<le> X n"
   1.140 +        using X[of "n - 1"] by auto }
   1.141 +    then have "filterlim X at_top sequentially"
   1.142 +      by (force intro!: filterlim_at_top_mono[OF filterlim_real_sequentially]
   1.143 +                simp: eventually_sequentially)
   1.144 +    from topological_tendstoD[OF *[OF this] A(2, 3), of m] X(1) show False
   1.145 +      by auto
   1.146    qed
   1.147 +  then obtain k where "\<And>m x. k m \<le> x \<Longrightarrow> f x \<in> A m"
   1.148 +    by metis
   1.149 +  then show ?thesis
   1.150 +    unfolding at_top_def A
   1.151 +    by (intro filterlim_base[where i=k]) auto
   1.152  qed
   1.153  
   1.154  lemma tendsto_at_topI_sequentially_real: