Theory LnSum3

(*  Title:      LnSum3.thy
    Author:     Kevin Donnelly and Jeremy Avigad
*)

header {* Identities involving sums and ln, part 3 *}

theory LnSum3 = LnSum2:;

lemma lndivxsum_minus: "sumr 0 (Suc n) (%m. ln ((real (Suc n)) / (real (Suc m))))
      = sumr 0 (Suc n) (%m. ln (real (Suc n))) - sumr 0 (Suc n) (%m. ln (real (Suc m)))";
proof -;
  have "0 < real (Suc n)";
    by (simp add: real_of_nat_ge_zero);
  moreover have "0 < real (Suc m)"
    by (simp add: real_of_nat_ge_zero);
  ultimately have "(%m. ln (real (Suc n) / real (Suc m))) = 
      (%m. ln (real (Suc n)) - ln(real (Suc m)))";
    by(simp add: ext ln_div);
  then have "sumr 0 (Suc n) (%m. ln ((real (Suc n)) / (real (Suc m)))) =
          sumr 0 (Suc n) (%m. ln (real (Suc n)) - ln(real (Suc m)))";
    by simp;
  also have "sumr 0 (Suc n) (%m. ln (real (Suc n)) - ln(real (Suc m))) =
           sumr 0 (Suc n) (%m. ln (real (Suc n))) - sumr 0 (Suc n) (%m. ln (real (Suc m)))";
    by(simp only: sumr_diff[THEN sym]);
  finally show ?thesis;.;
qed;

lemma lndivxsum_minus2: "sumr 0 (Suc n) (%m. ln ((real (Suc n)) / (real (Suc m)))) =
      (real (Suc n)) * (ln (real (Suc n))) - (sumr 0 (Suc n) (%m. ln (real (Suc m))))";
proof -;
  have "sumr 0 (Suc n) (%m. ln (real (Suc n))) = real (Suc n) * ln (real (Suc n))";      
    by (rule sumr_const);
  then show "sumr 0 (Suc n) (%m. ln ((real (Suc n)) / (real (Suc m)))) =
     (real (Suc n)) * (ln (real (Suc n))) - (sumr 0 (Suc n) (%m. ln (real (Suc m))))";
    apply(insert lndivxsum_minus[of n]);
    by(auto simp add: lndivxsum_minus simp del: sumr.simps);
qed;

lemma lndivxsum_eq_x_bigo_ln: "(%n. sumr 0 (Suc n) (%m. ln ((real (Suc n)) / (real (Suc m))))) :
  (%n. real n) +o O(%n. ln (real (Suc n)))";
proof -;
  have 1: "(%n. sumr 0 (Suc n) (%m. ln (real (Suc n) / real (Suc m)))) =
      (%n. (real (Suc n)) * (ln (real (Suc n)))) - (%n. (sumr 0 (Suc n) (%m. ln (real (Suc m)))))";
    apply(simp add: lndivxsum_minus2 del: sumr.simps);
    by(simp add: ext func_diff_minus);
  moreover have 2: "(%m. sumr 0 (Suc m)  (%n. (ln (real (Suc n))))) \<elteqo> 
  ((%m. ((real (m + 1)) * (ln (real (m + 1))))) - (%m. (real m))) +o 
  O(%n::nat. ln (real (n + 1)))" by(rule fn_lnx_sum_bigo_ln2);
  ultimately; have "(%n. sumr 0 (Suc n) (%m. ln (real (Suc n) / real (Suc m)))) :
       ((%n. (real (Suc n)) * (ln (real (Suc n)))) - (((%m. ((real (m + 1)) * (ln (real (m + 1))))) - (%m. (real m))))) +o O(%n::nat. ln (real (n + 1)))";
    apply(simp (no_asm_use));
    apply(erule bigo_minus_cong2);
    by(simp);                             
  moreover have "((%n. (real (Suc n)) * (ln (real (Suc n)))) - (((%m. ((real (m + 1)) * (ln (real (m + 1))))) - (%m. (real m))))) = (%m. (real m))";                                        
    apply(rule ext);
    by(simp add: func_diff_minus func_plus);
  ultimately show ?thesis;
    by(auto);
qed;
                              
lemma ln_sq_sum: "ln (real (Suc n)) * (ln (real (Suc n))) = sumr 0 n 
  (%i. ln (real (Suc (Suc i))) * (ln (real (Suc (Suc i)))) -
  ln (real (Suc i)) * (ln (real (Suc i))))";
apply(induct_tac n);
by(auto);

