# Theory LnSum4

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

theory LnSum4 = PartialSummation + LnSum3:

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

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

theory LnSum4 = PartialSummation + LnSum3:;

declare subsetI [rule del, intro];

subsection {* Previous identities, rewritten *}

lemma identity_one: "(λn::nat. ln (1 + 1 / (real n + 1))) \<elteqo>
(λn. 1 / (real n + 1)) \<pluso> O(λn. 1 / ((real n) + 1)^2)";
apply (rule set_minus_imp_plus);
apply (simp add: bigo_def func_minus diff_minus func_plus del: abs_nonneg
abs_nonpos);
apply (rule_tac x = 1 in exI);
apply (simp del: abs_nonneg abs_nonpos add: diff_minus [THEN sym]);
apply (rule allI);
apply (subgoal_tac "1 / (real x + 1)^2 = (1 / (real x + 1))^2");
apply (erule ssubst);
apply (rule abs_ln_one_plus_pos_minus_x_bound2);
apply force;
apply (rule real_le_mult_imp_div_pos_le);
apply auto;
apply (rule real_one_over_pow);
apply auto;
done;

lemma identity_two: "(λn. sumr 0 (n+1) (λi. 1/(real i + 1))) \<elteqo>
(λn. ln(real n + 1)) \<pluso> O(λn. 1)";
apply (insert sum_inverse_eq_ln_1);
apply (simp add: real_of_nat_Suc);
proof -;
assume "(λx. sumr 0 x (λi. 1 / (real i + 1)))
∈ (λn. ln (real n + 1)) \<pluso> O(λx. 1)";
then have "(λn. 1 / (real (n::nat) + 1)) +
(λx. sumr 0 x (λi. 1 / (real i + 1))) ∈
(λn. 1 / (real n + 1)) \<pluso> ((λn. ln (real n + 1)) \<pluso>
O(λx. 1))";
by (intro set_plus_intro2);
also have "… = ((λn. 1 / (real n + 1)) + (λn. ln (real n + 1)))
\<pluso> O(λx. 1)";
by (simp add: set_plus_rearranges);
also have "… = ((λn. ln (real n + 1)) + (λn. 1 / (real n + 1))) \<pluso>
O(λx. 1)";
by (simp add: plus_ac0);
also have "… = (λn. ln (real n + 1)) \<pluso> ((λn. 1 / (real n + 1))
\<pluso> O(λx. 1))";
by (simp add: set_plus_rearranges);
also have "… ⊆ (λn. ln (real n + 1)) \<pluso> (O(λx. 1) + O(λx. 1))";
apply (rule set_plus_mono);
apply (rule set_plus_mono4);
apply (simp add: bigo_def);
apply (rule_tac x = 1 in exI);
apply (rule allI);
apply (rule real_le_mult_imp_div_pos_le);
by auto;
also have "… ⊆ (λn. ln (real n + 1)) \<pluso> O(λx. 1)";
apply (rule set_plus_mono);
by (rule bigo_plus_self_subset);
also; have "(λn. 1 / (real n + 1)) +
(λx. sumr 0 x (λi. 1 / (real i + 1))) =
(λn. sumr 0 n (λi. 1 / (real i + 1)) + 1 / (real n + 1))";
by (simp add: func_plus plus_ac0);
finally; show "(λu. sumr 0 u (λi. 1 / (real i + 1)) +
1 / (real u + 1)) ∈ (λn. ln (real n + 1)) \<pluso> O(λx. 1)";.;
qed;

lemma identity_three:
"(λn. sumr 0 (n+1) (λi. ln(real i + 1))) \<elteqo>
((λn. (real n + 1) * ln(real n + 1)) - (λn. real n)) \<pluso>
O(λn. ln (real n + 1))";
apply (insert fn_lnx_sum_bigo_ln2);
by (simp add: real_of_nat_Suc);

