# Theory LnSum5

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

theory LnSum5 = LnSum4:

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

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

theory LnSum5 = LnSum4:;

lemma aux1: "(%n. ln(real n + 1) * sumr 0 (n + 1) (%i. ln (real i + 1))) =o
((%n. (real n + 1) * (ln (real n + 1))^2) - (%n. (real n) * ln (real n + 1)))
+o O(%n. (ln (real n + 1))^2)";
proof -;
have "(%n. ln(real n + 1) * sumr 0 (n + 1) (%i. ln (real i + 1))) =
(%n. ln(real n + 1)) * (%n. sumr 0 (n + 1) (%i. ln (real i + 1)))";
also from identity_three have "... =o (%n. ln(real n + 1)) *o
(((%n. (real n + 1) * ln(real n + 1)) - (λn. real n)) +o
O(λn. ln (real n + 1)))";
by auto;
also have "... = (%n. ln(real n + 1)) *
((%n. (real n + 1) * ln(real n + 1)) - (λn. real n)) +o
(%n. ln(real n + 1)) *o O(λn. ln (real n + 1))";
also have "(%n. ln(real n + 1)) *
((%n. (real n + 1) * ln(real n + 1)) - (λn. real n)) =
((%n. (real n + 1) * (ln(real n + 1))^2) -
(λn. (real n) * ln(real n + 1)))";
by (simp add: func_times diff_minus func_minus func_plus ring_distrib
realpow_two2 [THEN sym] mult_ac);
also; have "((%n. (real n + 1) * ln (real n + 1) ^ 2) -
(%n. real n * ln (real n + 1))) +o
(%n. ln (real n + 1)) *o O(%n. ln (real n + 1)) =s
((%n. (real n + 1) * ln (real n + 1) ^ 2) -
(%n. real n * ln (real n + 1))) +o O(%n. (ln (real n + 1))^2)";
apply (auto simp add: func_times realpow_two2 [THEN sym]);
apply (subgoal_tac "(%n. ln (real n + 1)) *o O(%n. ln (real n + 1))
=s O((%n. ln (real n + 1)) * (%n. ln (real n + 1)))");
by auto;
finally show ?thesis;.;
qed;

lemma aux2: "(%n. 2 * ln(real n + 1) * sumr 0 (n + 1) (%i. ln (real i + 1))) =o
((%n. 2 * (real n + 1) * (ln (real n + 1))^2) - (%n. 2 * (real n) *
ln (real n + 1))) +o O(%n. (ln (real n + 1))^2)"
(is "?LHS =o ?RHS");
proof -;
from aux1 have
"(%n. 2) * (%n. ln(real n + 1) * sumr 0 (n + 1) (%i. ln (real i + 1))) =o
(%n. 2) *o (((%n. (real n + 1) * (ln (real n + 1))^2) -
(%n. (real n) * ln (real n + 1))) +o O(%n. (ln (real n + 1))^2))"
(is "?LHS1 =o ?RHS1");
by auto;
also have "?LHS1 = ?LHS";
also have "?RHS1 = ?RHS";
by (simp add: func_times diff_minus func_minus func_plus
ring_distrib set_times_plus_distribs mult_ac);
finally show ?thesis;.;
qed;

lemma aux2a: "-(%n. 2 * ln(real n + 1) * sumr 0 (n + 1)
(%i. ln (real i + 1))) =o
(- (%n. 2 * (real n + 1) * (ln (real n + 1))^2) + (%n. 2 * (real n) *
ln (real n + 1))) +o O(%n. (ln (real n + 1))^2)";
proof -;
from aux2 have "-(%n. 2 * ln(real n + 1) * sumr 0 (n + 1)
(%i. ln (real i + 1))) =o
- ((%n. 2 * (real n + 1) * (ln (real n + 1))^2) - (%n. 2 * (real n) *
ln (real n + 1))) +o O(%n. (ln (real n + 1))^2)";
by (rule bigo_minus2);
then show ?thesis;
qed;

lemma aux3: "((x::real) - y)^2 = x^2 - 2 * x * y + y^2";
by (simp add: realpow_two2 [THEN sym] ring_distrib mult_ac
diff_minus);

