# Theory LnSum3

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

theory LnSum3 = LnSum2:

```(*  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)";
moreover have "0 < real (Suc m)"
ultimately have "(%m. ln (real (Suc n) / real (Suc m))) =
(%m. ln (real (Suc n)) - ln(real (Suc m)))";
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)))))";
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);
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)))";

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))";
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(subgoal_tac "1 = inverse 1",erule ssubst);
apply(rule real_inverse_le_swap);

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(subgoal_tac "1 = inverse 1",erule ssubst);
apply(rule real_inverse_le_swap);

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))";
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)))";
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)))";
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(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);
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(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(simp only: abs_mult mult_assoc real_divide_def);
apply(force);
apply(erule_tac x = xa in allE);
apply(simp);
apply(rule ext);
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 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";
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))";
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 (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(rule calc3);
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);
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 (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 (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))))";
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 (rule mult_mono);
apply auto;
done;
also have "... <= 8";
apply(insert lnsum_inv_sq_2[of x]);
apply(simp);
apply(erule order_trans);
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);

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(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 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(rule sumr_ge_zero);
apply(rule allI);
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 (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(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(rule 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);
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)";

end
```

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

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

lemma lndivxsum_eq_x_bigo_ln:

```  (%n. sumr 0 (Suc n) (%m. ln (real (Suc n) / real (Suc m))))
∈ real + O(%n. ln (real (Suc n)))```

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

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

lemma ln_factor_minus_1:

`  ln (real (Suc (Suc i))) - ln (real (Suc i)) = ln (1 + 1 / real (Suc i))`

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

lemma ln_factor_minus_ubound:

`  ln (real (Suc (Suc i))) - ln (real (Suc i)) ≤ 1 / real (Suc i)`

lemma ln_factor_plus_lbound:

`  2 * ln (real (Suc i)) ≤ ln (real (Suc (Suc i))) + ln (real (Suc i))`

lemma ln_factor_plus_ubound:

```  ln (real (Suc (Suc i))) + ln (real (Suc i))
≤ 2 * ln (real (Suc i)) + 1 / real (Suc i)```

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

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

lemma ln_sq_diff_all_bounds:

```  ∀n. 2 * ln (real (Suc n)) / real (Suc n) -
2 * ((ln (real (Suc n)) + 1) / real (Suc n) * (1 / real (Suc n)))
≤ ln (real (Suc (Suc n))) * ln (real (Suc (Suc n))) -
ln (real (Suc n)) * ln (real (Suc n)) ∧
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) -
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)))```

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(%i. (ln (real (Suc i)) + 1) / (real (Suc i) * real (Suc i)))```

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(%i. (ln (real (Suc i)) + 1) / (real (Suc i) * real (Suc i)))
⊆ (%i. 2 * ln (real (Suc i)) / real (Suc i)) +
O(%i. (ln (real (Suc i)) + 1) / (real (Suc i) * real (Suc i)))```

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(%i. (ln (real (Suc i)) + 1) / (real (Suc i) * real (Suc i)))```

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(%n. sumr 0 n (%i. (ln (real (Suc i)) + 1) / (real (Suc i) * real (Suc i))))```

lemma

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

lemma

```  0 < x
==> ln x / x - ln (x + 1) / (x + 1) =
ln (1 - 1 / (x + 1)) / (x + 1) + ln x / (x * (x + 1))```

lemma ln_one_minus_small_pos_lower_bound2:

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

lemma aux_calc4:

`  1 ≤ x ==> - (2 / ((x + 1) * (x + 1))) ≤ ln (1 - 1 / (x + 1)) / (x + 1)`

lemma aux_calc4_neg:

`  1 ≤ x ==> - (ln (1 - 1 / (x + 1)) / (x + 1)) ≤ 2 / ((x + 1) * (x + 1))`

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

lemma aux_bigo_calc:

`  sumr 0 x (%i. ln (real (Suc i)) / (real (Suc i) * real (Suc i))) ≤ 8`

lemma aux2_bigo_calc:

`  sumr 0 x (%i. 1 / (real (Suc i) * real (Suc i))) ≤ 2`

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

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(%x. 1)```

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(%x. 1)```

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(%x. 1)```

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(%x. 1)```