# Theory LnSum1a

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

theory LnSum1a = BigO + RealLib + Ln:

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

header {* Stronger versions of identities in LnSum1 *}

theory LnSum1a = BigO + RealLib + Ln:;

lemma real_inverse_mult_suc: "0 < k ==> 1 / (k * (k + (1::real))) = (1 / k - 1 / (k + 1))";
apply(simp only: minus_divide_left);
apply simp;
done;

lemma telescoping_sumr: "sumr x (x + y) (%n. 1 / ((real n + 1) * (real n + 2))) =
1 / (real (x + 1)) - 1 / (real (x + y + 1))" (is "?P y");
proof (induct_tac y);
show "?P(0)"; by simp;
next fix n; assume ih: "?P(n)"; show "?P(Suc n)";
proof -;
have "sumr x (x + Suc n) (%n. 1 / ((real n + 1) * (real n + 2))) =
sumr x (Suc (x + n)) (%n. 1 / ((real n + 1) * (real n + 2)))";
by simp;
also have "... =  sumr x (x + n) (%n. 1 / ((real n + 1) * (real n + 2))) +
(1 / ((real (x + n) + 1) * (real (x + n) + 2)))";
by simp;
also have "... = (1 / real (x + 1) - 1 / real (x + n + 1)) +
(1 / ((real (x + n) + 1) * (real (x + n) + 2)))";
also have "... = 1 / (real (x + 1)) - 1 / (real (x + Suc n + 1))";
proof -;
have "1 / ((real (x + n) + 1) * (real (x + n) + 2)) =
1 / ((real (x + n) + 1) * ((real (x + n) + 1) + 1))";
by simp;
also have "... = 1 / (real (x + n) + 1) - 1 / ((real (x + n) + 1) + 1)";
by (rule real_inverse_mult_suc, auto);
finally; have "1 / ((real (x + n) + 1) * (real (x + n) + 2)) =
1 / (real (x + n) + 1) - 1 / (real (x + n) + 1 + 1)";.;
then have "1 / real (x + 1) - 1 / real (x + n + 1) +
1 / ((real (x + n) + 1) * (real (x + n) + 2)) =
1 / real (x + 1) - 1 / real (x + n + 1) +
(1 / (real (x + n) + 1) - 1 / (real (x + n) + 1 + 1))";
by simp;
also have "... =  1 / real (x + 1) + (1 / (real (x + n) + 1) - (1 / (real (x + n) + 1))
- 1 / (real (x + n) + 1 + 1))";
by simp;
also have "... =  1 / real (x + 1) - 1 / real (x + Suc n + 1)";
by simp;
finally show ?thesis;.;
qed;
finally show ?thesis;.;
qed;
qed;

