equal
deleted
inserted
replaced
573 (* ------------------------------------------------------------------------- *) |
573 (* ------------------------------------------------------------------------- *) |
574 (* Version for ln(1 +/- x). Where is it?? *) |
574 (* Version for ln(1 +/- x). Where is it?? *) |
575 (* ------------------------------------------------------------------------- *) |
575 (* ------------------------------------------------------------------------- *) |
576 |
576 |
577 lemma sin_bound_lemma: |
577 lemma sin_bound_lemma: |
578 "[|x = y; abs u \<le> (v::real) |] ==> abs ((x + u) - y) \<le> v" |
578 "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v" |
579 by auto |
579 by auto |
580 |
580 |
581 lemma Maclaurin_sin_bound: |
581 lemma Maclaurin_sin_bound: |
582 "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * |
582 "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) * |
583 x ^ m)) \<le> inverse(real (fact n)) * abs(x) ^ n" |
583 x ^ m)) \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n" |
584 proof - |
584 proof - |
585 have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" |
585 have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" |
586 by (rule_tac mult_right_mono,simp_all) |
586 by (rule_tac mult_right_mono,simp_all) |
587 note est = this[simplified] |
587 note est = this[simplified] |
588 show ?thesis |
588 show ?thesis |