(* Title: Ln.thy Author: Jeremy Avigad *) header {* The derivative of ln *} theory Ln = RealLib:; (******************************************************************) (* *) (* Lower bound for ln (1 + x), for x positive and small *) (* *) (******************************************************************) subsection {* Lower bound for ln (1 + x), for x positive and small *} lemma exp_first_two_terms: "exp x = 1 + x + suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2)))" proof - fix x have "exp x = suminf(%n. inverse(real (fact n)) * (x ^ n))" by (unfold exp_def, simp) also from summable_exp have "... = sumr 0 2 (%n. inverse(real (fact n)) * (x ^ n)) + suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2)))" by (rule suminf_split_initial_segment) also have "sumr 0 2 (%n. inverse(real (fact n)) * (x ^ n)) = 1 + x" by (simp add: sumr_zero_to_two) finally show "exp x = 1 + x + suminf (%n. inverse (real (fact (n + 2))) * x ^ (n + 2))" . qed lemma exp_tail_after_first_two_terms_summable: "summable (%n. inverse(real (fact (n+2))) * (x ^ (n+2)))" proof - note summable_exp thus ?thesis by (frule summable_ignore_initial_segment) qed lemma aux1: assumes a: "0 <= x" and b: "x <= 1" shows "inverse (real (fact (n + 2))) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)" proof (induct n) show "inverse (real (fact (0 + 2))) * x ^ (0 + 2) <= x ^ 2 / 2 * (1 / 2) ^ 0" proof - have "real (fact (0 + 2)) = 2" by simp; moreover have "x ^ (0 + 2) = x ^ 2" proof - have "0 + 2 = (2::nat)" by simp thus ?thesis by (rule ssubst, simp) qed ultimately have "inverse (real (fact (0 + 2))) * x ^ (0 + 2) = inverse 2 * x ^ 2" by (simp only:); also have "... <= inverse 2 * x ^ 2" by auto finally show ?thesis by auto qed next fix n assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2) <= x ^ 2 / 2 * (1 / 2) ^ n" show "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2) <= x ^ 2 / 2 * (1 / 2) ^ Suc n" proof - have "inverse(real (fact (Suc n + 2))) <= (1/ 2) *inverse (real (fact (n+2)))" proof - have "Suc n + 2 = Suc (n + 2)" by simp then have "fact (Suc n + 2) = Suc (n + 2) * fact (n + 2)" by simp then have "real(fact (Suc n + 2)) = real(Suc (n + 2) * fact (n + 2))" apply (rule subst) by (rule refl) also have "... = real(Suc (n + 2)) * real(fact (n + 2))" by (rule real_of_nat_mult) finally have "real (fact (Suc n + 2)) = real (Suc (n + 2)) * real (fact (n + 2))" . then have "inverse(real (fact (Suc n + 2))) = inverse(real (Suc (n + 2))) * inverse(real (fact (n + 2)))" apply (rule ssubst); apply (rule inverse_mult_distrib); done; also have "... <= (1/2) * inverse(real (fact (n + 2)))" proof (intro mult_right_mono); show "0 <= inverse (real (fact (n + 2)))" by (rule inv_real_of_nat_fact_ge_zero) next show "inverse(real (Suc (n + 2))) <= 1/2" proof - have "2 <= Suc (n + 2)" by arith then have "real (2::nat) <= real(Suc (n + 2))" by (auto simp only: real_of_nat_le_iff) then have "inverse (real(Suc (n + 2))) <= inverse (real (2:: nat))" by (auto simp only: intro: real_inverse_le_swap) thus ?thesis by simp qed qed finally show ?thesis . qed moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)" proof - have "Suc n + 2 = Suc (n + 2)" by auto then have "x ^ (Suc n + 2) = x ^ Suc (n + 2)" by simp also have "... = x ^ (n + 2) * x" by simp also have "... <= x ^ (n + 2)" apply (rule real_mult_le_one_le) by (auto simp only: a b zero_le_power) finally show ?thesis . qed ultimately have "inverse (real (fact (Suc n + 2))) * x ^ (Suc n + 2) <= (1 / 2 * inverse (real (fact (n + 2)))) * x ^ (n + 2)" apply (rule mult_mono); apply (rule nonneg_times_nonneg); apply simp; apply (subst inverse_nonnegative_iff_nonnegative); apply (rule real_of_nat_fact_ge_zero); apply (rule zero_le_power); apply assumption; done; also have "... = 1 / 2 * (inverse (real (fact (n + 2))) * x ^ (n + 2))" by simp also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)" apply (rule mult_left_mono) apply (rule prems); apply simp; done; also have "... = x ^ 2 / 2 * (1 / 2 * (1 / 2) ^ n)" by auto also have "(1::real) / 2 * (1 / 2) ^ n = (1 / 2) ^ (Suc n)" by (rule realpow_Suc [THEN sym]) finally show ?thesis . qed qed lemma aux2: "(%n. x ^ 2 / 2 * (1 / 2) ^ n) sums x^2" proof - have "(%n. (1 / 2)^n) sums (1 / (1 - (1/2)))" apply (rule geometric_sums) by (simp add: abs_interval_iff) also have "(1::real) / (1 - 1/2) = 2" by simp finally have "(%n. (1 / 2)^n) sums 2" . then have "(%n. x ^ 2 / 2 * (1 / 2) ^ n) sums (x^2 / 2 * 2)" by (rule sums_mult) also have "x^2 / 2 * 2 = x^2" by simp finally show ?thesis . qed lemma exp_bound: "0 <= x ==> x <= 1 ==> exp x <= 1 + x + x^2" proof - assume a: "0 <= x" assume b: "x <= 1" have c: "exp x = 1 + x + suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2)))" by (rule exp_first_two_terms) moreover have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <= x^2" proof - have "suminf (%n. inverse(real (fact (n+2))) * (x ^ (n+2))) <= suminf (%n. (x^2/2) * ((1/2)^n))" apply (rule summable_le) apply (auto simp only: aux1 prems) apply (rule exp_tail_after_first_two_terms_summable) by (rule sums_summable, rule aux2) also have "... = x^2" by (rule sums_unique [THEN sym], rule aux2) finally show ?thesis . qed ultimately show ?thesis by auto qed lemma aux3: assumes a: "(0::real) <= x" and b: "x <= 1" shows "(1 + x + x^2)/(1 + x^2) <= 1 + x" proof - from a have "1 + x + x^2 <= 1 + x + x^2 + x^3" by (auto simp add: zero_le_power); also have "... = (1 + x^2) * (1 + x)" apply (auto simp add: left_distrib right_distrib); proof - have "x ^ 2 * x = x * x ^ 2" by auto moreover have "x ^ 3 = x ^ (Suc 2)" by auto ultimately show "x ^ 3 = x ^ 2 * x" by (auto simp only: realpow_Suc) qed finally have "1 + x + x^2 <= (1 + x^2) * (1 + x)" . moreover have "0 < 1 + x^2" proof - have "(0::real) = 0 + 0" by simp also have "... < 1 + x^2" by (rule real_add_less_le_mono, auto) finally show ?thesis . qed ultimately show ?thesis by (auto simp only: real_le_mult_imp_div_pos_le) qed theorem aux4: "0 <= x ==> x <= 1 ==> exp (x - x^2) <= 1 + x" proof - assume a: "0 <= x" and b: "x <= 1" have "exp (x - x^2) = exp x / exp (x^2)" by (rule exp_diff) also have "... <= (1 + x + x^2) / exp (x ^2)" proof (intro real_div_pos_le_mono) from a b show "exp x <= (1::real) + x + x ^ 2" by (rule exp_bound) then show "0 < exp (x^2)" by auto qed also have "... <= (1 + x + x^2) / (1 + x^2)" proof (intro real_pos_div_le_mono) show "(0::real) < (1::real) + x^2" by (rule real_gt_zero_plus_ge_zero_is_gt_zero, auto simp add: a) next show "(1::real) + x ^ 2 <= exp (x ^ 2)" by auto next show "(0::real) <= (1::real) + x + x ^ 2" apply (rule real_le_add_order)+ by (auto simp add: a) qed also from a b have "... <= 1 + x" by (rule aux3) finally show ?thesis . qed theorem ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> x - x^2 <= ln (1 + x)" proof - assume a: "0 <= x" and b: "x <= 1" then have "exp (x - x^2) <= 1 + x" by (rule aux4) also have "... = exp (ln (1 + x))" proof - from a have "0 < 1 + x" by auto thus ?thesis by (auto simp only: exp_ln_iff [THEN sym]) qed finally have "exp (x - x ^ 2) <= exp (ln (1 + x))" . thus ?thesis by (auto simp only: exp_le_cancel_iff) qed (******************************************************************) (* *) (* Bounds for ln (1 + x), for x negative and small *) (* *) (******************************************************************) subsection {* Bounds for ln (1 + x), for x negative and small *} lemma ln_one_plus_neg_upper_bound: "0 <= x ==> x < 1 ==> ln (1 - x) <= - x" proof - assume a: "0 <= (x::real)" and b: "x < 1" have "(1 - x) * (1 + x + x^2) = (1 - x^3)" by (simp add: right_distrib left_distrib diff_minus realpow_two2 real_x_times_x_squared); also have "... <= 1" by (auto intro: zero_le_power simp add: a) finally have "(1 - x) * (1 + x + x ^ 2) <= 1" . moreover have "0 < 1 + x + x^2" apply (rule real_gt_zero_plus_ge_zero_is_gt_zero)+ by (auto simp add: a) ultimately have "1 - x <= 1 / (1 + x + x^2)" by (intro real_mult_le_imp_le_div_pos) also have "... <= 1 / exp x" apply (rule real_one_div_le_anti_mono) apply auto apply (rule exp_bound, rule a) by (rule order_less_imp_le, rule b) also have "... = exp (-x)" by (auto simp add: exp_minus real_divide_def) finally have "1 - x <= exp (- x)" . also have "1 - x = exp (ln (1 - x))" proof - have "0 < 1 - x" by (auto simp add: b) thus ?thesis by (auto simp only: exp_ln_iff [THEN sym]) qed finally have "exp (ln (1 - x)) <= exp (- x)" . thus ?thesis by (auto simp only: exp_le_cancel_iff) qed lemma aux5: "x < 1 ==> ln(1 - x) = -ln(1 + x / (1 - x))" proof - assume a: "x < 1" have "ln(1 - x) = - ln(1 / (1 - x))" proof - have "ln(1 - x) = - (- ln (1 - x))" by auto also have "- ln(1 - x) = ln 1 - ln(1 - x)" by simp also have "... = ln(1 / (1 - x))" apply (rule ln_div [THEN sym]) by (auto simp add: a) finally show ?thesis . qed also have "1/ (1 - x) = 1 + x / (1 - x)" proof - have "1 = 1 - x + x" by simp then have "1/ (1 - x) = (1 - x + x) / (1 - x)" by auto also have "... = (1 - x) / (1 - x) + x / (1 - x)" by (rule add_divide_distrib) also have "... = 1 + x / (1-x)" apply (subst add_right_cancel); apply (simp); apply (rule less_imp_neq, assumption); done; finally show ?thesis . qed finally show ?thesis . qed lemma ln_one_plus_neg_lower_bound: "0 <= x ==> x <= (1 / 2) ==> x < 1 ==> - x - 2 * x^2 <= ln (1 - x)" proof - assume a: "0 <= x" and b: "x <= (1 / 2)" from b have c: "x < 1" by auto then have "ln (1 - x) = - ln (1 + x / (1 - x))" by (rule aux5) also have "- (x / (1 - x)) <= ..." proof - have "ln (1 + x / (1 - x)) <= x / (1 - x)" apply (rule ln_add_one_self_le_self) apply (rule real_ge_zero_div_gt_zero) by (auto simp add: a c) thus ?thesis by auto qed also have "- (x / (1 - x)) = -x / (1 - x)" by auto finally have d: "- x / (1 - x) <= ln (1 - x)" . have e: "-x - 2* x^2 <= - x / (1 - x)" proof - have "(1 - x)* (-x - 2* x^2) <= -x" apply (simp add: right_distrib left_distrib realpow_two2 real_x_times_x_squared diff_minus); proof - have "x * (2 * x^2) = (x * 2) * x^2" by auto also have "... <= x^2" proof - from b have "x * 2 <= (1 / 2) * 2" by auto also have "... = 1" by auto finally have "x * 2 <= 1" . hence "x * 2 * x^2 <= 1 * x^2" apply (rule mult_right_mono); by (rule zero_le_power, rule a) thus "x * 2 * x^2 <= x^2" by simp qed finally show "x * (2 * x ^ 2) <= x ^ 2" . qed thus ?thesis by (intro real_le_mult_imp_le_div_pos2, auto simp add: c) qed from e d show "- x - 2 * x^2 <= ln (1 - x)" by (rule real_le_trans) qed (******************************************************************) (* *) (* The derivative of ln *) (* *) (******************************************************************) subsection {* The derivative of ln *} lemma aux6: assumes a: "(h::real) ~= 0" and b: "x ~= 0" shows "(h / x - (h / x)^2) / h - 1 / x = - h / x^2" proof - from b have c: "h / x = (h * x) / (x * x)" by (simp add: real_mult_div_cancel2) have d: "(h / x)^2 = (h * h) / (x * x)" by (simp add: realpow_two2 [THEN sym]) from c d have "h / x - (h / x)^2 = (h * x - h * h) / (x * x)" by (simp add: real_minus_divide_distrib) also have "... / h = ((h * x - h * h) / h) / (x * x)" by simp also have "h * x - h * h = h * (x - h)" by (simp add: right_diff_distrib); also have "h * (x - h) / h = x - h" by (simp add: a) finally have "(h / x - (h / x) ^ 2) / h = (x - h) / (x * x)" . then have "(h / x - (h / x) ^ 2) / h - 1 / x = (x - h) / (x * x) - 1 / x" by simp also have "... = (x - h) / (x * x) - x / (x * x)" by (simp add: b) also have "... = ((x - h) - x) / (x * x)" by (rule diff_divide_distrib [THEN sym]) also have "(x - h) - x = -h" by simp finally show ?thesis by (simp add: realpow_two2) qed lemma aux7: assumes a: "(h::real) ~= 0" and b: "x ~= 0" shows "(h / x - 2 * (h / x)^2) / h - 1 / x = - 2 * h / x^2" proof - from b have c: "h / x = (h * x) / (x * x)" by (simp add: real_mult_div_cancel2) have "(h/x)^2 = (h * h) / (x * x)" by (simp add: realpow_two2 [THEN sym]) then have "2 * (h / x)^2 = 2 * (h * h) / (x * x)" by simp also have "... = (2 * h * h) / (x * x)" by (simp add: real_divide_def) finally have d: "2 * (h / x) ^ 2 = 2 * h * h / (x * x)" . from c d have "h / x - 2 * (h / x)^2 = (h * x - 2 * h * h) / (x * x)" by (simp add: real_minus_divide_distrib) also have "... / h = ((h * x - 2* h * h) / h) / (x * x)" by simp also have "h * x - 2 * h * h = h * (x - 2 * h)" by (simp add: right_diff_distrib); also have "... / h = x - 2 * h" by (simp add: a) finally have "(h / x - 2 * (h / x) ^ 2) / h = (x - 2 * h) / (x * x)" . then have "(h / x - 2 * (h / x) ^ 2) / h - 1 / x = (x - 2 * h) / (x * x) - 1 / x" by simp also have "... = (x - 2 * h) / (x * x) - x / (x * x)" by (simp add: b) also have "... = (x - 2 * h - x) / (x * x)" by (rule real_minus_divide_distrib [THEN sym]) also have "x - 2 * h - x = (- 2 * h)" by simp also have "x * x = x^2" by (simp add: realpow_two2) finally show ?thesis . qed (* Note: adding the following to the simplifier eliminates the need insert it explicitly in at least one instance below. Should it be added? What else would simplify the calculations above and below? lemma [simp]: "0 < (h::real) ==> h ~= 0" by auto *) lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x" apply (unfold deriv_def, unfold LIM_def, clarsimp) apply (rename_tac epsilon) apply (rule_tac x = "min (min (epsilon * x^2 / 2) (x / 2)) (1/2)" in exI) apply (rule conjI) apply (force simp add: real_mult_order) apply (clarify) apply (rename_tac epsilon h) apply (simp only: abs_interval_iff min_less_iff_conj); apply (subgoal_tac "ln(x + h) + - ln x = ln(1 + h / x)") apply (clarsimp); (*simp add: abs_interval_iff) thm abs_interval_iff; *) apply (case_tac "0 < (h::real)") proof - fix epsilon fix h assume "0 < (epsilon::real)" and u1: "0 < (h::real)" and u2: "h * 2 < x" and u3: "h * 2 < epsilon * x^2" and u4: "h * 2 < 1" show "- epsilon < ln (1 + h / x) / h + - (1 / x) & ln (1 + h / x) / h + - (1 / x) < epsilon" proof from u1 have v1: "h ~= 0" by auto from u1 have v2: "0 <= h" by auto from u1 u2 have v3: "h < x" by auto from v3 have v4: "h <= x" by auto from u1 v3 have v5: "0 < x" by auto then have v6: "0 <= x" by auto from v5 have v7: "x ~= 0" by auto from v2 v5 have v8: "0 <= (h / x)" by (rule real_ge_zero_div_gt_zero) from v4 v5 have v9: "(h / x) <= 1" by (auto simp add: pos_divide_le_eq) from u3 v2 have v10: "h < epsilon * x^2" by auto show "- epsilon < ln (1 + h / x) / h + - (1 / x)" proof - have "(h / x) - (h / x)^2 <= ln (1 + h / x)" apply (rule ln_one_plus_pos_lower_bound) by (auto simp add: real_0_le_divide_iff v6 v2 v9) then have "((h / x) - (h / x)^2) / h <= (ln (1 + h / x)) / h" apply (rule real_div_pos_le_mono) by (rule u1) then have "((h / x) - (h / x)^2) / h - 1 / x <= (ln (1 + h / x)) / h - 1 / x" by auto also have "((h / x) - (h / x)^2) / h - 1 / x = - h / x^2" by (rule aux6, rule v1, rule v7) also have "ln (1 + h / x) / h - 1 / x = ln (1 + h / x) / h + - (1 / x)" by simp finally have v11: "- h / x ^ 2 <= ln (1 + h / x) / h + - (1 / x)" . have "h / x^2 < epsilon" proof - from v5 have "0 < x^2" by (rule zero_less_power); thus ?thesis by (simp only: pos_divide_less_eq v10) qed then have v12: "-epsilon < - h / x^2" by auto from v12 v11 show ?thesis by (rule order_less_le_trans) qed show "ln (1 + h / x) / h + - (1 / x) < epsilon" proof - have "ln (1 + h / x) <= h / x" by (rule ln_add_one_self_le_self, rule v8) then have "ln (1 + h / x) / h <= (h / x) / h" by (intro real_div_pos_le_mono, assumption) also have "... = 1 / x" by (auto simp add: v1) finally have "ln (1 + h / x) / h <= 1 / x" . then have "ln (1 + h / x) / h + - (1 / x) <= 1 / x + - (1 / x)" by auto also have "... = 0" by auto also have "0 < epsilon" by assumption finally show ?thesis . qed qed next fix epsilon fix h assume b1: "0 < epsilon" and b2: "h ~= 0" and b3: "~ 0 < h" and b4: "- (1/2) < h" and b5: "- (epsilon * x ^ 2 / 2) < h" and b6: "- (x / 2) < h" show "- epsilon < ln (1 + h / x) / h + - (1 / x) & ln (1 + h / x) / h + - (1 / x) < epsilon" proof from b1 have b22: "-epsilon < 0" by auto from b2 b3 have b7: "h < 0" by auto from b7 have b8: "h <= 0" by auto from b7 have b16: "h ~= 0" by auto from b6 b7 have b9: "0 < x" by auto then have b18: "0 <= x" by auto from b9 have b15: "x ~= 0" by auto from b6 b7 have b10: "- x < h" by auto from b7 b9 have "h / x < 0" by (simp add: divide_less_eq) then have b20: "h / x <= 0" by simp have b11: "- 1 < h * 2 / x" proof - from b6 have "- (x / 2) * 2 < h * 2" by auto also have "- (x / 2) * 2 = - 1 * x" by auto finally have "- 1 * x < h * 2" . then show ?thesis apply (intro real_mult_less_imp_less_div_pos) by (rule b9) qed then have b12: "-1 <= h * 2 / x" by (simp add: order_less_imp_le) from b10 have "-1 * x < h" by simp then have b13: "- 1 < h / x" apply (intro real_mult_less_imp_less_div_pos) by (rule b9, simp) then have b14: "- 1 <= h / x" by (simp add: order_less_imp_le) from b13 have b13b: "-1 < h / x" by simp from b13 have b21: "- h / x < 1" by auto have b17: "- 2 * h / x^2 < epsilon" proof - from b5 have "- 2 * h < - 2 * - (epsilon * x ^ 2 / 2)" by auto also have "... = epsilon * x^2" by simp finally have "- 2 * h < epsilon * x ^ 2" . then show ?thesis apply (subst pos_divide_less_eq); apply (rule zero_less_power, rule b9, assumption); done; qed show "- epsilon < ln (1 + h / x) / h + - (1 / x)" proof - have "ln (1 - (- h / x)) <= - (- h / x)" apply (rule ln_one_plus_neg_upper_bound) by (simp add: b20, rule b21) also have "ln (1 - (- h / x)) = ln (1 + h / x)" by simp also have "- (- h / x) = h / x" by simp finally have "ln (1 + h / x) <= h / x" . then have "(h / x) / h <= ln (1 + h / x) / h" apply (rule real_div_neg_le_anti_mono) by (rule b7) also have "(h / x) / h = 1 / x" by (simp add: b16) finally have "1 / x <= ln (1 + h / x) / h" . then have "1 / x + - (1 / x) <= ln (1 + h / x) / h + - (1 / x)" by auto then have "0 <= ln (1 + h / x) / h + - (1 / x)" by simp with b22 show ?thesis by (rule order_less_le_trans) qed show "ln (1 + h / x) / h + - (1 / x) < epsilon" proof - have "- (- h / x) - 2 * (- h / x)^2 <= ln (1 - (- h / x))" apply (rule ln_one_plus_neg_lower_bound) by (auto simp add: b18 b4 b6 b8 b9 divide_le_0_iff b12 b13b) also have "- (- h / x) - 2 * (- h / x)^2 = ((h / x) - 2 * (h / x)^2)" by (simp add: real_neg_squared_eq_pos_squared) also have "ln (1 - - h / x) = ln (1 + h / x)" by simp finally have "h / x - 2 * (h / x) ^ 2 <= ln (1 + h / x)" . then have "ln (1 + h / x) / h <= (h / x - 2 * (h / x) ^ 2) / h" apply (intro real_div_neg_le_anti_mono) by (assumption, rule b7) then have "ln (1 + h / x) / h - 1 / x <= (h / x - 2 * (h / x) ^ 2) / h - 1 / x" by auto also have "... = - 2 * h / x^2" by (rule aux7, rule b16, rule b15) finally have "ln (1 + h / x) / h - 1 / x <= - 2 * h / x ^ 2" . also have "... < epsilon" by (rule b17) finally show ?thesis by simp qed qed next fix epsilon fix h assume c1: "(0::real) < x" assume c2: "h ~= (0::real)" (* assume c3: "abs h < min (min (epsilon * x ^ 2 / 2) (x / 2)) (1 / 2)" *) assume c3: "((- (epsilon * x ^ 2 / 2) < h & h < epsilon * x ^ 2 / 2) & - (x / 2) < h & h < x / 2) & - (1 / 2) < h & h < 1 / 2"; show "ln (x + h) + - ln x = ln (1 + h / x)" proof - from c1 have c4: "x ~= 0" by simp have "ln (x + h) + - ln x = ln (x + h) - ln x" by simp also have "... = ln ((x + h) / x)" apply (rule ln_div [THEN sym]) apply (auto simp add: prems) proof - have "- x < -(x / 2)"; by auto; also from c3 have "- (x / 2) < h"; by auto finally show "- x < h";.; qed also have "(x + h) / x = x / x + h / x" by (rule add_divide_distrib) also have "... = 1 + h / x" by (simp add: c4) finally show ?thesis . qed qed lemma abs_ln_one_plus_pos_minus_x_bound: "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= abs(x^2)"; proof -; assume "0 <= x"; assume "x <= 1"; have "ln (1 + x) <= x"; by (rule ln_add_one_self_le_self); then have "ln (1 + x) - x <= 0"; by simp; then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"; by (rule abs_nonpos); also have "... = x - ln (1 + x)"; by simp; also have "... <= x^2"; proof -; from prems have "x - x^2 <= ln (1 + x)"; by (intro ln_one_plus_pos_lower_bound); thus ?thesis; by simp; qed; also have "... = abs(x^2)"; by simp; finally show ?thesis;.; qed; end