lemma identity_four:
"(λn. sumr 0 n (λi. ln(real i+1)/(real i + 1))) \<elteqo>
(λn. (ln (real n+1))^2 / 2) \<pluso> O(λn. 1)";
apply (insert lnxdivx_bigo_final);
apply (simp add: real_of_nat_Suc realpow_two2);
apply (drule_tac a = "λn. 1 / 2" in set_times_intro2);
apply (simp add: func_times);
apply (subgoal_tac "(λx. sumr 0 x (λi. 2 * ln (real i + 1) / (real i + 1)) / 2) = (λn. sumr 0 n (λi. ln (real i + 1) / (real i + 1)))");
prefer 2;
apply (rule ext);
apply (induct_tac x);
apply simp;
apply (simp add: mult_ac);
apply (simp);
apply (rule set_mp);
prefer 2;
apply assumption;
apply (subgoal_tac "(λn. 1 / 2) \<timeso> ((λx. (ln (real x + 1))²) \<pluso> O(λx. 1)) ⊆ (λn. (ln (real n + 1))² / 2) \<pluso> O(λn. 1)");
apply force;
apply (subgoal_tac "(λn. 1 / 2) \<timeso> ((λx. (ln (real x + 1))²)
\<pluso> O(λx. 1)) ⊆ ((λn. 1 / 2) * (λx. (ln (real x + 1))^2)) \<pluso>
((λn. 1 / 2) \<timeso> O(λx. 1))");
apply (erule subset_trans)
apply (simp add: func_times);
by (simp add: set_times_plus_distrib);

lemma identity_five: "(λn. (ln(real (n::nat) + 2))^2 -
(ln(real n + 1))^2) \<elteqo>
(λn. 2 * ln(real n + 1) / (real n + 1)) \<pluso>
O(λn. (ln(real n + 1) + 1) / (real n + 1)^2)";
apply (insert ln_sq_diff_bigo2);
by (simp add: real_of_nat_Suc realpow_two2 plus_ac0);

theorem ln_sq_partial_sum: "sumr 0 (n+1) (%i. (ln (real (i+1)))^2) =
(real (n + 1))*(ln (real (n + 1)))^2 - sumr 0 n (%i. (real (i + 1)) *
((ln (real (i + 2)))^2 - (ln (real (i+1)))^2))";
apply(insert partial_sum0[of "%n. (real n)" "%n. (1::real)" "n" "%i. (ln (real i))^2"]);
apply(subgoal_tac "ALL n. real n = sumr 0 n (%i. 1)");
apply(rotate_tac 1);
apply(simp (no_asm_use) del: sumr.simps);
by(simp);

lemma real_nat_plus_two: "real ((n::nat) + 2) = real n + 2";
by auto;

theorem ln_sq_partial_sum2: "sumr 0 (n+1) (%i. (ln ((real i)+1))^2) =
((real n) + 1)*(ln ((real n) + 1))^2 - sumr 0 n (%i. ((real i) + 1) *
((ln ((real i) + 2))^2 - (ln ((real i)+1))^2))";
apply (insert ln_sq_partial_sum [of n]);
apply (simp only: real_nat_plus_one [THEN sym] real_nat_plus_two [THEN sym]);
done;

