# HG changeset patch
# User immler
# Date 1469718976 -7200
# Node ID 36e9732988ceecdadd0f05eee5f468b50c2e9c1e
# Parent  d00db72d86979596e6f4a7ab9fb78a611a731724
numerical bounds on pi

diff -r d00db72d8697 -r 36e9732988ce src/HOL/Filter.thy
--- 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
diff -r d00db72d8697 -r 36e9732988ce src/HOL/Limits.thy
--- 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"
diff -r d00db72d8697 -r 36e9732988ce src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- 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>
 
diff -r d00db72d8697 -r 36e9732988ce src/HOL/Real_Vector_Spaces.thy
--- 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>