author hoelzl Thu Jan 17 12:21:24 2013 +0100 (2013-01-17) changeset 50939 ae7cd20ed118 parent 50938 5b193d3dd6b6 child 50940 a7c273a83d27
replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy
```     1.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Jan 17 12:09:48 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Jan 17 12:21:24 2013 +0100
1.3 @@ -1403,14 +1403,14 @@
1.4    proof
1.5      fix x assume "x\<in>s" show "Cauchy (\<lambda>n. f n x)"
1.6      proof(cases "x=x0")
1.7 -      case True thus ?thesis using convergent_imp_cauchy[OF assms(5)] by auto
1.8 +      case True thus ?thesis using LIMSEQ_imp_Cauchy[OF assms(5)] by auto
1.9      next
1.10        case False show ?thesis unfolding Cauchy_def
1.11        proof(rule,rule)
1.12          fix e::real assume "e>0"
1.13          hence *:"e/2>0" "e/2/norm(x-x0)>0"
1.14            using False by (auto intro!: divide_pos_pos)
1.15 -        guess M using convergent_imp_cauchy[OF assms(5), unfolded Cauchy_def, rule_format,OF *(1)] .. note M=this
1.16 +        guess M using LIMSEQ_imp_Cauchy[OF assms(5), unfolded Cauchy_def, rule_format,OF *(1)] .. note M=this
1.17          guess N using lem1[rule_format,OF *(2)] .. note N = this
1.18          show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e"
1.19            apply(rule_tac x="max M N" in exI)
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 12:09:48 2013 +0100
2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 12:21:24 2013 +0100
2.3 @@ -3249,14 +3249,6 @@
2.4      by blast
2.5  qed
2.6
2.7 -lemma convergent_imp_cauchy:
2.8 - "(s ---> l) sequentially ==> Cauchy s"
2.9 -proof(simp only: cauchy_def, rule, rule)
2.10 -  fix e::real assume "e>0" "(s ---> l) sequentially"
2.11 -  then obtain N::nat where N:"\<forall>n\<ge>N. dist (s n) l < e/2" unfolding LIMSEQ_def by(erule_tac x="e/2" in allE) auto
2.12 -  thus "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e"  using dist_triangle_half_l[of _ l e _] by (rule_tac x=N in exI) auto
2.13 -qed
2.14 -
2.15  lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)"
2.16  proof-
2.17    from assms obtain N::nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto
2.18 @@ -3323,7 +3315,7 @@
2.19      then obtain f where f: "\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially"
2.20        unfolding islimpt_sequential by auto
2.21      then obtain l where l: "l\<in>s" "(f ---> l) sequentially"
2.22 -      using `complete s`[unfolded complete_def] using convergent_imp_cauchy[of f x] by auto
2.23 +      using `complete s`[unfolded complete_def] using LIMSEQ_imp_Cauchy[of f x] by auto
2.24      hence "x \<in> s"  using tendsto_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto
2.25    }
2.26    thus "closed s" unfolding closed_limpt by auto
2.27 @@ -3350,7 +3342,7 @@
2.28  lemma convergent_imp_bounded:
2.29    fixes s :: "nat \<Rightarrow> 'a::metric_space"
2.30    shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
2.31 -  by (intro cauchy_imp_bounded convergent_imp_cauchy)
2.32 +  by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
2.33
2.34  subsubsection{* Total boundedness *}
2.35
2.36 @@ -3377,7 +3369,7 @@
2.37      qed }
2.38    hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)" by blast+
2.39    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
2.40 -  from this(3) have "Cauchy (x \<circ> r)" using convergent_imp_cauchy by auto
2.41 +  from this(3) have "Cauchy (x \<circ> r)" using LIMSEQ_imp_Cauchy by auto
2.42    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
2.43    show False
2.44      using N[THEN spec[where x=N], THEN spec[where x="N+1"]]
```