lemma identity_nine: "(λn. sumr 0 n (λi. (real i + 1) *
((ln (real i + 2))^2 - (ln (real i + 1))^2))) \<elteqo>
(λn. 2 * sumr 0 n (λi. ln(real i+1))) \<pluso>
O(λn. sumr 0 n (λi. ln(real i+1) / (real i + 1))) +
O(λn. sumr 0 n (λi. 1 / (real i + 1)))";
proof -;
from identity_five have
"(λn. (real n + 1)) * (λn. (ln(real (n::nat) + 2))^2 -
(ln(real n + 1))^2) \<elteqo>
(λn. (real n + 1)) \<timeso>
((λn. 2 * ln(real n + 1) / (real n + 1)) \<pluso>
O(λn. (ln(real n + 1) + 1) / (real n + 1)^2))";
by auto;
also have "(λn. (real n + 1)) * (λn. (ln(real (n::nat) + 2))^2 -
(ln(real n + 1))^2) = (λn. (real n + 1) * ((ln(real (n::nat) + 2))^2 -
(ln(real n + 1))^2))";
by (simp add: func_times);
also; have "(λn. (real n + 1)) \<timeso>
((λn. 2 * ln(real n + 1) / (real n + 1)) \<pluso>
O(λn. (ln(real n + 1) + 1) / (real n + 1)^2)) =
((λn. (real n+1)) * (λn. 2 * ln(real n + 1) / (real n + 1)))
\<pluso>
((λn. (real n + 1)) \<timeso>
O(λn. (ln(real n + 1) + 1) / (real n + 1)^2))";
by (rule set_times_plus_distrib);
also; have "(λn::nat. (real n+1)) * (λn. 2 * ln(real n + 1) / (real n + 1))
= (λn. 2 * ln(real n + 1))";
apply (auto simp add: func_times);
done;
also; have "(λu. 2 * ln (real u + 1)) \<pluso>
(λn. real n + 1) \<timeso> O(λn. (ln (real n + 1) + 1) / (real n + 1)²)
⊆ (λu. 2 * ln (real u + 1)) \<pluso>
O((λn. real n + 1) * (λn. (ln (real n + 1) + 1) / (real n + 1)²))";
proof -;
have "(λn. real n + 1) \<timeso>
O(λn. (ln (real n + 1) + 1) / (real n + 1)²) ⊆
O((λn. real n + 1) * (λn. (ln (real n + 1) + 1) / (real n + 1)²))";
by auto;
thus ?thesis; by auto;
qed;
also; have "(λn. real n + 1) *
(λn. (ln (real n + 1) + 1) / (real n + 1)²) =
(λn. (ln (real n + 1) + 1) / (real n + 1))";
by (auto simp add: func_times realpow_two2 [THEN sym]);
finally; have "(λi::nat. (real i + 1) *
((ln (real i + 2))² - (ln (real i + 1))²)) \<elteqo>
(λi. 2 * ln (real i + 1)) \<pluso>
O(λi. (ln (real i + 1) + 1) / (real i + 1))";.;
then have "(λn. sumr 0 n (λi::nat. (real i + 1) *
((ln (real i + 2))² - (ln (real i + 1))²))) \<elteqo>
(λn. sumr 0 n (λi. 2 * ln (real i + 1))) \<pluso>
O(λn. sumr 0 n (λi. (ln (real i + 1) + 1) / (real i + 1)))";
apply (intro bigo_sumr_pos2);
apply auto;
apply (rule real_ge_zero_div_gt_zero);
apply force+;
done;
also have "(λn. sumr 0 n (λi. 2 * ln (real i + 1))) =
(λn. 2 * sumr 0 n (λi. ln(real i + 1)))";
apply (rule ext);
by (simp add: sumr_mult);
also; have "(λn. 2 * sumr 0 n (λi. ln (real i + 1))) \<pluso>
O(λn. sumr 0 n (λi. (ln (real i + 1) + 1) / (real i + 1))) \<seteqo>
(λn. 2 * sumr 0 n (λi. ln (real i + 1))) \<pluso>
(O(λn. sumr 0 n (λi. (ln (real i + 1)) / (real i + 1))) +
O(λn. sumr 0 n (λi. 1 / (real i + 1))))";
apply (auto);
apply (rule subset_trans);
prefer 2;
apply (rule bigo_plus_subset);
apply (subgoal_tac "(λn. sumr 0 n (λi. (ln (real i + 1) + 1) /
(real i + 1))) = (λn. sumr 0 n (λi. ln (real i + 1) / (real i + 1))) +
(λn. sumr 0 n (λi. 1 / (real i + 1)))");
apply simp;
apply (simp add: func_plus, rule ext);
apply (subgoal_tac "(λi. (ln (real i + 1) + 1) / (real i + 1)) =
(λi. (ln (real i + 1) / (real i + 1)) + 1 / (real i + 1))");
apply (erule ssubst);
apply (rule sumr_add [THEN sym]);
apply (rule ext);
finally show ?thesis;
by (simp add: set_plus_rearrange3);
qed;

lemma aux1: "(λn. 1) ∈ O(λn. (ln(real n + 1)^2 + 1))";
apply (rule bigo_bounded);
by auto;

lemma aux2: "(n::nat) ~= 0 ==> ln 2 ≤ ln(real n + 1)"
proof -;
assume "(n::nat) ~= 0";
then have "0 < n"; by auto;
then have "2 ≤ n + 1"; by auto;
then have "real (2::nat) ≤ real (n + 1)";
by (simp add: real_of_nat_le_iff [THEN sym]);
then have "real (2::nat) ≤ real n + 1";
by (simp only: real_nat_plus_one);
then have "ln (real (2::nat)) ≤ ln (real n + 1)";
by auto;
thus ?thesis;
by simp;
qed;

lemma aux3: "(λn::nat. ln(real n + 1)) ∈ O(λn. (ln(real n + 1)^2 + 1))";
apply (rule bigo_bounded_alt);
apply auto;
apply (subgoal_tac "ln (real x + 1) ≤ (1 / ln 2) *
(ln (real x + 1)^2 + 1)");
apply assumption;
apply (simp add: ring_distrib);
apply (subgoal_tac "ln (real x + 1) ≤ (ln (real x + 1))^2 / ln 2");
apply (erule order_trans);
apply auto;
apply (rule real_mult_le_imp_le_div_pos);
apply auto;
apply (subst realpow_two2 [THEN sym]);
apply (case_tac "x = 0");
apply simp;
apply (rule mult_mono);
apply auto;
done;

lemma first_term_a: "(λn. sumr 0 n (λi. ln(real i + 1))) \<elteqo>
((λn. (real n + 1) * ln (real n + 1)) -
(λn. real n)) \<pluso> O(λn. (ln(real n + 1)^2 + 1))";
proof -;
have "(λn. sumr 0 n (λi. ln(real i + 1))) =
(λn. sumr 0 (n + 1) (λi. ln(real i + 1))) - (λn. ln (real n + 1))";
by (simp add: diff_minus func_minus func_plus);
also have "… = - (λn. ln (real n + 1)) +
(λn. sumr 0 (n + 1) (λi. ln(real i + 1)))";
also from identity_three have "… \<elteqo> - (λn. ln (real n + 1)) \<pluso>
(((λn. (real n + 1) * ln(real n + 1)) - (λn. (real n))) \<pluso>
O(λn. ln (real n + 1)))";
by (rule set_plus_intro2);
also have "… = ((λn. (real n + 1) * ln (real n + 1)) - (λn. real n))
\<pluso>
( -(λn. ln (real n + 1)) \<pluso> O(λn. ln (real n + 1)))";
by (simp add: ring_eq_simps set_plus_rearranges);
also from aux3 have "… \<seteqo> ((λn::nat. (real n + 1) * ln (real n + 1))
- (λn. real n)) \<pluso>
O(λn. (ln (real n + 1))^2 + 1)";
by auto;
finally show ?thesis;.;
qed;

lemma first_term: "(λn. 2 * sumr 0 n (λi. ln(real i + 1))) \<elteqo>
((λn. 2* (real n + 1) * ln (real n + 1)) -
(λn. 2* (real n))) \<pluso> O(λn. (ln(real n + 1)^2 + 1))";
proof -;
note first_term_a;
then have "(λn. 2) * (λn. sumr 0 n (λi. ln (real i + 1))) \<elteqo>
(λn. 2) \<timeso> (((λn. (real n + 1) * ln (real n + 1)) -
(λn. (real n))) \<pluso>
O(λn. (ln (real n + 1))² + 1))" (is "?LHS ∈ ?RHS");
by (intro set_times_intro2);
also have "?LHS = (λn. 2 * sumr 0 n (λi. ln(real i + 1)))";
by (simp add: func_times);
also have "?RHS = ((λn. 2* (real n + 1) * ln (real n + 1)) -
(λn. 2* (real n))) \<pluso> O(λn. (ln(real n + 1)^2 + 1))";
by (simp add: set_times_plus_distribs func_times ring_distrib
diff_minus func_minus func_plus mult_ac);
finally show ?thesis;.;
qed;