lemma sums_one_over_n_n_plus_one:
"(%n. 1 / ((real (x + n) + 1) * (real (x + n) + 2))) sums (1 / (real x + 1))";
proof (unfold sums_def);
have "(%n. sumr 0 n (%n. 1 / ((real (x + n) + 1) * (real (x + n) + 2)))) =
(%y. sumr x (x + y) (%n. 1 / ((real n + 1) * (real n + 2))))";
apply (rule ext);
apply (rule sumr_shift);
done;
also have "... =  (%y. 1 / (real (x + 1)) - 1 / (real (x + y + 1)))";
apply (rule ext);
apply (subst telescoping_sumr);
apply (rule refl);
done;
finally have a:
"(%n. sumr 0 n (%n. 1 / ((real (x + n) + 1) * (real (x + n) + 2)))) =
(%y. 1 / (real (x + 1)) - 1 / (real (x + y + 1)))";.;
have "(%y. 1 / (real (x + 1))) ----> 1 / (real (x + 1))";
by (rule LIMSEQ_const);
moreover have "(%y. 1 / (real (x + y + 1))) ----> 0";
apply (unfold LIMSEQ_def);
apply auto;
apply (rule_tac x = "nat(ceiling(1 / r))" in exI);
apply auto;
proof -;
fix r; fix n;
assume a: "0 < r" and b: "nat(ceiling(1/r)) <= n";
show "1 / real(Suc (x + n)) < r";
proof -;
have "1 / r <= real(ceiling (1 / r))";
by auto;
also have "real(ceiling (1 / r)) = real(int(nat(ceiling(1/r))))";
apply auto;
apply (subgoal_tac "0 <= 1 / r");
apply (frule ceiling_le2);
apply simp;
apply simp;
apply (rule order_less_imp_le);
apply (rule prems);
done;
also have "… = real(nat(ceiling(1/r)))";
apply (subst real_of_int_real_of_nat);
apply (rule refl);
done;
also have "… <= real n";
also have "real n < real (Suc (x + n))";
by auto;
finally have "1 / r < real(Suc (x + n))";.;
then show ?thesis;
apply (subst pos_divide_less_eq);
apply force;
apply (subst mult_commute);
apply (subst pos_divide_less_eq [THEN sym]);
apply (rule prems);
apply (assumption);
done;
qed;
qed;
ultimately have "(%y. 1 / (real (x + 1)) - 1 / (real (x + y + 1))) ---->
1 / (real (x + 1)) - 0";
by (intro LIMSEQ_diff);
thus "(λn. sumr 0 n (λn. 1 / ((real (x + n) + 1) * (real (x + n) + 2))))
----> 1 / (real x + 1)";
apply (subst a);
apply (subgoal_tac "1 / real (x + 1) - 0 = 1 / (real x + 1)");
apply (erule subst, assumption);
apply simp;
done;
qed;

lemma summable_one_over_n_n_plus_one:
"summable (%n. 1 / ((real (x + n) + 1) * (real (x + n) + 2)))";
apply (unfold summable_def);
apply (rule exI);
apply (rule sums_one_over_n_n_plus_one);
done;

lemma suminf_one_over_n_n_plus_one: "suminf
(%n. 1 / ((real (x + n) + 1) * (real (x + n) + 2))) = 1 / (real x + 1)";
apply (rule sym);
apply (rule sums_unique);
apply (rule sums_one_over_n_n_plus_one);
done;

