Theory LnSum1

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

theory LnSum1 = BigO + Ln:

(*  Title:      LnSum1.thy
    Author:     Kevin Donnelly
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
*)

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

theory LnSum1 = BigO + Ln:;

lemma ln_sum_minus: "sumr 0 m (%m. (ln (real (Suc (Suc m))) - ln (real (Suc m)))) = ln (real (Suc m))";
apply (induct m);
by (simp+);

lemma ln_approx_upper: "[| 0 <= x; x <= 1 |] ==> ln((1::real) + x) <= x";
by(auto simp add: ln_add_one_self_le_self);

lemma ln_approx_lower: "[| 0 <= x; x <= 1 |] ==> (x - (x * x)) <= ln((1::real) + x)";
apply(insert ln_one_plus_pos_lower_bound[of x]);
apply(subgoal_tac "2 = Suc (Suc 0)");
by(auto);

lemma ln_sum_div: "sumr 0 m (%m. (ln ((real (Suc (Suc m))) / (real (Suc m))))) = ln (real (Suc m))";
by(auto simp add: ln_sum_minus ln_div);

lemma ln_sum_plus: "sumr 0 m (%m. (ln (1 + 1 / (real (Suc m))))) = ln (real (Suc m))";
apply(subgoal_tac "(%m. ln (1 + 1 / real (Suc m))) = (%m. ln ((real (Suc m)) / (real (Suc m)) + 1 / real (Suc m)))")
apply(erule ssubst);
apply(simp only: add_divide_distrib [THEN sym]);
apply(insert ln_sum_div[of m]);
apply(force simp add: real_of_nat_Suc);
by(simp);

lemma ln_sum_upper: "ln (real (Suc m)) <= sumr 0 m (%m. 1 / (real (Suc m)))";
apply(subst ln_sum_plus[THEN sym]);
apply(rule sumr_le2);
by(auto);

lemma ln_sum_lower: "sumr 0 m (%m. 1 / (real (Suc m))) - sumr 0 m (%m. 1 / (real (Suc m) * real (Suc m))) <= ln (real (Suc m))";
apply(subst ln_sum_plus[THEN sym]);
apply(simp only: sumr_diff);
apply(rule sumr_le2);
apply(rule allI);
apply(rule impI);
apply(subgoal_tac "1 / (real (Suc r) * real (Suc r)) = 1 / (real (Suc r)) * (1 / real (Suc r))", erule ssubst);
apply(rule ln_approx_lower);
apply(auto);
apply(auto simp add: real_divide_def);
apply(subst inverse_1[THEN sym]);
by(auto simp add: real_of_nat_Suc less_imp_inverse_less order_le_less simp del: inverse_1);

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 lnsum_inv_sq_2: "sumr 0 n (%i. 1 / (real (Suc i)) * 1 / (real (Suc i))) <= (2 - (1 / (real n)))";
apply(induct_tac n);
apply(simp); 
apply(case_tac "n <= 0");
apply(subgoal_tac "n = 0");
apply(simp); 
apply(simp);
apply(simp only: linorder_not_le);
apply(simp);
proof -;
  fix n;
  assume "0 < (n::nat)";
  assume "sumr 0 n (%i. 1 / (real (Suc i) * real (Suc i))) <= 2 - 1 / real n";
  have "2 - 1 / real n <= (2 - 1 / real (Suc n))";
    by(auto simp add: real_divide_def real_inverse_le_swap prems);
  then have "sumr 0 n (%i. 1 / (real (Suc i) * real (Suc i))) + 1 / (real (Suc n) * real (Suc n)) <=
 2 - 1 / real n + 1 / (real (Suc n) * real (Suc n))";
    by(auto simp add: prems simp del: sumr.simps);
  also have "... <= 2 - 1 / (real n) + 1 / ((real n) * real (Suc n))";
    by(auto simp add: real_divide_def real_inverse_le_swap prems); 
  also have "... = 2 - 1 / (real n) + 1 / (real n) -  1 / (real (Suc n))";
    by(auto simp add: real_of_nat_Suc prems real_inverse_mult_suc);
  finally show "sumr 0 n (%i. 1 / (real (Suc i) * real (Suc i))) + 1 / (real (Suc n) * real (Suc n)) <=
    2 -  1 / (real (Suc n))";
    by(simp add: prems);
qed;

