linear arithmetic splits certain operators (e.g. min, max, abs)
2 Author : Jacques D. Fleuriot
3 Copyright : 2001 University of Edinburgh
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004
7 header{*MacLaurin Series*}
13 subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
15 text{*This is a very long, messy proof even now that it's been broken down
18 lemma Maclaurin_lemma:
20 \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
21 (B * ((h^n) / real(fact n)))"
22 apply (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
28 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
31 text{*A crude tactic to differentiate by proof.*}
36 [thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
37 thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow",
38 thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus",
39 thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow",
40 thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos",
41 thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos"];
43 val DERIV_chain2 = thm "DERIV_chain2";
48 fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
49 | get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
50 | get_fun_name _ = raise DERIV_name;
53 SUBGOAL (fn (prem,i) =>
54 (resolve_tac deriv_rulesI i) ORELSE
55 ((rtac (read_instantiate [("f",get_fun_name prem)]
56 DERIV_chain2) i) handle DERIV_name => no_tac));;
58 val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i));
63 lemma Maclaurin_lemma2:
64 "[| \<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t;
67 (\<lambda>m t. diff m t -
68 ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
69 B * (t ^ (n - m) / real (fact (n - m)))))|] ==>
70 \<forall>m t. m < n & 0 \<le> t & t \<le> h -->
71 DERIV (difg m) t :> difg (Suc m) t"
73 apply (rule DERIV_diff)
74 apply (simp (no_asm_simp))
75 apply (tactic DERIV_tac)
76 apply (tactic DERIV_tac)
77 apply (rule_tac [2] lemma_DERIV_subst)
78 apply (rule_tac [2] DERIV_quotient)
79 apply (rule_tac [3] DERIV_const)
80 apply (rule_tac [2] DERIV_pow)
81 prefer 3 apply (simp add: fact_diff_Suc)
83 apply (frule_tac m = m in less_add_one, clarify)
84 apply (simp del: setsum_op_ivl_Suc)
85 apply (insert sumr_offset4 [of 1])
86 apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
87 apply (rule lemma_DERIV_subst)
88 apply (rule DERIV_add)
89 apply (rule_tac [2] DERIV_const)
90 apply (rule DERIV_sumr, clarify)
92 apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc realpow_Suc)
93 apply (rule DERIV_cmult)
94 apply (rule lemma_DERIV_subst)
95 apply (best intro: DERIV_chain2 intro!: DERIV_intros)
96 apply (subst fact_Suc)
97 apply (subst real_of_nat_mult)
98 apply (simp add: mult_ac)
102 lemma Maclaurin_lemma3:
103 "[|\<forall>k t. k < Suc m \<and> 0\<le>t & t\<le>h \<longrightarrow> DERIV (difg k) t :> difg (Suc k) t;
104 \<forall>k<Suc m. difg k 0 = 0; DERIV (difg n) t :> 0; n < m; 0 < t;
106 ==> \<exists>ta. 0 < ta & ta < t & DERIV (difg (Suc n)) ta :> 0"
107 apply (rule Rolle, assumption, simp)
108 apply (drule_tac x = n and P="%k. k<Suc m --> difg k 0 = 0" in spec)
109 apply (rule DERIV_unique)
110 prefer 2 apply assumption
112 apply (subgoal_tac "\<forall>ta. 0 \<le> ta & ta \<le> t --> (difg (Suc n)) differentiable ta")
113 apply (simp add: differentiable_def)
114 apply (blast dest!: DERIV_isCont)
115 apply (simp add: differentiable_def, clarify)
116 apply (rule_tac x = "difg (Suc (Suc n)) ta" in exI)
118 apply (simp add: differentiable_def, clarify)
119 apply (rule_tac x = "difg (Suc (Suc n)) x" in exI)
124 "[| 0 < h; 0 < n; diff 0 = f;
125 \<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
126 ==> \<exists>t. 0 < t &
129 setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
130 (diff n t / real (fact n)) * h ^ n"
131 apply (case_tac "n = 0", force)
132 apply (drule not0_implies_Suc)
134 apply (frule_tac f=f and n=n and j="%m. diff m 0" in Maclaurin_lemma)
136 apply (subgoal_tac "\<exists>g.
137 g = (%t. f t - (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n} + (B * (t^n / real(fact n)))))")
140 apply (subgoal_tac "g 0 = 0 & g h =0")
142 apply (simp del: setsum_op_ivl_Suc)
143 apply (cut_tac n = m and k = 1 in sumr_offset2)
144 apply (simp add: eq_diff_eq' del: setsum_op_ivl_Suc)
145 apply (subgoal_tac "\<exists>difg. difg = (%m t. diff m t - (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m} + (B * ((t ^ (n - m)) / real (fact (n - m))))))")
148 apply (subgoal_tac "difg 0 = g")
150 apply (frule Maclaurin_lemma2, assumption+)
151 apply (subgoal_tac "\<forall>ma. ma < n --> (\<exists>t. 0 < t & t < h & difg (Suc ma) t = 0) ")
152 apply (drule_tac x = m and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
154 apply (simp (no_asm_simp))
156 apply (rule_tac x = t in exI)
157 apply (simp del: realpow_Suc fact_Suc)
158 apply (subgoal_tac "\<forall>m. m < n --> difg m 0 = 0")
162 apply (frule_tac m = ma in less_add_one, clarify)
163 apply (simp del: setsum_op_ivl_Suc)
164 apply (insert sumr_offset4 [of 1])
165 apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
166 apply (subgoal_tac "\<forall>m. m < n --> (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ")
167 apply (rule allI, rule impI)
168 apply (drule_tac x = ma and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
169 apply (erule impE, assumption)
171 apply (rule_tac x = t in exI)
172 (* do some tidying up *)
173 apply (erule_tac [!] V= "difg = (%m t. diff m t - (setsum (%p. diff (m + p) 0 / real (fact p) * t ^ p) {0..<n-m} + B * (t ^ (n - m) / real (fact (n - m)))))"
175 apply (erule_tac [!] V="g = (%t. f t - (setsum (%m. diff m 0 / real (fact m) * t ^ m) {0..<n} + B * (t ^ n / real (fact n))))"
177 apply (erule_tac [!] V="f h = setsum (%m. diff m 0 / real (fact m) * h ^ m) {0..<n} + B * (h ^ n / real (fact n))"
179 (* back to business *)
180 apply (simp (no_asm_simp))
181 apply (rule DERIV_unique)
184 apply (rule allI, induct_tac "ma")
185 apply (rule impI, rule Rolle, assumption, simp, simp)
186 apply (subgoal_tac "\<forall>t. 0 \<le> t & t \<le> h --> g differentiable t")
187 apply (simp add: differentiable_def)
188 apply (blast dest: DERIV_isCont)
189 apply (simp add: differentiable_def, clarify)
190 apply (rule_tac x = "difg (Suc 0) t" in exI)
192 apply (simp add: differentiable_def, clarify)
193 apply (rule_tac x = "difg (Suc 0) x" in exI)
197 apply (frule Maclaurin_lemma3, assumption+, safe)
198 apply (rule_tac x = ta in exI, force)
201 lemma Maclaurin_objl:
202 "0 < h & 0 < n & diff 0 = f &
203 (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
204 --> (\<exists>t. 0 < t &
207 (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
208 diff n t / real (fact n) * h ^ n)"
209 by (blast intro: Maclaurin)
213 "[| 0 < h; diff 0 = f;
215 m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
216 ==> \<exists>t. 0 < t &
219 (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
220 diff n t / real (fact n) * h ^ n"
221 apply (case_tac "n", auto)
222 apply (drule Maclaurin, auto)
225 lemma Maclaurin2_objl:
226 "0 < h & diff 0 = f &
228 m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
229 --> (\<exists>t. 0 < t &
232 (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
233 diff n t / real (fact n) * h ^ n)"
234 by (blast intro: Maclaurin2)
236 lemma Maclaurin_minus:
237 "[| h < 0; 0 < n; diff 0 = f;
238 \<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t |]
239 ==> \<exists>t. h < t &
242 (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
243 diff n t / real (fact n) * h ^ n"
244 apply (cut_tac f = "%x. f (-x)"
245 and diff = "%n x. ((- 1) ^ n) * diff n (-x)"
246 and h = "-h" and n = n in Maclaurin_objl)
249 apply (subst minus_mult_right)
250 apply (rule DERIV_cmult)
251 apply (rule lemma_DERIV_subst)
252 apply (rule DERIV_chain2 [where g=uminus])
253 apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_Id)
256 apply (rule_tac x = "-t" in exI, auto)
257 apply (subgoal_tac "(\<Sum>m = 0..<n. -1 ^ m * diff m 0 * (-h)^m / real(fact m)) =
258 (\<Sum>m = 0..<n. diff m 0 * h ^ m / real(fact m))")
259 apply (rule_tac [2] setsum_cong[OF refl])
260 apply (auto simp add: divide_inverse power_mult_distrib [symmetric])
263 lemma Maclaurin_minus_objl:
264 "(h < 0 & 0 < n & diff 0 = f &
266 m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
267 --> (\<exists>t. h < t &
270 (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
271 diff n t / real (fact n) * h ^ n)"
272 by (blast intro: Maclaurin_minus)
275 subsection{*More Convenient "Bidirectional" Version.*}
277 (* not good for PVS sin_approx, cos_approx *)
279 lemma Maclaurin_bi_le_lemma [rule_format]:
280 "0 < n \<longrightarrow>
282 (\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) +
283 diff n 0 * 0 ^ n / real (fact n)"
284 by (induct "n", auto)
286 lemma Maclaurin_bi_le:
288 \<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t |]
289 ==> \<exists>t. abs t \<le> abs x &
291 (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
292 diff n t / real (fact n) * x ^ n"
293 apply (case_tac "n = 0", force)
294 apply (case_tac "x = 0")
295 apply (rule_tac x = 0 in exI)
296 apply (force simp add: Maclaurin_bi_le_lemma)
297 apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
298 txt{*Case 1, where @{term "x < 0"}*}
299 apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
300 apply (simp add: abs_if)
301 apply (rule_tac x = t in exI)
302 apply (simp add: abs_if)
303 txt{*Case 2, where @{term "0 < x"}*}
304 apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe)
305 apply (simp add: abs_if)
306 apply (rule_tac x = t in exI)
307 apply (simp add: abs_if)
310 lemma Maclaurin_all_lt:
312 \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
314 |] ==> \<exists>t. 0 < abs t & abs t < abs x &
315 f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
316 (diff n t / real (fact n)) * x ^ n"
317 apply (rule_tac x = x and y = 0 in linorder_cases)
319 apply (drule_tac [2] diff=diff in Maclaurin)
320 apply (drule_tac diff=diff in Maclaurin_minus, simp_all, safe)
321 apply (rule_tac [!] x = t in exI, auto)
324 lemma Maclaurin_all_lt_objl:
326 (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
328 --> (\<exists>t. 0 < abs t & abs t < abs x &
329 f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
330 (diff n t / real (fact n)) * x ^ n)"
331 by (blast intro: Maclaurin_all_lt)
333 lemma Maclaurin_zero [rule_format]:
336 (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
340 lemma Maclaurin_all_le: "[| diff 0 = f;
341 \<forall>m x. DERIV (diff m) x :> diff (Suc m) x
342 |] ==> \<exists>t. abs t \<le> abs x &
343 f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
344 (diff n t / real (fact n)) * x ^ n"
345 apply (insert linorder_le_less_linear [of n 0])
346 apply (erule disjE, force)
347 apply (case_tac "x = 0")
348 apply (frule_tac diff = diff and n = n in Maclaurin_zero, assumption)
349 apply (drule gr_implies_not0 [THEN not0_implies_Suc])
350 apply (rule_tac x = 0 in exI, force)
351 apply (frule_tac diff = diff and n = n in Maclaurin_all_lt, auto)
352 apply (rule_tac x = t in exI, auto)
355 lemma Maclaurin_all_le_objl: "diff 0 = f &
356 (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
357 --> (\<exists>t. abs t \<le> abs x &
358 f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
359 (diff n t / real (fact n)) * x ^ n)"
360 by (blast intro: Maclaurin_all_le)
363 subsection{*Version for Exponential Function*}
365 lemma Maclaurin_exp_lt: "[| x ~= 0; 0 < n |]
366 ==> (\<exists>t. 0 < abs t &
368 exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
369 (exp t / real (fact n)) * x ^ n)"
370 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
373 lemma Maclaurin_exp_le:
374 "\<exists>t. abs t \<le> abs x &
375 exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
376 (exp t / real (fact n)) * x ^ n"
377 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
380 subsection{*Version for Sine Function*}
383 "[| a < b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
384 ==> \<exists>z. a < z & z < b & (f b - f a = (b - a) * f'(z))"
386 apply (blast intro: DERIV_isCont)
387 apply (force dest: order_less_imp_le simp add: differentiable_def)
388 apply (blast dest: DERIV_unique order_less_imp_le)
391 lemma mod_exhaust_less_4:
392 "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
395 lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
396 "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"
397 by (induct "n", auto)
399 lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]:
400 "0 < n --> Suc (Suc (4*n - 2)) = 4*n"
401 by (induct "n", auto)
403 lemma Suc_mult_two_diff_one [rule_format, simp]:
404 "0 < n --> Suc (2 * n - 1) = 2*n"
405 by (induct "n", auto)
408 text{*It is unclear why so many variant results are needed.*}
410 lemma Maclaurin_sin_expansion2:
411 "\<exists>t. abs t \<le> abs x &
413 (\<Sum>m=0..<n. (if even m then 0
414 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
416 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
417 apply (cut_tac f = sin and n = n and x = x
418 and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
420 apply (simp (no_asm))
421 apply (simp (no_asm))
422 apply (case_tac "n", clarify, simp, simp)
423 apply (rule ccontr, simp)
424 apply (drule_tac x = x in spec, simp)
426 apply (rule_tac x = t in exI, simp)
427 apply (rule setsum_cong[OF refl])
428 apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
431 lemma Maclaurin_sin_expansion:
433 (\<Sum>m=0..<n. (if even m then 0
434 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
436 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
437 apply (insert Maclaurin_sin_expansion2 [of x n])
438 apply (blast intro: elim:);
443 lemma Maclaurin_sin_expansion3:
444 "[| 0 < n; 0 < x |] ==>
445 \<exists>t. 0 < t & t < x &
447 (\<Sum>m=0..<n. (if even m then 0
448 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
450 + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
451 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
454 apply (simp (no_asm))
456 apply (rule_tac x = t in exI, simp)
457 apply (rule setsum_cong[OF refl])
458 apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
461 lemma Maclaurin_sin_expansion4:
463 \<exists>t. 0 < t & t \<le> x &
465 (\<Sum>m=0..<n. (if even m then 0
466 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
468 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
469 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
472 apply (simp (no_asm))
474 apply (rule_tac x = t in exI, simp)
475 apply (rule setsum_cong[OF refl])
476 apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
480 subsection{*Maclaurin Expansion for Cosine Function*}
482 lemma sumr_cos_zero_one [simp]:
483 "(\<Sum>m=0..<(Suc n).
484 (if even m then (- 1) ^ (m div 2)/(real (fact m)) else 0) * 0 ^ m) = 1"
485 by (induct "n", auto)
487 lemma Maclaurin_cos_expansion:
488 "\<exists>t. abs t \<le> abs x &
490 (\<Sum>m=0..<n. (if even m
491 then (- 1) ^ (m div 2)/(real (fact m))
494 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
495 apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
497 apply (simp (no_asm))
498 apply (simp (no_asm))
499 apply (case_tac "n", simp)
500 apply (simp del: setsum_op_ivl_Suc)
501 apply (rule ccontr, simp)
502 apply (drule_tac x = x in spec, simp)
504 apply (rule_tac x = t in exI, simp)
505 apply (rule setsum_cong[OF refl])
506 apply (auto simp add: cos_zero_iff even_mult_two_ex)
509 lemma Maclaurin_cos_expansion2:
510 "[| 0 < x; 0 < n |] ==>
511 \<exists>t. 0 < t & t < x &
513 (\<Sum>m=0..<n. (if even m
514 then (- 1) ^ (m div 2)/(real (fact m))
517 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
518 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
521 apply (simp (no_asm))
523 apply (rule_tac x = t in exI, simp)
524 apply (rule setsum_cong[OF refl])
525 apply (auto simp add: cos_zero_iff even_mult_two_ex)
528 lemma Maclaurin_minus_cos_expansion:
529 "[| x < 0; 0 < n |] ==>
530 \<exists>t. x < t & t < 0 &
532 (\<Sum>m=0..<n. (if even m
533 then (- 1) ^ (m div 2)/(real (fact m))
536 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
537 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
540 apply (simp (no_asm))
542 apply (rule_tac x = t in exI, simp)
543 apply (rule setsum_cong[OF refl])
544 apply (auto simp add: cos_zero_iff even_mult_two_ex)
547 (* ------------------------------------------------------------------------- *)
548 (* Version for ln(1 +/- x). Where is it?? *)
549 (* ------------------------------------------------------------------------- *)
551 lemma sin_bound_lemma:
552 "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
555 lemma Maclaurin_sin_bound:
556 "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
557 x ^ m)) \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
559 have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
560 by (rule_tac mult_right_mono,simp_all)
561 note est = this[simplified]
563 apply (cut_tac f=sin and n=n and x=x and
564 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)"
565 in Maclaurin_all_le_objl)
568 apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
569 apply (cut_tac m=m in mod_exhaust_less_4, safe, simp+)
570 apply (rule DERIV_minus, simp+)
571 apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
573 apply (rule sin_bound_lemma)
574 apply (rule setsum_cong[OF refl])
575 apply (rule_tac f = "%u. u * (x^xa)" in arg_cong)
576 apply (subst even_even_mod_4_iff)
577 apply (cut_tac m=xa in mod_exhaust_less_4, simp, safe)
578 apply (simp_all add:even_num_iff)
579 apply (drule lemma_even_mod_4_div_2[simplified])
580 apply(simp add: numeral_2_eq_2 divide_inverse)
581 apply (drule lemma_odd_mod_4_div_2)
582 apply (simp add: numeral_2_eq_2 divide_inverse)
583 apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
584 simp add: est mult_nonneg_nonneg mult_ac divide_inverse
585 power_abs [symmetric] abs_mult)