lemma summable_one_over_n_squared: "summable (%n. 1 / (real n+1)^2)";
proof -;
have "summable (λn. 1 / ((real n + 1) * (real n + 2)))";
by (insert summable_one_over_n_n_plus_one [of 0], simp);
then have "summable (λn. 2 * (1 / ((real n + 1) * (real n + 2))))";
by (intro summable_const_times);
also have "(λn. 2 * (1 / ((real n + 1) * (real n + 2)))) =
(λn. 2 / ((real n + 1) * (real n + 2)))";
by simp;
finally have a: "summable (λn. 2 / ((real n + 1) * (real n + 2)))";.;
show ?thesis;
apply (rule summable_comparison_test);
prefer 2; apply (rule a);
apply (rule_tac x = 0 in exI);
apply auto;
apply (rule real_le_mult_imp_div_pos_le);
apply auto;
apply (rule real_mult_le_imp_le_div_pos);
apply (rule mult_pos);
apply auto;
apply (subst realpow_two2 [THEN sym]);
apply (subgoal_tac "(real n + 1) * (real n + 1) * 2 = (real n + 1) *
((real n + 1) * 2)");
apply (erule ssubst);
apply (rule mult_left_mono);
apply auto;
done;
qed;

lemma abs_ln_one_plus_pos_minus_x_bound2:
"0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2";
proof -;
assume "0 <= x";
assume "x <= 1";
have "ln (1 + x) <= x";
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;
finally show ?thesis;.;
qed;

lemma ln_successor_diff: "ln (real (n::nat) + 2) - ln (real n + 1) =
ln (1 + 1 / (real n + 1))";
apply (subst ln_div [THEN sym]);
apply auto;
apply (rule arg_cong);back;
apply auto;
done;

lemma gamma_lemma: "summable (%n. ln(real n+2) - ln(real n+1) - 1 / (real n + 1))";
apply (rule summable_comparison_test);
prefer 2;
apply (rule summable_one_over_n_squared);
apply (subgoal_tac "(%n. ln (real n + 2) - ln (real n + 1)) =
(%n. ln (1 + 1 / (real n + 1)))");
apply (erule ssubst);
apply (rule_tac x = 0 in exI);
apply clarify;
apply (subgoal_tac "1 / (real n + 1)^2 = (1 / (real n + 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 force;
apply force;
apply (rule real_one_over_pow);
apply force;
apply (rule ext);
apply (rule ln_successor_diff);
done;

constdefs
gamma :: real
"gamma == suminf (%n. ln (real n + 2) - ln (real n + 1) - 1 / (real n + 1))";

lemma gamma_def2: "(%n. ln (real n + 2) - ln (real n + 1) - 1 / (real n + 1))
sums gamma";
apply (unfold gamma_def);
apply (rule summable_sums);
apply (rule gamma_lemma);
done;

lemma bigo_minus4: "(f =o O(g::'a=>'b::ordered_ring)) = (- f =o O(g))";
apply (rule iffI);
apply (erule bigo_minus);
apply (subgoal_tac "f = - (- f)");
apply (erule ssubst);
apply (erule bigo_minus);
apply simp;
done;

lemma one_over_n_squared_bound_old: "1 / (real (n::nat) + 1)^2 <=
2 * (1 / (real n + 1) - 1 / (real n + 2))";
apply (subgoal_tac "real n + 2 = (real n + 1) + 1");
apply (erule ssubst);
apply (subst real_inverse_mult_suc [THEN sym]);
apply force;
apply simp;
apply (rule real_le_mult_imp_div_pos_le);
apply auto;
apply (rule real_mult_le_imp_le_div_pos);
apply (rule mult_pos);
apply auto;
apply (subst realpow_two2 [THEN sym]);
apply (subgoal_tac "(real n + 1) * (real n + 1) * 2 = (real n + 1) *
((real n + 1) * 2)");
apply (erule ssubst);
apply (rule mult_left_mono);
apply auto;
done;

lemma one_over_n_squared_bound: "1 / (real (n::nat) + 1)^2 <=
2 * (1 / ((real n + 1) * (real n + 2)))";
apply (subgoal_tac "real n + 2 = (real n + 1) + 1");
apply (erule ssubst);
apply simp;
apply (rule real_le_mult_imp_div_pos_le);
apply auto;
apply (rule real_mult_le_imp_le_div_pos);
apply (rule mult_pos);
apply auto;
apply (subst realpow_two2 [THEN sym]);
apply (subgoal_tac "(real n + 1) * (real n + 1) * 2 = (real n + 1) *
((real n + 1) * 2)");
apply (erule ssubst);
apply (rule mult_left_mono);
apply auto;
done;

lemma gamma_diff_bigo_one_over_x: "(%x. (gamma -
sumr 0 x (%n. ln (real n + 2) - ln (real n + 1) - 1 / (real n + 1)))) =o
O(%x. 1 / (real x + 1))" (is "(%x. (gamma - sumr 0 x ?f)) =o ?RHS");
proof -;
have "(%x. (gamma - sumr 0 x ?f)) = (%x. suminf (%n. ?f(n + x)))";
apply (rule ext);
apply (subgoal_tac "gamma = sumr 0 x ?f + suminf (%n. ?f(n + x))");
apply (erule ssubst);
apply simp;
apply (unfold gamma_def);
apply (rule suminf_split_initial_segment);
apply (rule gamma_lemma);
done;
also have "… =o O(%x. 2 / (real x + 1))";
apply (subst bigo_minus4);
apply (unfold func_minus);
apply (rule bigo_bounded);
apply (rule allI);
apply (subst suminf_neg [THEN sym]);
apply (rule summable_ignore_initial_segment);
apply (rule gamma_lemma);
apply (subst suminf_zero [THEN sym]);
apply (rule summable_le);
apply (rule allI);
apply (unfold func_minus);
apply (subst ln_successor_diff);
apply simp;
apply (rule summable_zero);
apply (rule summable_neg2);
apply (rule summable_ignore_initial_segment);
apply (rule gamma_lemma);
apply (rule allI);
apply (subst suminf_neg [THEN sym]);
apply (rule summable_ignore_initial_segment);
apply (rule gamma_lemma);
apply (unfold func_minus);
proof -;
fix x;
show "suminf (λn. - (ln (real (n + x) + 2) - ln (real (n + x) + 1) -
1 / (real (n + x) + 1))) ≤ 2 / (real x + 1)" (is "?LHS2 <= ?RHS2");
proof -;
have "?LHS2 <= suminf
(%n. 2 * (1 / ((real (x + n) + 1) * (real (x + n) + 2))))";
apply (rule summable_le);
apply (rule allI);
apply (subst ln_successor_diff);
apply (subgoal_tac "- (ln (1 + 1 / (real (n + x) + 1)) -
1 / (real (n + x) + 1)) <= (1 / (real (n + x) + 1))^2");
prefer 2;
apply (subst minus_le_iff);
apply (subst le_diff_eq);
apply (subgoal_tac "- (1 / (real (n + x) + 1))² + 1 / (real (n + x) + 1) =
1 / (real (n + x) + 1) - (1 / (real (n + x) + 1))²");
apply (erule ssubst);
apply (rule ln_one_plus_pos_lower_bound);
apply force;
apply (rule real_le_mult_imp_div_pos_le);
apply force;
apply force;
apply force;
apply (erule order_trans);
apply (subst real_one_over_pow [THEN sym]);
apply force;
apply (subgoal_tac "1 / (real (n + x) + 1)² =
1 / (real (x + n) + 1)²");
apply (erule ssubst);
apply (rule one_over_n_squared_bound);
apply (rule summable_ignore_initial_segment);
apply (rule summable_neg2);
apply (rule gamma_lemma);
apply (rule summable_const_times);
apply (rule summable_one_over_n_n_plus_one);
done;
also have "… = 2 *
suminf (λn. (1 / ((real (x + n) + 1) * (real (x + n) + 2))))";
apply (rule suminf_const_times);
apply (rule summable_one_over_n_n_plus_one);
done;
also have "suminf (λn. (1 / ((real (x + n) + 1) * (real (x + n) + 2))))
= 1 / (real x + 1)";
by (rule suminf_one_over_n_n_plus_one);
finally; show ?thesis; by simp;
qed;
qed;
also; have "O(%x. 2 / (real x + 1)) = O(%x. 2 * (1 / (real x + 1)))";
by simp;
also have "… = O(%x. 1 / (real x + 1))";
apply (rule bigo_const_mult);
apply force;
done;
finally show ?thesis;.;
qed;

lemma ln_sum_minus2: "sumr 0 x (%n. ln (real n + 2) - ln (real n + 1)) =
ln (real x + 1)";
apply (induct x);
apply simp+;
done;

lemma better_ln_theorem: "(%x. ln(real x + 1)) =o
((%x. sumr 0 x (%n. 1 / (real n + 1))) + (%x. gamma)) +o O(%x. 1 / (real x + 1))";
proof -;
have "- (%x. (gamma - sumr 0 x (%n. ln (real n + 2) -
ln (real n + 1) - 1 / (real n + 1)))) =o
O(%x. 1 / (real x + 1))" (is "?LHS =o ?RHS");
apply (rule bigo_minus);
by (rule gamma_diff_bigo_one_over_x);
also have "?LHS = (%x. sumr 0 x (%n. ln (real n + 2) -
ln (real n + 1) - 1 / (real n + 1))) - (%x. gamma)";
also have "(%x. sumr 0 x (%n. ln (real n + 2) -
ln (real n + 1) - 1 / (real n + 1))) =
(%x. sumr 0 x (%n. ln (real n + 2) -
ln (real n + 1))) - (%x. sumr 0 x (%n. 1 / (real n + 1)))";
sumr_minus);
also have "(%x. sumr 0 x (%n. ln (real n + 2) -
ln (real n + 1))) = (%x. ln(real x + 1))";
apply (rule ext);
apply (subst ln_sum_minus2);
apply (rule refl);
done;
finally; have "(λx. ln (real x + 1)) - (λx. sumr 0 x (λn. 1 / (real n + 1))) -
(λx. gamma) ∈ O(λx. 1 / (real x + 1))" (is "?a ∈ ?B");.;
then have "((λx. sumr 0 x (λn. 1 / (real n + 1))) + (λx. gamma)) + ?a :
((λx. sumr 0 x (λn. 1 / (real n + 1))) + (λx. gamma)) +o ?B";
by (rule set_plus_intro2);
thus ?thesis;
qed;

