numerical bounds on pi
authorimmler
Thu Jul 28 17:16:16 2016 +0200 (2016-07-28)
changeset 6355636e9732988ce
parent 63555 d00db72d8697
child 63559 113cee845044
numerical bounds on pi
src/HOL/Filter.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Real_Vector_Spaces.thy
     1.1 --- a/src/HOL/Filter.thy	Sun Jul 24 16:48:41 2016 +0200
     1.2 +++ b/src/HOL/Filter.thy	Thu Jul 28 17:16:16 2016 +0200
     1.3 @@ -618,6 +618,12 @@
     1.4    unfolding at_top_def
     1.5    by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
     1.6  
     1.7 +lemma eventually_at_top_linorderI:
     1.8 +  fixes c::"'a::linorder"
     1.9 +  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
    1.10 +  shows "eventually P at_top"
    1.11 +  using assms by (auto simp: eventually_at_top_linorder)
    1.12 +
    1.13  lemma eventually_ge_at_top:
    1.14    "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
    1.15    unfolding eventually_at_top_linorder by auto
     2.1 --- a/src/HOL/Limits.thy	Sun Jul 24 16:48:41 2016 +0200
     2.2 +++ b/src/HOL/Limits.thy	Thu Jul 28 17:16:16 2016 +0200
     2.3 @@ -1401,6 +1401,14 @@
     2.4  lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
     2.5   by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
     2.6  
     2.7 +lemma real_tendsto_divide_at_top:
     2.8 +  fixes c::"real"
     2.9 +  assumes "(f \<longlongrightarrow> c) F"
    2.10 +  assumes "filterlim g at_top F"
    2.11 +  shows "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
    2.12 +  by (auto simp: divide_inverse_commute
    2.13 +      intro!: tendsto_mult[THEN tendsto_eq_rhs] tendsto_inverse_0_at_top assms)
    2.14 +
    2.15  lemma mult_nat_left_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. c * x) at_top sequentially"
    2.16    for c :: nat
    2.17    by (rule filterlim_subseq) (auto simp: subseq_def)
    2.18 @@ -1489,6 +1497,13 @@
    2.19    qed
    2.20  qed
    2.21  
    2.22 +lemma filterlim_at_top_mult_tendsto_pos:
    2.23 +  assumes f: "(f \<longlongrightarrow> c) F"
    2.24 +    and c: "0 < c"
    2.25 +    and g: "LIM x F. g x :> at_top"
    2.26 +  shows "LIM x F. (g x * f x:: real) :> at_top"
    2.27 +  by (auto simp: mult.commute intro!: filterlim_tendsto_pos_mult_at_top f c g)
    2.28 +
    2.29  lemma filterlim_tendsto_pos_mult_at_bot:
    2.30    fixes c :: real
    2.31    assumes "(f \<longlongrightarrow> c) F" "0 < c" "filterlim g at_bot F"
    2.32 @@ -2139,6 +2154,26 @@
    2.33  lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) \<longlonglongrightarrow> 0"
    2.34    by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
    2.35  
    2.36 +lemma
    2.37 +  tendsto_power_zero:
    2.38 +  fixes x::"'a::real_normed_algebra_1"
    2.39 +  assumes "filterlim f at_top F"
    2.40 +  assumes "norm x < 1"
    2.41 +  shows "((\<lambda>y. x ^ (f y)) \<longlongrightarrow> 0) F"
    2.42 +proof (rule tendstoI)
    2.43 +  fix e::real assume "0 < e"
    2.44 +  from tendstoD[OF LIMSEQ_power_zero[OF \<open>norm x < 1\<close>] \<open>0 < e\<close>]
    2.45 +  have "\<forall>\<^sub>F xa in sequentially. norm (x ^ xa) < e"
    2.46 +    by simp
    2.47 +  then obtain N where N: "norm (x ^ n) < e" if "n \<ge> N" for n
    2.48 +    by (auto simp: eventually_sequentially)
    2.49 +  have "\<forall>\<^sub>F i in F. f i \<ge> N"
    2.50 +    using \<open>filterlim f sequentially F\<close>
    2.51 +    by (simp add: filterlim_at_top)
    2.52 +  then show "\<forall>\<^sub>F i in F. dist (x ^ f i) 0 < e"
    2.53 +    by (eventually_elim) (auto simp: N)
    2.54 +qed
    2.55 +
    2.56  text \<open>Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}.\<close>
    2.57  
    2.58  lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) \<longlonglongrightarrow> 0"
     3.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sun Jul 24 16:48:41 2016 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Jul 28 17:16:16 2016 +0200
     3.3 @@ -2397,6 +2397,47 @@
     3.4  lemma abs_tan_ge: "\<bar>x\<bar> < pi/2 \<Longrightarrow> \<bar>x\<bar> \<le> \<bar>tan x\<bar>"
     3.5    by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff)
     3.6  
     3.7 +lemma arctan_bounds:
     3.8 +  assumes "0 \<le> x" "x < 1"
     3.9 +  shows arctan_lower_bound:
    3.10 +    "(\<Sum>k<2 * n. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1))) \<le> arctan x"
    3.11 +    (is "(\<Sum>k<_. (- 1)^ k * ?a k) \<le> _")
    3.12 +    and arctan_upper_bound:
    3.13 +    "arctan x \<le> (\<Sum>k<2 * n + 1. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1)))"
    3.14 +proof -
    3.15 +  have tendsto_zero: "?a \<longlonglongrightarrow> 0"
    3.16 +    using assms
    3.17 +    apply -
    3.18 +    apply (rule tendsto_eq_rhs[where x="0 * 0"])
    3.19 +    subgoal by (intro tendsto_mult real_tendsto_divide_at_top)
    3.20 +        (auto simp: filterlim_real_sequentially filterlim_sequentially_iff_filterlim_real
    3.21 +          intro!: real_tendsto_divide_at_top tendsto_power_zero filterlim_real_sequentially
    3.22 +           tendsto_eq_intros filterlim_at_top_mult_tendsto_pos filterlim_tendsto_add_at_top)
    3.23 +    subgoal by simp
    3.24 +    done
    3.25 +  have nonneg: "0 \<le> ?a n" for n
    3.26 +    by (force intro!: divide_nonneg_nonneg mult_nonneg_nonneg zero_le_power assms)
    3.27 +  have le: "?a (Suc n) \<le> ?a n" for n
    3.28 +    by (rule mult_mono[OF _ power_decreasing]) (auto simp: divide_simps assms less_imp_le)
    3.29 +  from summable_Leibniz'(4)[of ?a, OF tendsto_zero nonneg le, of n]
    3.30 +    summable_Leibniz'(2)[of ?a, OF tendsto_zero nonneg le, of n]
    3.31 +    assms
    3.32 +  show "(\<Sum>k<2*n. (- 1)^ k * ?a k) \<le> arctan x" "arctan x \<le> (\<Sum>k<2 * n + 1. (- 1)^ k * ?a k)"
    3.33 +    by (auto simp: arctan_series)
    3.34 +qed
    3.35 +
    3.36 +subsection \<open>Bounds on pi using real arctangent\<close>
    3.37 +
    3.38 +lemma pi_machin: "pi = 16 * arctan (1 / 5) - 4 * arctan (1 / 239)"
    3.39 +  using machin
    3.40 +  by simp
    3.41 +
    3.42 +lemma pi_approx: "3.141592653588 \<le> pi" "pi \<le> 3.1415926535899"
    3.43 +  unfolding pi_machin
    3.44 +  using arctan_bounds[of "1/5"   4]
    3.45 +        arctan_bounds[of "1/239" 4]
    3.46 +  by (simp_all add: eval_nat_numeral)
    3.47 +
    3.48  
    3.49  subsection\<open>Inverse Sine\<close>
    3.50  
     4.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Jul 24 16:48:41 2016 +0200
     4.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Jul 28 17:16:16 2016 +0200
     4.3 @@ -1766,6 +1766,31 @@
     4.4    apply linarith
     4.5    done
     4.6  
     4.7 +lemma filterlim_nat_sequentially: "filterlim nat sequentially at_top"
     4.8 +  unfolding filterlim_at_top
     4.9 +  apply (rule allI)
    4.10 +  subgoal for Z by (auto intro!: eventually_at_top_linorderI[where c="int Z"])
    4.11 +  done
    4.12 +
    4.13 +lemma filterlim_floor_sequentially: "filterlim floor at_top at_top"
    4.14 +  unfolding filterlim_at_top
    4.15 +  apply (rule allI)
    4.16 +  subgoal for Z by (auto simp: le_floor_iff intro!: eventually_at_top_linorderI[where c="of_int Z"])
    4.17 +  done
    4.18 +
    4.19 +lemma filterlim_sequentially_iff_filterlim_real:
    4.20 +  "filterlim f sequentially F \<longleftrightarrow> filterlim (\<lambda>x. real (f x)) at_top F"
    4.21 +  apply (rule iffI)
    4.22 +  subgoal using filterlim_compose filterlim_real_sequentially by blast
    4.23 +  subgoal premises prems
    4.24 +  proof -
    4.25 +    have "filterlim (\<lambda>x. nat (floor (real (f x)))) sequentially F"
    4.26 +      by (intro filterlim_compose[OF filterlim_nat_sequentially]
    4.27 +          filterlim_compose[OF filterlim_floor_sequentially] prems)
    4.28 +    then show ?thesis by simp
    4.29 +  qed
    4.30 +  done
    4.31 +
    4.32  
    4.33  subsubsection \<open>Limits of Sequences\<close>
    4.34