Added some simple facts about limits
authorManuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:12:55 2018 +0200 (13 months ago)
changeset 6795099eaa5cedbb7
parent 67948 83902fff6243
child 67951 655aa11359dc
Added some simple facts about limits
src/HOL/Filter.thy
src/HOL/Limits.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Filter.thy	Sat Mar 24 22:45:06 2018 +0100
     1.2 +++ b/src/HOL/Filter.thy	Mon Mar 26 16:12:55 2018 +0200
     1.3 @@ -1210,6 +1210,11 @@
     1.4    apply auto
     1.5    done
     1.6  
     1.7 +lemma eventually_compose_filterlim:
     1.8 +  assumes "eventually P F" "filterlim f F G"
     1.9 +  shows "eventually (\<lambda>x. P (f x)) G"
    1.10 +  using assms by (simp add: filterlim_iff)
    1.11 +
    1.12  lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
    1.13    by (simp add: filtermap_mono_strong eq_iff)
    1.14  
     2.1 --- a/src/HOL/Limits.thy	Sat Mar 24 22:45:06 2018 +0100
     2.2 +++ b/src/HOL/Limits.thy	Mon Mar 26 16:12:55 2018 +0200
     2.3 @@ -1113,6 +1113,10 @@
     2.4  lemma filterlim_norm_at_top: "filterlim norm at_top at_infinity"
     2.5    by (rule filterlim_at_infinity_imp_norm_at_top) (rule filterlim_ident)
     2.6  
     2.7 +lemma filterlim_at_infinity_conv_norm_at_top:
     2.8 +  "filterlim f at_infinity G \<longleftrightarrow> filterlim (\<lambda>x. norm (f x)) at_top G"
     2.9 +  by (auto simp: filterlim_at_infinity[OF order.refl] filterlim_at_top_gt[of _ _ 0])
    2.10 +
    2.11  lemma eventually_not_equal_at_infinity:
    2.12    "eventually (\<lambda>x. x \<noteq> (a :: 'a :: {real_normed_vector})) at_infinity"
    2.13  proof -
    2.14 @@ -1322,6 +1326,28 @@
    2.15      and filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x. - f x" F]
    2.16    by auto
    2.17  
    2.18 +lemma filterlim_at_infinity_imp_filterlim_at_top:
    2.19 +  assumes "filterlim (f :: 'a \<Rightarrow> real) at_infinity F"
    2.20 +  assumes "eventually (\<lambda>x. f x > 0) F"
    2.21 +  shows   "filterlim f at_top F"
    2.22 +proof -
    2.23 +  from assms(2) have *: "eventually (\<lambda>x. norm (f x) = f x) F" by eventually_elim simp
    2.24 +  from assms(1) show ?thesis unfolding filterlim_at_infinity_conv_norm_at_top
    2.25 +    by (subst (asm) filterlim_cong[OF refl refl *])
    2.26 +qed
    2.27 +
    2.28 +lemma filterlim_at_infinity_imp_filterlim_at_bot:
    2.29 +  assumes "filterlim (f :: 'a \<Rightarrow> real) at_infinity F"
    2.30 +  assumes "eventually (\<lambda>x. f x < 0) F"
    2.31 +  shows   "filterlim f at_bot F"
    2.32 +proof -
    2.33 +  from assms(2) have *: "eventually (\<lambda>x. norm (f x) = -f x) F" by eventually_elim simp
    2.34 +  from assms(1) have "filterlim (\<lambda>x. - f x) at_top F"
    2.35 +    unfolding filterlim_at_infinity_conv_norm_at_top
    2.36 +    by (subst (asm) filterlim_cong[OF refl refl *])
    2.37 +  thus ?thesis by (simp add: filterlim_uminus_at_top)
    2.38 +qed
    2.39 +
    2.40  lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_top)"
    2.41    unfolding filterlim_uminus_at_top by simp
    2.42  
     3.1 --- a/src/HOL/Topological_Spaces.thy	Sat Mar 24 22:45:06 2018 +0100
     3.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Mar 26 16:12:55 2018 +0200
     3.3 @@ -743,10 +743,18 @@
     3.4  lemma tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
     3.5    by (simp add: tendsto_def)
     3.6  
     3.7 -lemma  filterlim_at:
     3.8 +lemma filterlim_at:
     3.9    "(LIM x F. f x :> at b within s) \<longleftrightarrow> eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f \<longlongrightarrow> b) F"
    3.10    by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
    3.11  
    3.12 +lemma (in -)
    3.13 +  assumes "filterlim f (nhds L) F"
    3.14 +  shows tendsto_imp_filterlim_at_right:
    3.15 +          "eventually (\<lambda>x. f x > L) F \<Longrightarrow> filterlim f (at_right L) F"
    3.16 +    and tendsto_imp_filterlim_at_left:
    3.17 +          "eventually (\<lambda>x. f x < L) F \<Longrightarrow> filterlim f (at_left L) F"
    3.18 +  using assms by (auto simp: filterlim_at elim: eventually_mono)
    3.19 +
    3.20  lemma  filterlim_at_withinI:
    3.21    assumes "filterlim f (nhds c) F"
    3.22    assumes "eventually (\<lambda>x. f x \<in> A - {c}) F"