lemma second_term: "O(λn. sumr 0 n (λi. ln(real i + 1) / (real i + 1)))
\<seteqo> O(λn. (ln(real n + 1))^2 + 1)";
proof -;
from identity_four have
"O(λn. sumr 0 n (λi. ln(real i + 1) / (real i + 1))) ⊆
O(λn. (ln(real n + 1))^2/2) + O(λn. 1)";
by auto;
also have "… ⊆ O(λn. (ln(real n + 1))^2 + 1)";
proof -;
have "O(λn. (ln(real n + 1))^2/2) ⊆ O(λn. (ln(real n + 1))^2 + 1)";
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply auto;
apply (subgoal_tac "-2 ≤ 0");
apply (erule order_trans);
by auto;
with aux1 show ?thesis;
by auto;
qed;
finally show ?thesis;.;
qed;

lemma third_term: "O(λn. sumr 0 n (λi. 1 / (real i + 1))) \<seteqo>
O(λn. (ln(real n + 1))^2 + 1)";
proof -;
have "(λn. sumr 0 n (λi. 1 / (real i + 1))) =
-(λn. 1 / (real n + 1)) + (λn. sumr 0 (n+1) (λi. 1 / (real i + 1)))";
by (simp add: func_plus func_minus);
also from identity_two have "… ∈ -(λn. 1 / (real n + 1)) \<pluso>
((λn. ln(real n + 1)) \<pluso> O(λn. 1))";
by auto;
also have "… ⊆ O(λn. (ln(real n + 1))^2 + 1)";
proof -;
have "-(λn::nat. 1 / (real n + 1)) ∈ O(λn. (ln(real n + 1))^2 + 1)";
apply (rule bigo_minus);
apply (rule bigo_bounded);
apply auto;
apply (subgoal_tac "1 / (real x + 1) ≤ 1");
apply (erule order_trans);
apply auto;
apply (rule real_le_mult_imp_div_pos_le);
apply (rule real_nat_plus_one_gt_zero);
by auto;
with aux1 aux3 show ?thesis; by auto;
qed;
finally show ?thesis; by auto;
qed;

