Theory Ln

(*  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