lemma ln_sq_diff_factor: "ln (real (Suc (Suc i))) * (ln (real (Suc (Suc i)))) -
  ln (real (Suc i)) * (ln (real (Suc i))) =
  (ln (real (Suc (Suc i))) - ln (real (Suc i))) * 
  (ln (real (Suc (Suc i))) + ln (real (Suc i)))";
  by (auto simp add: ring_eq_simps);

lemma ln_factor_minus_1: "ln (real (Suc (Suc i))) - ln (real (Suc i)) =
  ln (1 + 1 / (real (Suc i)))";
proof -;
  have "ln (real (Suc (Suc i))) - ln (real (Suc i)) = ln (real (Suc (Suc i)) /
    real (Suc i))";
    by(auto simp add: ln_div);
  also have "... = ln ((real (Suc i)) / (real (Suc i)) + 1 / real (Suc i))";
    apply (subgoal_tac "real(Suc (Suc i)) = real(Suc i) + 1"); 
    apply (erule ssubst);
    apply (simp only: add_divide_distrib [THEN sym]);
    apply simp;
    done;
  also have "... = ln (1 + 1 / (real (Suc i)))" by simp;
  finally show ?thesis;.;
qed;

lemma ln_factor_minus_lbound: "1 / (real (Suc i)) - 1 / (real (Suc i)) * (1 / (real (Suc i))) <= ln (real (Suc (Suc i))) - ln (real (Suc i))";
apply(subst ln_factor_minus_1);
apply(rule ln_approx_lower);
apply(auto simp add: real_divide_def);
apply(subgoal_tac "1 = inverse 1",erule ssubst);
apply(rule real_inverse_le_swap);
by(auto simp add: real_of_nat_Suc);

lemma ln_factor_minus_ubound: "ln (real (Suc (Suc i))) - ln (real (Suc i)) <= 1 / (real (Suc i))";
apply(subst ln_factor_minus_1);
apply(rule ln_approx_upper);
apply(auto simp add: real_divide_def);
apply(subgoal_tac "1 = inverse 1",erule ssubst);
apply(rule real_inverse_le_swap);
by(auto simp add: real_of_nat_Suc);

lemma ln_factor_plus_lbound: "2 * ln (real (Suc i)) <= (ln (real (Suc (Suc i))) + ln (real (Suc i)))";
by(auto);

lemma ln_factor_plus_ubound: "(ln (real (Suc (Suc i))) + ln (real (Suc i))) <= 2 * ln (real (Suc i)) + 1 / (real (Suc i))";
proof -;
  have "ln (real (Suc (Suc i))) + ln (real (Suc i)) = 2 * ln (real (Suc i)) + (ln (real (Suc (Suc i))) - ln (real (Suc i)))";
    by(auto);
  also have "2 * ln (real (Suc i)) + (ln (real (Suc (Suc i))) - ln (real (Suc i))) <=
    2 * ln (real (Suc i)) + 1 / (real (Suc i))";
    apply (rule add_left_mono);
    by(simp only: ln_factor_minus_ubound);
  finally show ?thesis;.;
qed;

lemma ln_sq_diff_lbound: "2 * ln (real (Suc i)) / (real (Suc i)) -  
  2 * ln (real (Suc i)) / (real (Suc i)) * (1 / (real (Suc i))) <= 
  ln (real (Suc (Suc i))) * (ln (real (Suc (Suc i)))) - 
  ln (real (Suc i)) * (ln (real (Suc i)))";
proof -;
  have " 2 * ln (real (Suc i)) / real (Suc i) -
    2 * ln (real (Suc i)) / real (Suc i) * (1 / real (Suc i)) = 
    2 * ln (real (Suc i)) * (1 / (real (Suc i)) - 1 / (real (Suc i)) * (1 / (real (Suc i))))"; by(auto simp add: ring_eq_simps);
  also have "... <= (ln (real (Suc (Suc i))) + ln (real (Suc i))) *
       (ln (real (Suc (Suc i))) - ln (real (Suc i)))";
    apply (rule mult_mono);
    apply simp;
    apply (rule ln_factor_minus_lbound);
    apply (rule nonneg_plus_nonneg);
    apply auto;
    apply (rule real_one_div_le_anti_mono);
    apply auto;
    apply (subgoal_tac "1 * real(Suc i) <= real(Suc i) * real(Suc i)");
    apply simp;
    apply (rule mult_right_mono);
    apply simp;
    apply simp;
    done;
  also have "... = (ln (real (Suc (Suc i))) - ln (real (Suc i))) *
       (ln (real (Suc (Suc i))) + ln (real (Suc i)))"; by simp;
  finally show ?thesis;
    apply(subst ln_sq_diff_factor);.;
qed;

