2 Author : Jacques D. Fleuriot |
2 Author : Jacques D. Fleuriot |
3 Copyright : 2001 University of Edinburgh |
3 Copyright : 2001 University of Edinburgh |
4 Description : MacLaurin series |
4 Description : MacLaurin series |
5 *) |
5 *) |
6 |
6 |
7 MacLaurin = Log |
7 theory MacLaurin = Log |
|
8 files ("MacLaurin_lemmas.ML"): |
|
9 |
|
10 use "MacLaurin_lemmas.ML" |
|
11 |
|
12 lemma Maclaurin_sin_bound: |
|
13 "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * |
|
14 x ^ m)) <= inverse(real (fact n)) * abs(x) ^ n" |
|
15 proof - |
|
16 have "!! x (y::real). x <= 1 \<Longrightarrow> 0 <= y \<Longrightarrow> x * y \<le> 1 * y" |
|
17 by (rule_tac mult_right_mono,simp_all) |
|
18 note est = this[simplified] |
|
19 show ?thesis |
|
20 apply (cut_tac f=sin and n=n and x=x and |
|
21 diff = "%n x. if n mod 4 = 0 then sin(x) else if n mod 4 = 1 then cos(x) else if n mod 4 = 2 then -sin(x) else -cos(x)" |
|
22 in Maclaurin_all_le_objl) |
|
23 apply (tactic{* (Step_tac 1) *}) |
|
24 apply (simp) |
|
25 apply (subst mod_Suc_eq_Suc_mod) |
|
26 apply (tactic{* cut_inst_tac [("m1","m")] (CLAIM "0 < (4::nat)" RS mod_less_divisor RS lemma_exhaust_less_4) 1*}) |
|
27 apply (tactic{* Step_tac 1 *}) |
|
28 apply (simp)+ |
|
29 apply (rule DERIV_minus, simp+) |
|
30 apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp) |
|
31 apply (tactic{* dtac ssubst 1 THEN assume_tac 2 *}) |
|
32 apply (tactic {* rtac (ARITH_PROVE "[|x = y; abs u <= (v::real) |] ==> abs ((x + u) - y) <= v") 1 *}) |
|
33 apply (rule sumr_fun_eq) |
|
34 apply (tactic{* Step_tac 1 *}) |
|
35 apply (tactic{*rtac (CLAIM "x = y ==> x * z = y * (z::real)") 1*}) |
|
36 apply (subst even_even_mod_4_iff) |
|
37 apply (tactic{* cut_inst_tac [("m1","r")] (CLAIM "0 < (4::nat)" RS mod_less_divisor RS lemma_exhaust_less_4) 1 *}) |
|
38 apply (tactic{* Step_tac 1 *}) |
|
39 apply (simp) |
|
40 apply (simp_all add:even_num_iff) |
|
41 apply (drule lemma_even_mod_4_div_2[simplified]) |
|
42 apply(simp add: numeral_2_eq_2 real_divide_def) |
|
43 apply (drule lemma_odd_mod_4_div_2 ); |
|
44 apply (simp add: numeral_2_eq_2 real_divide_def) |
|
45 apply (auto intro: real_mult_le_lemma mult_right_mono simp add: est mult_pos_le mult_ac real_divide_def abs_mult abs_inverse power_abs[symmetric]) |
|
46 done |
|
47 qed |
|
48 |
|
49 end |