lemma penultimate_equation: "(λn. sumr 0 n (λi. (real i + 1) *
((ln(real i + 2))^2 - (ln(real i + 1))^2))) \<elteqo>
((λn. 2 * (real n + 1) * ln(real n + 1)) - (λn. 2 * (real n))) \<pluso>
O(λn. (ln (real n + 1))^2 + 1)" (is "?LHS \<elteqo> ?RHS");
proof -;
from identity_nine have
"?LHS \<elteqo>
(λn. 2 * sumr 0 n (λi. ln(real i+1))) \<pluso>
(O(λn. sumr 0 n (λi. ln(real i+1) / (real i + 1))) +
O(λn. sumr 0 n (λi. 1 / (real i + 1))))"
by (simp add: set_plus_rearranges);
also from second_term third_term have "… ⊆
(λn. 2 * sumr 0 n (λi. ln(real i+1))) \<pluso>
O(λn. (ln (real n + 1))^2 + 1)";
by auto;
also from first_term have "… ⊆
(((λn. 2* (real n + 1) * ln (real n + 1)) -
(λn. 2* (real n))) \<pluso> O(λn. (ln(real n + 1)^2 + 1))) +
O(λn. (ln (real n + 1))^2 + 1)";
by auto;
also have "… =
((λn. 2* (real n + 1) * ln (real n + 1)) -
(λn. 2* (real n))) \<pluso> (O(λn. (ln(real n + 1)^2 + 1)) +
O(λn. (ln (real n + 1))^2 + 1))";
by (simp add: set_plus_rearranges);
also have "… ⊆ ((λn. 2* (real n + 1) * ln (real n + 1)) -
(λn. 2* (real n))) \<pluso> O(λn. (ln(real n + 1)^2 + 1))";
by auto;
finally show ?thesis;.;
qed;

