equal
deleted
inserted
replaced
90 apply (rule mult_nonneg_nonneg) |
90 apply (rule mult_nonneg_nonneg) |
91 apply simp |
91 apply simp |
92 apply (subst inverse_nonnegative_iff_nonnegative) |
92 apply (subst inverse_nonnegative_iff_nonnegative) |
93 apply (rule real_of_nat_fact_ge_zero) |
93 apply (rule real_of_nat_fact_ge_zero) |
94 apply (rule zero_le_power) |
94 apply (rule zero_le_power) |
95 apply assumption |
95 apply (rule a) |
96 done |
96 done |
97 also have "... = 1 / 2 * (inverse (real (fact (n + 2))) * x ^ (n + 2))" |
97 also have "... = 1 / 2 * (inverse (real (fact (n + 2))) * x ^ (n + 2))" |
98 by simp |
98 by simp |
99 also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)" |
99 also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)" |
100 apply (rule mult_left_mono) |
100 apply (rule mult_left_mono) |
319 done |
319 done |
320 |
320 |
321 lemma abs_ln_one_plus_x_minus_x_bound_nonneg: |
321 lemma abs_ln_one_plus_x_minus_x_bound_nonneg: |
322 "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2" |
322 "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2" |
323 proof - |
323 proof - |
324 assume "0 <= x" |
324 assume x: "0 <= x" |
325 assume "x <= 1" |
325 assume "x <= 1" |
326 have "ln (1 + x) <= x" |
326 from x have "ln (1 + x) <= x" |
327 by (rule ln_add_one_self_le_self) |
327 by (rule ln_add_one_self_le_self) |
328 then have "ln (1 + x) - x <= 0" |
328 then have "ln (1 + x) - x <= 0" |
329 by simp |
329 by simp |
330 then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)" |
330 then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)" |
331 by (rule abs_of_nonpos) |
331 by (rule abs_of_nonpos) |