2395 by (metis abs_arctan_le abs_of_nonneg zero_le_arctan_iff) |
2395 by (metis abs_arctan_le abs_of_nonneg zero_le_arctan_iff) |
2396 |
2396 |
2397 lemma abs_tan_ge: "\<bar>x\<bar> < pi/2 \<Longrightarrow> \<bar>x\<bar> \<le> \<bar>tan x\<bar>" |
2397 lemma abs_tan_ge: "\<bar>x\<bar> < pi/2 \<Longrightarrow> \<bar>x\<bar> \<le> \<bar>tan x\<bar>" |
2398 by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff) |
2398 by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff) |
2399 |
2399 |
|
2400 lemma arctan_bounds: |
|
2401 assumes "0 \<le> x" "x < 1" |
|
2402 shows arctan_lower_bound: |
|
2403 "(\<Sum>k<2 * n. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1))) \<le> arctan x" |
|
2404 (is "(\<Sum>k<_. (- 1)^ k * ?a k) \<le> _") |
|
2405 and arctan_upper_bound: |
|
2406 "arctan x \<le> (\<Sum>k<2 * n + 1. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1)))" |
|
2407 proof - |
|
2408 have tendsto_zero: "?a \<longlonglongrightarrow> 0" |
|
2409 using assms |
|
2410 apply - |
|
2411 apply (rule tendsto_eq_rhs[where x="0 * 0"]) |
|
2412 subgoal by (intro tendsto_mult real_tendsto_divide_at_top) |
|
2413 (auto simp: filterlim_real_sequentially filterlim_sequentially_iff_filterlim_real |
|
2414 intro!: real_tendsto_divide_at_top tendsto_power_zero filterlim_real_sequentially |
|
2415 tendsto_eq_intros filterlim_at_top_mult_tendsto_pos filterlim_tendsto_add_at_top) |
|
2416 subgoal by simp |
|
2417 done |
|
2418 have nonneg: "0 \<le> ?a n" for n |
|
2419 by (force intro!: divide_nonneg_nonneg mult_nonneg_nonneg zero_le_power assms) |
|
2420 have le: "?a (Suc n) \<le> ?a n" for n |
|
2421 by (rule mult_mono[OF _ power_decreasing]) (auto simp: divide_simps assms less_imp_le) |
|
2422 from summable_Leibniz'(4)[of ?a, OF tendsto_zero nonneg le, of n] |
|
2423 summable_Leibniz'(2)[of ?a, OF tendsto_zero nonneg le, of n] |
|
2424 assms |
|
2425 show "(\<Sum>k<2*n. (- 1)^ k * ?a k) \<le> arctan x" "arctan x \<le> (\<Sum>k<2 * n + 1. (- 1)^ k * ?a k)" |
|
2426 by (auto simp: arctan_series) |
|
2427 qed |
|
2428 |
|
2429 subsection \<open>Bounds on pi using real arctangent\<close> |
|
2430 |
|
2431 lemma pi_machin: "pi = 16 * arctan (1 / 5) - 4 * arctan (1 / 239)" |
|
2432 using machin |
|
2433 by simp |
|
2434 |
|
2435 lemma pi_approx: "3.141592653588 \<le> pi" "pi \<le> 3.1415926535899" |
|
2436 unfolding pi_machin |
|
2437 using arctan_bounds[of "1/5" 4] |
|
2438 arctan_bounds[of "1/239" 4] |
|
2439 by (simp_all add: eval_nat_numeral) |
|
2440 |
2400 |
2441 |
2401 subsection\<open>Inverse Sine\<close> |
2442 subsection\<open>Inverse Sine\<close> |
2402 |
2443 |
2403 definition Arcsin :: "complex \<Rightarrow> complex" where |
2444 definition Arcsin :: "complex \<Rightarrow> complex" where |
2404 "Arcsin \<equiv> \<lambda>z. -\<i> * Ln(\<i> * z + csqrt(1 - z\<^sup>2))" |
2445 "Arcsin \<equiv> \<lambda>z. -\<i> * Ln(\<i> * z + csqrt(1 - z\<^sup>2))" |