lemma ln_sq_diff_ubound: "ln (real (Suc (Suc i))) * (ln (real (Suc (Suc i)))) - 
  ln (real (Suc i)) * (ln (real (Suc i))) <= 2 * ln (real (Suc i)) / (real (Suc i)) + 1 / (real (Suc i) * (real (Suc i)))";
proof -;
  have "ln (real (Suc (Suc i))) * ln (real (Suc (Suc i))) -
    ln (real (Suc i)) * ln (real (Suc i)) =
    (ln (real (Suc (Suc i))) - ln (real (Suc i))) * 
    (ln (real (Suc (Suc i))) + ln (real (Suc i)))";
    by(simp add: ln_sq_diff_factor);
  also have "... <= 1 / (real (Suc i)) * (2 * ln (real (Suc i)) + 1 / (real (Suc i)))";
    apply(rule mult_mono);
    apply (rule ln_factor_minus_ubound);
    apply (rule ln_factor_plus_ubound);
    apply force;
    apply (subst ln_mult [THEN sym]);
    apply auto;
    apply (rule ln_ge_zero);
    apply(subgoal_tac "1 = 1 * (1::real)", erule ssubst);
    apply(rule mult_mono);
    apply auto;
    done;
  also have "... = 2 * ln (real (Suc i)) / (real (Suc i)) + 1 / (real (Suc i) * (real (Suc i)))";                                       
    by(simp add: ring_eq_simps);
  finally show ?thesis;.;
qed;

lemma ln_sq_diff_all_bounds: "ALL n. (%i. 2 * ln (real (Suc i)) / (real (Suc i)) -  
  2 * ((ln (real (Suc i)) + 1) / (real (Suc i)) * (1 / (real (Suc i))))) n <= 
  (%i. ln (real (Suc (Suc i))) * (ln (real (Suc (Suc i)))) - 
  ln (real (Suc i)) * (ln (real (Suc i)))) n & (%i. ln (real (Suc (Suc i))) * (ln (real (Suc (Suc i)))) - 
  ln (real (Suc i)) * (ln (real (Suc i)))) n <= (%i. 2 * ln (real (Suc i)) / (real (Suc i)) -  
  2 * ((ln (real (Suc i)) + 1) / (real (Suc i)) * (1 / (real (Suc i))))) n + (%i. 3 * ((ln (real (Suc i)) + 1) / (real (Suc i)) * (1 / (real (Suc i))))) n";