lemma better_ln_theorem2: "(%x. ln(real x + 1)) =o
((%x. sumr 0 (x+1) (%n. 1 / (real n + 1))) + (%x. gamma)) +o
O(%x. 1 / (real x + 1))" (is "?LHS =o ?RHS");
proof -;
note better_ln_theorem;
also have "((λx. sumr 0 x (λn. 1 / (real n + 1))) + (λx. gamma)) +o
O(λx. 1 / (real x + 1)) = ?RHS" (is "?LHS2 = ?RHS");
proof -;
have "(%x. sumr 0 (x+1) (%n. 1 / (real n + 1))) =
(%x. sumr 0 x (%n. 1 / (real n + 1))) + (%x. 1 / (real x + 1))";
then have "?RHS = ((%x. sumr 0 x (%n. 1 / (real n + 1))) + (%x. gamma))
+o ((%x. (1 / (real x + 1))) +o O(%x. 1 / (real x + 1)))";
also have "(%x. (1 / (real x + 1))) +o O(%x. 1 / (real x + 1)) =
O(%x. 1 / (real x + 1))";
by (rule bigo_plus_absorb, rule bigo_refl);
finally show ?thesis; by (rule sym);
qed;
finally show ?thesis;.;
qed;

end;

```

lemma real_inverse_mult_suc:

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

lemma telescoping_sumr:

```  sumr x (x + y) (%n. 1 / ((real n + 1) * (real n + 2))) =
1 / real (x + 1) - 1 / real (x + y + 1)```

lemma sums_one_over_n_n_plus_one:

`  (%n. 1 / ((real (x + n) + 1) * (real (x + n) + 2))) sums (1 / (real x + 1))`

lemma summable_one_over_n_n_plus_one:

`  summable (%n. 1 / ((real (x + n) + 1) * (real (x + n) + 2)))`

lemma suminf_one_over_n_n_plus_one:

`  suminf (%n. 1 / ((real (x + n) + 1) * (real (x + n) + 2))) = 1 / (real x + 1)`

lemma summable_one_over_n_squared:

`  summable (%n. 1 / (real n + 1)²)`

lemma abs_ln_one_plus_pos_minus_x_bound2:

`  [| 0 ≤ x; x ≤ 1 |] ==> ¦ln (1 + x) - x¦ ≤ x²`

lemma ln_successor_diff:

`  ln (real n + 2) - ln (real n + 1) = ln (1 + 1 / (real n + 1))`

lemma gamma_lemma:

`  summable (%n. ln (real n + 2) - ln (real n + 1) - 1 / (real n + 1))`

lemma gamma_def2:

`  (%n. ln (real n + 2) - ln (real n + 1) - 1 / (real n + 1)) sums gamma`

lemma bigo_minus4:

`  (f ∈ O(g)) = (- f ∈ O(g))`

lemma one_over_n_squared_bound_old:

`  1 / (real n + 1)² ≤ 2 * (1 / (real n + 1) - 1 / (real n + 2))`

lemma one_over_n_squared_bound:

`  1 / (real n + 1)² ≤ 2 * (1 / ((real n + 1) * (real n + 2)))`

lemma gamma_diff_bigo_one_over_x:

```  (%x. gamma -
sumr 0 x (%n. ln (real n + 2) - ln (real n + 1) - 1 / (real n + 1)))
∈ O(%x. 1 / (real x + 1))```

lemma ln_sum_minus2:

`  sumr 0 x (%n. ln (real n + 2) - ln (real n + 1)) = ln (real x + 1)`

lemma better_ln_theorem:

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

lemma better_ln_theorem2:

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