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:
```