Theory LnSum4

(*  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 (rule real_le_add_order);
    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);
    by (rule add_divide_distrib);
  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)))";
    by (simp add: diff_minus add_ac);
  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;