lemma aux4: "(%n. sumr 0 (n + 1) (%i. (ln ((real n + 1) / (real i + 1)))^2)) =
(%n. (real n+1) * ln(real n + 1)^2) -
(%n. 2 * ln(real n + 1) * sumr 0 (n+1) (%i. ln(real i + 1))) +
(%n. sumr 0 (n + 1) (%i. (ln (real i + 1))^2))";
apply (simp only: diff_minus func_minus func_plus);
apply (rule ext);
proof -;
fix n;
show "sumr 0 (n + 1) (%i. ln ((real n + 1) / (real i + 1)) ^ 2) =
(real n + 1) * ln (real n + 1) ^ 2 +
- (2 * ln (real n + 1) * sumr 0 (n + 1) (%i. ln (real i + 1))) +
sumr 0 (n + 1) (%i. (ln (real i + 1)) ^ 2)";
proof -;
have "(%i::nat. (ln ((real n + 1) / (real i + 1)))^2) =
(%i. (ln (real n + 1) - ln(real i + 1))^2)";
apply (rule ext);
apply (subst ln_div);
apply (rule real_nat_plus_one_gt_zero)+;
by (rule refl);
also have "... = (%i. (ln (real n + 1))^2 -
2 * ln (real n + 1) * ln (real i + 1) + ln(real i + 1)^2)";
apply (rule ext);
by (rule aux3);
finally; have "(%i::nat.
ln ((real (n::nat) + (1::real)) / (real i + (1::real))) ^ 2) =
(%i::nat. ln (real n + (1::real)) ^ 2 -
(2::real) * ln (real n + (1::real)) * ln (real i + (1::real)) +
ln (real i + (1::real)) ^ 2)" (is "?LHS = ?RHS");.;
then have "sumr 0 (n + 1) (?LHS) = sumr 0 (n + 1) (?RHS)";
by auto;
also have "... = sumr 0 (n+1) (%i. ln (real n + 1) ^ 2) -
sumr 0 (n+1) (%i. 2 * ln (real n + 1) * ln (real i + 1)) +
sumr 0 (n+1) (%i. ln (real i + 1) ^ 2)";
by (simp only: sumr_add diff_minus func_minus func_plus
sumr_minus [THEN sym]);
also have "sumr 0 (n+1) (%i. ln (real n + 1) ^ 2) =
real (n + 1) * ln (real n + 1) ^ 2";
by (rule sumr_const);
also have "real (n + 1) = real n + 1";
by (rule real_nat_plus_one);
also; have "sumr 0 (n + 1) (%i. 2 * ln (real n + 1) * ln (real i + 1))
= 2 * ln (real n + 1) * sumr 0 (n + 1) (%i. ln (real i + 1))";
by (subst sumr_mult, rule refl);
finally show ?thesis;
by (simp only: diff_minus);
qed;
qed;

