# Theory LnSum2

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

theory LnSum2 = LnSum1:

(*  Title:      LnSum2.thy
Author:     Kevin Donnelly
*)

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

theory LnSum2 = LnSum1:;

lemma inverse_func_pos: "ALL x::nat. 0 <= 1 / (real (Suc x))";
apply auto;
done;

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

lemma abs_ln_one_plus_pos_minus_x_bound2: "[| 0 <= x; x <= 1 |] ==>
abs (ln (1 + x) - x) <= x ^ 2";
apply (subgoal_tac "x ^ 2 = abs(x ^ 2)");
apply (erule ssubst);
apply (rule abs_ln_one_plus_pos_minus_x_bound);
apply auto;
done;

lemma ln_1_plus_small: "(%n::nat. ln (1 + (1 / (real (n + 1))))) ∈ (%n::nat. 1 / (real (n + 1))) +o
O(%n::nat. 1 / ((real (n + 1)) * (real (n + 1))))";
apply simp;
apply (rule set_minus_imp_plus);
apply (unfold bigo_def);
apply simp;
apply (rule_tac x = 1 in exI);
apply (clarsimp);
apply (subgoal_tac "1 / (real (Suc x) * real (Suc x)) = (1 / real (Suc x))^2");
apply (simp only: func_diff_minus);
apply (rule abs_ln_one_plus_pos_minus_x_bound2);
apply auto;
proof -;
fix x;
show "1 / real(Suc x) <= 1";
proof -;
have "1 <= Suc x";
by auto;
then have "inverse(real(Suc x)) <= 1";
by (rule real_inverse_nat_le_one);
thus "1 / real(Suc x) <= 1";
qed;
next;
fix x;
show "1 / (real (Suc x) * real (Suc x)) = (1 / real (Suc x)) ^ 2";
proof -;
have "1 / (real(Suc x) * real (Suc x)) = (1 / real(Suc x)) * (1 / real(Suc x))";
by simp;
also have "... = (1 / real(Suc x))^2";
by (rule realpow_two2);
finally show ?thesis;.;
qed;
qed;

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

lemma xlnx_sum: "sumr 0 m  (%n. (real (n + 2)) * (ln (real (n + 2))) -
(real (n + 1)) * (ln (real (n + 1)))) = ((real (m + 1)) * (ln (real (m + 1))))";
apply(induct_tac m);
by(simp_all);

