# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1522073575 -7200
# Node ID 99eaa5cedbb74e6d12214a579ccff6583a4a2b99
# Parent  83902fff62439d01c1b6e2dd1ca8361872b19682
Added some simple facts about limits

diff -r 83902fff6243 -r 99eaa5cedbb7 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Sat Mar 24 22:45:06 2018 +0100
+++ b/src/HOL/Filter.thy	Mon Mar 26 16:12:55 2018 +0200
@@ -1210,6 +1210,11 @@
   apply auto
   done
 
+lemma eventually_compose_filterlim:
+  assumes "eventually P F" "filterlim f F G"
+  shows "eventually (\<lambda>x. P (f x)) G"
+  using assms by (simp add: filterlim_iff)
+
 lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
   by (simp add: filtermap_mono_strong eq_iff)
 
diff -r 83902fff6243 -r 99eaa5cedbb7 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sat Mar 24 22:45:06 2018 +0100
+++ b/src/HOL/Limits.thy	Mon Mar 26 16:12:55 2018 +0200
@@ -1113,6 +1113,10 @@
 lemma filterlim_norm_at_top: "filterlim norm at_top at_infinity"
   by (rule filterlim_at_infinity_imp_norm_at_top) (rule filterlim_ident)
 
+lemma filterlim_at_infinity_conv_norm_at_top:
+  "filterlim f at_infinity G \<longleftrightarrow> filterlim (\<lambda>x. norm (f x)) at_top G"
+  by (auto simp: filterlim_at_infinity[OF order.refl] filterlim_at_top_gt[of _ _ 0])
+
 lemma eventually_not_equal_at_infinity:
   "eventually (\<lambda>x. x \<noteq> (a :: 'a :: {real_normed_vector})) at_infinity"
 proof -
@@ -1322,6 +1326,28 @@
     and filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\<lambda>x. - f x" F]
   by auto
 
+lemma filterlim_at_infinity_imp_filterlim_at_top:
+  assumes "filterlim (f :: 'a \<Rightarrow> real) at_infinity F"
+  assumes "eventually (\<lambda>x. f x > 0) F"
+  shows   "filterlim f at_top F"
+proof -
+  from assms(2) have *: "eventually (\<lambda>x. norm (f x) = f x) F" by eventually_elim simp
+  from assms(1) show ?thesis unfolding filterlim_at_infinity_conv_norm_at_top
+    by (subst (asm) filterlim_cong[OF refl refl *])
+qed
+
+lemma filterlim_at_infinity_imp_filterlim_at_bot:
+  assumes "filterlim (f :: 'a \<Rightarrow> real) at_infinity F"
+  assumes "eventually (\<lambda>x. f x < 0) F"
+  shows   "filterlim f at_bot F"
+proof -
+  from assms(2) have *: "eventually (\<lambda>x. norm (f x) = -f x) F" by eventually_elim simp
+  from assms(1) have "filterlim (\<lambda>x. - f x) at_top F"
+    unfolding filterlim_at_infinity_conv_norm_at_top
+    by (subst (asm) filterlim_cong[OF refl refl *])
+  thus ?thesis by (simp add: filterlim_uminus_at_top)
+qed
+
 lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \<longleftrightarrow> (LIM x F. - (f x) :: real :> at_top)"
   unfolding filterlim_uminus_at_top by simp
 
diff -r 83902fff6243 -r 99eaa5cedbb7 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Sat Mar 24 22:45:06 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy	Mon Mar 26 16:12:55 2018 +0200
@@ -743,10 +743,18 @@
 lemma tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
   by (simp add: tendsto_def)
 
-lemma  filterlim_at:
+lemma filterlim_at:
   "(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"
   by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
 
+lemma (in -)
+  assumes "filterlim f (nhds L) F"
+  shows tendsto_imp_filterlim_at_right:
+          "eventually (\<lambda>x. f x > L) F \<Longrightarrow> filterlim f (at_right L) F"
+    and tendsto_imp_filterlim_at_left:
+          "eventually (\<lambda>x. f x < L) F \<Longrightarrow> filterlim f (at_left L) F"
+  using assms by (auto simp: filterlim_at elim: eventually_mono)
+
 lemma  filterlim_at_withinI:
   assumes "filterlim f (nhds c) F"
   assumes "eventually (\<lambda>x. f x \<in> A - {c}) F"