# Theory LnSum1

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

theory LnSum1 = BigO + Ln:

```(*  Title:      LnSum1.thy
Author:     Kevin Donnelly
*)

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";

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))";

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(insert ln_sum_div[of m]);
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(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(simp only: minus_divide_left);
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))";
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)))";
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(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);
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);
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)))))";
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)))))";
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)";

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