Theory LnSum5

(*  Title:      LnSum5.thy
    Author:     Jeremy Avigad
*)

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)))";
    by (simp add: func_times);
  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))";
    by (simp add: set_times_plus_distribs);
  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)))");
    apply (simp add: func_times);
    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";
    by (simp add: func_times mult_ac);
  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;
    by (simp add: minus_add_distrib diff_minus);
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)";
    by (simp add: set_plus_rearranges plus_ac0);
  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;
    by (simp add: ring_distrib);
  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))";
    by (simp add: set_plus_rearranges plus_ac0);
  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;