src/HOL/Lim.thy
changeset 44532 a2e9b39df938
parent 44314 dbad46932536
child 44568 e6f291cb5810
equal deleted inserted replaced
44531:1d477a2b1572 44532:a2e9b39df938
   442 by (rule isUCont [THEN isUCont_Cauchy])
   442 by (rule isUCont [THEN isUCont_Cauchy])
   443 
   443 
   444 
   444 
   445 subsection {* Relation of LIM and LIMSEQ *}
   445 subsection {* Relation of LIM and LIMSEQ *}
   446 
   446 
       
   447 lemma sequentially_imp_eventually_within:
       
   448   fixes a :: "'a::metric_space"
       
   449   assumes "\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow>
       
   450     eventually (\<lambda>n. P (f n)) sequentially"
       
   451   shows "eventually P (at a within s)"
       
   452 proof (rule ccontr)
       
   453   let ?I = "\<lambda>n. inverse (real (Suc n))"
       
   454   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"
       
   455   assume "\<not> eventually P (at a within s)"
       
   456   hence P: "\<forall>d>0. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
       
   457     unfolding Limits.eventually_within Limits.eventually_at by fast
       
   458   hence "\<And>n. \<exists>x. x \<in> s \<and> x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
       
   459   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)"
       
   460     unfolding F_def by (rule someI_ex)
       
   461   hence F0: "\<forall>n. F n \<in> s" and F1: "\<forall>n. F n \<noteq> a"
       
   462     and F2: "\<forall>n. dist (F n) a < ?I n" and F3: "\<forall>n. \<not> P (F n)"
       
   463     by fast+
       
   464   from LIMSEQ_inverse_real_of_nat have "F ----> a"
       
   465     by (rule metric_tendsto_imp_tendsto,
       
   466       simp add: dist_norm F2 less_imp_le)
       
   467   hence "eventually (\<lambda>n. P (F n)) sequentially"
       
   468     using assms F0 F1 by simp
       
   469   thus "False" by (simp add: F3)
       
   470 qed
       
   471 
       
   472 lemma sequentially_imp_eventually_at:
       
   473   fixes a :: "'a::metric_space"
       
   474   assumes "\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow>
       
   475     eventually (\<lambda>n. P (f n)) sequentially"
       
   476   shows "eventually P (at a)"
       
   477   using assms sequentially_imp_eventually_within [where s=UNIV]
       
   478   unfolding within_UNIV by simp
       
   479 
   447 lemma LIMSEQ_SEQ_conv1:
   480 lemma LIMSEQ_SEQ_conv1:
   448   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   481   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   449   assumes f: "f -- a --> l"
   482   assumes f: "f -- a --> l"
   450   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   483   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   451   using tendsto_compose_eventually [OF f, where F=sequentially] by simp
   484   using tendsto_compose_eventually [OF f, where F=sequentially] by simp
   452 
   485 
   453 lemma LIMSEQ_SEQ_conv2_lemma:
       
   454   fixes a :: "'a::metric_space"
       
   455   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> eventually (\<lambda>x. P (S x)) sequentially"
       
   456   shows "eventually P (at a)"
       
   457 proof (rule ccontr)
       
   458   let ?I = "\<lambda>n. inverse (real (Suc n))"
       
   459   let ?F = "\<lambda>n::nat. SOME x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x"
       
   460   assume "\<not> eventually P (at a)"
       
   461   hence P: "\<forall>d>0. \<exists>x. x \<noteq> a \<and> dist x a < d \<and> \<not> P x"
       
   462     unfolding eventually_at by simp
       
   463   hence "\<And>n. \<exists>x. x \<noteq> a \<and> dist x a < ?I n \<and> \<not> P x" by simp
       
   464   hence F: "\<And>n. ?F n \<noteq> a \<and> dist (?F n) a < ?I n \<and> \<not> P (?F n)"
       
   465     by (rule someI_ex)
       
   466   hence F1: "\<And>n. ?F n \<noteq> a"
       
   467     and F2: "\<And>n. dist (?F n) a < ?I n"
       
   468     and F3: "\<And>n. \<not> P (?F n)"
       
   469     by fast+
       
   470   have "?F ----> a"
       
   471     using LIMSEQ_inverse_real_of_nat
       
   472     by (rule metric_tendsto_imp_tendsto,
       
   473       simp add: dist_norm F2 [THEN less_imp_le])
       
   474   moreover have "\<forall>n. ?F n \<noteq> a"
       
   475     by (rule allI) (rule F1)
       
   476   ultimately have "eventually (\<lambda>n. P (?F n)) sequentially"
       
   477     using assms by simp
       
   478   thus "False" by (simp add: F3)
       
   479 qed
       
   480 
       
   481 lemma LIMSEQ_SEQ_conv2:
   486 lemma LIMSEQ_SEQ_conv2:
   482   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   487   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   483   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   488   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
   484   shows "f -- a --> l"
   489   shows "f -- a --> l"
   485   using assms unfolding tendsto_def [where l=l]
   490   using assms unfolding tendsto_def [where l=l]
   486   by (simp add: LIMSEQ_SEQ_conv2_lemma)
   491   by (simp add: sequentially_imp_eventually_at)
   487 
   492 
   488 lemma LIMSEQ_SEQ_conv:
   493 lemma LIMSEQ_SEQ_conv:
   489   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
   494   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
   490    (X -- a --> (L::'b::topological_space))"
   495    (X -- a --> (L::'b::topological_space))"
   491   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
   496   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..