lemma lnsum_inv_sq_2b: "sumr 0 (Suc n) (%i. 1 / (real (Suc i)) * 1 / (real (Suc i))) <= (2 - (1 / (real (Suc n))))";
apply(induct_tac n);
apply auto;
proof -;
  fix n;
  assume "sumr 0 n (%i. 1 / (real (Suc i) * real (Suc i))) +
         1 / (real (Suc n) * real (Suc n))
         <= 2 - 1 / real (Suc n)"  (is "?lhs <= ?rhs");
  show "?lhs + 1 / (real (Suc (Suc n)) * real (Suc (Suc n)))
             <= 2 - 1 / real (Suc (Suc n))";
  proof -; 
    from prems have "?lhs +  1 / (real (Suc (Suc n)) * real (Suc (Suc n)))
      <= ?rhs + 1 / (real (Suc (Suc n)) * real (Suc (Suc n)))";
      by auto;
    also have "... <= 2 - 1 / real (Suc (Suc n))";
      proof -;
        have "1 / (real (Suc (Suc n)) * real (Suc (Suc n))) <= 
            1 / (real (Suc n) * real (Suc (Suc n)))";
          by (auto simp add: real_divide_def real_inverse_le_swap
             prems real_mult_order);
        also have "... = 1 / (real (Suc n)) - 1 / (real (Suc (Suc n)))";
          apply (simp only: real_of_nat_Suc real_inverse_mult_suc);
          done;
        finally; have "(2 - (1 / real (Suc n)))
            + (1 / (real(Suc (Suc n)) * real(Suc (Suc n)))) <=
          (2 - (1 / real (Suc n))) + (1 / real (Suc n) - 1 / real (Suc (Suc n)))";
          by (rule add_left_mono);
        thus ?thesis; by simp;
      qed;
     finally show ?thesis;.;
  qed;
qed;

lemma lnsum_upper_bigo_1: "(%m. sumr 0 m (%i. 1 / (real (Suc i) * (real (Suc i))))) : O(%x. 1)";
apply(auto simp add: bigo_def simp del: sumr.simps);
apply(rule_tac x = 2 in exI);
apply(rule allI);
apply(auto simp add: abs_if);
apply(subgoal_tac "0 <= sumr 0 x (%i. 1 / (real (Suc i) * real (Suc i)))");
apply(simp);
apply(rule sumr_ge_zero2);
apply(rule allI, rule impI);
apply(simp add: real_divide_def);
proof -;
  fix x      
  have "sumr 0 x (%i. 1 / (real (Suc i) * real (Suc i))) <= 2 - 1 / real x";
    apply (insert lnsum_inv_sq_2);
    by(force);                              
  then show "sumr 0 x (%i. 1 / (real (Suc i) * real (Suc i))) <= 2";
    apply(rule order_trans);
    by(auto simp add: real_divide_def);                              
qed;

lemma lnsum_sumr_bounds: "ALL m. (%m. sumr 0 m (%m. 1 / (real (Suc m)) - 1 / (real (Suc m) * real (Suc m)))) m <= (%m. ln (real (Suc m))) m & (%m. ln (real (Suc m))) m <=  (%m. sumr 0 m (%m. 1 / (real (Suc m)))) m";
apply(rule allI);
by(auto simp add: ln_sum_lower ln_sum_upper sumr_diff[THEN sym]);

lemma lnsum_sumr_bounds2: "ALL m. (%m. sumr 0 m (%m. 1 / (real (Suc m)) - 1 / (real (Suc m) * real (Suc m)))) m <= (%m. ln (real (Suc m))) m & (%m. ln (real (Suc m))) m <= (%m. sumr 0 m (%m. 1 / (real (Suc m)) - 1 / (real (Suc m) * real (Suc m)))) m + (%m. sumr 0 m (%i. 1 / (real (Suc i) * (real (Suc i))))) m";
apply(rule allI);
by(auto simp add: ln_sum_lower ln_sum_upper sumr_diff[THEN sym]);

lemma ln_eq_sum_inverse_bigo_1: "(%m. ln (real (Suc m))) : (% x. sumr 0 x (%m. 1 / (real (Suc m)))) +o O(% x. 1)";
proof -;
  have "(%m. ln (real (Suc m))) =o (%m. sumr 0 m (%m. 1 / (real (Suc m)) - 1 / (real (Suc m) * real (Suc m))))
  +o O(%m. sumr 0 m (%i. 1 / (real (Suc i) * (real (Suc i)))))";
    apply (insert lnsum_sumr_bounds2);
    apply (rule bigo_bounded2);
    apply auto;
    done;
  also have "(%m. sumr 0 m (%m. 1 / (real (Suc m)) - 
      1 / (real (Suc m) * real (Suc m)))) = 
      (%m. sumr 0 m (%m. 1 / (real (Suc m)))) + (- (%m. sumr 0 m (%m. 
        1 / (real (Suc m) * real (Suc m)))))";
    by (simp add: diff_minus func_plus func_minus ext sumr_add
      sumr_minus [THEN sym]);
  also; have "((%m. sumr 0 m (%m. 1 / real (Suc m))) +
     - (%m. sumr 0 m (%m. 1 / (real (Suc m) * real (Suc m))))) +o
    O(%m. sumr 0 m (%i. 1 / (real (Suc i) * real (Suc i)))) = 
      (%m. sumr 0 m (%m. 1 / real (Suc m))) +o 
     (- (%m. sumr 0 m (%m. 1 / (real (Suc m) * real (Suc m)))) +o
      O(%m. sumr 0 m (%i. 1 / (real (Suc i) * real (Suc i)))))";
    by (simp add: set_plus_rearranges);
  also; have "(%m. sumr 0 m (%m. 1 / real (Suc m))) +o
    (- (%m. sumr 0 m (%m. 1 / (real (Suc m) * real (Suc m)))) +o
     O(%m. sumr 0 m (%i. 1 / (real (Suc i) * real (Suc i))))) <=
    (%m. sumr 0 m (%m. 1 / real (Suc m))) +o O(%m.1)";
    proof (rule set_plus_mono);
      have "- (%m. sumr 0 m (%m. 1 / (real (Suc m) * real (Suc m)))) +o
        O(%m. sumr 0 m (%i. 1 / (real (Suc i) * real (Suc i)))) =
        O(%m. sumr 0 m (%i. 1 / (real (Suc i) * real (Suc i))))";
        apply (subst bigo_plus_absorb);
        apply auto;
        done;
      also have "... <= O(%m.1)";
        apply (rule bigo_elt_subset);
        apply (rule lnsum_upper_bigo_1);
        done;
       finally show "- (%m. sumr 0 m (%m. 1 / (real (Suc m) * real (Suc m)))) 
         +o O(%m. sumr 0 m (%i. 1 / (real (Suc i) * real (Suc i))))
         <= O(%m. 1)";.;
     qed;
  finally; show ?thesis;.;
