(* Title: Error.thy
Author: Jeremy Avigad
*)
header {* Estimates on the error term *}
theory Error = Selberg:;
declare One_nat_def [simp del];
constdefs
R :: "real => real"
"R x == psi (natfloor x) - x";
lemma R_alt_def: "psi (natfloor x) = x + R x";
by (simp add: R_def);
lemma R_alt_def2: "psi (natfloor x) = R x + x";
by (simp add: R_def);
lemma R_alt_def3: "psi n = real n + R (real n)";
by (simp add: R_def);
lemma R_alt_def4: "psi n = R (real n) + real n";
by (simp add: R_def);
lemma R_bound_imp_PNT: "ALL epsilon. (0 < epsilon -->
(EX z. ALL x. (z <= x --> abs (R x) < epsilon * x))) ==>
(%x. psi x / (real x)) ----> 1";
apply (unfold LIMSEQ_def);
apply clarsimp;
apply (drule_tac x = r in spec);
apply clarsimp;
apply (rule_tac x = "natfloor z + 1" in exI);
apply clarify;
apply (drule_tac x = "real n" in spec);
apply (unfold R_def);
apply (subgoal_tac "z <= real n");
apply (clarsimp simp del: One_nat_def);
apply (subgoal_tac "abs (psi n - real n) / real n < r");
prefer 2;
apply (subst pos_divide_less_eq);
apply arith;
apply assumption;
apply (subgoal_tac "abs (psi n - real n) / real n =
abs(psi n / real n + -1)");
apply (erule subst);
apply assumption;
apply (subst abs_div_pos);
apply force;
apply (rule arg_cong);back;
apply (simp add: ring_eq_simps diff_divide_distrib);
apply (rule order_less_imp_le);
apply (erule ge_natfloor_plus_one_imp_gt);
done;
lemma aux: "f + g =o h +o O(k::'a=>'b::ordered_ring) ==>
g =o l +o O(k) ==> f + l =o h +o O(k)";
apply (rule set_minus_imp_plus);
apply (drule set_plus_imp_minus)+;
apply (drule bigo_minus);back;
apply (drule bigo_add_useful);
apply assumption;
apply (subgoal_tac "f + g - h + - (g - l) = f + l - h");
apply (erule subst);
apply assumption;
apply (simp add: ring_eq_simps compare_rls minus_diff_eq);
done;
lemma error0: "R =o O(%x. abs x)";
apply (subgoal_tac "R = (%x. psi (natfloor x)) + (%x. - x)");
apply (erule ssubst);
apply (subst bigo_plus_idemp [THEN sym]);
apply (rule set_plus_intro);
apply (rule subsetD);
apply (subgoal_tac "O(%x. real(natfloor x)) <= O(%x. abs x)");
apply assumption;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (case_tac "0 <= x");
apply simp;
apply (erule real_natfloor_le);
apply (rule order_trans);
prefer 2;
apply (rule abs_ge_zero);
apply (subst natfloor_neg);
apply simp;
apply simp;
apply (rule bigo_compose1);
apply (rule psi_bigo);
apply (unfold bigo_def);
apply auto;
apply (rule_tac x = 1 in exI);
apply auto;
apply (rule ext);
apply (subst func_plus);
apply (subst diff_minus [THEN sym]);
apply (simp add: R_def);
done;
lemma R_zero [simp]: "R 0 = 0";
apply (unfold R_def);
apply (simp add: psi_zero);
done;
lemma error1: "(%x. ∑ n = 1..natfloor (abs x).
R (real n) / (real n * real (n + 1))) =o O(%x. 1)";
proof -;
have "(%x. ∑n = 1..natfloor (abs x) + 1. Lambda n / (real n)) =
(%x.∑n=1..natfloor(abs x) + 1. (1 / real n) * (psi n - psi (n - 1)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst psi_diff2);
apply force;
apply simp;
done;
also have "... = (%x. ∑ n = 1..natfloor (abs x) + 1. 1 / real n) +
(%x. ∑ n = 1..natfloor (abs x) + 1. 1 / real n *
(R(real n) - R(real (n - 1))))";
apply (subst func_plus);
apply (rule ext);
apply (subst setsum_addf [THEN sym]);
apply (rule setsum_cong2);
apply (subst R_alt_def3)+;
apply (subst real_of_nat_diff);
apply force;
apply (simp add: ring_eq_simps);
done;
also have "(%x. ∑ n = 1..natfloor (abs x) + 1.
1 / real n * (R (real n) - R (real (n - 1))))
= (%x. R (real (natfloor (abs x) + 1)) / real (natfloor (abs x) + 1)) +
(%x. (∑ n = 1..natfloor (abs x).
R (real n) * (1 / real n - 1 / real (n + 1))))";
apply (subst func_plus);
apply (rule ext);
apply (subst another_partial_sum);
apply simp;
done;
also have "(%x. ∑ n = 1..natfloor (abs x).
R (real n) * (1 / real n - 1 / real (n + 1))) =
(%x. ∑ n = 1..natfloor (abs x).
R (real n) / ((real n) * (real (n + 1))))";
apply (rule ext);
apply (rule setsum_cong2);
apply (simp add: right_diff_distrib);
apply (subst diff_frac_eq);
apply (auto simp add: ring_eq_simps);
done;
also have "
(%x. R (real (natfloor (abs x) + 1)) / real (natfloor (abs x) + 1)) =
(%x. 1 / (real (natfloor (abs x) + 1))) *
(%x. R(real(natfloor(abs x) + 1)))";
by (simp add: func_times);
finally have "(%x. ∑ n = 1..natfloor (abs x).
R (real n) / (real n * real (n + 1))) =
(%x. ∑ n = 1..natfloor (abs x) + 1. Lambda n / real n) +
- (%x. ∑ n = 1..natfloor (abs x) + 1. 1 / real n) +
- ((%x. 1 / (real (natfloor (abs x) + 1))) *
(%x. R(real(natfloor(abs x) + 1))))";
by (simp add: compare_rls);
also have "... =o
((%x. ln(abs x + 1)) +o O(%x. 1)) +
(- 1) *o ((%x. ln(abs x + 1)) +o O(%x. 1)) +
(- 1) *o (O(%x. 1 / (abs x + 1)) * (O(%x. abs x + 1) + O(%x. abs x + 1)))";
apply (rule set_plus_intro);
apply (rule set_plus_intro);
apply (rule Mertens_theorem_real2);
apply (rule set_neg_intro2);
apply (rule bigo_add_commute_imp);
apply (rule ln_sum_real2);
apply (rule set_neg_intro2);
apply (rule set_times_intro);
apply (rule one_over_natfloor_one_over_bigo);
apply (unfold R_def);
apply (subgoal_tac "(%x. psi (natfloor (real (natfloor (abs x) + 1))) -
real (natfloor (abs x) + 1)) = (%x. psi(natfloor (abs x) + 1)) +
- (%x. real(natfloor(abs x) + 1))");
apply (erule ssubst);
apply (rule set_plus_intro);
apply (rule set_mp);
prefer 2;
apply (rule bigo_compose1);back;
apply (rule psi_bigo);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply clarsimp;
apply (rule real_natfloor_le);
apply force;
apply (rule bigo_minus);
apply (rule bigo_bounded);
apply force;
apply clarsimp;
apply (rule real_natfloor_le);
apply force;
apply (simp add: func_minus func_plus);
apply (rule ext);
apply (simp add: ring_eq_simps compare_rls);
done;
also have "... <= O(%x. 1)";
apply (simp add: set_times_plus_distribs set_plus_rearranges);
apply (rule subset_trans);
prefer 2;
apply (subgoal_tac "O(%x. 1) + O(%x. 1) + O(%x. 1) <= O(%x. 1)");
apply assumption;
apply simp;
apply (rule set_plus_mono2)+;
apply simp;
apply (simp add: func_one func_minus);
apply (rule subset_trans);
apply (subgoal_tac "?t <= (- 1) *o O(%x. 1)");
apply assumption;
apply (rule set_times_mono);
apply (rule subset_trans);
apply (rule bigo_mult);
apply (simp add: func_times);
apply (rule bigo_elt_subset);
apply (subgoal_tac "(%x. (abs x + 1) / (abs x + 1)) = (%x. 1)");
apply (erule ssubst);
apply (rule bigo_refl);
apply (rule ext);
apply simp;
apply arith;
apply (simp add: func_one func_minus);
done;
finally show ?thesis;.;
qed;
lemma sum_lambda_n_ln_n_over_n_bigo:
"(%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) / real n) =o
(%x. ln (abs x + 1) ^ 2 / 2) +o O(%x. 1 + ln (abs x + 1))";
proof -;
have "(%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) / real n) =
((%x. (ln (abs x + 1))) * (%x. (∑ n = 1..natfloor (abs x) + 1.
Lambda n / real n))) +
((%x. - 1) * (%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n / real n * ln((abs x + 1) / real n)))";
apply (simp add: func_plus func_times);
apply (rule ext);
apply (subst setsum_const_times [THEN sym]);
apply (subst setsum_negf' [THEN sym]);
apply (subst setsum_addf [THEN sym]);
apply (rule setsum_cong2);
apply (subst ln_div);
apply arith;
apply force;
apply (simp add: ring_eq_simps diff_divide_distrib);
done;
also have "... =o
((%x. ln(abs x + 1)) *o ((%x. ln (abs x + 1)) +o O(%x. 1))) +
((%x. - 1) *o
((%x. ln (abs x + 1) ^ 2 / 2) +o O(%x. 1 + ln (abs x + 1))))";
apply (rule set_plus_intro);
apply (rule set_times_intro2);
apply (rule Mertens_theorem_real2);
apply (rule set_times_intro2);
apply (rule sum_lambda_m_over_m_ln_x_over_m_bigo);
done;
also have "... =
(%x. ln(abs x + 1)^2 / 2) +o ((%x. ln(abs x + 1)) *o O(%x. 1) +
O(%x. 1 + ln(abs x + 1)))";
by (simp add: set_plus_rearranges plus_ac0 set_times_plus_distribs
func_times func_plus power2_eq_square ring_eq_simps
compare_rls);
also have "... <= (%x. ln(abs x + 1)^2 / 2) +o O(%x. 1 + ln(abs x + 1))";
apply (rule set_plus_mono);
apply (subst bigo_plus_idemp [THEN sym]);back;
apply (rule set_plus_mono2);
apply (rule order_trans);
apply (rule bigo_mult2);
apply (simp add: func_times);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply auto;
done;
finally show ?thesis;.;
qed;
lemma error2: " (%x. R (abs x + 1) * ln (abs x + 1) ^ 2) +
(%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * R ((abs x + 1) / real n))) =o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
proof -;
have "(%x. psi (natfloor (abs x) + 1) * ln (abs x + 1)) +
(%x. ∑ n = 1..natfloor (abs x) + 1.
∑ u | u dvd n. Lambda u * Lambda (n div u))
=o (%x. 2 * (abs x + 1) * ln (abs x + 1)) +o O(%x. abs x + 1)"
(is "?LHS1 + ?LHS2 =o ?RHS1 +o ?RHS2");
by (rule Selberg4);
then have "(%x. ln (abs x + 1)) * (?LHS1 + ?LHS2) =o
(%x. ln(abs x + 1)) *o (?RHS1 +o ?RHS2)";
by (rule set_times_intro2);
then have "(%x. ln (abs x + 1)) * ?LHS1 +
(%x. ln(abs x + 1)) * ?LHS2 =o
(%x. ln (abs x + 1)) * ?RHS1 +o
(%x. ln(abs x + 1)) *o ?RHS2";
by (simp add: ring_distrib set_times_plus_distribs);
also have "... <= (%x. ln (abs x + 1)) * ?RHS1 +o
O(%x. ln(abs x + 1) * (abs x + 1))";
apply (rule set_plus_mono);
apply (rule subset_trans);
apply (rule bigo_mult2);
apply (simp add: func_times);
done;
also have "... <= (%x. ln (abs x + 1)) * ?RHS1 +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
apply (rule set_plus_mono);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule nonneg_times_nonneg);
apply force;
apply arith;
apply (rule allI);
apply (simp add: ring_eq_simps compare_rls);
apply arith;
done;
also have "(%x. ln (abs x + 1)) * ?LHS1 = (%x. psi(natfloor(abs x) + 1) *
(ln (abs x + 1))^2)";
by (simp add: func_times mult_ac power2_eq_square);
also have "(%x. ln (abs x + 1)) * ?LHS2 = (%x. ln(abs x + 1) *
(∑ n = 1..natfloor (abs x) + 1.
∑ u | u dvd n. Lambda u * Lambda (n div u)))";
by (simp add: func_times);
also have "(%x. ln (abs x + 1)) * ?RHS1 = (%x. 2 * (abs x + 1) *
ln(abs x + 1)^2)";
by (simp add: func_times mult_ac power2_eq_square);
finally have a: "(%x. psi (natfloor (abs x) + 1) * ln (abs x + 1) ^ 2) +
(%x. ln (abs x + 1) *
(∑ n = 1..natfloor (abs x) + 1.
∑ u | u dvd n. Lambda u * Lambda (n div u))) =o
(%x. 2 * (abs x + 1) * ln (abs x + 1) ^ 2) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";.;
note Selberg6a;
then have "(%x. 2) * (%x. ln (abs x + 1) / 2 *
(∑ n = 1..natfloor (abs x) + 1.
∑ u | u dvd n. Lambda u * Lambda (n div u))) =o
(%x. 2) *o ((%x. ∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
Lambda m * Lambda n * ln (real n)) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1))))"
(is "?LHS3 =o ?RHS3");
apply (intro set_times_intro2);
apply (erule bigo_add_commute_imp);
done;
also have "?LHS3 = (%x. ln (abs x + 1) *
(∑ n = 1..natfloor (abs x) + 1.
∑ u | u dvd n. Lambda u * Lambda (n div u)))";
by (simp add: func_times);
also have "?RHS3 = (%x. 2 * (∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
Lambda m * Lambda n * ln (real n))) +o
(%x. 2) *o O(%x. (abs x + 1) * (1 + ln (abs x + 1)))"
(is "?RHS3 = ?RHS4 +o ?RHS5");
by (simp add: set_times_plus_distribs func_times);
also have "... <= ?RHS4 +o O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
apply (rule set_plus_mono);
apply (rule bigo_const_mult6);
done;
finally; have b: "(%x. ln (abs x + 1) *
(∑ n = 1..natfloor (abs x) + 1.
∑ u | u dvd n. Lambda u * Lambda (n div u))) =o
(%x. 2 *
(∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
Lambda m * Lambda n * ln (real n))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";.;
have "(%x. psi (natfloor (abs x) + 1) * ln (abs x + 1) ^ 2) +
(%x. 2 *
(∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
Lambda m * Lambda n * ln (real n))) =o
(%x. 2 * (abs x + 1) * ln (abs x + 1) ^ 2) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
by (rule aux [OF a, OF b]);
also have "(%x. 2 * (∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
Lambda m * Lambda n * ln (real n))) =
(%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * psi((natfloor (abs x) + 1) div n)))";
apply (rule ext);
apply (rule arg_cong);back;
apply (subst general_inversion_nat2_cor1_modified);
apply force;
apply (rule setsum_cong2);
apply (subst psi_def_alt);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
done;
also have "... =
(%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * psi(natfloor ((abs x + 1) / real n))))";
apply (rule ext);
apply (rule arg_cong);back;
apply (rule setsum_cong2);
apply (subst natfloor_div_nat);
apply simp;
apply force;
apply (subst natfloor_add [THEN sym]);
apply simp;
apply simp;
done;
also have "... = (%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * R((abs x + 1) / real n))) +
(%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * ((abs x + 1) / real n)))";
apply (subst func_plus);
apply (rule ext);
apply (subst right_distrib [THEN sym]);
apply (rule arg_cong);back;
apply (subst setsum_addf [THEN sym]);
apply (rule setsum_cong2);
apply (subst R_alt_def);
apply (simp add: ring_eq_simps);
done;
also have "(%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * ((abs x + 1) / real n))) =
(%x. 2 * (abs x + 1)) *
(%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) / real n)";
apply (subst func_times);
apply (rule ext);
apply (subst mult_assoc);
apply (rule arg_cong);back;
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply (simp add: ring_eq_simps);
done;
also have "(%x. psi (natfloor (abs x) + 1) * ln (abs x + 1) ^ 2) =
(%x. R(abs x + 1) * ln (abs x + 1) ^ 2) +
(%x. (abs x + 1) * ln (abs x + 1) ^ 2)";
apply (subst func_plus);
apply (rule ext);
apply (subst natfloor_add [THEN sym]);
apply simp;
apply simp;
apply (subst R_alt_def);
apply (simp add: ring_eq_simps);
done;
finally have "(%x. R (abs x + 1) * ln (abs x + 1) ^ 2) +
(%x. (abs x + 1) * ln (abs x + 1) ^ 2) +
((%x. 2 *
(∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * R ((abs x + 1) / real n))) +
(%x. 2 * (abs x + 1)) *
(%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) / real n)) =o
(%x. 2 * (abs x + 1) * ln (abs x + 1) ^ 2) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))"
(is "?LHS =o ?RHS");.;
then have "- (%x. (abs x + 1) * ln (abs x + 1) ^ 2) +
- (%x. 2 * (abs x + 1)) *
(%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) / real n) + ?LHS =o
(- (%x. (abs x + 1) * ln (abs x + 1) ^ 2) +
(- (%x. 2 * (abs x + 1)) *
(%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) / real n))) +o ?RHS"
(is "?LHS2 =o ?RHS2");
by (rule set_plus_intro2);
also have "?LHS2 = (%x. R (abs x + 1) * ln (abs x + 1) ^ 2) +
(%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * R ((abs x + 1) / real n)))";
by (simp add: func_plus func_minus func_times ring_eq_simps
compare_rls);
also have "?RHS2 = (%x. (abs x + 1) * ln (abs x + 1) ^ 2) +o
((- (%x. 2 * (abs x + 1)) *
(%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) / real n)) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1))))";
by (simp add: set_plus_rearranges func_minus func_plus
func_times ring_eq_simps compare_rls);
finally have "(%x. R (abs x + 1) * ln (abs x + 1) ^ 2) +
(%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * R ((abs x + 1) / real n))) =o
(%x. (abs x + 1) * ln (abs x + 1) ^ 2) +o
((- (%x. 2 * (abs x + 1)) *
(%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) / real n)) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1))))";.;
also have "... <= (%x. (abs x + 1) * ln (abs x + 1) ^ 2) +o
(((- (%x. 2 * (abs x + 1))) *o
((%x. ln(abs x + 1)^2 / 2) +o O(%x. 1 + ln (abs x + 1)))) +
O(%x. (abs x + 1) * (1 + ln (abs x + 1))))";
apply (rule set_plus_mono);
apply (rule set_plus_mono5);
apply (rule set_times_intro2);
apply (rule sum_lambda_n_ln_n_over_n_bigo);
apply simp;
done;
also have "... = O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
apply (simp only: set_plus_rearranges set_times_plus_distribs
func_minus func_plus func_times);
apply (subgoal_tac "(%x. (abs x + 1) * ln (abs x + 1) ^ 2 +
- (2 * (abs x + 1)) * (ln (abs x + 1) ^ 2 / 2)) = 0");
apply (erule ssubst);
apply simp;
apply (subgoal_tac "(%x. - (2 * abs x) + -2) *o O(%x. 1 + ln (abs x + 1))
= O(%x. (abs x + 1) * (1 + ln (abs x + 1)))");
apply (erule ssubst);
apply simp;
apply (subgoal_tac "(%x. - (2 * abs x) + -2) *o O(%x. 1 + ln (abs x + 1))
= (%x. (abs x + 1)) *o ((%x. -2) *o
O(%x. (1 + ln (abs x + 1))))");
apply (erule ssubst);
apply (subst bigo_const_mult5);
apply simp;
apply (subst bigo_mult6 [THEN sym]);
apply (rule allI);
apply arith;
apply (simp add: func_times);
apply (simp only: set_times_rearranges func_times ring_eq_simps);
apply (subgoal_tac "(%x. -2 + - (abs x * 2)) = (%x. 1 * -2 + abs x * -2)");
apply (erule ssubst);
apply (rule refl);
apply (rule ext);
apply simp;
apply (simp add: func_zero);
apply (rule ext);
apply (simp add: ring_eq_simps add_divide_distrib);
done;
finally show ?thesis;.;
qed;
lemma error3: "(%x. abs(R (abs x + 1)) * ln (abs x + 1) ^ 2) <o
(%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * abs(R ((abs x + 1) / real n)))) =o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
proof -;
note error2;
then have "(%x. R (abs x + 1) * ln (abs x + 1) ^ 2) =o
- (%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * R ((abs x + 1) / real n))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))"
(is "?LHS =o ?RHS1 +o ?RHS2");
by (intro set_minus_imp_plus, simp);
then have "(%x. abs(?LHS x)) =o (%x. abs(?RHS1 x)) +o ?RHS2";
by (rule bigo_abs4);
also have "(%x. abs(?LHS x)) =
(%x. abs(R (abs x + 1)) * ln (abs x + 1) ^ 2)";
apply (rule ext);
apply (subst abs_times_pos);
apply force;
apply (rule refl);
done;
also have "(%x. abs(?RHS1 x)) = (%x. 2 *
abs (∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * R ((abs x + 1) / real n)))"
apply (rule ext);
apply (simp add: func_minus);
done;
finally have a: "(%x. abs (R (abs x + 1)) * ln (abs x + 1) ^ 2) =o
(%x. 2 *
abs (∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * R ((abs x + 1) / real n))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";.;
show "(%x. abs (R (abs x + 1)) * ln (abs x + 1) ^ 2) <o
(%x. 2 *
(∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * abs(R ((abs x + 1) / real n)))) =o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
apply (rule bigo_lesso3 [OF a]);
apply (rule allI);
apply (rule nonneg_times_nonneg);
apply force;
apply (rule setsum_nonneg);
apply force;
apply clarsimp;
apply (rule nonneg_times_nonneg);
apply (rule nonneg_times_nonneg);
apply (rule Lambda_ge_zero);
apply force;
apply force;
apply (rule allI);
apply (rule mult_left_mono);
apply (rule order_trans);
apply (rule abs_setsum);
apply (rule setsum_le_cong);
apply simp;
apply (rule mult_right_mono);
apply (subst abs_nonneg);
apply force;
apply (subst abs_nonneg);
apply (rule Lambda_ge_zero);
apply simp;
apply auto;
done;
qed;
lemma error4_aux: "(%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n / real n *
(∑ m = 1..(natfloor (abs x) + 1) div n. Lambda m / real m)) =o
(%x. ln (abs x + 1)^2 / 2) +o O(%x. 1 + ln (abs x + 1))";
proof -;
thm bigo_setsum6 [OF Mertens_theorem_real2];
have "(%x. ∑ n = 1..natfloor (abs x) + 1. Lambda n / real n *
(∑ m = 1..(natfloor (abs x) + 1) div n. Lambda m / real m)) =
(%x. ∑ n = 1..natfloor (abs x) + 1. Lambda n / real n *
(∑m=1..natfloor(abs ((abs x + 1) / (real n) - 1)) + 1.
Lambda m / real m))";
apply (rule ext);
apply (rule setsum_cong2);
apply (rule arg_cong);back;
apply (subst Selberg.aux);
apply (rule div_ge_1);
apply force;
apply (subgoal_tac "real (natfloor (abs x)) <= abs x");
apply force;
apply (rule real_natfloor_le);
apply force;
apply (subst natfloor_div_nat);
apply force;
apply force;
apply (subst natfloor_add [THEN sym]);
apply force;
apply simp;
done;
also have "... =o
(%x. ∑ n = 1..natfloor (abs x) + 1. Lambda n / real n *
ln (abs ((abs x + 1) / real n - 1) + 1)) +o
O(%x. ∑ n = 1..natfloor (abs x) + 1. Lambda n / real n * 1)";
apply (rule bigo_setsum6 [OF Mertens_theorem_real2]);
apply (rule allI)+;
apply (case_tac "n = 0");
apply simp;
apply (rule real_ge_zero_div_gt_zero);
apply (rule Lambda_ge_zero);
apply force;
apply force;
done;
also have "(%x. ∑ n = 1..natfloor (abs x) + 1. Lambda n / real n *
ln (abs ((abs x + 1) / real n - 1) + 1)) =
(%x. ∑ n = 1..natfloor (abs x) + 1. Lambda n / real n *
ln ((abs x + 1) / real n))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst Selberg.aux2);
apply (rule div_ge_1);
apply force;
apply (subgoal_tac "real(natfloor(abs x)) <= abs x");
apply force;
apply (rule real_natfloor_le);
apply simp;
apply (rule refl);
done;
also; have "(%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n / real n * ln ((abs x + 1) / real n)) +o
O(%x. ∑ n = 1..natfloor (abs x) + 1. Lambda n / real n * 1) <=
(%x. ln (abs x + 1) ^ 2 / 2) +o
O(%x. 1 + ln (abs x + 1)) + O(%x. 1 + ln (abs x + 1))";
apply (rule set_plus_mono5);
apply (rule sum_lambda_m_over_m_ln_x_over_m_bigo);
apply (rule bigo_elt_subset);
apply (rule subsetD);
prefer 2;
apply simp;
apply (rule Mertens_theorem_real2);
apply (rule bigo_plus_absorb2);
apply (rule bigo_bounded);
apply force;
apply force;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply force;
done;
also have "... = (%x. ln (abs x + 1)^2 / 2) +o O(%x. 1 + ln(abs x + 1))";
by (simp add: set_plus_rearranges);
finally show ?thesis;.;
qed;
lemma error4: "(%x. R (abs x + 1) * ln (abs x + 1) ^ 2) =o
(%x. 2 * (∑ c = 1..natfloor (abs x) + 1. ∑ v | v dvd c.
Lambda v * Lambda (c div v) * R ((abs x + 1) / real c))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
proof -;
note Selberg8a;
also have "(%x. psi (natfloor (abs x) + 1) * ln (abs x + 1) ^ 2) =
(%x. R(abs x + 1) * ln(abs x + 1)^2) +
(%x. (abs x + 1) * ln (abs x + 1)^2)";
apply (subst func_plus);
apply (rule ext);
apply (subst R_def);
apply (simp add: ring_eq_simps);
apply (subst add_commute);back;back;
apply (subst natfloor_add [THEN sym]);
apply simp;
apply (simp add: add_ac);
done;
also; have "(%x. 2 * (∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c. Lambda v * Lambda (c div v) *
psi ((natfloor (abs x) + 1) div c))) =
(%x. 2 * (∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c. Lambda v * Lambda (c div v) *
R ((abs x + 1) / real c))) +
(%x. 2 * (∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c. Lambda v * Lambda (c div v) *
(abs x + 1) / real c))";
apply (simp add: func_plus);
apply (rule ext);
apply (subst right_distrib [THEN sym]);
apply (rule arg_cong);back;
apply (subst setsum_addf [THEN sym]);
apply (rule setsum_cong2);
apply (subst setsum_addf [THEN sym]);
apply (rule setsum_cong2);
apply (subst R_def);
apply (subst natfloor_div_nat);
apply force;
apply force;
apply (simp add: ring_eq_simps);
apply (subst add_commute);back;
apply (subst natfloor_add [THEN sym]);
apply force;
apply (simp add: add_commute);
done;
also have "(%x. 2 * (∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c. Lambda v * Lambda (c div v) *
(abs x + 1) / real c)) =
(%x. 2) * (%x. ∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c.
Lambda v * Lambda (c div v) * (abs x + 1) / real ((c div v) * v))";
apply (subst func_times);
apply (rule ext);
apply (rule arg_cong);back;
apply (rule setsum_cong2)+;
apply (subst mult_commute);
apply (subst nat_dvd_mult_div);
apply clarsimp;
apply (rule dvd_pos_pos);
prefer 2;
apply assumption;
apply force;
apply force;
apply (rule refl);
done;
also have "(%x. ∑ c = 1..natfloor (abs x) + 1. ∑ v | v dvd c.
Lambda v * Lambda (c div v) * (abs x + 1) / real (c div v * v)) =
(%x. abs x + 1) * (%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n / (real n) * (∑ m = 1..(natfloor (abs x) + 1) div n.
Lambda m / (real m)))";
apply (subst func_times);
apply (rule ext);
apply (subst setsum_const_times [THEN sym]);
apply (subst general_inversion_nat2_modified [THEN sym]);
apply force;
apply (rule setsum_cong2);
apply (subst setsum_const_times [THEN sym])+;
apply (rule setsum_cong2);
apply (simp add: mult_ac);
done;
also; have "((%x. 2 * (∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c.
Lambda v * Lambda (c div v) * R ((abs x + 1) / real c))) +
(%x. 2) * ((%x. abs x + 1) * (%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n / real n *
(∑ m = 1..(natfloor (abs x) + 1) div n.
Lambda m / real m)))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1))) <=
((%x. 2 * (∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c.
Lambda v * Lambda (c div v) * R ((abs x + 1) / real c))) +o
(%x. 2) *o ((%x. abs x + 1) *o
((%x. ln (abs x + 1)^2 / 2) +o O(%x. 1 + ln (abs x + 1))) )) +
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
apply (rule set_plus_mono3);
apply (rule set_plus_intro2);
apply (rule set_times_intro2);
apply (rule set_times_intro2);
apply (rule error4_aux);
done;
also have "... <= ((%x. 2 * (∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c.
Lambda v * Lambda (c div v) * R ((abs x + 1) / real c))) +
(%x. (abs x + 1) * ln (abs x + 1)^2)) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
apply (simp add: set_times_plus_distribs set_plus_rearranges
plus_ac0 func_times func_plus);
apply (rule set_plus_mono);
apply (rule bigo_plus_subset4);
apply simp;
apply (rule subset_trans);
apply (rule set_times_mono);
apply (rule bigo_mult2);
apply (simp add: func_times);
done;
finally; have "(%x. R (abs x + 1) * ln (abs x + 1) ^ 2) +
(%x. (abs x + 1) * ln (abs x + 1) ^ 2) =o
((%x. 2 * (∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c.
Lambda v * Lambda (c div v) * R ((abs x + 1) / real c))) +
(%x. (abs x + 1) * ln (abs x + 1) ^ 2)) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))"
(is "?LHS =o ?RHS"); .;
then have "- (%x. (abs x + 1) * ln (abs x + 1) ^ 2) + ?LHS =o
- (%x. (abs x + 1) * ln (abs x + 1) ^ 2) +o ?RHS";
by (rule set_plus_intro2);
thus ?thesis
by (simp add: set_plus_rearranges func_plus func_minus plus_ac0);
qed;
lemma error5: "(%x. abs(R (abs x + 1)) * ln (abs x + 1) ^ 2) <o
(%x. 2 * (∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c.
Lambda v * Lambda (c div v) * abs(R ((abs x + 1) / real c)))) =o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
proof -;
have "(%x. R (abs x + 1) * ln (abs x + 1) ^ 2) =o
(%x. 2 * (∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c.
Lambda v * Lambda (c div v) * R ((abs x + 1) / real c))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))"
(is "?LHS =o ?RHS1 +o ?RHS2");
by (rule error4);
then have "(%x. abs(?LHS x)) =o (%x. abs(?RHS1 x)) +o ?RHS2";
by (rule bigo_abs4);
also have "(%x. abs(?LHS x)) =
(%x. abs(R (abs x + 1)) * ln (abs x + 1) ^ 2)";
apply (rule ext);
apply (subst abs_times_pos);
apply force;
apply (rule refl);
done;
also have "(%x. abs(?RHS1 x)) = (%x. 2 *
abs (∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c.
Lambda v * Lambda (c div v) * R ((abs x + 1) / real c)))";
apply (rule ext);
apply (simp add: func_minus);
done;
finally have a: " (%x. abs (R (abs x + 1)) * ln (abs x + 1) ^ 2) =o
(%x. 2 * abs (∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c.
Lambda v * Lambda (c div v) * R ((abs x + 1) / real c))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";.;
show ?thesis;
apply (rule bigo_lesso3 [OF a]);
apply (rule allI);
apply (rule nonneg_times_nonneg);
apply force;
apply (rule setsum_nonneg);
apply force;
apply clarsimp;
apply (rule setsum_nonneg);
apply (rule finite_nat_dvd_set);
apply force;
apply clarsimp;
apply (rule nonneg_times_nonneg);
apply (rule nonneg_times_nonneg);
apply (rule Lambda_ge_zero);
apply (rule Lambda_ge_zero);
apply force;
apply (rule allI);
apply (rule mult_left_mono);
apply (rule order_trans);
apply (rule abs_setsum);
apply (rule setsum_le_cong);
apply simp;
apply (rule order_trans);
apply (rule abs_setsum);
apply (rule setsum_le_cong);
apply simp;
apply (subst abs_nonneg);back;back;back;back;back;back;
apply (rule Lambda_ge_zero);
apply (subst abs_nonneg);back;back;back;back;back;back;
apply (rule Lambda_ge_zero);
apply (rule mult_right_mono);
apply auto;
done;
qed;
(* Generalize to ordered rings! *)
lemma max_zero_add: "max (a + b) 0 <= max (a::real) 0 + max b 0";
by (simp split: split_max);
lemma max_zero_times: "(0::real) <= c ==> max (c * a) 0 =
c * (max a 0)";
by (auto simp add: max_def mult_le_0_iff);
lemma aux2: "(f + f) <o ((%x. 2 * g x) + (%x. 2 * h x)) =o O(k::'a=>real)
==> f <o (g + h) =o O(k)";
apply (simp add: func_plus);
apply (unfold lesso_def);
apply (subgoal_tac "(%x. max (2 * f x - (2 * g x + 2 * h x)) 0) =
(%x. 2) * (%x. max (f x - (g x + h x)) 0)");
apply simp;
apply (rule bigo_useful_const_mult);
apply (auto simp add: func_times);
apply (rule ext);
apply (subgoal_tac "2 * f x - (2 * g x + 2 * h x) =
2 * (f x - (g x + h x))");
apply (erule ssubst);
apply (rule max_zero_times);
apply force;
apply simp;
done;
lemma error_cor1: "(%x. abs (R (abs x + 1)) * ln (abs x + 1) ^ 2) <o
((%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * abs (R ((abs x + 1) / real n))) +
(%x. ∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c.
Lambda v * Lambda (c div v) * abs (R ((abs x + 1) / real c)))) =o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
by (rule aux2 [OF lesso_add [OF error3, OF error5]]);
constdefs
rho :: "nat => real"
"rho x == ∑n = 1..x.
Lambda n * ln (real n) +
(∑ u | u dvd n. Lambda u * Lambda (n div u))";
lemma aux2: "1 <= (n::nat) ==> (∑i=1..n. f i) -
(∑i=1..(n - 1). f i) = ((f n)::'a::ordered_ring)";
apply (subgoal_tac "{1..n} = {1..(n - 1) + 1}");
apply (erule ssubst);
apply (subst setsum_range_plus_one_nat');
apply auto;
done;
lemma rho_zero: "rho 0 = 0";
by (simp add: rho_def);
lemma aux3: "1 <= n ==> rho n - rho (n - 1) =
Lambda n * ln (real n) +
(∑ u | u dvd n. Lambda u * Lambda (n div u))";
apply (unfold rho_def);
apply (erule aux2);
done;
lemma rho_bigo: "rho =o (%x. 2 * real x * ln (real x)) +o O(%x. real x)";
proof -
have "(%x. rho(x + 1)) = (%x. (∑ n = 1..natfloor (abs (real x)) + 1.
Lambda n * ln (real n) +
(∑ u | u dvd n. Lambda u * Lambda (n div u))))";
apply (rule ext);
apply (unfold rho_def);
apply (subgoal_tac "x + 1 = natfloor(abs (real x)) + 1");
apply (erule ssubst);
apply (rule refl);
apply simp;
done;
also have "... =o (%x. 2 * (abs (real x) + 1) * ln (abs (real x) + 1)) +o
O(%x. abs (real x) + 1)";
by (rule bigo_compose2 [OF Selberg2]);
also have "(%x::nat. 2 * (abs (real x) + 1) * ln (abs (real x) + 1)) =
(%x. 2 * (real (x + 1)) * ln (real (x + 1)))";
apply (rule ext);
apply (subst abs_nonneg);
apply force;
apply simp;
done;
also have "(%x::nat. abs (real x) + 1) = (%x. real(x + 1))";
apply (rule ext);
apply (subst abs_nonneg);
apply simp_all;
done;
finally have "(%x. rho (x + 1)) =o
(%x. 2 * real (x + 1) * ln (real (x + 1))) +o O(%x. real (x + 1))";.;
thus ?thesis;
apply (rule bigo_fix3);
apply (simp add: rho_zero);
done;
qed;
lemma R_bigo: "(%x. R(abs x)) =o O(%x. abs x)";
apply (subgoal_tac "(%x. R(abs x)) = (%x. psi(natfloor(abs x))) +
- (%x. abs x)");
apply (erule ssubst);
apply (rule subsetD);
apply (subgoal_tac "O(%x. real(natfloor (abs x))) + O(%x. abs x) <=
O(%x. abs x)");
apply assumption;
apply (rule bigo_plus_subset4);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (rule real_natfloor_le);
apply force;
apply simp;
apply (rule set_plus_intro);
apply (rule bigo_compose1 [OF psi_bigo]);
apply (rule bigo_minus);
apply (rule bigo_refl);
apply (rule ext);
apply (unfold R_def);
apply (simp add: func_plus func_minus);
done;
lemma error6_aux: "(%x. abs (R ((abs x + 1) / (real (natfloor (abs x)) + 1))))
=o O(%x. 1)";
apply (rule subsetD);
prefer 2;
apply (rule bigo_abs);
apply (rule bigo_elt_subset);
apply (subgoal_tac
"(%x. R ((abs x + 1) / (real (natfloor (abs x)) + 1))) =
(%x. R (abs((abs x + 1) / (real (natfloor (abs x)) + 1))))");
apply (erule ssubst);
apply (rule subsetD);
prefer 2;
apply (rule bigo_compose1 [OF R_bigo]);
apply (rule bigo_elt_subset);
apply (rule subsetD);
prefer 2;
apply (rule bigo_abs);
apply (rule bigo_elt_subset);
apply (rule_tac c = 2 in bigo_bounded_alt);
apply (rule allI);
apply (rule real_ge_zero_div_gt_zero);
apply arith;
apply force;
apply (rule allI);
apply simp;
apply (rule real_le_mult_imp_div_pos_le);
apply force;
apply simp;
apply (subst mult_commute);
apply (subgoal_tac "abs x <= real(natfloor(abs x)) + 1");
apply force;
apply (rule real_natfloor_plus_one_ge);
apply (rule ext);
apply (subst abs_nonneg);
apply (rule real_ge_zero_div_gt_zero);
apply arith;
apply force;
apply (rule refl);
done;
lemma error6_aux2: "(%n::nat. real (n + 1) * ln (real (n + 1)) -
(real n) * ln (real n)) =o (%n. ln (real (n + 1))) +o O(%n. 1)";
apply (rule set_minus_imp_plus);
apply (subst func_diff);
apply (rule bigo_bounded);
apply (rule allI);
apply (case_tac "x = 0");
apply simp;
apply (simp add: left_distrib);
apply (rule allI);
apply (case_tac "x = 0");
apply simp;
apply (simp add: left_distrib);
apply (subgoal_tac "real x * (ln(real x + 1) - ln(real x)) <= 1");
apply (simp add: diff_minus right_distrib);
apply (subst ln_div [THEN sym]);
apply force;
apply force;
apply (subst mult_commute);
apply (subst pos_le_divide_eq [THEN sym]);
apply force;
apply (subst add_divide_distrib);
apply simp;
done;
lemma error6: "(%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * abs (R ((abs x + 1) / real n))) +
(%x. ∑ c = 1..natfloor (abs x) + 1. ∑ v | v dvd c.
Lambda v * Lambda (c div v) * abs (R ((abs x + 1) / real c))) =o
(%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
abs (R ((abs x + 1) / real n)) * ln (real (n - 1 + 1)))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
proof -;
have "((%x. ∑ n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) * abs (R ((abs x + 1) / real n))) +
(%x. ∑ c = 1..natfloor (abs x) + 1.
∑ v | v dvd c.
Lambda v * Lambda (c div v) * abs (R ((abs x + 1) / real c)))) =
(%x. ∑n = 1..natfloor (abs x) + 1.
abs(R ((abs x + 1) / real n)) * (rho n - rho (n - 1)))";
apply (subst func_plus);
apply (rule ext);
apply (subst setsum_addf [THEN sym]);
apply (rule setsum_cong2);
apply (subst aux3);
apply force;
apply (simp add: ring_eq_simps);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
done;
also have "... =
(%x. abs (R ((abs x + 1) / (real (natfloor (abs x)) + 1))) *
rho (natfloor (abs x) + 1) +
(∑ n = 1..natfloor (abs x). rho n *
(abs (R ((abs x + 1) / real n)) -
abs (R ((abs x + 1) / (real n + 1))))))";
apply (rule ext);
apply (subst another_partial_sum);
apply (simp add: rho_zero);
done;
also have "... =
(%x. abs (R ((abs x + 1) / (real (natfloor (abs x)) + 1)))) *
(%x. rho (natfloor (abs x) + 1)) +
(%x. ∑ n = 1..natfloor (abs x).
(abs (R ((abs x + 1) / real n)) -
abs (R ((abs x + 1) / (real n + 1)))) * rho n)";
apply (subst func_times);
apply (subst func_plus);
apply (rule ext);
apply (simp add: mult_ac);
done;
also have "... =o
((%x. abs (R ((abs x + 1) / (real (natfloor (abs x)) + 1)))) *o
((%x. 2 * real (natfloor (abs x) + 1) *
ln (real (natfloor (abs x) + 1))) +o
O(%x. real (natfloor(abs x) + 1)))) +
((%x. ∑ n = 1..natfloor (abs x).
(abs (R ((abs x + 1) / real n)) -
abs (R ((abs x + 1) / (real n + 1)))) *
(2 * (real n) * ln(real n))) +o
O(%x. ∑ n = 1..natfloor (abs x).
abs((abs (R ((abs x + 1) / real n)) -
abs (R ((abs x + 1) / (real n + 1)))) * real n)))"
(is "?LHS =o ?term1 + (?term2 +o ?term3)");
apply (rule set_plus_intro);
apply (rule set_times_intro2);
apply (rule bigo_compose2 [OF rho_bigo]);
apply (rule bigo_setsum4 [OF rho_bigo]);
done;
also have "... <= (O(%x. 1) * O(%x. (abs x + 1) * (1 + ln (abs x + 1)))) +
(?term2 +o ?term3)";
apply (rule set_plus_mono2);
apply (rule set_times_mono5);
apply (rule error6_aux);
apply (rule bigo_plus_absorb2);
apply (rule_tac c = 2 in bigo_bounded_alt);
apply (rule allI);
apply (rule nonneg_times_nonneg);
apply force;
apply (rule ln_ge_zero);
apply force;
apply (rule allI);
apply (subst mult_assoc);
apply (rule mult_left_mono);
apply (rule mult_mono);
apply simp;
apply (rule real_natfloor_le);
apply force;
apply (subgoal_tac
"ln (real (natfloor (abs x) + 1)) <= ln (abs x + 1)");
apply arith;
apply (subst ln_le_cancel_iff);
apply force;
apply arith;
apply simp;
apply (rule real_natfloor_le);
apply force;
apply arith;
apply force;
apply force;
apply (rule subset_trans);
apply (subgoal_tac "?t <= O(%x. abs x + 1)");
apply assumption;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply clarsimp;
apply (rule real_natfloor_le);
apply force;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply arith;
apply (rule allI);
apply (subst right_distrib);
apply simp;
apply (rule nonneg_times_nonneg);
apply arith;
apply force;
apply (rule order_refl);
done;
also have "... <= O(%x. (abs x + 1) * (1 + ln (abs x + 1))) +
(?term2 +o ?term3)";
apply (rule set_plus_mono2);
apply (rule subset_trans);
apply (rule bigo_mult);
apply (simp add: func_times);
apply (rule order_refl);
done;
also have "... = ?term2 +o (?term3 +
O(%x. (abs x + 1) * (1 + ln (abs x + 1))))"
(is "?temp = ?term2 +o (?term3 + ?term4)");
by (simp only: set_plus_rearranges plus_ac0);
also have "?term2 = (%x. 2) * (
(- (%x. (abs (R ((abs x + 1) / (real (natfloor (abs x)) + 1)))))) *
(%x. ((real (natfloor (abs x)) + 1) *
ln (real (natfloor (abs x)) + 1))) +
(%x. ∑n=1..natfloor (abs x) + 1.
abs (R ((abs x + 1) / real n)) * ((real n) * ln (real n) -
(real (n - 1) * ln (real (n - 1))))))"
(is "?term2 = (%x. 2) * ?term2a");
apply (simp only: func_minus func_plus func_times);
apply (rule ext);
apply (subst another_partial_sum);
apply simp;
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
done;
also have "?term2a =
(- (%x. (abs (R ((abs x + 1) / (real (natfloor (abs x)) + 1)))))) *
(%x. ((real (natfloor (abs x)) + 1) *
ln (real (natfloor (abs x)) + 1))) +
(%x. ∑n=1..natfloor (abs x) + 1.
abs (R ((abs x + 1) / real n)) * ((real ((n - 1) + 1)) *
ln (real ((n - 1)+1)) -
(real (n - 1) * ln (real (n - 1)))))"
(is "?term2a = ?term2b");
apply (simp only: func_times func_minus func_plus);
apply (rule ext);
apply (rule arg_cong);back;
apply (rule setsum_cong2);
apply (subgoal_tac "xa - 1 + 1 = xa");
apply (erule ssubst);
apply (rule refl);
apply simp;
done;
also have "(%x. 2) * ?term2b +o (?term3 + ?term4) <=
(%x. 2) *o (O(%x. 1) * ?term4 +
((%x. ∑ n = 1..natfloor (abs x) + 1.
abs (R ((abs x + 1) / real n)) * ln (real (n - 1 + 1)))
+o O(%x. ∑ n = 1..natfloor (abs x) + 1.
abs (R ((abs x + 1) / real n)) * 1))) + (?term3 + ?term4)";
apply (rule set_plus_mono3);
apply (rule set_times_intro2);
apply (rule set_plus_intro);
apply (rule set_times_intro);
apply (rule bigo_minus);
apply (rule error6_aux);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule nonneg_times_nonneg);
apply force;
apply force;
apply (rule allI);
apply (rule mult_mono);
apply (force intro: real_natfloor_le);
apply (subgoal_tac "ln (real (natfloor (abs x)) + 1) <= ln (abs x + 1)");
apply arith;
apply (subst ln_le_cancel_iff);
apply force;
apply arith;
apply (force intro: real_natfloor_le);
apply arith;
apply force;
apply (rule bigo_setsum6);
apply (rule bigo_compose2 [OF error6_aux2]);
apply force;
apply force;
done;
also have "... <= (%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
abs (R ((abs x + 1) / real n)) * ln (real (n - 1 + 1)))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1))) +
(O(%x. (abs x + 1) * (1 + ln (abs x + 1))) +
(O(%x. (abs x + 1) * (1 + ln (abs x + 1))) + ?term3))";
apply (simp only: set_times_plus_distribs func_times
set_plus_rearranges plus_ac0);
apply (rule set_plus_mono);
apply (rule set_plus_mono2);
apply (rule order_refl);
apply (rule set_plus_mono2);
apply (rule subset_trans);
prefer 2;
apply (subgoal_tac "(%x. 2) *o ?t <= ?t");
apply assumption;
apply (rule bigo_const_mult6);
apply (rule set_times_mono);
apply (rule order_trans);
apply (rule bigo_mult);
apply (simp add: func_times);
apply (subst bigo_const_mult5);
apply force;
apply (rule set_plus_mono2);
apply simp;
apply (rule bigo_elt_subset);
apply (subgoal_tac "(%x. ∑ n = 1..1 + natfloor (abs x).
abs (R ((1 + abs x) / real n))) =
(%x. ∑ n = 1..natfloor (abs x) + 1.
1 * abs (R (abs((abs x + 1) / real n))))");
apply (erule ssubst);
apply (rule subsetD);
prefer 2;
apply (subgoal_tac "(%x. ∑ n = 1..natfloor (abs x) + 1.
1 * abs (R (abs((abs x + 1) / real n)))) =o
O(%x. ∑ n = 1..natfloor (abs x) + 1.
1 * abs((abs x + 1) / real n))");
apply assumption;
apply (rule bigo_setsum5);back;
apply (rule subsetD);
prefer 2;
apply (rule bigo_abs);
apply (rule bigo_elt_subset);
apply (rule R_bigo);
apply force;
apply force;
apply (rule bigo_elt_subset);
apply (subgoal_tac "(%x. ∑ n = 1..natfloor (abs x) + 1.
1 * abs ((abs x + 1) / real n)) =
(%x. abs x + 1) *
(%x. ∑ n = 1..natfloor (abs x) + 1. 1 / real n)");
apply (erule ssubst);
apply (rule subsetD);
apply (subgoal_tac "(%x. abs x + 1) *o O(%x. 1 + ln (1 + abs x)) <=
O(%x. (abs x + 1) * (1 + ln (1 + abs x)))");
apply (simp add: add_ac);
apply (rule subset_trans);
apply (rule bigo_mult2);
apply (simp add: func_times);
apply (simp add: add_ac);
apply (rule set_times_intro2);
apply (subgoal_tac "(%x. ∑ n = 1..1 + natfloor (abs x). 1 / real n)
= (%x. ∑ n = 1..natfloor (abs x) + 1. 1 / real n)");
apply (erule ssubst);
apply (rule subsetD);
prefer 2;
apply (rule bigo_add_commute_imp [OF ln_sum_real2]);
apply (rule bigo_plus_absorb2);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (simp add: add_commute);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply force;
apply (simp add: add_ac);
apply (rule ext);
apply (subst func_times);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
apply (rule abs_nonneg);
apply (rule real_ge_zero_div_gt_zero);
apply arith;
apply force;
apply (rule ext);
apply (simp add: add_ac);
apply (rule setsum_cong2);
apply (subst abs_nonneg);back;
apply (rule real_ge_zero_div_gt_zero);
apply arith;
apply force;
apply (rule refl);
apply (rule order_refl);
done;
also have "... = (%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
abs (R ((abs x + 1) / real n)) * ln (real (n - 1 + 1)))) +o
(O(%x. (abs x + 1) * (1 + ln (abs x + 1))) + ?term3)";
apply (simp only: set_plus_rearranges);
apply (subst plus_ac0.assoc [THEN sym]);
apply (subst bigo_plus_idemp);
apply (subst plus_ac0.assoc [THEN sym]);
apply (subst bigo_plus_idemp);
apply (rule refl);
done;
also have "... <= (%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
abs (R ((abs x + 1) / real n)) * ln (real (n - 1 + 1)))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
apply (rule set_plus_mono);
apply (rule bigo_plus_subset4);
apply (rule order_refl);
apply (rule bigo_elt_subset);
apply (rule bigo_lesseq3);
prefer 2;
apply (rule allI);
apply (rule setsum_nonneg);
apply force;
apply clarify;
apply (rule abs_ge_zero);
prefer 2;
proof -;
show "ALL x. (∑ n = 1..natfloor (abs x).
abs ((abs (R ((abs x + 1) / real n)) -
abs (R ((abs x + 1) / (real n + 1)))) * real n)) <=
(abs x + 1) *
(∑ n = 1..natfloor (abs x) + 1. 1 / real n) +
(∑ n = 1..natfloor (abs x) + 1.
psi (natfloor ((abs x + 1) / real n)))";
proof;
fix x;
have "(∑ n = 1..natfloor (abs x).
abs ((abs (R ((abs x + 1) / real n)) -
abs (R ((abs x + 1) / (real n + 1)))) * real n)) <=
(∑ n = 1..natfloor (abs x).
abs ((R ((abs x + 1) / real n) -
R ((abs x + 1) / (real n + 1)))) * real n)";
apply (rule setsum_le_cong);
apply (subst abs_mult)+;
apply (subgoal_tac "abs(real x) = real x");
apply (erule ssubst);
apply (rule mult_right_mono);
apply (rule abs_triangle_ineq3);
apply force;
apply force;
done;
also have "... = (∑ n = 1..natfloor (abs x).
abs (
(((abs x + 1) / real (n + 1)) - ((abs x + 1) / (real n))) +
(psi(natfloor((abs x + 1) / real n)) -
psi(natfloor((abs x + 1) / (real (n + 1)))))) * real n)";
apply (rule setsum_cong2);
apply (unfold R_def);
apply (simp add: ring_eq_simps compare_rls);
done;
also have "... <= (∑ n = 1..natfloor (abs x). abs (
(((abs x + 1) / real (n + 1)) - ((abs x + 1) / (real n)))) *
real n) +
(∑ n = 1..natfloor (abs x). abs (
(psi(natfloor((abs x + 1) / real n)) -
psi(natfloor((abs x + 1) / (real (n + 1)))))) * real n)";
apply (subst setsum_addf [THEN sym]);
apply (rule setsum_le_cong);
apply (subst left_distrib [THEN sym]);
apply (rule mult_right_mono);
apply (rule abs_triangle_ineq);
apply force;
done;
also have "... = (∑ n = 1..natfloor (abs x). (real n) *
(((abs x + 1) / real n) - (abs x + 1) / real (n + 1))) +
(∑ n = 1..natfloor (abs x). (real n) *
(psi(natfloor((abs x + 1) / real n)) -
psi(natfloor((abs x + 1) / (real (n + 1))))))";
apply (simp only: setsum_addf [THEN sym]);
apply (rule setsum_cong2);
apply (subgoal_tac
"abs ((abs ?y + 1) / real (x + 1) - (abs ?y + 1) / real x) =
-((abs ?y + 1) / real (x + 1) - (abs ?y + 1) / real x)");
apply (erule ssubst);
apply (subgoal_tac "abs (psi (natfloor ((abs ?y + 1) / real x)) -
psi (natfloor ((abs ?y + 1) / real (x + 1)))) =
(psi (natfloor ((abs ?y + 1) / real x)) -
psi (natfloor ((abs ?y + 1) / real (x + 1))))");
apply (erule ssubst);
apply (simp add: ring_eq_simps);
apply (rule abs_nonneg);
apply (simp add: compare_rls);
apply (rule psi_mono);
apply (rule natfloor_mono);
apply (rule divide_left_mono);
apply force;
apply arith;
apply (rule mult_pos);
apply force;
apply force;
apply (rule abs_nonpos);
apply (simp add: compare_rls);
apply (rule divide_left_mono);
apply force;
apply arith;
apply (rule mult_pos);
apply force;
apply force;
done;
also have "... = (∑ n = 1..natfloor (abs x) + 1.
(abs x + 1) * (real n - real (n - 1)) / real n) -
(abs x + 1) +
((∑ n = 1..natfloor (abs x) + 1.
psi (natfloor ((abs x + 1) / real n)) * (real n - real (n - 1))) -
psi (natfloor ((abs x + 1) / (real (natfloor (abs x)) + 1))) *
(real (natfloor (abs x)) + 1))";
apply (subst another_partial_sum2);
apply (subst another_partial_sum2);
apply simp;
done;
also have "... = (abs x + 1) *
(∑ n = 1..natfloor (abs x) + 1. 1 / real n) +
(∑ n = 1..natfloor (abs x) + 1.
psi (natfloor ((abs x + 1) / real n))) -
((abs x + 1) +
psi (natfloor ((abs x + 1) / (real (natfloor (abs x)) + 1))) *
(real (natfloor (abs x)) + 1))";
apply (simp add: compare_rls);
apply (simp add: setsum_addf [THEN sym] setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply (subgoal_tac "real x - real (x - 1) = 1");
apply (erule ssubst);
apply simp;
apply (subgoal_tac "real (x - 1) = real x - real (1::nat)");
apply simp;
apply (rule real_of_nat_diff);
apply force;
done;
also have "... <= (abs x + 1) *
(∑ n = 1..natfloor (abs x) + 1. 1 / real n) +
(∑ n = 1..natfloor (abs x) + 1.
psi (natfloor ((abs x + 1) / real n)))";
apply (simp only: compare_rls);
apply (subst add_commute);
apply (rule add_increasing);
apply (rule nonneg_plus_nonneg);
apply arith;
apply (rule nonneg_times_nonneg);
apply (rule psi_ge_zero);
apply force;
apply (rule order_refl);
done;
finally; show "(∑ n = 1..natfloor (abs x).
abs ((abs (R ((abs x + 1) / real n)) -
abs (R ((abs x + 1) / (real n + 1)))) * real n))
<= (abs x + 1) * (∑ n = 1..natfloor (abs x) + 1. 1 / real n) +
(∑ n = 1..natfloor (abs x) + 1.
psi (natfloor ((abs x + 1) / real n)))";.;
qed;
next show "(%x. (abs x + 1) *
(∑ n = 1..natfloor (abs x) + 1. 1 / real n) +
(∑ n = 1..natfloor (abs x) + 1.
psi (natfloor ((abs x + 1) / real n)))) =o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
apply (subst bigo_plus_idemp [THEN sym]);
apply (subgoal_tac
"(%x. (abs x + 1) * (∑ n = 1..natfloor (abs x) + 1. 1 / real n) +
(∑ n = 1..natfloor (abs x) + 1.
psi (natfloor ((abs x + 1) / real n)))) =
(%x. (abs x + 1) * (∑ n = 1..natfloor (abs x) + 1. 1 / real n)) +
(%x. (∑ n = 1..natfloor (abs x) + 1.
psi (natfloor ((abs x + 1) / real n))))");
apply (erule ssubst);
apply (rule set_plus_intro);
apply (rule subsetD);
apply (subgoal_tac "(%x. (abs x + 1)) *o O(%x. 1 + ln(abs x + 1)) <= ?t");
apply assumption;
apply (rule subset_trans);
apply (rule bigo_mult2);
apply (simp add: func_times);
apply (subgoal_tac
"(%x. (abs x + 1) * (∑ n = 1..natfloor (abs x) + 1. 1 / real n)) =
(%x. (abs x + 1)) *
(%x. ∑ n = 1..natfloor (abs x) + 1. 1 / real n)");
apply (erule ssubst);
apply (rule set_times_intro2);
apply (rule subsetD);
prefer 2;
apply (rule bigo_add_commute_imp [OF ln_sum_real2]);
apply (rule bigo_plus_absorb2);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (simp add: add_commute);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply force;
apply (simp add: add_ac);
apply (rule ext);
apply (subst func_times);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
apply (rule subsetD);
prefer 2;
apply (subgoal_tac "(%x. ∑ n = 1..natfloor (abs x) + 1.
1 * psi (natfloor ((abs x + 1) / real n))) =o
O(%x. ∑ n = 1..natfloor (abs x) + 1.
abs(1 * real(natfloor ((abs x + 1) / real n))))");
apply simp;
apply (rule bigo_setsum3 [OF psi_bigo]);
apply (rule bigo_elt_subset);
apply (subgoal_tac "(%x. ∑ n = 1..natfloor (abs x) + 1.
real (natfloor ((abs x + 1) / real n))) =
(%x. ∑ n = 1..natfloor (abs x) + 1.
real (natfloor (abs x + 1) div n))");
apply (erule ssubst);
apply (rule bigo_lesseq3);
apply (subgoal_tac "(%x. ∑ n = 1..natfloor (abs x) + 1.
real (natfloor (abs x + 1)) / (real n)) =o ?t");
apply assumption;
apply (rule subsetD);
apply (subgoal_tac "O(%x. (abs x + 1)) * O(%x. (1 + ln (abs x + 1))) <=
?t");
apply assumption;
apply (rule subset_trans);
apply (rule bigo_mult);
apply (simp add: func_times);
apply (subgoal_tac "(%x. ∑ n = 1..natfloor (abs x) + 1.
real (natfloor (abs x + 1)) / real n) =
(%x. real (natfloor (abs x + 1))) *
(%x. ∑ n = 1..natfloor (abs x) + 1. 1 / real n)");
apply (erule ssubst);
apply (rule set_times_intro);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (rule real_natfloor_le);
apply arith;
apply (rule subsetD);
prefer 2;
apply (rule bigo_add_commute_imp [OF ln_sum_real2]);
apply (rule bigo_plus_absorb2);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (simp add: add_commute);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply force;
apply (subst func_times);
apply (rule ext);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
apply (rule allI);
apply (rule setsum_nonneg');
apply force;
apply (rule allI);
apply (rule setsum_le_cong);
apply (rule real_nat_div_le_real_div);
apply (rule ext);
apply (rule setsum_cong2);
apply (subst natfloor_div_nat);
apply force+;
apply (subst func_plus);
apply (rule refl);
done;
qed;
finally show ?thesis;.;
qed;
lemma error7: "(%x. abs (R (abs x + 1)) * ln (abs x + 1) ^ 2) <o
(%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
abs (R ((abs x + 1) / real n)) * ln (real n))) =o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
proof -;
note bigo_lesso4 [OF error_cor1, OF error6];
also have "(%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
abs (R ((abs x + 1) / real n)) * ln (real (n - 1 + 1)))) =
(%x. 2 * (∑ n = 1..natfloor (abs x) + 1.
abs (R ((abs x + 1) / real n)) * ln (real n)))";
apply (rule ext);
apply (rule arg_cong);back;
apply (rule setsum_cong2);
apply (subgoal_tac "xa - 1 + 1 = xa");
apply (erule ssubst);
apply (rule refl);
apply simp;
done;
finally show ?thesis;.;
qed;
end;
lemma R_alt_def:
psi (natfloor x) = x + R x
lemma R_alt_def2:
psi (natfloor x) = R x + x
lemma R_alt_def3:
psi n = real n + R (real n)
lemma R_alt_def4:
psi n = R (real n) + real n
lemma R_bound_imp_PNT:
∀epsilon. 0 < epsilon --> (∃z. ∀x. z ≤ x --> ¦R x¦ < epsilon * x) ==> (%x. psi x / real x) ----> 1
lemma aux:
[| f + g ∈ h + O(k); g ∈ l + O(k) |] ==> f + l ∈ h + O(k)
lemma error0:
R ∈ O(abs)
lemma R_zero:
R 0 = 0
lemma error1:
(%x. ∑n = 1..natfloor ¦x¦. R (real n) / (real n * real (n + 1))) ∈ O(%x. 1)
lemma sum_lambda_n_ln_n_over_n_bigo:
(%x. ∑n = 1..natfloor ¦x¦ + 1. Lambda n * ln (real n) / real n) ∈ (%x. (ln (¦x¦ + 1))² / 2) + O(%x. 1 + ln (¦x¦ + 1))
lemma error2:
(%x. R (¦x¦ + 1) * (ln (¦x¦ + 1))²) + (%x. 2 * (∑n = 1..natfloor ¦x¦ + 1. Lambda n * ln (real n) * R ((¦x¦ + 1) / real n))) ∈ O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))
lemma error3:
(%x. ¦R (¦x¦ + 1)¦ * (ln (¦x¦ + 1))²) <o (%x. 2 * (∑n = 1..natfloor ¦x¦ + 1. Lambda n * ln (real n) * ¦R ((¦x¦ + 1) / real n)¦)) ∈ O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))
lemma error4_aux:
(%x. ∑n = 1..natfloor ¦x¦ + 1. Lambda n / real n * (∑m = 1..(natfloor ¦x¦ + 1) div n. Lambda m / real m)) ∈ (%x. (ln (¦x¦ + 1))² / 2) + O(%x. 1 + ln (¦x¦ + 1))
lemma error4:
(%x. R (¦x¦ + 1) * (ln (¦x¦ + 1))²) ∈ (%x. 2 * (∑c = 1..natfloor ¦x¦ + 1. ∑v | v dvd c. Lambda v * Lambda (c div v) * R ((¦x¦ + 1) / real c))) + O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))
lemma error5:
(%x. ¦R (¦x¦ + 1)¦ * (ln (¦x¦ + 1))²) <o (%x. 2 * (∑c = 1..natfloor ¦x¦ + 1. ∑v | v dvd c. Lambda v * Lambda (c div v) * ¦R ((¦x¦ + 1) / real c)¦)) ∈ O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))
lemma max_zero_add:
max (a + b) 0 ≤ max a 0 + max b 0
lemma max_zero_times:
0 ≤ c ==> max (c * a) 0 = c * max a 0
lemma aux2:
(f + f) <o ((%x. 2 * g x) + (%x. 2 * h x)) ∈ O(k) ==> f <o (g + h) ∈ O(k)
lemma error_cor1:
(%x. ¦R (¦x¦ + 1)¦ * (ln (¦x¦ + 1))²) <o ((%x. ∑n = 1..natfloor ¦x¦ + 1. Lambda n * ln (real n) * ¦R ((¦x¦ + 1) / real n)¦) + (%x. ∑c = 1..natfloor ¦x¦ + 1. ∑v | v dvd c. Lambda v * Lambda (c div v) * ¦R ((¦x¦ + 1) / real c)¦)) ∈ O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))
lemma aux2:
1 ≤ n ==> setsum f {1..n} - setsum f {1..n - 1} = f n
lemma rho_zero:
rho 0 = 0
lemma aux3:
1 ≤ n ==> rho n - rho (n - 1) = Lambda n * ln (real n) + (∑u | u dvd n. Lambda u * Lambda (n div u))
lemma rho_bigo:
rho ∈ (%x. 2 * real x * ln (real x)) + O(real)
lemma R_bigo:
(%x. R ¦x¦) ∈ O(abs)
lemma error6_aux:
(%x. ¦R ((¦x¦ + 1) / (real (natfloor ¦x¦) + 1))¦) ∈ O(%x. 1)
lemma error6_aux2:
(%n. real (n + 1) * ln (real (n + 1)) - real n * ln (real n)) ∈ (%n. ln (real (n + 1))) + O(%n. 1)
lemma error6:
(%x. ∑n = 1..natfloor ¦x¦ + 1. Lambda n * ln (real n) * ¦R ((¦x¦ + 1) / real n)¦) + (%x. ∑c = 1..natfloor ¦x¦ + 1. ∑v | v dvd c. Lambda v * Lambda (c div v) * ¦R ((¦x¦ + 1) / real c)¦) ∈ (%x. 2 * (∑n = 1..natfloor ¦x¦ + 1. ¦R ((¦x¦ + 1) / real n)¦ * ln (real (n - 1 + 1)))) + O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))
lemma error7:
(%x. ¦R (¦x¦ + 1)¦ * (ln (¦x¦ + 1))²) <o (%x. 2 * (∑n = 1..natfloor ¦x¦ + 1. ¦R ((¦x¦ + 1) / real n)¦ * ln (real n))) ∈ O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))