--- 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)
--- 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
--- 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"