qed;

lemma sum_inverse_eq_ln_1: "(λx. sumr 0 x (λi. 1 / (real (Suc i))))
  \<elteqo> (λn. ln (real (Suc n))) \<pluso> O(λx. 1)";
by(simp only: ln_eq_sum_inverse_bigo_1 bigo_add_commute_imp);

lemma sum_inverse_bigo_ln: "(λx. sumr 0 x (λi. 1 / (real (Suc i)))) \<elteqo> 
  O(λn. ln (real (Suc n)))";
apply(insert sum_inverse_eq_ln_1);
apply(auto simp add: bigo_def bigo_pos_const elt_set_plus_def func_plus);
apply(rule_tac x = "1 + (c / (ln 2))" in exI);
apply(rule allI);
apply (case_tac x);
apply force;
apply (erule ssubst);
apply (simp add: ring_distrib);
apply (rule order_trans);
apply (rule abs_triangle_ineq);
apply simp;
apply (rule order_trans);
apply (erule spec);
apply (rule real_mult_le_imp_le_div_pos);
apply force;
apply (rule mult_left_mono);
apply (subst ln_le_cancel_iff);
apply auto;
apply (rule order_trans);
prefer 2;
apply (erule spec);
apply force;
done;

end;

lemma ln_sum_minus:

  sumr 0 m (%m. ln (real (Suc (Suc m))) - ln (real (Suc m))) = ln (real (Suc m))

lemma ln_approx_upper:

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

lemma ln_approx_lower:

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

lemma ln_sum_div:

  sumr 0 m (%m. ln (real (Suc (Suc m)) / real (Suc m))) = ln (real (Suc m))

lemma ln_sum_plus:

  sumr 0 m (%m. ln (1 + 1 / real (Suc m))) = ln (real (Suc m))

lemma ln_sum_upper:

  ln (real (Suc m)) ≤ sumr 0 m (%m. 1 / real (Suc m))

lemma ln_sum_lower:

  sumr 0 m (%m. 1 / real (Suc m)) -
  sumr 0 m (%m. 1 / (real (Suc m) * real (Suc m)))
  ≤ ln (real (Suc m))

lemma real_inverse_mult_suc:

  0 < k ==> 1 / (k * (k + 1)) = 1 / k - 1 / (k + 1)

lemma lnsum_inv_sq_2:

  sumr 0 n (%i. 1 / real (Suc i) * 1 / real (Suc i)) ≤ 2 - 1 / real n

lemma lnsum_inv_sq_2b:

  sumr 0 (Suc n) (%i. 1 / real (Suc i) * 1 / real (Suc i)) ≤ 2 - 1 / real (Suc n)

lemma lnsum_upper_bigo_1:

  (%m. sumr 0 m (%i. 1 / (real (Suc i) * real (Suc i)))) ∈ O(%x. 1)

lemma lnsum_sumr_bounds:

m. sumr 0 m (%m. 1 / real (Suc m) - 1 / (real (Suc m) * real (Suc m)))
      ≤ ln (real (Suc m)) ∧
      ln (real (Suc m)) ≤ sumr 0 m (%m. 1 / real (Suc m))

lemma lnsum_sumr_bounds2:

m. sumr 0 m (%m. 1 / real (Suc m) - 1 / (real (Suc m) * real (Suc m)))
      ≤ ln (real (Suc m)) ∧
      ln (real (Suc m))
      ≤ sumr 0 m (%m. 1 / real (Suc m) - 1 / (real (Suc m) * real (Suc m))) +
        sumr 0 m (%i. 1 / (real (Suc i) * real (Suc i)))

lemma ln_eq_sum_inverse_bigo_1:

  (%m. ln (real (Suc m))) ∈ (%x. sumr 0 x (%m. 1 / real (Suc m))) + O(%x. 1)

lemma sum_inverse_eq_ln_1:

  (%x. sumr 0 x (%i. 1 / real (Suc i))) ∈ (%n. ln (real (Suc n))) + O(%x. 1)

lemma sum_inverse_bigo_ln:

  (%x. sumr 0 x (%i. 1 / real (Suc i))) ∈ O(%n. ln (real (Suc n)))