# Theory Ln

Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

theory Ln = RealLib:

```(*  Title:      Ln.thy
*)

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"
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)
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"
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"
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"
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)+
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"
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])
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)"
also have "... = 1 + x / (1-x)"
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 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)"
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)"
also have "... / h = ((h * x - h * h) / h) / (x * x)"
by simp
also have "h * x - h * h = h * (x - h)"
also have "h * (x - h) / h = x - h"
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)"
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
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)"
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)"
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)"
also have "... / h = ((h * x - 2* h * h) / h) / (x * x)"
by simp
also have "h * x - 2 * h * h = h * (x - 2 * h)"
also have "... / h = x - 2 * h"
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)"
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 (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);
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"
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"
then have "ln (1 + h / x) / h <= (h / x) / h"
by (intro real_div_pos_le_mono, assumption)
also have "... = 1 / x"
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"
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"
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"
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"
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)"
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])
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"
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";
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

```

### 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))`

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)`

### 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`

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)`

### The derivative of ln

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²¦`