Theory LnSum2

(*  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";
      by (simp add: real_divide_def);
  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(auto simp add: plus_ac0 diff_minus right_distrib left_distrib add_assoc);
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);
apply(simp only: real_add_mult_distrib[THEN sym]);
apply(simp add: real_of_nat_Suc);
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(simp add: sumr_add);
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 add: add_divide_distrib);
apply(simp only: real_of_nat_Suc);
by(auto simp add: ln_div);

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);
apply(simp add: diff_minus right_distrib);
apply(simp only: sumr_add[THEN sym]);
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(simp add: bigo_def elt_set_plus_def);
apply(auto);
apply(rule_tac x = c in exI);
apply(rule allI);
apply(erule_tac x = x in allE);
apply(erule ssubst);
apply (auto simp add: func_plus);
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)))))";
    by(auto simp add: bigo_mult3);
  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))";
    by(simp add: func_times);
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))"
    by (simp add: func_times);
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);
apply(simp add: inverse_func_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(simp add: func_plus func_diff_minus);
    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(auto simp add: elt_set_plus_def);
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(simp add: func_diff_minus func_plus func_minus);
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(auto simp add: elt_set_plus_def);
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(simp add: func_diff_minus func_plus func_minus);
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