lemma almost_there: "(λn. sumr 0 (n+1) (λi. (ln (real i + 1))^2)) \<elteqo>
((λn. (real n + 1) * (ln(real n + 1))^2) -
(λn. 2 * (real n + 1) * ln(real n + 1)) + (λn. 2 * (real n)))
\<pluso> O(λn. (ln (real n + 1))^2 + 1)";
proof -;
from penultimate_equation have  "-(λn. sumr 0 n (λi. (real i + 1) *
((ln(real i + 2))^2 - (ln(real i + 1))^2))) \<elteqo>
-((λn. 2 * (real n + 1) * ln(real n + 1)) - (λn. 2 * (real n))) \<pluso>
O(λn. (ln (real n + 1))^2 + 1)" (is "?LHS \<elteqo> ?RHS");
by (rule bigo_minus2);
then have "(λn. ((real n) + 1)*(ln ((real n) + 1))^2) + ?LHS
\<elteqo> (λn. ((real n) + 1)*(ln ((real n) + 1))^2) \<pluso> ?RHS"
(is "?LHS2 \<elteqo> ?RHS2");
by auto;
also; from ln_sq_partial_sum2 have "?LHS2 =
(λn. sumr 0 (n+1) (%i. (ln ((real i)+1))^2))";
by (simp add: diff_minus func_minus func_plus ext);
finally show ?thesis;
by (simp add: diff_minus set_plus_rearranges ring_eq_simps);
qed;

lemma aux5: "f ∈ O(λn::nat. (ln (real n + 1))^2 + 1)  ==>
f(0) = 0  ==> f ∈ O(λn::nat. (ln (real n + 1))^2)";
apply (auto simp add: bigo_alt_def);
apply (rule_tac x = "c + c / (ln 2)^2" in exI);
apply auto;
apply (subgoal_tac "- c < 0");
apply (subgoal_tac "0 < c / (ln 2)^2");
apply (erule order_less_trans);
apply (assumption);
apply (rule real_mult_less_imp_less_div_pos);
apply (auto);
apply (case_tac "x = 0");
apply (simp add: realpow_two2 [THEN sym]);
apply (drule_tac x = x in spec);
apply (subgoal_tac "abs((ln (real x + 1))² + 1) = (ln (real x + 1))² + 1");
apply (simp add: left_distrib right_distrib);
apply (erule order_trans);
apply auto;
apply (subgoal_tac "c * 1 ≤ c * ((ln (real x + 1)) ^ 2 / (ln 2) ^ 2)");
apply simp;
apply (rule mult_left_mono);
apply (rule div_ge_1);
apply force;
apply (rule power_mono);
apply (rule aux2);
apply force;
apply force;
apply force;
apply (rule abs_nonneg);
apply (rule nonneg_plus_nonneg);
apply auto;
done;

lemma aux6: "f ∈ g \<pluso> O(λn::nat. (ln (real n + 1)^2 + 1)) ==>
f 0 = g 0 ==> f ∈ g \<pluso> O(λn. (ln (real n + 1))^2)";
proof -;
assume "f ∈ g \<pluso> O(λn. (ln (real n + 1)^2 + 1))";
then have a: "f - g ∈ O(λn. (ln (real n + 1)^2 + 1))";
by (rule set_plus_imp_minus);
assume "f 0 = g 0";
then have b: "(f - g)0 = 0";
by (simp add: diff_minus func_minus func_plus);
from a b have "f - g ∈ O(λn. (ln (real n + 1)^2))";
by (intro aux5);
then show "f ∈ g \<pluso> O(λn. (ln (real n + 1)^2))";
by (rule set_minus_imp_plus);
qed;

theorem identity_six: "(λn. sumr 0 (n+1) (λi. (ln (real i + 1))^2)) \<elteqo>
((λn. (real n + 1) * (ln(real n + 1))^2) -
(λn. 2 * (real n + 1) * ln(real n + 1)) + (λn. 2 * (real n)))
\<pluso> O(λn. (ln (real n + 1))^2)";
apply (rule aux6);
apply (rule almost_there);
by (simp add: realpow_two2 [THEN sym] diff_minus func_minus func_plus);

end;