apply(rule allI);
apply(rule conjI);
apply(subgoal_tac " 2 * ln (real (Suc n)) / real (Suc n) -
         2 * ((ln (real (Suc n)) + 1)/ real (Suc n) * (1 / real (Suc n)))
         <= 2 * ln (real (Suc n)) / real (Suc n) -
         2 * ln (real (Suc n)) / real (Suc n) * (1 / real (Suc n))");
apply(erule order_trans);
apply(simp only: ln_sq_diff_lbound);
apply(simp add: real_divide_def);
apply(subgoal_tac "2 * ln (real (Suc n)) / real (Suc n) -
            2 * ((ln (real (Suc n)) + 1)/ real (Suc n) * (1 / real (Suc n))) +
            3 * ((ln (real (Suc n)) + 1)/ real (Suc n) * (1 / real (Suc n))) =
      2 * ln (real (Suc n)) / real (Suc n) + ((ln (real (Suc n)) + 1)/ real (Suc n) * (1 / real (Suc n)))", erule ssubst);
apply(subgoal_tac "ln (real (Suc (Suc n))) * (ln (real (Suc (Suc n)))) - 
  ln (real (Suc n)) * (ln (real (Suc n))) <= 2 * ln (real (Suc n)) / (real (Suc n)) + 1 / (real (Suc n) * (real (Suc n)))");
apply(erule order_trans);
apply(simp);
apply(rule real_div_pos_le_mono);
apply force;
apply (rule mult_pos);
apply force;
apply force;
apply (rule ln_sq_diff_ubound);
apply (auto simp add: ring_eq_simps add_divide_distrib [THEN sym]);
done;

(*
declare ring_abs_pos [simp del];
declare ring_abs_neg [simp del];
*)

lemma ln_sq_diff_bigo: "(%i. ln (real (Suc (Suc i))) * (ln (real (Suc (Suc i)))) - 
  ln (real (Suc i)) * (ln (real (Suc i)))) : (%i. 2 * ln (real (Suc i)) / (real (Suc i)) - 2 * ((ln (real (Suc i)) + 1) / (real (Suc i)) * (1 / (real (Suc i))))) +o O(%i. (ln (real (Suc i)) + 1)/ (real (Suc i) * (real (Suc i))))";
proof -;
  have "(%i. ln (real (Suc (Suc i))) * ln (real (Suc (Suc i))) -
     ln (real (Suc i)) * ln (real (Suc i))) :
       (%i. 2 * ln (real (Suc i)) / real (Suc i) -
          2 * ((ln (real (Suc i)) + 1) / real (Suc i) * (1 / real (Suc i)))) +o
         O(%i. 3 * ((ln (real (Suc i)) + 1) / real (Suc i) * (1 / real (Suc i))))";
    apply (rule bigo_bounded3);
    apply (rule ln_sq_diff_all_bounds);
    done;
  also have "O(%i. 3 * ((ln (real (Suc i)) + 1) / real (Suc i) * (1 / real (Suc i)))) =
      O(%i. (ln (real (Suc i)) + 1) / real (Suc i) * (1 / real (Suc i)))";
    apply (rule bigo_const_mult);
    apply simp;
    done;
  also have "... =  O(%i. (ln (real (Suc i)) + 1)/ (real (Suc i) * (real (Suc i))))";
    by simp;
  finally show ?thesis;.;
qed;

(*
declare ring_abs_pos [simp];
declare ring_abs_neg [simp];
*)

lemma ln_sq_diff_bigo_subset: "(%i. 2 * ln (real (Suc i)) / (real (Suc i)) - 2 * ((ln (real (Suc i)) + 1) / (real (Suc i)) * (1 / (real (Suc i))))) +o O(%i. (ln (real (Suc i)) + 1)/ (real (Suc i) * (real (Suc i)))) <= (%i. 2 * ln (real (Suc i)) / (real (Suc i))) +o O(%i. (ln (real (Suc i)) + 1)/ (real (Suc i) * (real (Suc i))))";
apply(simp add: bigo_def elt_set_plus_def func_plus);
apply(clarify);
apply(rule_tac x = "(%x. (- 2) * (ln (real (Suc x)) + 1) /
                   (real (Suc x) * real (Suc x)) +
                   b x)" in exI);
apply(rule conjI);
apply(rule_tac x = "2 + c" in exI);
apply(rule allI);
apply(simp only: abs_mult left_distrib);
apply(subgoal_tac "abs ((- 2) * (ln (real (Suc xa)) + 1) /
                (real (Suc xa) * real (Suc xa)) +
                b xa) <=
  abs ((- 2) * (ln (real (Suc xa)) + 1) /
                (real (Suc xa) * real (Suc xa))) + abs (
                b xa)");
apply(erule order_trans);
apply(rule add_mono);
apply(simp only: abs_mult mult_assoc real_divide_def);
apply(force);
apply(erule_tac x = xa in allE);
apply(simp);
apply(simp add: abs_triangle_ineq);
apply(rule ext);
apply(simp add: real_divide_def);
apply(simp only: minus_mult_left minus_add_distrib); 
apply simp;
done;

lemma ln_sq_diff_bigo2: "(%i. ln (real (Suc (Suc i))) * (ln (real (Suc (Suc i)))) - 
  ln (real (Suc i)) * (ln (real (Suc i)))) : (%i. 2 * ln (real (Suc i)) / (real (Suc i))) +o O(%i. (ln (real (Suc i)) + 1)/ (real (Suc i) * (real (Suc i))))";
apply(insert ln_sq_diff_bigo_subset);
apply(erule subsetD);
by(simp only: ln_sq_diff_bigo);

lemma ln_sq_sum_bigo: "(%n. ln (real (Suc n)) * (ln (real (Suc n)))) : 
  (%n. 2 * sumr 0 n (%i. ln (real (Suc i)) / (real (Suc i)))) +o
  O(%n. sumr 0 n (%i. (ln (real (Suc i)) + 1)/ (real (Suc i) * (real (Suc i)))))";
apply(subgoal_tac "(%n. 2 *
           sumr 0 n (%i. ln (real (Suc i)) / real (Suc i))) +o
      O(%n. sumr 0 n
             (%i. (ln (real (Suc i)) + 1) /
                  (real (Suc i) * real (Suc i)))) =
       (%n. sumr 0 n (%i. 2 * (ln (real (Suc i)) / real (Suc i)))) +o
      O(%n. sumr 0 n
             (%i. (ln (real (Suc i)) + 1) /
                  (real (Suc i) * real (Suc i))))");
