Theory LnSum1a

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

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(auto simp add: diff_minus); 
  apply(simp only: minus_divide_left);
  apply (simp only: real_frac_add);
  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)))";
      by (simp add: ih);
    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";
          by (auto simp add: prems);
        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";
    by (rule ln_add_one_self_le_self);
  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 (simp add: nonzero_divide_eq_eq ring_distrib);
  apply (subst add_divide_distrib [THEN sym]);
  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 (simp add: add_ac);
            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)";
    by (simp add: func_minus diff_minus func_plus add_ac); 
  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)))";
    by (simp add: diff_minus func_minus func_plus add_ac sumr_add [THEN sym]
      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;
    by (simp add: set_plus_rearranges add_ac compare_rls);
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))";
      by (simp add: func_plus);
    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)))";
      by (elim ssubst, simp add: set_plus_rearranges add_ac);
    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;