```

### Previous identities, rewritten

lemma identity_one:

```  (%n. ln (1 + 1 / (real n + 1)))
∈ (%n. 1 / (real n + 1)) + O(%n. 1 / (real n + 1)²)```

lemma identity_two:

`  (%n. sumr 0 (n + 1) (%i. 1 / (real i + 1))) ∈ (%n. ln (real n + 1)) + O(%n. 1)`

lemma identity_three:

```  (%n. sumr 0 (n + 1) (%i. ln (real i + 1)))
∈ ((%n. (real n + 1) * ln (real n + 1)) - real) + O(%n. ln (real n + 1))```

lemma identity_four:

```  (%n. sumr 0 n (%i. ln (real i + 1) / (real i + 1)))
∈ (%n. (ln (real n + 1))² / 2) + O(%n. 1)```

lemma identity_five:

```  (%n. (ln (real n + 2))² - (ln (real n + 1))²)
∈ (%n. 2 * ln (real n + 1) / (real n + 1)) +
O(%n. (ln (real n + 1) + 1) / (real n + 1)²)```

theorem ln_sq_partial_sum:

```  sumr 0 (n + 1) (%i. (ln (real (i + 1)))²) =
real (n + 1) * (ln (real (n + 1)))² -
sumr 0 n (%i. real (i + 1) * ((ln (real (i + 2)))² - (ln (real (i + 1)))²))```

lemma real_nat_plus_two:

`  real (n + 2) = real n + 2`

theorem ln_sq_partial_sum2:

```  sumr 0 (n + 1) (%i. (ln (real i + 1))²) =
(real n + 1) * (ln (real n + 1))² -
sumr 0 n (%i. (real i + 1) * ((ln (real i + 2))² - (ln (real i + 1))²))```

lemma identity_nine:

```  (%n. sumr 0 n (%i. (real i + 1) * ((ln (real i + 2))² - (ln (real i + 1))²)))
∈ (%n. 2 * sumr 0 n (%i. ln (real i + 1))) +
O(%n. sumr 0 n (%i. ln (real i + 1) / (real i + 1))) +
O(%n. sumr 0 n (%i. 1 / (real i + 1)))```

lemma aux1:

`  (%n. 1) ∈ O(%n. (ln (real n + 1))² + 1)`

lemma aux2:

`  n ≠ 0 ==> ln 2 ≤ ln (real n + 1)`

lemma aux3:

`  (%n. ln (real n + 1)) ∈ O(%n. (ln (real n + 1))² + 1)`

lemma first_term_a:

```  (%n. sumr 0 n (%i. ln (real i + 1)))
∈ ((%n. (real n + 1) * ln (real n + 1)) - real) + O(%n. (ln (real n + 1))² + 1)```

lemma first_term:

```  (%n. 2 * sumr 0 n (%i. ln (real i + 1)))
∈ ((%n. 2 * (real n + 1) * ln (real n + 1)) - (%n. 2 * real n)) +
O(%n. (ln (real n + 1))² + 1)```

lemma second_term:

```  O(%n. sumr 0 n (%i. ln (real i + 1) / (real i + 1)))
⊆ O(%n. (ln (real n + 1))² + 1)```

lemma third_term:

`  O(%n. sumr 0 n (%i. 1 / (real i + 1))) ⊆ O(%n. (ln (real n + 1))² + 1)`

lemma penultimate_equation:

```  (%n. sumr 0 n (%i. (real i + 1) * ((ln (real i + 2))² - (ln (real i + 1))²)))
∈ ((%n. 2 * (real n + 1) * ln (real n + 1)) - (%n. 2 * real n)) +
O(%n. (ln (real n + 1))² + 1)```

lemma almost_there:

```  (%n. sumr 0 (n + 1) (%i. (ln (real i + 1))²))
∈ ((%n. (real n + 1) * (ln (real n + 1))²) -
(%n. 2 * (real n + 1) * ln (real n + 1)) +
(%n. 2 * real n)) +
O(%n. (ln (real n + 1))² + 1)```

lemma aux5:

```  [| f ∈ O(%n. (ln (real n + 1))² + 1); f 0 = 0 |]
==> f ∈ O(%n. (ln (real n + 1))²)```

lemma aux6:

```  [| f ∈ g + O(%n. (ln (real n + 1))² + 1); f 0 = g 0 |]
==> f ∈ g + O(%n. (ln (real n + 1))²)```

theorem identity_six:

```  (%n. sumr 0 (n + 1) (%i. (ln (real i + 1))²))
∈ ((%n. (real n + 1) * (ln (real n + 1))²) -
(%n. 2 * (real n + 1) * ln (real n + 1)) +
(%n. 2 * real n)) +
O(%n. (ln (real n + 1))²)```