415 lemma sin_expansion_lemma: |
415 lemma sin_expansion_lemma: |
416 "sin (x + real (Suc m) * pi / 2) = |
416 "sin (x + real (Suc m) * pi / 2) = |
417 cos (x + real (m) * pi / 2)" |
417 cos (x + real (m) * pi / 2)" |
418 by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto) |
418 by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto) |
419 |
419 |
|
420 lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0" |
|
421 unfolding sin_coeff_def by simp (* TODO: move *) |
|
422 |
420 lemma Maclaurin_sin_expansion2: |
423 lemma Maclaurin_sin_expansion2: |
421 "\<exists>t. abs t \<le> abs x & |
424 "\<exists>t. abs t \<le> abs x & |
422 sin x = |
425 sin x = |
423 (\<Sum>m=0..<n. (if even m then 0 |
426 (\<Sum>m=0..<n. sin_coeff m * x ^ m) |
424 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) * |
|
425 x ^ m) |
|
426 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
427 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
427 apply (cut_tac f = sin and n = n and x = x |
428 apply (cut_tac f = sin and n = n and x = x |
428 and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl) |
429 and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl) |
429 apply safe |
430 apply safe |
430 apply (simp (no_asm)) |
431 apply (simp (no_asm)) |
431 apply (simp (no_asm) add: sin_expansion_lemma) |
432 apply (simp (no_asm) add: sin_expansion_lemma) |
432 apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin) |
433 apply (subst (asm) setsum_0', clarify, case_tac "a", simp, simp) |
|
434 apply (cases n, simp, simp) |
433 apply (rule ccontr, simp) |
435 apply (rule ccontr, simp) |
434 apply (drule_tac x = x in spec, simp) |
436 apply (drule_tac x = x in spec, simp) |
435 apply (erule ssubst) |
437 apply (erule ssubst) |
436 apply (rule_tac x = t in exI, simp) |
438 apply (rule_tac x = t in exI, simp) |
437 apply (rule setsum_cong[OF refl]) |
439 apply (rule setsum_cong[OF refl]) |
438 apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex) |
440 apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex) |
439 done |
441 done |
440 |
442 |
441 lemma Maclaurin_sin_expansion: |
443 lemma Maclaurin_sin_expansion: |
442 "\<exists>t. sin x = |
444 "\<exists>t. sin x = |
443 (\<Sum>m=0..<n. (if even m then 0 |
445 (\<Sum>m=0..<n. sin_coeff m * x ^ m) |
444 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) * |
|
445 x ^ m) |
|
446 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
446 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
447 apply (insert Maclaurin_sin_expansion2 [of x n]) |
447 apply (insert Maclaurin_sin_expansion2 [of x n]) |
448 apply (blast intro: elim:) |
448 apply (blast intro: elim:) |
449 done |
449 done |
450 |
450 |
451 lemma Maclaurin_sin_expansion3: |
451 lemma Maclaurin_sin_expansion3: |
452 "[| n > 0; 0 < x |] ==> |
452 "[| n > 0; 0 < x |] ==> |
453 \<exists>t. 0 < t & t < x & |
453 \<exists>t. 0 < t & t < x & |
454 sin x = |
454 sin x = |
455 (\<Sum>m=0..<n. (if even m then 0 |
455 (\<Sum>m=0..<n. sin_coeff m * x ^ m) |
456 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) * |
|
457 x ^ m) |
|
458 + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)" |
456 + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)" |
459 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) |
457 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) |
460 apply safe |
458 apply safe |
461 apply simp |
459 apply simp |
462 apply (simp (no_asm) add: sin_expansion_lemma) |
460 apply (simp (no_asm) add: sin_expansion_lemma) |
463 apply (erule ssubst) |
461 apply (erule ssubst) |
464 apply (rule_tac x = t in exI, simp) |
462 apply (rule_tac x = t in exI, simp) |
465 apply (rule setsum_cong[OF refl]) |
463 apply (rule setsum_cong[OF refl]) |
466 apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex) |
464 apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex) |
467 done |
465 done |
468 |
466 |
469 lemma Maclaurin_sin_expansion4: |
467 lemma Maclaurin_sin_expansion4: |
470 "0 < x ==> |
468 "0 < x ==> |
471 \<exists>t. 0 < t & t \<le> x & |
469 \<exists>t. 0 < t & t \<le> x & |
472 sin x = |
470 sin x = |
473 (\<Sum>m=0..<n. (if even m then 0 |
471 (\<Sum>m=0..<n. sin_coeff m * x ^ m) |
474 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) * |
|
475 x ^ m) |
|
476 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
472 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
477 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) |
473 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) |
478 apply safe |
474 apply safe |
479 apply simp |
475 apply simp |
480 apply (simp (no_asm) add: sin_expansion_lemma) |
476 apply (simp (no_asm) add: sin_expansion_lemma) |
481 apply (erule ssubst) |
477 apply (erule ssubst) |
482 apply (rule_tac x = t in exI, simp) |
478 apply (rule_tac x = t in exI, simp) |
483 apply (rule setsum_cong[OF refl]) |
479 apply (rule setsum_cong[OF refl]) |
484 apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex) |
480 apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex) |
485 done |
481 done |
486 |
482 |
487 |
483 |
488 subsection{*Maclaurin Expansion for Cosine Function*} |
484 subsection{*Maclaurin Expansion for Cosine Function*} |
489 |
485 |
|
486 lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1" |
|
487 unfolding cos_coeff_def by simp (* TODO: move *) |
|
488 |
490 lemma sumr_cos_zero_one [simp]: |
489 lemma sumr_cos_zero_one [simp]: |
491 "(\<Sum>m=0..<(Suc n). |
490 "(\<Sum>m=0..<(Suc n). cos_coeff m * 0 ^ m) = 1" |
492 (if even m then -1 ^ (m div 2)/(real (fact m)) else 0) * 0 ^ m) = 1" |
|
493 by (induct "n", auto) |
491 by (induct "n", auto) |
494 |
492 |
495 lemma cos_expansion_lemma: |
493 lemma cos_expansion_lemma: |
496 "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)" |
494 "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)" |
497 by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto) |
495 by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto) |
498 |
496 |
499 lemma Maclaurin_cos_expansion: |
497 lemma Maclaurin_cos_expansion: |
500 "\<exists>t. abs t \<le> abs x & |
498 "\<exists>t. abs t \<le> abs x & |
501 cos x = |
499 cos x = |
502 (\<Sum>m=0..<n. (if even m |
500 (\<Sum>m=0..<n. cos_coeff m * x ^ m) |
503 then -1 ^ (m div 2)/(real (fact m)) |
|
504 else 0) * |
|
505 x ^ m) |
|
506 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
501 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
507 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) |
502 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) |
508 apply safe |
503 apply safe |
509 apply (simp (no_asm)) |
504 apply (simp (no_asm)) |
510 apply (simp (no_asm) add: cos_expansion_lemma) |
505 apply (simp (no_asm) add: cos_expansion_lemma) |
513 apply (rule ccontr, simp) |
508 apply (rule ccontr, simp) |
514 apply (drule_tac x = x in spec, simp) |
509 apply (drule_tac x = x in spec, simp) |
515 apply (erule ssubst) |
510 apply (erule ssubst) |
516 apply (rule_tac x = t in exI, simp) |
511 apply (rule_tac x = t in exI, simp) |
517 apply (rule setsum_cong[OF refl]) |
512 apply (rule setsum_cong[OF refl]) |
518 apply (auto simp add: cos_zero_iff even_mult_two_ex) |
513 apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex) |
519 done |
514 done |
520 |
515 |
521 lemma Maclaurin_cos_expansion2: |
516 lemma Maclaurin_cos_expansion2: |
522 "[| 0 < x; n > 0 |] ==> |
517 "[| 0 < x; n > 0 |] ==> |
523 \<exists>t. 0 < t & t < x & |
518 \<exists>t. 0 < t & t < x & |
524 cos x = |
519 cos x = |
525 (\<Sum>m=0..<n. (if even m |
520 (\<Sum>m=0..<n. cos_coeff m * x ^ m) |
526 then -1 ^ (m div 2)/(real (fact m)) |
|
527 else 0) * |
|
528 x ^ m) |
|
529 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
521 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
530 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) |
522 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) |
531 apply safe |
523 apply safe |
532 apply simp |
524 apply simp |
533 apply (simp (no_asm) add: cos_expansion_lemma) |
525 apply (simp (no_asm) add: cos_expansion_lemma) |
534 apply (erule ssubst) |
526 apply (erule ssubst) |
535 apply (rule_tac x = t in exI, simp) |
527 apply (rule_tac x = t in exI, simp) |
536 apply (rule setsum_cong[OF refl]) |
528 apply (rule setsum_cong[OF refl]) |
537 apply (auto simp add: cos_zero_iff even_mult_two_ex) |
529 apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex) |
538 done |
530 done |
539 |
531 |
540 lemma Maclaurin_minus_cos_expansion: |
532 lemma Maclaurin_minus_cos_expansion: |
541 "[| x < 0; n > 0 |] ==> |
533 "[| x < 0; n > 0 |] ==> |
542 \<exists>t. x < t & t < 0 & |
534 \<exists>t. x < t & t < 0 & |
543 cos x = |
535 cos x = |
544 (\<Sum>m=0..<n. (if even m |
536 (\<Sum>m=0..<n. cos_coeff m * x ^ m) |
545 then -1 ^ (m div 2)/(real (fact m)) |
|
546 else 0) * |
|
547 x ^ m) |
|
548 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
537 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" |
549 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) |
538 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) |
550 apply safe |
539 apply safe |
551 apply simp |
540 apply simp |
552 apply (simp (no_asm) add: cos_expansion_lemma) |
541 apply (simp (no_asm) add: cos_expansion_lemma) |
553 apply (erule ssubst) |
542 apply (erule ssubst) |
554 apply (rule_tac x = t in exI, simp) |
543 apply (rule_tac x = t in exI, simp) |
555 apply (rule setsum_cong[OF refl]) |
544 apply (rule setsum_cong[OF refl]) |
556 apply (auto simp add: cos_zero_iff even_mult_two_ex) |
545 apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex) |
557 done |
546 done |
558 |
547 |
559 (* ------------------------------------------------------------------------- *) |
548 (* ------------------------------------------------------------------------- *) |
560 (* Version for ln(1 +/- x). Where is it?? *) |
549 (* Version for ln(1 +/- x). Where is it?? *) |
561 (* ------------------------------------------------------------------------- *) |
550 (* ------------------------------------------------------------------------- *) |