(* 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)))