lemma aux5: "(%n. (real n+1) * ln(real n + 1)^2) -
(%n. 2 * ln(real n + 1) * sumr 0 (n+1) (%i. ln(real i + 1))) =o
((%n. - (real n + 1) * ln (real n + 1)^2) +
(%n. 2 * (real n) * ln(real n + 1))) +o O(%n. ln(real n + 1)^2)";
proof -;
have "(%n. (real n+1) * ln(real n + 1)^2) -
(%n. 2 * ln(real n + 1) * sumr 0 (n+1) (%i. ln(real i + 1))) =
(%n. (real n+1) * ln(real n + 1)^2) + -
(%n. 2 * ln(real n + 1) * sumr 0 (n+1) (%i. ln(real i + 1)))";
by (simp only: diff_minus);
also from aux2a have "... =o (%n. (real n+1) * ln(real n + 1)^2) +o
((- (%n. 2 * (real n + 1) * (ln (real n + 1))^2) + (%n. 2 * (real n) *
ln (real n + 1))) +o O(%n. (ln (real n + 1))^2))";
by auto;
also have "... = ((%n. (real n+1) * ln(real n + 1)^2) +
(- (%n. 2 * (real n + 1) * (ln (real n + 1))^2)) + (%n. 2 * (real n) *
ln (real n + 1))) +o O(%n. (ln (real n + 1))^2)";
also have "(%n. (real n+1) * ln(real n + 1)^2) +
(- (%n. 2 * (real n + 1) * (ln (real n + 1))^2)) + (%n. 2 * (real n) *
ln (real n + 1)) = (%n. - (real n + 1) * ln (real n + 1)^2) +
(%n. 2 * (real n) * ln(real n + 1))";
apply (subgoal_tac "(%n. (real n+1) * ln(real n + 1)^2) +
(- (%n. 2 * (real n + 1) * (ln (real n + 1))^2)) =
(%n. - (real n + 1) * ln (real n + 1)^2)");
apply (erule ssubst, rule refl);
apply (auto simp add: func_plus func_minus);
apply (rule ext);
apply (subgoal_tac "(real x + 1) * ln (real x + 1) ^ 2 +
- ((2 * real x + 2) * ln (real x + 1) ^ 2) =
((real x + 1) + - (2 * real x + 2)) * ln (real x + 1)^2");
apply force;
finally show ?thesis;.;
qed;

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

theorem almost_there:
"(%n. sumr 0 (n+1) (%i. ln((real n + 1)/(real i + 1))^2)) =o
(%n. 2 * (real n)) +o O(%n. ln(real n + 1)^2)";
proof -;
from aux4 identity_six have
"(%n. sumr 0 (n + 1) (%i. (ln ((real n + 1) / (real i + 1)))^2)) =o
((%n. (real n+1) * ln(real n + 1)^2) -
(%n. 2 * ln(real n + 1) * sumr 0 (n+1) (%i. ln(real i + 1)))) +o
(((λn. (real n + 1) * (ln(real n + 1))^2) -
(λn. 2 * (real n + 1) * ln(real n + 1)) + (λn. 2 * (real n)))
+o O(λn. (ln (real n + 1))^2))";
by auto;
also have "… = ((%n. (real n + 1) * (ln(real n + 1))^2) -
(%n. 2 * (real n + 1) * ln(real n + 1)) + (%n. 2 * (real n))) +o
(((%n. (real n+1) * ln(real n + 1)^2) -
(%n. 2 * ln(real n + 1) * sumr 0 (n+1) (%i. ln(real i + 1)))) +o
O(%n. (ln (real n + 1))^2))";
also from aux5 have "… =s ((%n. (real n + 1) * (ln(real n + 1))^2) -
(%n. 2 * (real n + 1) * ln(real n + 1)) + (%n. 2 * (real n))) +o
(((%n. - (real n + 1) * ln (real n + 1)^2) +
(%n. 2 * (real n) * ln(real n + 1))) +o O(%n. ln(real n + 1)^2)
+ O(%n. ln(real n + 1)^2))";
by auto;
also have "… = ((%n. (real n + 1) * (ln(real n + 1))^2) -
(%n. 2 * (real n + 1) * ln(real n + 1)) + (%n. 2 * (real n)) +
(%n. - (real n + 1) * ln (real n + 1)^2) +
(%n. 2 * (real n) * ln(real n + 1))) +o O(%n. ln(real n + 1)^2)";
by (simp add: diff_minus plus_ac0 set_plus_rearranges
set_plus_rearrange4);
also have "((%n. (real n + 1) * (ln(real n + 1))^2) -
(%n. 2 * (real n + 1) * ln(real n + 1)) + (%n. 2 * (real n)) +
(%n. - (real n + 1) * ln (real n + 1)^2) +
(%n. 2 * (real n) * ln(real n + 1))) = (%n. 2 * (real n)) -
(%n. 2 * ln(real n + 1))";
apply (simp add: diff_minus func_minus func_plus);
apply (rule ext);
by (auto simp add: plus_ac0 ring_distrib);
also have "((%n. 2 * real n) - (%n. 2 * ln (real n + 1))) +o
O(%n. (ln (real n + 1))^2) = (%n. 2 * real n) +o
(- (%n. 2 * ln (real n + 1)) +o O(%n. (ln (real n + 1))^2))";
by (auto simp add: diff_minus set_plus_rearranges);
also have
"… =s (%n. 2 * real (n::nat)) +o O(%n. (ln (real n + 1))^2)";
proof -;
from aux6 have "- (%n::nat. 2 * ln (real n + 1)) =o
O(%n. (ln (real n + 1))^2)";
by auto;
thus ?thesis; by auto;
qed;
finally show ?thesis;.;
qed;

end;

```

lemma aux1:

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

lemma aux2:

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

lemma aux2a:

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

lemma aux3:

`  (x - y)² = x² - 2 * x * y + y²`

lemma aux4:

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

lemma aux5:

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

lemma aux6:

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

theorem almost_there:

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