--- a/src/HOL/Limits.thy Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Limits.thy Thu Feb 22 15:17:25 2018 +0100
@@ -52,6 +52,9 @@
for f :: "_ \<Rightarrow> real"
by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
+lemma filterlim_real_at_infinity_sequentially: "filterlim real at_infinity sequentially"
+ by (simp add: filterlim_at_top_imp_at_infinity filterlim_real_sequentially)
+
lemma lim_infinity_imp_sequentially: "(f \<longlongrightarrow> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) \<longlongrightarrow> l) sequentially"
by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)
@@ -1256,6 +1259,20 @@
for a :: real
unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
+lemma at_to_0: "at a = filtermap (\<lambda>x. x + a) (at 0)"
+ for a :: "'a::real_normed_vector"
+ using filtermap_at_shift[of "-a" 0] by simp
+
+lemma filterlim_at_to_0:
+ "filterlim f F (at a) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at 0)"
+ for a :: "'a::real_normed_vector"
+ unfolding filterlim_def filtermap_filtermap at_to_0[of a] ..
+
+lemma eventually_at_to_0:
+ "eventually P (at a) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at 0)"
+ for a :: "'a::real_normed_vector"
+ unfolding at_to_0[of a] by (simp add: eventually_filtermap)
+
lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a)"
for a :: "'a::real_normed_vector"
by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
@@ -1268,6 +1285,7 @@
for a :: real
by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
+
lemma filterlim_at_left_to_right:
"filterlim f F (at_left a) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
for a :: real
@@ -1486,6 +1504,36 @@
for c :: nat
by (rule filterlim_subseq) (auto simp: strict_mono_def)
+lemma filterlim_times_pos:
+ "LIM x F1. c * f x :> at_right l"
+ if "filterlim f (at_right p) F1" "0 < c" "l = c * p"
+ for c::"'a::{linordered_field, linorder_topology}"
+ unfolding filterlim_iff
+proof safe
+ fix P
+ assume "\<forall>\<^sub>F x in at_right l. P x"
+ then obtain d where "c * p < d" "\<And>y. y > c * p \<Longrightarrow> y < d \<Longrightarrow> P y"
+ unfolding \<open>l = _ \<close> eventually_at_right_field
+ by auto
+ then have "\<forall>\<^sub>F a in at_right p. P (c * a)"
+ by (auto simp: eventually_at_right_field \<open>0 < c\<close> field_simps intro!: exI[where x="d/c"])
+ from that(1)[unfolded filterlim_iff, rule_format, OF this]
+ show "\<forall>\<^sub>F x in F1. P (c * f x)" .
+qed
+
+lemma filtermap_nhds_times: "c \<noteq> 0 \<Longrightarrow> filtermap (times c) (nhds a) = nhds (c * a)"
+ for a c :: "'a::real_normed_field"
+ by (rule filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"])
+ (auto intro!: tendsto_eq_intros filterlim_ident)
+
+lemma filtermap_times_pos_at_right:
+ fixes c::"'a::{linordered_field, linorder_topology}"
+ assumes "c > 0"
+ shows "filtermap (times c) (at_right p) = at_right (c * p)"
+ using assms
+ by (intro filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"])
+ (auto intro!: filterlim_ident filterlim_times_pos)
+
lemma at_to_infinity: "(at (0::'a::{real_normed_field,field})) = filtermap inverse at_infinity"
proof (rule antisym)
have "(inverse \<longlongrightarrow> (0::'a)) at_infinity"
@@ -1936,6 +1984,10 @@
lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
using lim_1_over_n by (simp add: inverse_eq_divide)
+lemma lim_inverse_n': "((\<lambda>n. 1 / n) \<longlongrightarrow> 0) sequentially"
+ using lim_inverse_n
+ by (simp add: inverse_eq_divide)
+
lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>n. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially"