src/HOL/Lim.thy
changeset 51473 1210309fddab
parent 51472 adb441e4b9e9
child 51478 270b21f3ae0a
equal deleted inserted replaced
51472:adb441e4b9e9 51473:1210309fddab
   224 
   224 
   225 lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   225 lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   226 by (rule isUCont [THEN isUCont_Cauchy])
   226 by (rule isUCont [THEN isUCont_Cauchy])
   227 
   227 
   228 
   228 
   229 subsection {* Relation of LIM and LIMSEQ *}
       
   230 
       
   231 lemma sequentially_imp_eventually_within:
       
   232   fixes a :: "'a::metric_space"
       
   233   assumes "\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow>
       
   234     eventually (\<lambda>n. P (f n)) sequentially"
       
   235   shows "eventually P (at a within s)"
       
   236 proof (rule ccontr)
       
   237   let ?I = "\<lambda>n. inverse (real (Suc n))"
       
   238   def F \<equiv> "\<lambda>n::nat. SOME x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
       
   239   assume "\<not> eventually P (at a within s)"
       
   240   hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
       
   241     unfolding eventually_within eventually_at by fast
       
   242   hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
       
   243   hence F: "\<And>n. F n \<in> s \<and> F n \<noteq> a \<and> dist (F n) a < ?I n \<and> \<not> P (F n)"
       
   244     unfolding F_def by (rule someI_ex)
       
   245   hence F0: "\<forall>n. F n \<in> s" and F1: "\<forall>n. F n \<noteq> a"
       
   246     and F2: "\<forall>n. dist (F n) a < ?I n" and F3: "\<forall>n. \<not> P (F n)"
       
   247     by fast+
       
   248   from LIMSEQ_inverse_real_of_nat have "F ----> a"
       
   249     by (rule metric_tendsto_imp_tendsto,
       
   250       simp add: dist_norm F2 less_imp_le)
       
   251   hence "eventually (\<lambda>n. P (F n)) sequentially"
       
   252     using assms F0 F1 by simp
       
   253   thus "False" by (simp add: F3)
       
   254 qed
       
   255 
       
   256 lemma sequentially_imp_eventually_at:
       
   257   fixes a :: "'a::metric_space"
       
   258   assumes "\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow>
       
   259     eventually (\<lambda>n. P (f n)) sequentially"
       
   260   shows "eventually P (at a)"
       
   261   using assms sequentially_imp_eventually_within [where s=UNIV] by simp
       
   262 
       
   263 lemma LIMSEQ_SEQ_conv1:
       
   264   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
       
   265   assumes f: "f -- a --> l"
       
   266   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
       
   267   using tendsto_compose_eventually [OF f, where F=sequentially] by simp
       
   268 
       
   269 lemma LIMSEQ_SEQ_conv2:
       
   270   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
       
   271   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
       
   272   shows "f -- a --> l"
       
   273   using assms unfolding tendsto_def [where l=l]
       
   274   by (simp add: sequentially_imp_eventually_at)
       
   275 
       
   276 lemma LIMSEQ_SEQ_conv:
       
   277   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
       
   278    (X -- a --> (L::'b::topological_space))"
       
   279   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
       
   280 
       
   281 lemma LIM_less_bound: 
   229 lemma LIM_less_bound: 
   282   fixes f :: "real \<Rightarrow> real"
   230   fixes f :: "real \<Rightarrow> real"
   283   assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
   231   assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
   284   shows "0 \<le> f x"
   232   shows "0 \<le> f x"
   285 proof (rule tendsto_le_const)
   233 proof (rule tendsto_le_const)