apply(erule ssubst);
apply(subgoal_tac "(%n. ln (real (Suc n)) * ln (real (Suc n))) =
   (%n. sumr 0 n
 (%i. ln (real (Suc (Suc i))) * ln (real (Suc (Suc i))) -
      ln (real (Suc i)) * ln (real (Suc i))))");
apply(erule ssubst);
apply(rule bigo_sumr_pos2);
apply(rule allI);
apply(simp add: real_divide_def);
apply(simp only: order_le_less);
apply(clarify);
apply(rule real_mult_order);
apply(subgoal_tac "0 <= ln (real (Suc n))");
apply arith;
apply (rule ln_ge_zero);
apply force;
apply (rule mult_pos);
apply force;
apply force;
apply(insert ln_sq_diff_bigo2);
apply(simp);
apply(rule ext);
apply(subst ln_sq_sum);
apply(simp);
by(simp only: sumr_mult);

lemma calc2: assumes a: "0 < x"
    shows "ln x - ln (x + 1) = ln (1 - 1 / (x + 1))";
proof -;
  have b: "0 < x + 1"
    by (auto simp only: real_add_order a);
  from a have c: "x ~= 0" by auto;
  from b have d: "x + 1 ~= 0" by auto;
  have "ln x - ln (x + 1) = ln (x / (x + 1))";
    by (rule ln_div [THEN sym], rule a, rule b);
  also have "x / (x + 1) = 1 - 1/(x + 1)";
  proof -;
    have "x = x + 1 - 1";
      by auto;
    then have "x / (x + 1) = (x + 1 - 1) / (x + 1)";
      by simp;
    also have "... = (x + 1) / (x + 1) - 1 / (x + 1)";
      by (rule real_minus_divide_distrib);
    also have "(x + 1) / (x + 1) = 1";
       by (rule divide_self, rule d);
    finally show ?thesis;.;
  qed;
  finally show ?thesis;.;
qed;

lemma calc3: assumes a: "0 < x"
    shows "(ln x / x) - (ln (x + 1) / (x + 1)) =
        ln (1 - (1/(x+1))) / (x + 1) + ln x / (x * (x + 1))";
proof -;
  have b: "0 < x + 1"
    by (auto simp only: real_add_order a);
  from a have c: "x ~= 0" by auto;
  from b have d: "x + 1 ~= 0" by auto;
  have "ln x / x = ((x + 1) * ln x) / ((x + 1) * x)";
    by (subst mult_divide_cancel_left, rule d, rule refl);
  also have "(x + 1) * x = x * (x + 1)";
    by auto;
  finally; have "ln x / x = (x + 1) * ln x / (x * (x + 1))";.;
  then have "ln x / x - (ln (x + 1) / (x + 1)) = 
      (x + 1) * ln x / (x * (x + 1)) - (ln (x + 1) / (x + 1))";
    by simp;
  also have "... = (x + 1) * ln x / (x * (x + 1)) - 
      (x * ln (x + 1) / (x *(x + 1)))";
    by (subst mult_divide_cancel_left, rule c, rule refl);
  also have "... = ((x + 1) * ln x - x * ln(x + 1)) / (x * (x + 1))";
    by (rule real_minus_divide_distrib [THEN sym]);
  also have "(x + 1) * ln x = x * ln x + ln x";
    by (auto simp add: real_add_mult_distrib);
  also; have "x * ln x + ln x - x * ln (x + 1) = 
      x * ln x - x * ln (x + 1) + ln x";
    by simp;
  also have "x * ln x - x * ln (x + 1) = x * (ln x - ln (x + 1))";
    by (rule right_diff_distrib [THEN sym]);
  also have "ln x - ln (x + 1) = ln (1 - 1/(x + 1))";
    by (rule calc2, rule a);
  finally; have "ln x / x - ln (x + 1) / (x + 1) =
      (x * ln (1 - 1 / (x + 1)) + ln x) / (x * (x + 1))";.;
  also have "... = x * ln (1 - 1 / (x + 1)) / (x * (x + 1)) +
      ln x / (x * (x + 1))";
    by (rule add_divide_distrib);
  also; have "x * ln (1 - 1 / (x + 1)) / (x * (x + 1)) =
      ln (1 - 1 / (x + 1)) / (x + 1)";
    by (subst mult_divide_cancel_left, rule c, rule refl);
  finally show ?thesis;.;
qed;

lemma ln_one_minus_small_pos_lower_bound2:
  "0 <= x ==> x <= (1 / 2) ==> - 2 * x <= ln (1 - x)";
proof -;
  assume a: "0 <= (x::real)";
  assume b: "x <= (1 / 2)";
  then have c: "x < 1";
    by auto;
  have d: "2 * x^2 <= x";
  proof -;
    have "x^2 = x * x";
      by (rule realpow_two2 [THEN sym]);
    also have "... <= (1 / 2) * x";
      by (rule mult_right_mono);
    finally have "x^2 <= (1 / 2) * x";.;
    then have "2 * x^2 <= 2 * ((1 / 2) * x)";
      by auto;
    also have "... = x";
      by simp;
    finally show ?thesis;.;
  qed;
  then have "- x - x <= - x - 2 * x^2";
    by auto;
  also have "... <= ln(1 - x)";
    apply (rule ln_one_plus_neg_lower_bound);
    by (rule a, rule b, rule c);
  also have "-x - x = - 2 * x";
    by simp;
  finally show ?thesis;.;
qed;


lemma aux_calc4: "1 <= x ==> - (2 / ((x + 1) * (x + 1))) <= ln (1 - 1 / (x + 1)) / (x + 1)";
apply(insert ln_one_minus_small_pos_lower_bound2[of "1 / (x + 1)"]);
apply(simp);
apply(subgoal_tac "2 / (x + 1) <= 1");
apply(simp);
apply(subgoal_tac "- (2 / ((x + 1) * (x + 1))) = -2 / (x + 1) / (x + 1)");
apply(erule ssubst);
apply(simp only: real_divide_def);
apply(force);
apply (simp add: divide_divide_eq_left nonzero_minus_divide_left);
apply (rule real_le_mult_imp_div_pos_le);
apply arith;
apply simp;
done;

lemma aux_calc4_neg: "1 <= x ==> - (ln (1 - 1 / (x + 1)) / (x + 1)) <= 2 / ((x + 1) * (x + 1))";
  apply(insert aux_calc4[of x]);
  apply simp;
  done;

lemma calc4: "ln (real (Suc n)) / (real (Suc n) * (real (Suc n))) <= 2 * (ln (real (Suc n)) / (real (Suc n)) - (ln (real (Suc (Suc n))) / (real (Suc (Suc n))))) + 4 / (real (Suc (Suc n)) * (real (Suc (Suc n))))";
proof -;
  have "ln (real (Suc n)) / (real (Suc n) * (real (Suc n))) <= 2 * ln (real (Suc n)) / (real (Suc n) * (real (Suc (Suc n))))";
        apply(subgoal_tac "(ln (real (Suc n)) / (real (Suc n) * real (Suc n))
    <= 2 * ln (real (Suc n)) / (real (Suc n) * real (Suc (Suc n)))) =
          ((ln (real (Suc n)) / (real (Suc n) * real (Suc n))) / 2 <=              ln (real (Suc n)) / (real (Suc n) * real (Suc (Suc n))))");  
        apply(erule ssubst);
        apply(simp);
        apply(subgoal_tac "real (Suc (Suc n)) = real (Suc n) + 1");
        apply(erule ssubst);
        apply(simp only: left_distrib real_divide_def);
        apply(rule mult_left_mono);
        apply(rule real_inverse_le_swap);
        apply(simp only: real_of_nat_ge_zero real_of_nat_Suc);
        apply (rule mult_pos);
        apply force;
        apply force;
        apply (subst mult_assoc);
        apply (rule mult_left_mono);
        apply (simp_all);
        apply (subgoal_tac "ln (real (Suc n)) / (real (Suc n) * real (Suc n))
            = 2 * ((ln (real (Suc n)) / (real (Suc n) * real (Suc n) * 2)))");
        apply (erule ssubst);
        apply (subgoal_tac "2 * ln (real (Suc n)) / 
          (real (Suc n) * real (Suc (Suc n))) = 2 * ((ln (real (Suc n)) / 
          (real (Suc n) * real (Suc (Suc n)))))");
        apply (erule ssubst);
        apply (subst mult_le_cancel_left);
        apply auto;
        done;
    also have "... = 2 * (ln (real (Suc n))/(real (Suc n)) - (ln (real (Suc (Suc n))) / (real (Suc (Suc n))))) - 2 * (ln (1 - 1 / (real (Suc (Suc n)))) / (real (Suc (Suc n))))";
      apply(subgoal_tac "ln (real (Suc (Suc n))) / real (Suc (Suc n)) =
        ln (real (Suc n) + 1) / (real (Suc n) + 1)");
      apply(erule ssubst);
      apply(subgoal_tac "ln (real (Suc n)) / real (Suc n) -
         ln (real (Suc n) + 1) / (real (Suc n) + 1) =
         ln (1 - (1/((real (Suc n))+1))) / ((real (Suc n)) + 1) + ln (real (Suc n)) / ((real (Suc n)) * ((real (Suc n)) + 1))");
      apply(erule ssubst);
      apply(simp add: real_of_nat_Suc);
      apply(rule calc3);
      apply(simp add: real_of_nat_ge_zero);
      by(simp add: real_of_nat_Suc);
    also have "... <= 2 * (ln (real (Suc n))/(real (Suc n)) - (ln (real (Suc (Suc n))) / (real (Suc (Suc n))))) + 4 / (real (Suc (Suc n)) * (real (Suc (Suc n))))";
      apply(simp);
      apply(subgoal_tac "- (2 * ln (1 - 1 / real (Suc (Suc n))) / real (Suc (Suc n))) =
        2 * (- (ln (1 - 1 / (real (Suc n) + 1)) / (real (Suc n) + 1)))");
      apply(erule ssubst);
      apply(subgoal_tac "4 / (real (Suc (Suc n)) * real (Suc (Suc n))) =
        2 * (2 / ((real (Suc n) + 1) * (real (Suc n) + 1)))");
      apply(erule ssubst);               
      apply(simp only: real_mult_le_cancel_iff2);
      apply(rule aux_calc4_neg);
      apply(simp add: real_of_nat_Suc);                         
      apply(simp add: real_of_nat_Suc);  
      by(simp add: real_of_nat_Suc);                                                   
    finally;show ?thesis;.;
qed;

lemma aux_bigo_calc[rule_format]: "sumr 0 x (%i. ln (real (Suc i)) / (real (Suc i) * real (Suc i))) <= 8";
proof -;
  have "sumr 0 x (%i. ln (real (Suc i)) / (real (Suc i) * real (Suc i))) <= 
    sumr 0 x (%n. 2 * (ln (real (Suc n)) / (real (Suc n)) - (ln (real (Suc (Suc n))) / (real (Suc (Suc n))))) + 4 / (real (Suc (Suc n)) * (real (Suc (Suc n)))))";
    apply(rule sumr_le2);
    apply(rule allI);    
    apply(simp only: calc4);
    by(simp);
  also have "... <= sumr 0 x (%n. 2 * (ln (real (Suc n)) / (real (Suc n)) - (ln (real (Suc (Suc n))) / (real (Suc (Suc n)))))) + sumr 0 x (%n. 4 / (real (Suc (Suc n)) * (real (Suc (Suc n)))))";
    apply (subst sumr_add);
    apply (rule order_refl);
    done;
  also have "sumr 0 x
         (%n. 2 * (ln (real (Suc n)) / real (Suc n) -
                   ln (real (Suc (Suc n))) / real (Suc (Suc n)))) +
        sumr 0 x (%n. 4 / (real (Suc (Suc n)) * real (Suc (Suc n)))) <= sumr 0 x (%n. 4 / (real (Suc (Suc n)) * real (Suc (Suc n))))";                                   
    apply(simp);

        apply(subgoal_tac "sumr 0 x
          (%n. 2 * ln (real (Suc n)) / real (Suc n) -
          2 * ln (real (Suc (Suc n))) / real (Suc (Suc n))) =
          2 * (ln (real (Suc 0)) / real (Suc 0) - ln (real (Suc x))/ (real (Suc x)))");

    apply(simp add: real_divide_def);
    apply (rule nonneg_times_nonneg);
    apply auto;
    apply(induct_tac x);                                              
    apply(simp);                                                                  
    by(simp (no_asm_simp));
  also have "sumr 0 x (%n. 4 / (real (Suc (Suc n)) * real (Suc (Suc n)))) =
    4 * sumr 0 x (%n. 1 / (real (Suc (Suc n))) * (1 / real (Suc (Suc n))))";
    by(simp add: sumr_mult);
  also have "... <= 4 * sumr 0 x (%n. 1 / (real (Suc n)) * (1 / real (Suc n)))";
    apply(simp);
    apply(rule sumr_le2);            
    apply(rule allI);                                 
    apply(auto simp add: real_divide_def);
    apply (rule mult_mono);
    apply auto;
    done;
  also have "... <= 8";
    apply(insert lnsum_inv_sq_2[of x]);
    apply(simp);                                   
    apply(erule order_trans);                                               
    by(simp add: real_divide_def);
  finally; show "sumr 0 x (%i. ln (real (Suc i)) / (real (Suc i) * real (Suc i))) <= 8";.;
qed;

lemma aux2_bigo_calc[rule_format]: "sumr 0 x (%i. 1 / (real (Suc i) * real (Suc i))) <= 2";
apply(insert lnsum_inv_sq_2[of x]);
apply(simp);
apply(erule order_trans);
by(simp add: real_divide_def);

lemma ln_sq_diff_part_bigo_1: "(%n. sumr 0 n (%i. (ln (real (Suc i)) + 1)/ (real (Suc i) * (real (Suc i))))) : O(%x. 1)";
apply(auto simp add: bigo_def);
apply(rule_tac x = "8 + 2" in exI); 
apply(rule allI);
apply(subgoal_tac "abs (sumr 0 x
               (%i. (ln (real (Suc i)) + 1) /
                    (real (Suc i) * real (Suc i)))) <=
  sumr 0 x (%i. (ln (real (Suc i)))/ (real (Suc i) * real (Suc i))) + 
  sumr 0 x (%i. 1 / (real (Suc i) * real (Suc i)))");
apply(erule order_trans);
apply(subgoal_tac "sumr 0 x (%i. 1 / (real (Suc i) * real (Suc i))) <= 2");
apply(rule add_mono);
apply(rule aux_bigo_calc);
apply(simp);
apply(rule aux2_bigo_calc);
apply(subgoal_tac "0 <= sumr 0 x (%i. (ln (real (Suc i)) + 1) / (real (Suc i) * real (Suc i)))");
apply(auto simp add: real_abs_def);
apply(simp add: sumr_add real_abs_def add_divide_distrib);
apply(rule sumr_ge_zero);
apply(rule allI);
apply(simp add: real_divide_def);
apply(rule nonneg_times_nonneg);
apply(rule nonneg_plus_nonneg);
apply auto;
done;

declare subsetI [rule del, intro];

lemma ln_sq_diff_bigo3: "(%x. sumr 0 x (%i. ln (real (Suc (Suc i))) * (ln (real (Suc (Suc i)))) - 
  ln (real (Suc i)) * (ln (real (Suc i))))) : (%x. sumr 0 x (%i. 2 * ln (real (Suc i)) / (real (Suc i)))) +o O(%x. 1)";
proof -;
  have "(%x. sumr 0 x
          (%i. ln (real (Suc (Suc i))) * ln (real (Suc (Suc i))) -
               ln (real (Suc i)) * ln (real (Suc i))))
    : (%x. sumr 0 x (%i. 2 * ln (real (Suc i)) / real (Suc i))) +o O(%x. sumr 0 x 
    (%i. (ln (real (Suc i)) + 1)/ (real (Suc i) * (real (Suc i)))))";
    apply(rule bigo_sumr_pos2);
    apply(rule allI);                            
    apply(simp add: real_divide_def);
    apply (rule nonneg_times_nonneg);
    apply (rule nonneg_plus_nonneg);
    apply force; apply force; apply force;
    by(simp only: ln_sq_diff_bigo2);
  moreover have "O((%x. sumr 0 x 
    (%i. (ln (real (Suc i)) + 1)/ (real (Suc i) * (real (Suc i)))))) 
      <= O(%x. 1)";
    apply (rule bigo_elt_subset);
    by(simp only: ln_sq_diff_part_bigo_1);
  ultimately have "(%x. sumr 0 x
          (%i. ln (real (Suc (Suc i))) * ln (real (Suc (Suc i))) -
               ln (real (Suc i)) * ln (real (Suc i))))
    : (%x. sumr 0 x (%i. 2 * ln (real (Suc i)) / real (Suc i))) +o O(%x. 1)";
    by (elim set_plus_mono_b);
  then show ?thesis;.;
qed;

lemma lnxdivx_bigo: "(%x. ln (real (Suc x)) * (ln (real (Suc x)))) : 
  (%x. sumr 0 x (%i. 2 * ln (real (Suc i)) / (real (Suc i)))) +o O(%x. 1)";      
apply(insert ln_sq_diff_bigo3);
by(simp only: ln_sq_sum[THEN sym]);

lemma lnxdivx2_bigo: "(%x. ln (real (Suc x)) * (ln (real (Suc x))) / 2) :
  (%x. sumr 0 x (%i. ln (real (Suc i)) / (real (Suc i)))) +o O(%x. 1)";
apply(insert lnxdivx_bigo);
apply(simp add: bigo_def elt_set_plus_def func_plus);
apply(erule exE);
apply(rule_tac x = "(%x. 1 / 2 * b x)" in exI);
apply(clarify);
apply(rule conjI);
apply(rule_tac x = c in exI);
apply(simp);
apply(rule allI);
apply(erule_tac x = x in allE);
apply(subgoal_tac "abs(b x / 2) <= abs(b x)");
apply(erule order_trans);
apply(simp);
apply(simp add: real_abs_def);
apply(rule ext);
apply(simp add: ext);
apply(subgoal_tac "(%x. ln (real (Suc x)) * ln (real (Suc x))) x =
          (%x. sumr 0 x (%i. 2 * ln (real (Suc i)) / real (Suc i)) + b x) x");
apply(simp);
apply(simp only: mult_commute sumr_mult);
apply(rule sumr_fun_eq);
apply(clarify);
apply(simp add: mult_commute);
by(erule ssubst,simp);

lemma lnxdivx_bigo_final: "(%x. sumr 0 x (%i. 2 * ln (real (Suc i)) / (real (Suc i)))) : 
 (%x. ln (real (Suc x)) * (ln (real (Suc x)))) +o O(%x. 1)";
by(simp add: bigo_add_commute lnxdivx_bigo);

end