lemma exp_first_two_terms:

exp x = 1 + x + suminf (%n. inverse (real (fact (n + 2))) * x ^ (n + 2))

lemma exp_tail_after_first_two_terms_summable:

summable (%n. inverse (real (fact (n + 2))) * x ^ (n + 2))

lemma

[| 0 ≤ x; x ≤ 1 |] ==> inverse (real (fact (n + 2))) * x ^ (n + 2) ≤ x² / 2 * (1 / 2) ^ n

lemma aux2:

(%n. x² / 2 * (1 / 2) ^ n) sums x²

lemma exp_bound:

[| 0 ≤ x; x ≤ 1 |] ==> exp x ≤ 1 + x + x²

lemma

[| 0 ≤ x; x ≤ 1 |] ==> (1 + x + x²) / (1 + x²) ≤ 1 + x

theorem aux4:

[| 0 ≤ x; x ≤ 1 |] ==> exp (x - x²) ≤ 1 + x

theorem ln_one_plus_pos_lower_bound:

[| 0 ≤ x; x ≤ 1 |] ==> x - x² ≤ ln (1 + x)

lemma ln_one_plus_neg_upper_bound:

[| 0 ≤ x; x < 1 |] ==> ln (1 - x) ≤ - x

lemma aux5:

x < 1 ==> ln (1 - x) = - ln (1 + x / (1 - x))

lemma ln_one_plus_neg_lower_bound:

[| 0 ≤ x; x ≤ 1 / 2; x < 1 |] ==> - x - 2 * x² ≤ ln (1 - x)

lemma

[| h ≠ 0; x ≠ 0 |] ==> (h / x - (h / x)²) / h - 1 / x = - h / x²

lemma

[| h ≠ 0; x ≠ 0 |] ==> (h / x - 2 * (h / x)²) / h - 1 / x = - 2 * h / x²

lemma DERIV_ln:

0 < x ==> DERIV ln x :> 1 / x

lemma abs_ln_one_plus_pos_minus_x_bound:

[| 0 ≤ x; x ≤ 1 |] ==> ¦ln (1 + x) - x¦ ≤ ¦x²¦