--- a/src/HOL/Filter.thy Sun Jul 24 16:48:41 2016 +0200
+++ b/src/HOL/Filter.thy Thu Jul 28 17:16:16 2016 +0200
@@ -618,6 +618,12 @@
unfolding at_top_def
by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
+lemma eventually_at_top_linorderI:
+ fixes c::"'a::linorder"
+ assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
+ shows "eventually P at_top"
+ using assms by (auto simp: eventually_at_top_linorder)
+
lemma eventually_ge_at_top:
"eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
unfolding eventually_at_top_linorder by auto
--- a/src/HOL/Limits.thy Sun Jul 24 16:48:41 2016 +0200
+++ b/src/HOL/Limits.thy Thu Jul 28 17:16:16 2016 +0200
@@ -1401,6 +1401,14 @@
lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
+lemma real_tendsto_divide_at_top:
+ fixes c::"real"
+ assumes "(f \<longlongrightarrow> c) F"
+ assumes "filterlim g at_top F"
+ shows "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
+ by (auto simp: divide_inverse_commute
+ intro!: tendsto_mult[THEN tendsto_eq_rhs] tendsto_inverse_0_at_top assms)
+
lemma mult_nat_left_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. c * x) at_top sequentially"
for c :: nat
by (rule filterlim_subseq) (auto simp: subseq_def)
@@ -1489,6 +1497,13 @@
qed
qed
+lemma filterlim_at_top_mult_tendsto_pos:
+ assumes f: "(f \<longlongrightarrow> c) F"
+ and c: "0 < c"
+ and g: "LIM x F. g x :> at_top"
+ shows "LIM x F. (g x * f x:: real) :> at_top"
+ by (auto simp: mult.commute intro!: filterlim_tendsto_pos_mult_at_top f c g)
+
lemma filterlim_tendsto_pos_mult_at_bot:
fixes c :: real
assumes "(f \<longlongrightarrow> c) F" "0 < c" "filterlim g at_bot F"
@@ -2139,6 +2154,26 @@
lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) \<longlonglongrightarrow> 0"
by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
+lemma
+ tendsto_power_zero:
+ fixes x::"'a::real_normed_algebra_1"
+ assumes "filterlim f at_top F"
+ assumes "norm x < 1"
+ shows "((\<lambda>y. x ^ (f y)) \<longlongrightarrow> 0) F"
+proof (rule tendstoI)
+ fix e::real assume "0 < e"
+ from tendstoD[OF LIMSEQ_power_zero[OF \<open>norm x < 1\<close>] \<open>0 < e\<close>]
+ have "\<forall>\<^sub>F xa in sequentially. norm (x ^ xa) < e"
+ by simp
+ then obtain N where N: "norm (x ^ n) < e" if "n \<ge> N" for n
+ by (auto simp: eventually_sequentially)
+ have "\<forall>\<^sub>F i in F. f i \<ge> N"
+ using \<open>filterlim f sequentially F\<close>
+ by (simp add: filterlim_at_top)
+ then show "\<forall>\<^sub>F i in F. dist (x ^ f i) 0 < e"
+ by (eventually_elim) (auto simp: N)
+qed
+
text \<open>Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}.\<close>
lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) \<longlonglongrightarrow> 0"
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Sun Jul 24 16:48:41 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Thu Jul 28 17:16:16 2016 +0200
@@ -2397,6 +2397,47 @@
lemma abs_tan_ge: "\<bar>x\<bar> < pi/2 \<Longrightarrow> \<bar>x\<bar> \<le> \<bar>tan x\<bar>"
by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff)
+lemma arctan_bounds:
+ assumes "0 \<le> x" "x < 1"
+ shows arctan_lower_bound:
+ "(\<Sum>k<2 * n. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1))) \<le> arctan x"
+ (is "(\<Sum>k<_. (- 1)^ k * ?a k) \<le> _")
+ and arctan_upper_bound:
+ "arctan x \<le> (\<Sum>k<2 * n + 1. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1)))"
+proof -
+ have tendsto_zero: "?a \<longlonglongrightarrow> 0"
+ using assms
+ apply -
+ apply (rule tendsto_eq_rhs[where x="0 * 0"])
+ subgoal by (intro tendsto_mult real_tendsto_divide_at_top)
+ (auto simp: filterlim_real_sequentially filterlim_sequentially_iff_filterlim_real
+ intro!: real_tendsto_divide_at_top tendsto_power_zero filterlim_real_sequentially
+ tendsto_eq_intros filterlim_at_top_mult_tendsto_pos filterlim_tendsto_add_at_top)
+ subgoal by simp
+ done
+ have nonneg: "0 \<le> ?a n" for n
+ by (force intro!: divide_nonneg_nonneg mult_nonneg_nonneg zero_le_power assms)
+ have le: "?a (Suc n) \<le> ?a n" for n
+ by (rule mult_mono[OF _ power_decreasing]) (auto simp: divide_simps assms less_imp_le)
+ from summable_Leibniz'(4)[of ?a, OF tendsto_zero nonneg le, of n]
+ summable_Leibniz'(2)[of ?a, OF tendsto_zero nonneg le, of n]
+ assms
+ show "(\<Sum>k<2*n. (- 1)^ k * ?a k) \<le> arctan x" "arctan x \<le> (\<Sum>k<2 * n + 1. (- 1)^ k * ?a k)"
+ by (auto simp: arctan_series)
+qed
+
+subsection \<open>Bounds on pi using real arctangent\<close>
+
+lemma pi_machin: "pi = 16 * arctan (1 / 5) - 4 * arctan (1 / 239)"
+ using machin
+ by simp
+
+lemma pi_approx: "3.141592653588 \<le> pi" "pi \<le> 3.1415926535899"
+ unfolding pi_machin
+ using arctan_bounds[of "1/5" 4]
+ arctan_bounds[of "1/239" 4]
+ by (simp_all add: eval_nat_numeral)
+
subsection\<open>Inverse Sine\<close>
--- a/src/HOL/Real_Vector_Spaces.thy Sun Jul 24 16:48:41 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Thu Jul 28 17:16:16 2016 +0200
@@ -1766,6 +1766,31 @@
apply linarith
done
+lemma filterlim_nat_sequentially: "filterlim nat sequentially at_top"
+ unfolding filterlim_at_top
+ apply (rule allI)
+ subgoal for Z by (auto intro!: eventually_at_top_linorderI[where c="int Z"])
+ done
+
+lemma filterlim_floor_sequentially: "filterlim floor at_top at_top"
+ unfolding filterlim_at_top
+ apply (rule allI)
+ subgoal for Z by (auto simp: le_floor_iff intro!: eventually_at_top_linorderI[where c="of_int Z"])
+ done
+
+lemma filterlim_sequentially_iff_filterlim_real:
+ "filterlim f sequentially F \<longleftrightarrow> filterlim (\<lambda>x. real (f x)) at_top F"
+ apply (rule iffI)
+ subgoal using filterlim_compose filterlim_real_sequentially by blast
+ subgoal premises prems
+ proof -
+ have "filterlim (\<lambda>x. nat (floor (real (f x)))) sequentially F"
+ by (intro filterlim_compose[OF filterlim_nat_sequentially]
+ filterlim_compose[OF filterlim_floor_sequentially] prems)
+ then show ?thesis by simp
+ qed
+ done
+
subsubsection \<open>Limits of Sequences\<close>