lemma xlnx_sum_plus: "sumr 0 m  (%n. (ln (real (n + 2))) +
(real (n + 1)) * ((ln (real (n + 2))) - (ln (real (n + 1))))) = ((real (m + 1)) * (ln (real (m + 1))))";
apply(subgoal_tac "(%n. ln (real ((n::nat) + 2)) + real (n + 1) * (ln (real (n + 2)) - ln (real (n + 1)))) =
(%n. (real (n + 2)) * (ln (real (n + 2))) - (real (n + 1)) * (ln (real (n + 1))))");
apply(erule ssubst);
apply(simp only: xlnx_sum);
apply(rule ext);
apply(subgoal_tac "ln (real (Suc (Suc n))) + real (Suc n) * ln (real (Suc (Suc n))) =
1 *  ln (real (Suc (Suc n))) + real (Suc n) * ln (real (Suc (Suc n)))");
apply(erule ssubst);
by(simp);

lemma xlnx_sum_split1: "sumr 0 m  (%n. (ln (real (n + 2)))) + sumr 0 m (%n. (real (n + 1)) * (ln (1 + 1 / (real (n + 1))))) = ((real (m + 1)) * (ln (real (m + 1))))";
apply(subgoal_tac "sumr 0 m (%n. ln (real (n + 2))) +
sumr 0 m (%n. real (n + 1) * ln (1 + 1 / real (n + 1))) =
sumr 0 m  (%n. (ln (real (n + 2))) +
(real (n + 1)) * ((ln (real (n + 2))) - (ln (real (n + 1)))))");
apply(erule ssubst);
apply(simp only: xlnx_sum_plus);
apply(subgoal_tac "(%n. ln (real (Suc (Suc n))) + real (Suc n) * ln (1 + 1 / real (Suc n))) =
(%n. ln (real (Suc (Suc n))) +
real (Suc n) * (ln (real (Suc (Suc n))) - ln (real (Suc n))))");
apply(erule ssubst, simp);
apply(rule ext,simp);
apply(subgoal_tac "ln (1 + 1 / real (Suc n)) = (ln (real (Suc (Suc n))) - ln (real (Suc n)))");
apply(erule ssubst, simp);
apply(subgoal_tac "ln (real (Suc (Suc n))) - ln (real (Suc n)) = ln (real (Suc (Suc n)) / (real (Suc n)))");
apply(simp);
apply(subgoal_tac "real (Suc (Suc n)) = real (Suc n) + 1");
apply(simp only: real_of_nat_Suc);

lemma xlnx_sum_split2: "sumr 0 m  (%n. (ln (real (n + 2)))) + sumr 0 m (%n. (real (n + 1)) * (1 / (real (n + 1)) + (ln (1 + 1 / (real (n + 1)))) - 1 / (real (n + 1)))) = ((real (m + 1)) * (ln (real (m + 1))))";
apply(subgoal_tac "sumr 0 m  (%n. (ln (real (n + 2)))) + sumr 0 m (%n. (real (n + 1)) * (1 / (real (n + 1)) + (ln (1 + 1 / (real (n + 1)))) - 1 / (real (n + 1)))) =
sumr 0 m  (%n. (ln (real (n + 2)))) + sumr 0 m (%n. (real (n + 1)) * (ln (1 + 1 / (real (n + 1)))))");
apply(erule ssubst, simp only: xlnx_sum_split1);
by(simp);

lemma xlnx_sum_split3: "sumr 0 m  (%n. (ln (real (n + 2)))) + (real m) + sumr 0 m (%n. (real (n + 1)) * (ln (1 + 1 / (real (n + 1))) - 1 / (real (n + 1)))) = ((real (m + 1)) * (ln (real (m + 1))))";
apply(subgoal_tac "sumr 0 m (%n. ln (real (n + 2))) + real m +
sumr 0 m (%n. real (n + 1) * (ln (1 + 1 / real (n + 1)) - 1 / real (n + 1))) =
sumr 0 m  (%n. (ln (real (n + 2)))) + sumr 0 m (%n. (real (n + 1)) * (1 / (real (n + 1)) + (ln (1 + 1 / (real (n + 1)))) - 1 / (real (n + 1))))");
apply(erule ssubst, simp only: xlnx_sum_split2);
by(simp);

lemma ln_1_plus_small_minus: "(%n::nat. ln (1 + (1 / (real (n + 1)))) - 1 / (real (n + 1))) ∈
O(%n::nat. 1 / ((real (n + 1)) * (real (n + 1))))";
apply(insert ln_1_plus_small);
apply(auto);
apply(rule_tac x = c in exI);
apply(rule allI);
apply(erule_tac x = x in allE);
apply(erule ssubst);
apply (subgoal_tac "- b x <= abs (b x)");
apply (erule order_trans);
apply assumption;
apply (rule abs_ge_minus_self);
done;

lemma xln_1_plus_small_minus: "(%n::nat. (real (n + 1)) * (ln (1 + (1 / (real (n + 1)))) -
1 / (real (n + 1)))) \<elteqo> O(%n::nat. 1 / (real (n + 1)))";
apply(subgoal_tac "(%n::nat. (real (n + 1)) * (ln (1 + (1 / (real (n + 1)))) -
1 / (real (n + 1)))) = (%n::nat. (real (n + 1))) * (%n. (ln (1 + (1 / (real (n + 1)))) -
1 / (real (n + 1))))");
apply(erule ssubst);
proof -;
have 1: "(%n::nat. real (n + 1)) \<elteqo> O(%n::nat. real (n + 1))" by (simp add: bigo_refl);
also have "(%n::nat. ln (1 + 1 / real (n + 1)) - 1 / real (n + 1)) \<elteqo> O(%n::nat. 1 / ((real (n + 1)) * (real (n + 1))))"; by (simp only: ln_1_plus_small_minus);
ultimately have "(%n. real (n + 1)) *
(%n. ln (1 + 1 / real (n + 1)) - 1 / real (n + 1)) \<elteqo> O((%n. real (n + 1)) * (%n::nat. 1 / ((real (n + 1)) * (real (n + 1)))))";
then show "(%n::nat. real (n + 1)) *
(%n. ln (1 + 1 / real (n + 1)) - 1 / real (n + 1)) \<elteqo> O(%n. 1 / real (n + 1))";
next;
show "(%n. real (n + 1) * (ln (1 + 1 / real (n + 1)) - 1 / real (n + 1))) =
(%n. real (n + 1)) * (%n. ln (1 + 1 / real (n + 1)) - 1 / real (n + 1))"
qed;

lemma xlnx_sum_snd_bigo: "(%m. sumr 0 m (%n. (real (n + 1)) * (ln (1 + 1 / (real (n + 1))) - 1 / (real (n + 1))))) \<elteqo> O(%m. sumr 0 m (%n::nat. 1 / (real (n + 1))))";
apply(simp);
apply(rule bigo_sumr_pos);
by(insert xln_1_plus_small_minus,simp);

lemma fn_xlnx_sum_split3: "(%m. sumr 0 m  (%n. (ln (real (n + 2))))) + (%m. (real m)) + (%m. sumr 0 m (%n. (real (n + 1)) * (ln (1 + 1 / (real (n + 1))) - 1 / (real (n + 1))))) = (%m. ((real (m + 1)) * (ln (real (m + 1)))))";
apply(simp only: func_plus);
by(rule ext, simp only: xlnx_sum_split3);

lemma fn_lnx_sum: "(%m. sumr 0 m  (%n. (ln (real (n + 2))))) = (%m. ((real (m + 1)) * (ln (real (m + 1))))) - (%m. (real m)) - (%m. sumr 0 m (%n. (real (n + 1)) * (ln (1 + 1 / (real (n + 1))) - 1 / (real (n + 1)))))";
apply(insert fn_xlnx_sum_split3);
proof -;
assume "(%m. sumr 0 m (%n. ln (real (n + 2)))) + real +
(%m. sumr 0 m (%n. real (n + 1) * (ln (1 + 1 / real (n + 1)) - 1 / real (n + 1)))) =
(%m. real (m + 1) * ln (real (m + 1)))";
have "(%m. sumr 0 m (%n. ln (real (n + 2)))) + real +
(%m. sumr 0 m (%n. real (n + 1) * (ln (1 + 1 / real (n + 1)) - 1 / real (n + 1)))) + - real =
(%m. real (m + 1) * ln (real (m + 1))) + - real";
apply(subst prems);
by(simp);
then have "(%m. sumr 0 m (%n. ln (real (n + 2)))) + real +
(%m. sumr 0 m (%n. real (n + 1) * (ln (1 + 1 / real (n + 1)) - 1 / real (n + 1)))) + - real + - (%m. sumr 0 m (%n. real (n + 1) * (ln (1 + 1 / real (n + 1)) - 1 / real (n + 1)))) =  (%m. real (m + 1) * ln (real (m + 1))) + - real + - (%m. sumr 0 m (%n. real (n + 1) * (ln (1 + 1 / real (n + 1)) - 1 / real (n + 1))))";
by(simp);
then show ?thesis;
apply(simp);
apply(rule ext);
apply(simp only: expand_fun_eq func_diff_minus);
apply(erule_tac x = m in allE);
by(simp);
qed;

lemma fn_lnx_sum_bigo: "(%m. sumr 0 m  (%n. (ln (real (n + 2))))) \<elteqo> ((%m. ((real (m + 1)) * (ln (real (m + 1))))) - (%m. (real m))) +o O(%m. sumr 0 m (%n::nat. 1 / (real (n + 1))))";
apply(subst fn_lnx_sum);
apply(rule_tac x = "- (%m. sumr 0 m (%n. real (Suc n) * (ln (1 + 1 / real (Suc n)) - 1 / real (Suc n))))" in bexI);
apply(rule ext);
apply(insert xlnx_sum_snd_bigo);
by auto;

lemma xlnx_sum_snd_bigo_ln: "(%m. sumr 0 m (%n. (real (n + 1)) * (ln (1 + 1 / (real (n + 1))) - 1 / (real (n + 1))))) \<elteqo> O(%n::nat. ln (real (n + 1)))";
apply(insert xlnx_sum_snd_bigo);
apply(insert sum_inverse_bigo_ln);
apply(simp only: bigo_def bigo_pos_const elt_set_plus_def);
apply(auto simp add: bigo_def bigo_pos_const elt_set_plus_def);
(* apply(simp only: bigo_pos_const[THEN sym]); *)
apply(rule_tac x = "c * ca" in exI);
apply auto;
apply (elim mult_pos);
apply assumption;
apply(erule_tac x = x in allE);
apply(erule order_trans);
apply(erule_tac x = x in allE);
apply(simp only: mult_assoc);
by(simp);

lemma fn_lnx_sum_bigo_ln: "(%m. sumr 0 m  (%n. (ln (real (n + 2))))) \<elteqo> ((%m. ((real (m + 1)) * (ln (real (m + 1))))) - (%m. (real m))) +o O(%n::nat. ln (real (n + 1)))";
apply(subst fn_lnx_sum);
apply(rule_tac x = "- (%m. sumr 0 m (%n. real (Suc n) * (ln (1 + 1 / real (Suc n)) - 1 / real (Suc n))))" in bexI);
apply(rule ext);
apply(insert xlnx_sum_snd_bigo_ln);
by auto;

lemma fn_lnx_sum_bigo_ln2: "(λm. sumr 0 (Suc m) (λn. ln (real (Suc n))))
\<elteqo> ((λm. ((real (m + 1)) * (ln (real (m + 1))))) - (λm. (real m)))
\<pluso> O(λn::nat. ln (real (n + 1)))";
proof -;
have "(%m. sumr 0 (Suc m)  (%n. (ln (real (Suc n))))) =
(%m. sumr 0 m  (%n. (ln (real (n + 2)))))";
apply(rule ext);
apply(induct_tac m);
by(auto);
then show ?thesis by (auto simp only: fn_lnx_sum_bigo_ln);
qed;

end

lemma inverse_func_pos:

x. 0 ≤ 1 / real (Suc x)

lemma abs_ln_one_plus_pos_minus_x_bound2:

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

lemma ln_1_plus_small:

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

lemma xlnx_sum:

sumr 0 m
(%n. real (n + 2) * ln (real (n + 2)) - real (n + 1) * ln (real (n + 1))) =
real (m + 1) * ln (real (m + 1))

lemma xlnx_sum_plus:

sumr 0 m
(%n. ln (real (n + 2)) +
real (n + 1) * (ln (real (n + 2)) - ln (real (n + 1)))) =
real (m + 1) * ln (real (m + 1))

lemma xlnx_sum_split1:

sumr 0 m (%n. ln (real (n + 2))) +
sumr 0 m (%n. real (n + 1) * ln (1 + 1 / real (n + 1))) =
real (m + 1) * ln (real (m + 1))

lemma xlnx_sum_split2:

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

lemma xlnx_sum_split3:

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

lemma ln_1_plus_small_minus:

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

lemma xln_1_plus_small_minus:

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

lemma xlnx_sum_snd_bigo:

(%m. sumr 0 m
(%n. real (n + 1) * (ln (1 + 1 / real (n + 1)) - 1 / real (n + 1))))
∈ O(%m. sumr 0 m (%n. 1 / real (n + 1)))

lemma fn_xlnx_sum_split3:

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

lemma fn_lnx_sum:

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

lemma fn_lnx_sum_bigo:

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

lemma xlnx_sum_snd_bigo_ln:

(%m. sumr 0 m
(%n. real (n + 1) * (ln (1 + 1 / real (n + 1)) - 1 / real (n + 1))))
∈ O(%n. ln (real (n + 1)))

lemma fn_lnx_sum_bigo_ln:

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

lemma fn_lnx_sum_bigo_ln2:

(%m. sumr 0 (Suc m) (%n. ln (real (Suc n))))
∈ ((%m. real (m + 1) * ln (real (m + 1))) - real) + O(%n. ln (real (n + 1)))