(* Title: Selberg.thy
Author: Jeremy Avigad
*)
header {* The Selberg symmetry formula *}
theory Selberg = MuSum:;
lemma Selberg1: "0 < n ==> ln(real n) ^ 2 = (∑ d | d dvd n.
Lambda d * ln (real d) +
(∑ u | u dvd d. Lambda u * Lambda (d div u)))";
proof -;
assume "0 < (n::nat)";
have "(ln(real n))^2 = (∑x:{(p, a). 0 < a & p : prime & p ^ a dvd n}.
ln (real (fst x)))^2" (is "?temp = (?term1)^2");
apply (subst ln_eq_setsum_Lambda2);
apply (rule prems);
apply (rule refl);
done;
also have "... = ?term1 * ?term1";
by (rule realpow_two2 [THEN sym]);
also have "... = (∑x:{(p, a). 0 < a & p : prime & p ^ a dvd n}.
(∑y:{(q, b). 0 < b & q : prime & q ^ b dvd n}.
ln (real(fst x)) * ln (real(fst y))))";
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply (subst mult_commute);
apply (subst setsum_const_times [THEN sym]);
apply (rule refl);
done;
also have "... = (∑x: {((p, a), (q, b)).
0 < a & p : prime & p ^ a dvd n &
0 < b & q : prime & q ^ b dvd n}.
ln (real (fst (fst x))) * ln (real (fst (snd x))))"
(is "?temp = (∑x: {((p, a), (q, b)). (?P p a q b)}. ?t x)");
apply (subst setsum_cartesian_product);
apply (rule finite_subset);
prefer 2;
apply (rule l.finite_C [of n]);
apply (force intro: dvd_imp_le prems);
apply (rule finite_subset);
prefer 2;
apply (rule l.finite_C [of n]);
apply (force intro: dvd_imp_le prems);
apply (rule setsum_cong);
apply auto;
done;
also; have "... = (∑x: {((p, a), (q, b)). (?P p a q b) & (p ~= q |
(a + b) <= multiplicity (int p) (int n))}. ?t x) +
(∑x: {((p, a), (q, b)). (?P p a q b) & (p = q &
multiplicity (int p) (int n) < a + b)}. ?t x)"
(is "?temp = ?term2 + ?term3");
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule finite_subset);
prefer 2;
apply (rule finite_cartesian_product);
apply (rule l.finite_C [of n]);
apply (rule l.finite_C [of n]);
apply (force intro: dvd_imp_le prems);
apply (rule finite_subset);
prefer 2;
apply (rule finite_cartesian_product);
apply (rule l.finite_C [of n]);
apply (rule l.finite_C [of n]);
apply (force intro: dvd_imp_le prems);
apply force;
apply (rule setsum_cong);
apply simp;
apply auto;
done;
also have "?term2 = (∑x:{((p,a),(q,b)). (?P p a q b) &
((p^a * q^b) dvd n)}. ?t x)";
apply (rule setsum_cong);
apply auto;
apply (rule relprime_dvd_prod_dvd);
apply (erule distinct_primes_power_gcd_1);
apply assumption+;
apply (case_tac "a ~= aa");
apply (rule relprime_dvd_prod_dvd);
apply (erule distinct_primes_power_gcd_1);
apply assumption+;
apply simp;
apply (subst power_add [THEN sym]);
apply (subst multiplicity_power_dvd [THEN sym]);
apply (rule prems);
apply assumption+;
apply (subst multiplicity_power_dvd);
apply (rule prems);
apply assumption;
apply (subst power_add);
apply assumption;
done;
also have "... = (∑x:{(p,a). 0 < a & p : prime & p^a dvd n}.
∑y:{(q,b). 0 < b & q : prime & q^b dvd n &
(fst x)^(snd x) * q^b dvd n}. ln(real(fst x)) * ln(real (fst y)))";
apply (subst setsum_Sigma);
apply (rule finite_subset);
prefer 2;
apply (rule l.finite_C [of n]);
apply (force intro: dvd_imp_le prems);
apply (rule ballI);
apply (rule finite_subset);
prefer 2;
apply (rule l.finite_C [of n]);
apply (force intro: dvd_imp_le prems);
apply (rule setsum_cong);
apply auto;
done;
also have "... = (∑x:{(p,a). 0 < a & p : prime & p^a dvd n}.
ln(real (fst x)) * (∑y:{(q,b). 0 < b & q : prime & q^b dvd n &
(fst x)^(snd x) * q^b dvd n}. ln(real (fst y))))";
apply (rule setsum_cong2);
apply (rule setsum_const_times);
done;
also have "... = (∑x:{(p,a). 0 < a & p : prime & p^a dvd n}.
Lambda((fst x)^(snd x)) *
(∑y:{(q,b). 0 < b & q : prime & q^b dvd n &
(fst x)^(snd x) * q^b dvd n}. Lambda((fst y)^(snd y))))";
apply (rule setsum_cong2);
apply (subst Lambda_eq [THEN sym]);
apply force;
apply (subgoal_tac "0 < snd x");
apply assumption;
apply force;
apply (rule arg_cong);back;
apply (rule setsum_cong2);
apply (rule Lambda_eq [THEN sym]);
apply auto;
done;
also; have "... = (∑u | (EX p a. 0 < a & p : prime & p^a = u &
u dvd n). Lambda u *
(∑y:{(q,b). 0 < b & q : prime & q^b dvd n &
u * q^b dvd n}. Lambda((fst y)^(snd y))))";
apply (rule setsum_reindex_cong' [THEN sym]);
apply (rule finite_subset);
prefer 2;
apply (rule l.finite_C [of n]);
apply (force intro: prems dvd_imp_le);
apply (subgoal_tac "inj_on (%x. (fst x)^(snd x)) ?Q");
apply (assumption);
apply (clarsimp simp add: inj_on_def);
apply (rule conjI);
apply (rule prime_prop_rzero);
apply assumption+;back;
apply (rule prime_prop2);
prefer 5;
apply assumption+;
apply (auto simp add: image_def);
done;
also have "... = ... + (∑ u | ~(EX p a. 0 < a & p : prime & p ^ a = u) &
u dvd n. Lambda u * (∑y:{(q, b). 0 < b & q : prime &
q ^ b dvd n & u * q ^ b dvd n}. Lambda (fst y ^ snd y)))"
(is "?temp = ?temp + ?zeroterm");
apply (subgoal_tac "?zeroterm = 0");
apply simp;
apply (rule setsum_0');
apply (rule ballI);
apply (subst Lambda_eq2);
apply blast;
apply simp;
done;
also have "... = (∑ u | u dvd n. Lambda u *
(∑y:{(q, b). 0 < b & q : prime &
q ^ b dvd n & u * q ^ b dvd n}. Lambda (fst y ^ snd y)))";
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule finite_subset);
prefer 2;
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply force;
apply (rule finite_subset);
prefer 2;
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply force;
apply blast;
apply (rule setsum_cong);
apply auto;
done;
also have "... = (∑ u | u dvd n. Lambda u *
(∑y:{(q, b). 0 < b & q : prime & u * q ^ b dvd n}.
Lambda (fst y ^ snd y)))";
apply (rule setsum_cong2);
apply (rule arg_cong);back;
apply (rule setsum_cong);
apply auto;
apply (auto simp add: dvd_def);
done;
also have "... = (∑ u | u dvd n. Lambda u *
(∑v | (EX q b. 0 < b & q : prime & v = q^b) & u * v dvd n.
Lambda v))";
apply (rule setsum_cong2);
apply (rule arg_cong);back;
apply (rule setsum_reindex_cong' [THEN sym]);
apply (rule finite_subset);
prefer 2;
apply (rule l.finite_C [of n]);
apply clarsimp;
apply (rule dvd_imp_le);
apply (force simp add: dvd_def);
apply (rule prems);
apply (subgoal_tac "inj_on (%x. (fst x)^(snd x)) ?Q");
apply (assumption);
apply (clarsimp simp add: inj_on_def);
apply (rule conjI);
apply (rule prime_prop_rzero);
apply assumption+;back;
apply (rule prime_prop2);
prefer 5;
apply assumption+;
apply (auto simp add: image_def);
done;
also have "... = (∑ u | u dvd n. Lambda u *
(∑v | (u * v) dvd n. Lambda v))";
apply (rule setsum_cong2);
apply (rule arg_cong);back;
proof -;
fix x;
have "(∑ v | (EX q b. 0 < b & q : prime & v = q ^ b) & x * v dvd n.
Lambda v) =
(∑ v | (EX q b. 0 < b & q : prime & v = q ^ b) & x * v dvd n.
Lambda v) +
(∑ v | ~(EX q b. 0 < b & q : prime & v = q ^ b) & x * v dvd n.
Lambda v)" (is "?temp = ?temp2 + ?zeroterm");
apply (subgoal_tac "?zeroterm = 0");
apply simp;
apply (rule setsum_0');
apply (rule ballI);
apply (subst Lambda_eq2);
apply auto;
done;
also have "... = (∑ v | x * v dvd n. Lambda v)";
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule finite_subset);
prefer 2;
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply (force simp add: dvd_def);
apply (rule finite_subset);
prefer 2;
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply (force simp add: dvd_def);
apply blast;
apply (rule setsum_cong);
apply blast;
apply (rule refl);
done;
finally; show "(∑ v | (EX q b. 0 < b & q : prime & v = q ^ b) &
x * v dvd n. Lambda v) = (∑ v | x * v dvd n. Lambda v)";.;
qed;
also have "... = (∑ u | u dvd n. (∑v | (u * v) dvd n.
Lambda u * Lambda v))";
apply (rule setsum_cong2);
apply (subst setsum_const_times);
apply (rule refl);
done;
also have "... = (∑ u | u dvd n.
(∑ v | v dvd (n div u). Lambda u * Lambda v))";
apply (rule setsum_cong2);
apply (rule setsum_cong);
apply auto;
apply (force simp add: prems dvd_def);
apply (force simp add: prems dvd_def);
done;
also have "... = (∑ d | d dvd n.
(∑ u | u dvd d. Lambda u * Lambda (d div u)))";
apply (rule general_inversion_nat3);
apply (rule prems);
done;
also have "?term3 = (∑x: {((p,a),c). p : prime & p ^ a dvd n &
0 < a & c < a}. ln(real (fst (fst x))) * ln(real (fst (fst x))))";
apply (rule setsum_reindex_cong');
apply (rule finite_subset);
prefer 2;
apply (rule finite_SigmaI);
apply (rule l.finite_C [of n]);
apply (subgoal_tac "finite {..snd a(}");
apply assumption;
apply simp;
apply clarsimp;
apply (erule dvd_imp_le);
apply (rule prems);
apply (subgoal_tac "inj_on (%x. ((fst x), ((fst (fst x)),
multiplicity (int (fst (fst x))) (int n) - (snd x)))) ?Q");
apply assumption;
apply (clarsimp simp add: inj_on_def);
apply (simp only: prems multiplicity_power_dvd [THEN sym]);
apply arith;
prefer 2;
apply simp;
apply (unfold image_def);
apply (insert prems);
apply (rule set_ext);
apply (rule iffI);
apply clarsimp;
apply (rule_tac x = aa in exI);
apply clarify;
apply (rule_tac x = b in exI);
apply clarify;
apply (rule_tac x = "multiplicity (int aa) (int n) - ba" in exI);
apply (clarsimp simp add: prems multiplicity_power_dvd [THEN sym]);
apply arith;
apply (clarsimp simp add: prems multiplicity_power_dvd [THEN sym]);
apply arith;
done;
also have "... = (∑x:{(p, a). p : prime & p ^ a dvd n & 0 < a}.
∑c:{0..snd x(}. ln (real (fst x)) * ln (real (fst x)))";
apply (subst setsum_Sigma);
apply (rule finite_subset);
prefer 2;
apply (rule l.finite_C [of n]);
apply (force intro: prems dvd_imp_le);
apply (rule ballI);
apply simp;
apply (rule setsum_cong);
apply auto;
done;
also have "... = (∑x:{(p, a). p : prime & p ^ a dvd n & 0 < a}.
ln (real ((fst x)^(snd x))) * ln (real (fst x)))";
apply (rule setsum_cong2);
apply (subst setsum_constant);
apply simp;
apply (simp add: real_eq_of_nat [THEN sym] realpow_real_of_nat [THEN sym]);
apply (subst ln_realpow);
apply auto;
apply (auto simp add: prime_def);
done;
also have "... = (∑x:{(p, a). p : prime & p ^ a dvd n & 0 < a}.
ln (real((fst x)^(snd x))) * Lambda((fst x)^(snd x)))";
apply (rule setsum_cong2);
apply (subst Lambda_eq);
apply auto;
done;
also have "... = (∑d | d dvd n & (EX p a. p : prime & 0 < a & d = p^a).
ln (real d) * Lambda d)";
apply (rule setsum_reindex_cong' [THEN sym]);
apply (rule finite_subset);
prefer 2;
apply (rule l.finite_C [of n]);
apply (force intro: prems dvd_imp_le);
apply (subgoal_tac "inj_on (%x. (fst x)^(snd x)) ?Q");
apply assumption;
apply (clarsimp simp add: inj_on_def);
apply (rule conjI);
apply (rule prime_prop_rzero);
apply assumption+;back;
apply (rule prime_prop2);
prefer 5;
apply assumption+;
apply (auto simp add: image_def);
done;
also; have "... =
(∑ d | d dvd n & (EX p a. p : prime & 0 < a & d = p ^ a).
ln (real d) * Lambda d) +
(∑ d | d dvd n & ~(EX p a. p : prime & 0 < a & d = p ^ a).
ln (real d) * Lambda d)" (is "?temp = ?temp' + ?zeroterm");
apply (subgoal_tac "?zeroterm = 0");
apply simp;
apply (rule setsum_0');
apply (rule ballI);
apply (subst Lambda_eq2);
apply auto;
done;
also have "... = (∑ d | d dvd n. Lambda d * ln (real d))";
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule finite_subset);
prefer 2;
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply force;
apply (rule finite_subset);
prefer 2;
apply (rule finite_nat_dvd_set);
apply (rule prems);
apply force;
apply blast;
apply (rule setsum_cong);
apply blast;
apply (rule mult_commute);
done;
finally; have "ln(real n) ^ 2 =
(∑ d | d dvd n. Lambda d * ln (real d)) +
(∑ d | d dvd n. ∑ u | u dvd d. Lambda u * Lambda (d div u))";
by (subst add_commute);
thus ?thesis;
by (subst setsum_addf);
qed;
lemma Selberg2: "(%x. ∑n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n) +
(∑ 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)";
proof -;
have "(%x. ∑n=1..natfloor(abs x) + 1.
Lambda n * ln(real n) +
(∑ u | u dvd n. Lambda u * Lambda (n div u))) =
(%x. ∑n:{)0..natfloor(abs x) + 1}.
(∑d | d dvd n. mu2(d) * (ln(real (n div d)))^2))";
apply (rule ext);
apply (rule setsum_cong);
apply force;
apply (rule mu_inversion_nat1a'_real);
apply clarify;
apply (rule Selberg1);
apply assumption+;
apply force;
done;
also have "... = (%x. ∑d:{)0..natfloor(abs x)+1}.
∑k:{)0..(natfloor (abs x) + 1) div d}. mu2(d) * (ln(real k)^2))";
apply (rule ext);
apply (rule general_inversion_nat2 [THEN sym]);
apply force;
done;
also have "... = (%x. sumr 0 (natfloor (abs x) + 1) (%d.
mu2(d+1) * (sumr 0 (natfloor ((abs x + 1) / (real d+1)))
(%k. ln(real k + 1)^2))))";
apply (rule ext);
apply (subst setsum_sumr3);
apply (rule sumr_cong);
apply (subst setsum_const_times);
apply (rule arg_cong);back;
apply (subst setsum_sumr3);
apply (subgoal_tac "(natfloor (abs x) + 1) div (y + 1) =
natfloor ((abs x + 1) / (real y + 1))");
apply (erule ssubst);
apply (rule sumr_cong);
apply (rule arg_cong);back;
apply (rule arg_cong);back;
apply simp;
apply (subst natfloor_add [THEN sym]);
apply force;
apply (subst natfloor_div_nat [THEN sym]);
apply force;
apply force;
apply (subst real_nat_plus_one);
apply simp;
done;
also have "... = (%x. sumr 0 (natfloor (abs x) + 1) (%d.
mu2(d+1) * (sumr 0 (natfloor (abs((abs x + 1) / (real d+1) - 1)) + 1)
(%k. ln(real k + 1)^2))))";
apply (rule ext);
apply (rule sumr_cong);
apply (rule arg_cong);back;
apply (subgoal_tac "natfloor ((abs x + 1) / (real y + 1)) =
natfloor (abs ((abs x + 1) / (real y + 1) - 1)) + 1");
apply (erule ssubst, rule refl);
apply (subst natfloor_add [THEN sym]);
apply force;
apply (rule arg_cong);back;
apply (subst abs_nonneg);
apply simp;
apply (rule div_ge_1);
apply force;
apply auto;
apply (rule nat_le_natfloor);
apply force;
apply force;
done;
also have "... =o (%x. sumr 0 (natfloor (abs x) + 1) (%d. mu2(d+1) *
((%y. (abs y + 1) * ln (abs y + 1) ^ 2) -
(%y. 2 * (abs y + 1) * ln (abs y + 1)) +
(%y. 2 * (abs y + 1))) ((abs x + 1) / (real d + 1) - 1))) +o
O(%x. sumr 0 (natfloor (abs x) + 1) (%d. abs( mu2(d+1) *
(1 + ln(abs ((abs x + 1) / (real d + 1) - 1) + 1)^2))))"
(is "?temp =o ?term1 +o ?oterm");
by (rule bigo_sumr8 [OF identity_six_real]);
also have "?term1 = (%x. sumr 0 (natfloor (abs x) + 1) (%d.
(mu2(d+1) * (abs x + 1) / (real d + 1) *
ln((abs x + 1) / (real d + 1))^2) -
(mu2(d+1) * 2 * ((abs x + 1) / (real d + 1)) *
ln((abs x + 1) / (real d + 1))) +
(mu2(d+1) * 2 * ((abs x + 1) / (real d + 1)))))";
apply (simp only: func_plus func_diff);
apply (rule ext);
apply (rule sumr_cong);
apply (subgoal_tac "abs ((abs x + 1) / (real y + 1) - 1) + 1 =
(abs x + 1) / (real y + 1)");
apply (simp add: ring_eq_simps);
apply (subst abs_nonneg);back;back;
apply simp;
apply (rule div_ge_1);
apply auto;
apply (rule nat_le_natfloor);
apply auto;
done;
also have "... = (%x. (abs x + 1) * sumr 0 (natfloor(abs x) + 1)
(%d. mu2(d+1) / (real (d + 1)) *
ln((abs x + 1) / (real (d + 1)))^2)) + -
(%x. 2 * (abs x + 1) * sumr 0 (natfloor(abs x) + 1)
(%d. mu2(d+1) / (real (d + 1)) * ln((abs x + 1) / (real (d + 1))))) +
(%x. 2 * (abs x + 1) * sumr 0 (natfloor(abs x) + 1)
(%d. mu2(d+1) / (real (d + 1))))";
apply (rule ext);
apply (simp only: func_plus func_minus);
apply (simp only: sumr_mult sumr_add sumr_minus [THEN sym]);
apply (rule sumr_cong);
apply (subst real_nat_plus_one);
apply (simp add: ring_eq_simps ring_distrib add_divide_distrib);
done;
also have "... = (%x. (abs x + 1)) *
((%x. sumr 0 (natfloor(abs x) + 1)
(%d. mu2(d+1) / (real (d + 1)) *
ln((abs x + 1) / (real (d + 1)))^2)) + -
(%x. 2) * (%x. sumr 0 (natfloor(abs x) + 1)
(%d. mu2(d+1) / (real (d + 1)) * ln((abs x + 1) / (real (d + 1))))) +
(%x. 2) * (%x. sumr 0 (natfloor(abs x) + 1)
(%d. mu2(d+1) / (real (d + 1)))))" (is "?temp = ?term1a");
apply (simp only: func_times func_minus func_plus);
apply (rule ext);
apply (simp only: right_distrib right_diff_distrib mult_ac);
done;
also
have "(%x. sumr 0 (natfloor (abs x) + 1) (%d. abs( mu2(d + 1) *
(1 + ln(abs ((abs x + 1) / (real d + 1) - 1) + 1)^2)))) =
(%x. sumr 0 (natfloor (abs x) + 1) (%d. abs( mu2(d + 1) *
(1 + ln(((abs x + 1) / (real d + 1)))^2))))";
apply (rule ext);
apply (rule sumr_cong);
apply (rule arg_cong);back;
apply (rule arg_cong);back;
apply (rule arg_cong);back;
apply (rule arg_cong);back;
apply (rule arg_cong);back;
apply (subst abs_nonneg);back;back;
apply simp;
apply (rule div_ge_1);
apply force;
apply simp;
apply (rule nat_le_natfloor);
apply auto;
done;
also have "?term1a +o O(...) <= (%x. abs x + 1) *o
(((%x. 2 * ln(abs x + 1)) +o O(%x. 1)) +
((-(%x. 2)) *o O(%x. 1)) +
((%x. 2) *o O(%x. 1))) +
O(%x. sumr 0 (natfloor (abs x) + 1) (%d.
(1 + ln((abs x + 1) / (real d + 1))^2)))";
apply (rule set_plus_mono5);
apply (rule set_times_intro2);
apply (rule set_plus_intro);
apply (rule set_plus_intro);
apply (rule sumr_mu_div_n_times_ln_squared_div_nbigo);
apply (rule set_times_intro2);
apply (rule sumr_mu_div_n_times_ln_div_nbigo);
apply (rule set_times_intro2);
apply (rule bigo_compose1 [OF sumr_mu_div_n_bigo]);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule sumr_ge_zero);
apply arith;
apply (rule allI);
apply (rule sumr_le_cong);
apply (subst abs_mult);
apply (subst abs_nonneg);back;back;
apply (rule nonneg_plus_nonneg);
apply force;
apply force;
apply (rule real_mult_le_lemma);
apply (rule abs_mu2_leq_1);
apply (rule nonneg_plus_nonneg);
apply auto;
done;
also have "(- (%x. 2)) *o O(%x. 1) = O(%x. (1::real))";
apply (subst func_minus);
apply (rule bigo_const_mult5);
apply simp;
done;
also have "(%x. 2) *o O(%x. 1) = O(%x. (1::real))";
by (rule bigo_const_mult5, simp);
also; have "(%x. 2 * ln (abs x + 1)) +o O(%x. 1) + O(%x. 1) + O(%x. 1) =
(%x. 2 * ln (abs x + 1)) +o (O(%x. 1) + O(%x. 1) + O(%x. 1))";
by (simp only: set_plus_rearranges);
also have "O(%x. 1) + O(%x. 1) + O(%x. 1) = O(%x. (1::real))";
apply (subst bigo_plus_idemp)+;
apply (rule refl);
done;
also; have "(%x. abs x + 1) *o ((%x. 2 * ln (abs x + 1)) +o O(%x. 1)) =
(%x. 2 * (abs x + 1) * ln (abs x + 1)) +o (%x. abs x + 1) *o O(%x. 1)";
by (simp only: set_times_plus_distribs func_times mult_ac);
also; have "... + O(%x. sumr 0 (natfloor (abs x) + 1)
(%d. 1 + ln ((abs x + 1) / (real d + 1)) ^ 2)) <=
(%x. 2 * (abs x + 1) * ln (abs x + 1)) +o O(%x. abs x + 1)";
apply (simp only: set_plus_rearranges);
apply (rule set_plus_mono);
apply (rule bigo_useful_intro);
apply (rule order_trans);
apply (rule bigo_mult2);
apply (simp add: func_times);
apply (subgoal_tac "(%x. sumr 0 (natfloor (abs x) + 1)
(%d. 1 + ln ((abs x + 1) / (real d + 1)) ^ 2)) =
(%x. sumr 0 (natfloor (abs x) + 1) (%d. 1)) +
(%x. sumr 0 (natfloor (abs x) + 1)
(%d. ln ((abs x + 1) / (real d + 1)) ^ 2))");
apply (erule ssubst);
apply (rule order_trans);
apply (rule bigo_plus_subset);
apply (rule bigo_useful_intro);
apply (rule bigo_elt_subset);
apply simp;
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply simp;
apply (rule real_natfloor_le);
apply force;
apply (rule bigo_elt_subset);
apply (rule sum_ln_x_div_x_squared_real_bigo_cor);
apply (simp only: func_plus sumr_add);
done;
finally show ?thesis;.;
qed;
lemma Selberg3: "(%x. ∑n = 1..natfloor (abs x) + 1.
Lambda n * ln (real n))+ (%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 "?LHS =o ?RHS");
apply (subgoal_tac "?LHS = ?temp");
apply (erule ssubst);
apply (rule Selberg2);
apply (subst func_plus);
apply (rule ext);
apply (subst setsum_addf);
apply (rule refl);
done;
lemma sum_lambda_ln_bigo:
"(%x. ∑n = 1..x + 1. Lambda n * ln (real n)) =o
(%x. psi (x + 1) * ln (real (x + 1))) +o O(%x. real x)";
proof -;
have "(%x. ∑n=1..x+1. Lambda n * ln (real n)) =
(%x. ∑n=1..x+1. (psi n - psi (n - 1)) * ln (real n))";
apply (rule ext);
apply (rule setsum_cong2);
apply (simp add: psi_diff2);
done;
also have "... = (%x. psi (x + 1) * ln (real (x + 1))) + -
(%x. ∑n = 1..x. psi n * (ln (real (n + 1)) - ln (real n)))";
apply (simp only: func_minus func_plus);
apply (rule ext);
apply (subst partial_sum_b0);
apply clarify;
apply (erule telescoping_sum [THEN sym]);
apply (simp add: psi_zero);
done;
also have "... =o (%x. psi(x + 1) * ln(real (x + 1))) +o
O(%x. sumr 0 x (%i. 1))";
apply (rule set_plus_intro2);
apply (rule bigo_minus);
apply (subgoal_tac "(%x. ∑ n = 1..x. psi n *
(ln (real (n + 1)) - ln (real n))) = (%x. ?s x)");
prefer 2;
apply (rule ext);
apply (rule setsum_sumr4);
apply (erule ssubst);
apply (rule bigo_sumr_pos);
apply simp;
apply (subgoal_tac "(%i. psi (i + 1) *
(ln (real (i + 1 + 1)) - ln (real (i + 1)))) =
(%i. psi (i + 1)) * (%i. (ln (real (i + 1 + 1)) - ln (real (i + 1))))");
apply (erule ssubst);
apply (subgoal_tac "O(%i. real (i + 1)) * O(%i. 1 / (real i + 1)) =
O(%i. 1)");
apply (erule subst);
apply (rule set_times_intro);
apply (rule bigo_compose1);
apply (rule psi_bigo);
apply (subgoal_tac "(%i. ln (real (i + 1 + 1)) - ln (real (i + 1))) =
(%i. ln(1 + 1 / (real i + 1)))");
apply (erule ssubst);
apply (rule ln_one_plus_one_over_x_bigo);
apply (rule ext);
apply (subst ln_div [THEN sym]);
apply force;
apply force;
apply (rule arg_cong);back;
apply (subgoal_tac "real (i + 1 + 1) = real (i + 1) + 1");
apply (erule ssubst);
apply (subst add_divide_distrib);
apply simp;
apply simp;
apply (subst bigo_mult8 [THEN sym]);
apply force;
apply (subst func_times);
apply (subgoal_tac "(%u. real (u + 1) * (1 / (real u + 1))) = (%i. 1)");
apply (erule ssubst);
apply simp;
apply (rule ext);
apply (subgoal_tac "real (u + 1) = real u + 1");
apply (erule ssubst);
apply simp;
apply simp;
apply (subst func_times, rule refl);
done;
also have "... <= (%x. psi(x + 1) * ln(real (x + 1))) +o O(%x. real x)";
by simp;
finally show ?thesis;.;
qed;
lemma sum_lambda_ln_bigo_real:
"(%x. ∑n = 1..natfloor (abs x) + 1. Lambda n * ln (real n)) =o
(%x. psi (natfloor (abs x) + 1) * ln (abs x + 1)) +o O(%x. abs x + 1)";
proof -;
have "(%x. ∑n = 1..natfloor (abs x) + 1. Lambda n * ln (real n)) =o
(%x. psi (natfloor (abs x) + 1) * ln (real (natfloor (abs x) + 1))) +o
O(%x. real (natfloor (abs x)))";
by (rule bigo_compose2 [OF sum_lambda_ln_bigo]);
also have "(%x. psi (natfloor (abs x) + 1) *
ln (real (natfloor (abs x) + 1))) =
(%x. psi (natfloor (abs x) + 1) * ln(abs x + 1)) +
(%x. psi (natfloor (abs x) + 1)) * (%x. (ln(real(natfloor (abs x) + 1)) -
(ln(abs x + 1))))";
apply (simp only: func_plus func_times);
apply (rule ext);
apply (subst right_diff_distrib);
apply simp;
done;
also have "((%x. psi (natfloor (abs x) + 1) * ln (abs x + 1)) +
(%x. psi (natfloor (abs x) + 1)) *
(%x. ln (real (natfloor (abs x) + 1)) - ln (abs x + 1))) +o
O(%x. real (natfloor (abs x))) =
(%x. psi (natfloor (abs x) + 1) * ln (abs x + 1)) +o
(((%x. psi (natfloor (abs x) + 1)) *
(%x. ln (real (natfloor (abs x) + 1)) - ln (abs x + 1))) +o
O(%x. real (natfloor (abs x))))";
by (simp add: set_plus_rearranges);
also have "... <= (%x. psi (natfloor (abs x) + 1) * ln (abs x + 1)) +o
(O(%x. real (natfloor(abs x) + 1)) * O(%x. 1 / (abs x + 1)) +
O(%x. abs x + 1))";
apply (rule set_plus_mono);
apply (rule set_plus_mono5);
apply (rule set_times_intro);
apply (rule bigo_compose1 [OF psi_bigo]);
apply (subst func_diff [THEN sym]);back;
apply (rule set_plus_imp_minus);
apply (rule bigo_add_commute_imp);
apply (subgoal_tac "(%x. ln (real (natfloor (abs x) + 1))) =
(%x. ln (real (natfloor (abs x)) + 1))");
apply (erule ssubst);
apply (rule ln_real_approx_ln_nat);
apply (rule ext);
apply simp;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (rule order_trans);
apply (rule real_natfloor_le);
apply auto;
done;
also; have "... <= (%x. psi (natfloor (abs x) + 1) * ln (abs x + 1)) +o
(O(%x. (abs x + 1)) * O(%x. 1) + O(%x. abs x + 1))";
apply (rule set_plus_mono);
apply (rule set_plus_mono2);
apply (rule set_times_mono2);
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (subgoal_tac "real(natfloor(abs x)) <= abs x");
apply force;
apply (rule real_natfloor_le);
apply force;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply (rule allI);
apply (rule real_ge_zero_div_gt_zero);
apply force;
apply arith;
apply (rule allI);
apply (rule real_le_mult_imp_div_pos_le);
apply arith;
apply force;
apply force;
done;
also have "... <= (%x. psi (natfloor (abs x) + 1) * ln (abs x + 1)) +o
O(%x. (abs x + 1))";
apply (rule set_plus_mono);
apply (rule bigo_useful_intro);
apply (subst bigo_mult8 [THEN sym]);
apply (rule allI);
apply arith;
apply (simp add: func_times);
apply force;
done;
finally show ?thesis;.;
qed;
lemma Selberg4: "(%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 ?RHS");
proof -;
have "(%x. ∑ n = 1..natfloor (abs x) + 1. Lambda n * ln (real n)) +
(%x. ∑ n = 1..natfloor (abs x) + 1.
∑ u | u dvd n. Lambda u * Lambda (n div u)) =o ?RHS"
(is "?LHS0 + ?LHS2 =o ?RHS");
by (rule Selberg3);
then have "(?LHS1 - ?LHS0) + (?LHS0 + ?LHS2) =o O(%x. abs x + 1) + ?RHS";
apply (intro set_plus_intro);
apply (rule set_plus_imp_minus);
apply (rule bigo_add_commute_imp);
apply (rule sum_lambda_ln_bigo_real);
apply assumption;
done;
also have "... <= ?RHS";
by (simp add: set_plus_rearranges);
also have "(?LHS1 - ?LHS0) + (?LHS0 + ?LHS2) = ?LHS1 + ?LHS2";
by (simp add: ring_eq_simps);
finally show ?thesis;.;
qed;
lemma Selberg4a: "(%x. psi (natfloor (abs x) + 1) * ln (abs x + 1)) +
(%x. ∑ d = 1..natfloor (abs x) + 1.
Lambda d * psi((natfloor(abs x) + 1) div d))
=o (%x. 2 * (abs x + 1) * ln (abs x + 1)) +o O(%x. abs x + 1)";
proof -;
note Selberg4;
also have "(%x. ∑ n = 1..natfloor (abs x) + 1.
∑ u | u dvd n. Lambda u * Lambda (n div u)) =
(%x. ∑ d = 1..natfloor (abs x) + 1. Lambda d *
psi((natfloor(abs x) + 1) div d))";
apply (rule ext);
apply (subst general_inversion_nat2_modified [THEN sym]);
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;
finally show ?thesis;.;
qed;
lemma aux: "1 <= (z::real) ==> natfloor(abs(z - 1)) + 1 = natfloor z";
apply (subst natfloor_add [THEN sym]);
apply force;
apply simp;
done;
lemma aux2: "(1::real) <= z ==> abs(z - 1) + 1 = z";
by simp;
lemma sum_lambda_m_over_m_ln_x_over_m_bigo:
"(%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m * ln ((abs x + 1) / real m)) =o
(%x. ln (abs x + 1) ^ 2 / 2) +o O(%x. 1 + ln (abs x + 1))";
proof -;
have "(%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m * ln ((abs x + 1) / real m)) =
(%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m * ln (abs((abs x + 1) / real m - 1) + 1))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst 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 auto;
done;
also have "... =o (%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m *
(∑i=1..natfloor(abs((abs x + 1) / real m - 1))+1.
1 / (real i))) +o
O(%x. ∑ m = 1..natfloor (abs x) + 1.
abs(Lambda m / real m * 1))";
by (rule bigo_setsum4 [OF ln_sum_real2]);
also have "(%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m *
(∑i=1..natfloor(abs((abs x + 1) / real m - 1))+1.
1 / (real i))) =
(%x. ∑ m = 1..natfloor (abs x) + 1.
(∑i=1..natfloor((abs x + 1) / real m).
Lambda m / (real (m * i))))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst setsum_const_times [THEN sym]);
apply (subgoal_tac "natfloor(abs ((abs x + 1) / real xa - 1)) + 1
= natfloor((abs x + 1) / real xa)");
apply (erule ssubst);
apply (rule setsum_cong2);
apply force;
apply (subst natfloor_add [THEN sym]);
apply force;
apply (subst real_nat_one);
apply (subst 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 force;
apply (rule refl);
done;
also have "... = (%x. ∑ m = 1..natfloor (abs x) + 1.
∑ i = 1..(natfloor (abs x) + 1) div m.
Lambda m / real (m * i))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst natfloor_div_nat);
apply force;
apply force;
apply (subst natfloor_add [THEN sym]);
apply force;
apply simp;
done;
also have "... = (%x. ∑c=1..natfloor(abs x) + 1.
∑ m | m dvd c. Lambda m / real (m * (c div m)))";
apply (rule ext);
apply (rule general_inversion_nat2_modified);
apply force;
done;
also have "... = (%x. ∑c=1..natfloor(abs x) + 1.
∑ m | m dvd c. Lambda m / (real c))";
apply (rule ext);
apply (rule setsum_cong2);
apply (rule setsum_cong2);
apply (subst dvd_mult_div_cancel);
apply auto;
done;
also have "... = (%x. ∑c=1..natfloor(abs x) + 1.
1 / (real c) * (∑ m | m dvd c. Lambda m))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
done;
also have "... = (%x. ∑c=1..natfloor(abs x) + 1.
ln (real c) / (real c))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst ln_eq_setsum_Lambda [THEN sym]);
apply force;
apply simp;
done;
also have "(%x. ∑ m = 1..natfloor (abs x) + 1.
abs (Lambda m / real m * 1)) =
(%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m)";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst abs_nonneg);
apply simp;
apply (rule real_ge_zero_div_gt_zero);
apply (rule Lambda_ge_zero);
apply force;
apply simp;
done;
finally; have " (%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m * ln ((abs x + 1) / real m)) =o
(%x. ∑ c = 1..natfloor (abs x) + 1. ln (real c) / real c) +o
O(%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m)";.;
also have "... <= ((%x. ln(abs x + 1)^2 / 2) +o O(%x. 1)) +
(O(%x. ln (abs x + 1)) + O(%x. 1))";
apply (rule set_plus_mono5);
apply (rule identity_four_real_b_cor);
apply (rule bigo_elt_subset2);
apply (rule Mertens_theorem_real2);
done;
also have "... <= (%x. ln(abs x + 1)^2 / 2) +o O(%x. 1 + ln (abs x + 1))";
apply (simp add: set_plus_rearranges);
apply (rule set_plus_mono);
apply (rule bigo_useful_intro);
apply (rule bigo_one_subset_bigo_one_plus_ln);
apply (rule bigo_useful_intro);
apply (rule bigo_ln_subset_bigo_one_plus_ln);
apply (rule bigo_one_subset_bigo_one_plus_ln);
done;
finally show ?thesis;.;
qed;
lemma bigo_pos_mono: "ALL x. 0 <= f x ==>
ALL x. 0 <= g x ==> f =o O(f + g)";
apply (erule bigo_bounded);
apply (auto simp add: func_plus);
apply (subgoal_tac "f x + 0 <= f x + g x");
apply simp;
apply (rule add_left_mono);
apply (erule spec);
done;
lemma Mertens_real_cor: "(%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m) =o O(%x. 1 + ln (abs x + 1))";
apply (rule subsetD);
prefer 2;
apply (rule Mertens_theorem_real2);
apply (rule bigo_plus_absorb2);
apply (rule subsetD);
prefer 2;
apply (rule bigo_pos_mono);
apply force;
apply (subgoal_tac "ALL x. 0 <= (%x. 1) x");
apply assumption;
apply force;
apply (simp add: func_plus);
prefer 2;
apply (rule bigo_elt_subset);
apply (rule bigo_bounded);
apply force;
apply force;
apply (subgoal_tac "(%x. ln (abs x + 1) + 1) = (%x. 1 + ln (abs x + 1))");
apply simp;
apply (rule ext);
apply simp;
done;
lemma Selberg5: "(%x. ∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
Lambda m * Lambda n * ln (real n)) +
(%x. ∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
∑ u | u dvd n. Lambda m * Lambda u * Lambda (n div u)) =o
(%x. (abs x + 1) * ln (abs x + 1) ^ 2) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
proof -;
have "(%x. ∑m=1..natfloor(abs x) + 1.
∑n=1..(natfloor(abs x) + 1) div m.
(Lambda m) * (Lambda n) * ln (real n)) +
(%x. ∑m=1..natfloor(abs x) + 1.
∑n=1..(natfloor(abs x) + 1) div m.
∑u | u dvd n. (Lambda m) * (Lambda u) * (Lambda (n div u))) =
(%x. ∑m=1..natfloor(abs x) + 1. Lambda m *
(∑n=1..natfloor(abs (
(abs x + 1) / (real m) - 1)) + 1.
Lambda n * ln (real n) +
(∑ u | u dvd n. Lambda u * Lambda (n div u))))";
apply (subst func_plus);
apply (rule ext);
apply (subst setsum_addf [THEN sym]);
apply (rule setsum_cong2);
apply (subst setsum_addf [THEN sym]);
apply (subst setsum_const_times [THEN sym]);
apply (subst 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 simp;
apply (rule setsum_cong);
apply simp;
apply (simp add: ring_eq_simps);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
done;
also have "... =o (%x. ∑m=1..natfloor (abs x) + 1.
Lambda m * (2 * (abs(((abs x + 1) / real m) - 1) + 1) *
ln (abs(((abs x + 1) / real m) - 1) + 1))) +o
O(%x. ∑m=1..natfloor (abs x) + 1. Lambda m *
(abs(((abs x + 1) / real m) - 1) + 1))"
(is "?temp =o ?term1 +o O(?term2::real=>real)");
apply (rule bigo_setsum6 [OF Selberg2]);
apply (rule allI)+;
apply (rule Lambda_ge_zero);
apply (rule allI);
apply arith;
done;
also have "?term1 = (%x. ∑m=1..natfloor (abs x) + 1.
Lambda m * (2 * (((abs x + 1) / real m)) *
ln (((abs x + 1) / real m))))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst 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 force;
apply (rule refl);
done;
also have "?term2 = (%x. ∑m=1..natfloor (abs x) + 1. Lambda m *
(((abs x + 1) / real m)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst 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 force;
apply (rule refl);
done;
also; have "(%x. ∑ m = 1..natfloor (abs x) + 1. Lambda m *
(2 * ((abs x + 1) / real m) * ln ((abs x + 1) / real m))) =
(%x. 2 * (abs x + 1)) * (%x. ∑m = 1..natfloor (abs x) + 1.
(Lambda m / real m) * ln ((abs x + 1) / real m))"
(is "?temp = ?term3");
apply (subst func_times);
apply (rule ext);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply (simp only: times_divide_eq_left times_divide_eq_right mult_ac);
done;
also have "(%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m * ((abs x + 1) / real m)) =
(%x. (abs x + 1)) * (%x. (∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m))"
(is "?temp = ?term4");
apply (subst func_times);
apply (rule ext);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply (simp only: times_divide_eq_right mult_ac);
done;
also have "?term3 +o O(?term4) <= ((%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) * O((%x. 1 + ln(abs x + 1))))";
apply (rule set_plus_mono5);
apply (rule set_times_intro2);
prefer 2;
apply (rule order_trans);
apply (rule bigo_mult7);
apply arith;
apply (rule set_times_mono2);
apply force;
apply (rule bigo_elt_subset);
apply (rule Mertens_real_cor);
apply (rule sum_lambda_m_over_m_ln_x_over_m_bigo);
done;
also have "... <= (%x. (abs x + 1) * (ln (abs x + 1))^2) +o
O(%x. (abs x + 1) * (1 + ln(abs x + 1)))";
apply (simp only: func_times set_times_plus_distribs
set_plus_rearranges plus_ac0 mult_ac);
apply (subgoal_tac "(%x. (1 + abs x) * (2 * (ln (1 + abs x) ^ 2 / 2))) =
(%x. (1 + abs x) * (ln (1 + abs x) ^ 2))");
apply (erule ssubst);
apply (rule set_plus_mono);
apply (rule bigo_useful_intro);
apply (rule subset_trans);
apply (rule bigo_mult);
apply (subst func_times);
apply simp;
apply (subgoal_tac "(%x. (1 + abs x) * 2) *o O(%x. 1 + ln (1 + abs x)) =
(%x. 2) *o ((%x. (1 + abs x)) *o O(%x. 1 + ln (1 + abs x)))");
apply (erule ssubst);
apply (subgoal_tac "O(%x. (1 + abs x) * (1 + ln (1 + abs x))) =
(%x. 2) *o O(%x. (1 + abs x) * (1 + ln (1 + abs x))) ");
apply (erule ssubst);
apply (rule set_times_mono);
apply (rule subset_trans);
apply (rule bigo_mult2);
apply (simp add: func_times);
apply (rule bigo_const_mult5 [THEN sym]);
apply force;
apply (simp add: set_times_rearranges func_times mult_ac);
apply (rule ext);
apply simp;
done;
finally show ?thesis;.;
qed;
lemma Selberg6: "(%x. ∑m = 1..natfloor (abs x) + 1.
∑n = 1..(natfloor (abs x) + 1) div m.
Lambda m * Lambda n * ln (real n)) =o
(%x. ln (abs x + 1) / 2 *
(∑m = 1..natfloor (abs x) + 1.
Lambda m * psi (natfloor ((abs x + 1) / real m)))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
proof -;
have "(%x. ∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
Lambda m * Lambda n * ln (real n)) =
(%x. ∑ m = 1..natfloor (abs x) + 1. Lambda m *
(∑ n = 1..(natfloor (abs x) + 1) div m.
Lambda n * ln (real n)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
done;
also have "... =
(%x. ∑ m = 1..natfloor(abs x) + 1. Lambda m *
(∑ n = 1..natfloor(abs( (abs x + 1) / (real m) - 1)) + 1.
Lambda n * ln (real n)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst 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. ∑ m = 1..natfloor (abs x) + 1.
Lambda m * (psi(natfloor(abs ((abs x + 1) / real m - 1)) + 1) *
ln (abs ((abs x + 1) / real m - 1) + 1))) +o
O(%x. ∑ m = 1..natfloor (abs x) + 1. Lambda m *
((abs ((abs x + 1) / real m - 1)) + 1))"
(is "?temp =o ?term1 +o O(?term2::real=>real)");
apply (rule bigo_setsum6 [OF sum_lambda_ln_bigo_real]);
apply (rule allI)+;
apply (rule Lambda_ge_zero);
apply (rule allI);
apply arith;
done;
also have "?term1 = (%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m * (psi(natfloor((abs x + 1) / real m)) *
ln ((abs x + 1) / real m)))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst 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 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 force;
apply (rule refl);
done;
also have "?term2 = (%x. ∑ m = 1..natfloor (abs x) + 1. Lambda m *
((abs x + 1) / real m))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst 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 force;
apply (rule refl);
done;
also have "(%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m * (psi (natfloor ((abs x + 1) / real m)) *
ln ((abs x + 1) / real m))) =
(%x. ln (abs x + 1) * (∑ m = 1..natfloor (abs x) + 1.
Lambda m * psi (natfloor ((abs x + 1) / real m)))) -
(%x. ∑m = 1..natfloor (abs x) + 1.
Lambda m * ln(real m) * psi (natfloor ((abs x + 1) / real m)))";
apply (subst func_diff);
apply (rule ext);
apply (subst setsum_const_times [THEN sym]);
apply (subst setsum_subtractf' [THEN sym]);
apply (rule setsum_cong2);
apply (subst ln_div);
apply arith;
apply force;
apply (simp add: ring_eq_simps);
done;
also have "(%x. ∑m = 1..natfloor (abs x) + 1.
Lambda m * ln(real m) * psi (natfloor ((abs x + 1) / real m))) =
(%x. ∑m = 1..natfloor (abs x) + 1.
Lambda m * ln(real m) * (∑ n = 1..(natfloor (abs x) + 1) div m.
Lambda n))";
apply (rule ext);
apply (rule setsum_cong2);
apply (subst psi_def_alt);
apply (subst natfloor_div_nat);
apply force;
apply force;
apply (subst natfloor_add [THEN sym]);
apply force;
apply simp;
done;
also have "... = (%x. ∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
Lambda m * Lambda n * ln (real n))";
apply (rule ext);
apply (subst general_inversion_nat2_cor1_modified);
apply force;
apply (rule setsum_cong2);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
done;
also have "(%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m * ((abs x + 1) / real m)) =
(%x. abs x + 1) * (%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m)";
apply (subst func_times);
apply (rule ext);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
done;
finally; have " (%x. ∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
Lambda m * Lambda n * ln (real n)) =o
((%x. ln (abs x + 1) *
(∑ m = 1..natfloor (abs x) + 1.
Lambda m * psi (natfloor ((abs x + 1) / real m)))) -
(%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) * (%x. ∑ m = 1..natfloor (abs x) + 1.
Lambda m / real m))"
(is "?LHS =o ?RHS +o ?temp");.;
also have "... <= ?RHS +o ((%x. abs x + 1) *o
O(%x. ∑ m = 1..natfloor (abs x) + 1. Lambda m / real m))";
apply (rule set_plus_mono);
apply (rule bigo_mult5);
apply arith;
done;
also have "... <= ?RHS +o ((%x. abs x + 1) *o O(%x. 1 + ln (abs x + 1)))";
apply (rule set_plus_mono);
apply (rule set_times_mono);
apply (rule bigo_elt_subset);
apply (rule Mertens_real_cor);
done;
also have "... <= ?RHS +o O(%x. (abs x + 1) * (1 + ln (abs x + 1)))"
(is "?temp <= ?RHS +o ?Oterm");
apply (rule set_plus_mono);
apply (rule subset_trans);
apply (rule bigo_mult2);
apply (simp add: func_times);
done;
finally have "?LHS =o ?RHS +o ?Oterm";.;
then have "?LHS + ?LHS =o ?LHS +o (?RHS +o ?Oterm)";
by (rule set_plus_intro2);
also have "?LHS + ?LHS = (%x. 2) * ?LHS";
by (simp add: func_plus func_times);
also; have "?LHS +o (?RHS +o ?Oterm) =
(%x. ln (abs x + 1) *
(∑ m = 1..natfloor (abs x) + 1.
Lambda m * psi (natfloor ((abs x + 1) / real m)))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))"
(is "?temp = ?RHS2");
by (simp add: set_plus_rearranges ring_eq_simps);
finally have "(%x. 1 / 2) * ((%x. 2) * ?LHS) =o (%x. 1 / 2) *o ?RHS2";
by (rule set_times_intro2);
also have "(%x. 1 / 2) * ((%x. 2) * ?LHS) = ?LHS";
by (simp add: func_times);
also have "(%x. 1 / 2) *o ?RHS2 = (%x. ln (abs x + 1) / 2 *
(∑ m = 1..natfloor (abs x) + 1.
Lambda m * psi (natfloor ((abs x + 1) / real m)))) +o
(%x. 1 / 2) *o O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
by (simp add: set_times_plus_distribs func_times);
also have "... <= (%x. ln (abs x + 1) / 2 *
(∑ m = 1..natfloor (abs x) + 1.
Lambda m * psi (natfloor ((abs x + 1) / real m)))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
apply (rule set_plus_mono);
apply (rule bigo_const_mult6);
done;
finally show ?thesis;.;
qed;
lemma Selberg6a: "(%x. ∑m = 1..natfloor (abs x) + 1.
∑n = 1..(natfloor (abs x) + 1) div m.
Lambda m * Lambda n * ln (real n)) =o
(%x. ln (abs x + 1) / 2 *
(∑ n = 1..natfloor (abs x) + 1.
∑ u | u dvd n. Lambda u * Lambda (n div u))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
proof -;
note Selberg6;
also have "(%x. ln (abs x + 1) / 2 *
(∑m = 1..natfloor (abs x) + 1.
Lambda m * psi (natfloor ((abs x + 1) / real m)))) =
(%x. ln (abs x + 1) / 2 *
(∑ n = 1..natfloor (abs x) + 1.
∑ u | u dvd n. Lambda u * Lambda (n div u)))";
apply (rule ext);
apply (rule arg_cong);back;
apply (subst general_inversion_nat2_modified [THEN sym]);
apply force;
apply (rule setsum_cong2);
apply (subst setsum_const_times);
apply (rule arg_cong);back;
apply (subst psi_def_alt);
apply (subst natfloor_div_nat);
apply force;
apply force;
apply (subst natfloor_add [THEN sym]);
apply simp;
apply simp;
done;
finally show ?thesis;.;
qed;
lemma aux4: "f + g =o h +o O(k::'a=>('b::ordered_ring)) ==>
f =o l +o O(k) ==> l + g =o h +o O(k)";
apply (rule set_minus_imp_plus);
apply (drule set_plus_imp_minus)+;
apply (drule bigo_minus);
apply (subgoal_tac "(f - l) + - (f + g - h) =o O(k) + O(k)");
apply simp;
apply (subgoal_tac "l + g - h = -(f - l + (h - (f + g)))");
apply (erule ssubst);
apply (erule bigo_minus);
apply (simp add: ring_eq_simps);
apply (erule set_plus_intro);
apply assumption;
done;
lemma Selberg7: "(%x. ln (abs x + 1) / 2 *
(∑m = 1..natfloor (abs x) + 1.
Lambda m * psi (natfloor ((abs x + 1) / real m)))) +
(%x. ∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
∑ u | u dvd n. Lambda m * Lambda u * Lambda (n div u)) =o
(%x. (abs x + 1) * ln (abs x + 1) ^ 2) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
by (rule aux4 [OF Selberg5, OF Selberg6]);
lemma Selberg7a: "(%x. ln (abs x + 1) / 2 *
(∑ n = 1..natfloor (abs x) + 1.
∑ u | u dvd n. Lambda u * Lambda (n div u))) +
(%x. ∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
∑ u | u dvd n. Lambda m * Lambda u * Lambda (n div u)) =o
(%x. (abs x + 1) * ln (abs x + 1) ^ 2) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
by (rule aux4 [OF Selberg5, OF Selberg6a]);
lemma aux5: "f + g =o h +o O(k::'a=>('b::ordered_ring)) ==>
g + l =o h +o O(k) ==> f =o l +o O(k)";
apply (rule set_minus_imp_plus);
apply (drule set_plus_imp_minus)+;
apply (subgoal_tac "f - l = (f + g - h) + -(g + l - h)");
apply (erule ssubst);
apply (subgoal_tac "O(k) = O(k) + O(k)");
apply (erule ssubst);
apply (rule set_plus_intro);
apply assumption;
apply (erule bigo_minus);
apply simp;
apply (simp add: ring_eq_simps);
done;
lemma Selberg8: "(%x. psi (natfloor (abs x) + 1) * ln (abs x + 1) ^ 2) =o
(%x. 2 * (∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
∑ u | u dvd n. Lambda m * Lambda u * Lambda (n div u))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
proof -;
note Selberg4;
then have "(%x. ln(abs x + 1) / 2) * (
(%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. ln(abs x + 1) / 2) *o
((%x. 2 * (abs x + 1) * ln (abs x + 1)) +o O(%x. abs x + 1))"
(is "?LHS =o ?RHS");
by (rule set_times_intro2);
also have "?LHS = (%x. psi (natfloor (abs x) + 1) * ln (abs x + 1)^2 / 2)
+ (%x. ln(abs x + 1) / 2 * (∑ n = 1..natfloor (abs x) + 1.
∑ u | u dvd n. Lambda u * Lambda (n div u)))";
apply (simp add: set_times_plus_distribs func_times func_plus);
apply (rule ext);
apply (simp add: ring_eq_simps realpow_two2 [THEN sym]);
done;
also have "?RHS = (%x. (abs x + 1) * ln (abs x + 1)^2) +o
(%x. ln(abs x + 1) / 2) *o O(%x. abs x + 1)";
apply (simp add: set_times_plus_distribs func_times
realpow_two2 [THEN sym]);
apply (subgoal_tac "(%x. ln (abs x + 1) * ((2 * abs x + 2) *
ln (abs x + 1)) / 2) =
(%x. (abs x + 1) * (ln (abs x + 1) * ln (abs x + 1)))");
apply (erule ssubst, rule refl);
apply (rule ext);
apply (simp add: ring_eq_simps);
done;
also have "... <= (%x. (abs x + 1) * ln (abs x + 1)^2) +o
(O(%x. 1 + ln(abs x + 1)) * O(%x. abs x + 1))";
apply (rule set_plus_mono);
apply (rule set_times_mono3);
apply (rule bigo_bounded);
apply force;
apply (rule allI);
apply (rule real_le_mult_imp_div_pos_le);
apply force;
apply simp;
apply (subgoal_tac "0 <= ln(abs x + 1)");
apply arith;
apply auto;
done;
also have "... <= (%x. (abs x + 1) * ln (abs x + 1)^2) +o
O((%x. 1 + ln(abs x + 1)) * (%x. abs x + 1))";
apply (rule set_plus_mono);
apply (rule bigo_mult);
done;
also have "(%x. 1 + ln(abs x + 1)) * (%x. abs x + 1) =
(%x. (abs x + 1) * (1 + ln(abs x + 1)))";
apply (rule ext);
apply (subst mult_commute);
apply (subst func_times);
apply (rule refl);
done;
finally have a: "(%x. psi (natfloor (abs x) + 1) * ln (abs x + 1) ^ 2 / 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. (abs x + 1) * ln (abs x + 1) ^ 2) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";.;
have "(%x. psi (natfloor (abs x) + 1) * ln (abs x + 1) ^ 2 / 2) =o
(%x. ∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
∑ u | u dvd n. Lambda m * Lambda u * Lambda (n div u)) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))"
(is "?LHS =o ?RHS1 +o ?RHS2");
by (rule aux5 [OF a, OF Selberg7a]);
then have "(%x. 2) * ?LHS =o (%x. 2) *o (?RHS1 +o ?RHS2)";
by (rule set_times_intro2);
also have "... = (%x. 2) * ?RHS1 +o (%x. 2) *o ?RHS2";
by (rule set_times_plus_distrib);
also have "(%x. 2) * ?LHS =
(%x. psi (natfloor (abs x) + 1) * ln (abs x + 1) ^ 2)";
by (simp add: func_times);
also have "(%x. 2) * ?RHS1 =
(%x. 2 * (∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
∑ u | u dvd n. Lambda m * Lambda u * Lambda (n div u)))";
by (simp add: func_times);
also have "(%x. 2) *o ?RHS2 = ?RHS2";
by (rule bigo_const_mult5, force);
finally show ?thesis;.;
qed;
lemma Selberg8a: "(%x. psi (natfloor (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) *
psi((natfloor (abs x) + 1) div c))) +o
O(%x. (abs x + 1) * (1 + ln (abs x + 1)))";
proof -;
note Selberg8;
also have "(%x. 2 * (∑ m = 1..natfloor (abs x) + 1.
∑ n = 1..(natfloor (abs x) + 1) div m.
∑ u | u dvd n. Lambda m * Lambda u * Lambda (n div u))) =
(%x. 2 * (∑ m = 1..natfloor (abs x) + 1.
∑ c = 1..(natfloor (abs x) + 1) div m.
∑ u = 1..((natfloor (abs x) + 1) div m) div c.
Lambda m * Lambda u * Lambda c))";
apply (rule ext);
apply (rule arg_cong);back;
apply (rule setsum_cong2);
apply (rule sym);
apply (subst general_inversion_nat2_modified);
apply (rule nat_div_gr_0);
apply force;
apply force;
apply (rule setsum_cong2)+;
apply simp;
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 div v) * v))))";
apply (rule ext);
apply (rule arg_cong);back;
apply (subst general_inversion_nat2_cor1_modified);
apply force;
apply (subst general_inversion_nat2_modified [THEN sym]);
apply force;
apply (rule setsum_cong2);
apply (rule setsum_cong2);
apply (subst psi_def_alt);
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong);
apply (subst div_mult2_eq);
apply (rule refl);
apply simp;
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 div v * v)))) =
(%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)))";
apply (rule ext);
apply (rule arg_cong);back;
apply (rule setsum_cong2)+;
apply (subst mult_commute);back;back;back;back;
apply (subst nat_dvd_mult_div);
apply clarsimp;
apply (rule dvd_pos_pos);
prefer 2;
apply assumption;
apply auto;
done;
finally show ?thesis;.;
qed;
end;
lemma Selberg1:
0 < n ==> (ln (real n))² = (∑d | d dvd n. Lambda d * ln (real d) + (∑u | u dvd d. Lambda u * Lambda (d div u)))
lemma Selberg2:
(%x. ∑n = 1..natfloor ¦x¦ + 1. Lambda n * ln (real n) + (∑u | u dvd n. Lambda u * Lambda (n div u))) ∈ (%x. 2 * (¦x¦ + 1) * ln (¦x¦ + 1)) + O(%x. ¦x¦ + 1)
lemma Selberg3:
(%x. ∑n = 1..natfloor ¦x¦ + 1. Lambda n * ln (real n)) + (%x. ∑n = 1..natfloor ¦x¦ + 1. ∑u | u dvd n. Lambda u * Lambda (n div u)) ∈ (%x. 2 * (¦x¦ + 1) * ln (¦x¦ + 1)) + O(%x. ¦x¦ + 1)
lemma sum_lambda_ln_bigo:
(%x. ∑n = 1..x + 1. Lambda n * ln (real n)) ∈ (%x. psi (x + 1) * ln (real (x + 1))) + O(real)
lemma sum_lambda_ln_bigo_real:
(%x. ∑n = 1..natfloor ¦x¦ + 1. Lambda n * ln (real n)) ∈ (%x. psi (natfloor ¦x¦ + 1) * ln (¦x¦ + 1)) + O(%x. ¦x¦ + 1)
lemma Selberg4:
(%x. psi (natfloor ¦x¦ + 1) * ln (¦x¦ + 1)) + (%x. ∑n = 1..natfloor ¦x¦ + 1. ∑u | u dvd n. Lambda u * Lambda (n div u)) ∈ (%x. 2 * (¦x¦ + 1) * ln (¦x¦ + 1)) + O(%x. ¦x¦ + 1)
lemma Selberg4a:
(%x. psi (natfloor ¦x¦ + 1) * ln (¦x¦ + 1)) + (%x. ∑d = 1..natfloor ¦x¦ + 1. Lambda d * psi ((natfloor ¦x¦ + 1) div d)) ∈ (%x. 2 * (¦x¦ + 1) * ln (¦x¦ + 1)) + O(%x. ¦x¦ + 1)
lemma aux:
1 ≤ z ==> natfloor ¦z - 1¦ + 1 = natfloor z
lemma aux2:
1 ≤ z ==> ¦z - 1¦ + 1 = z
lemma sum_lambda_m_over_m_ln_x_over_m_bigo:
(%x. ∑m = 1..natfloor ¦x¦ + 1. Lambda m / real m * ln ((¦x¦ + 1) / real m)) ∈ (%x. (ln (¦x¦ + 1))² / 2) + O(%x. 1 + ln (¦x¦ + 1))
lemma bigo_pos_mono:
[| ∀x. (0::'b) ≤ f x; ∀x. (0::'b) ≤ g x |] ==> f ∈ O(f + g)
lemma Mertens_real_cor:
(%x. ∑m = 1..natfloor ¦x¦ + 1. Lambda m / real m) ∈ O(%x. 1 + ln (¦x¦ + 1))
lemma Selberg5:
(%x. ∑m = 1..natfloor ¦x¦ + 1. ∑n = 1..(natfloor ¦x¦ + 1) div m. Lambda m * Lambda n * ln (real n)) + (%x. ∑m = 1..natfloor ¦x¦ + 1. ∑n = 1..(natfloor ¦x¦ + 1) div m. ∑u | u dvd n. Lambda m * Lambda u * Lambda (n div u)) ∈ (%x. (¦x¦ + 1) * (ln (¦x¦ + 1))²) + O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))
lemma Selberg6:
(%x. ∑m = 1..natfloor ¦x¦ + 1. ∑n = 1..(natfloor ¦x¦ + 1) div m. Lambda m * Lambda n * ln (real n)) ∈ (%x. ln (¦x¦ + 1) / 2 * (∑m = 1..natfloor ¦x¦ + 1. Lambda m * psi (natfloor ((¦x¦ + 1) / real m)))) + O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))
lemma Selberg6a:
(%x. ∑m = 1..natfloor ¦x¦ + 1. ∑n = 1..(natfloor ¦x¦ + 1) div m. Lambda m * Lambda n * ln (real n)) ∈ (%x. ln (¦x¦ + 1) / 2 * (∑n = 1..natfloor ¦x¦ + 1. ∑u | u dvd n. Lambda u * Lambda (n div u))) + O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))
lemma aux4:
[| f + g ∈ h + O(k); f ∈ l + O(k) |] ==> l + g ∈ h + O(k)
lemma Selberg7:
(%x. ln (¦x¦ + 1) / 2 * (∑m = 1..natfloor ¦x¦ + 1. Lambda m * psi (natfloor ((¦x¦ + 1) / real m)))) + (%x. ∑m = 1..natfloor ¦x¦ + 1. ∑n = 1..(natfloor ¦x¦ + 1) div m. ∑u | u dvd n. Lambda m * Lambda u * Lambda (n div u)) ∈ (%x. (¦x¦ + 1) * (ln (¦x¦ + 1))²) + O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))
lemma Selberg7a:
(%x. ln (¦x¦ + 1) / 2 * (∑n = 1..natfloor ¦x¦ + 1. ∑u | u dvd n. Lambda u * Lambda (n div u))) + (%x. ∑m = 1..natfloor ¦x¦ + 1. ∑n = 1..(natfloor ¦x¦ + 1) div m. ∑u | u dvd n. Lambda m * Lambda u * Lambda (n div u)) ∈ (%x. (¦x¦ + 1) * (ln (¦x¦ + 1))²) + O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))
lemma aux5:
[| f + g ∈ h + O(k); g + l ∈ h + O(k) |] ==> f ∈ l + O(k)
lemma Selberg8:
(%x. psi (natfloor ¦x¦ + 1) * (ln (¦x¦ + 1))²) ∈ (%x. 2 * (∑m = 1..natfloor ¦x¦ + 1. ∑n = 1..(natfloor ¦x¦ + 1) div m. ∑u | u dvd n. Lambda m * Lambda u * Lambda (n div u))) + O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))
lemma Selberg8a:
(%x. psi (natfloor ¦x¦ + 1) * (ln (¦x¦ + 1))²) ∈ (%x. 2 * (∑c = 1..natfloor ¦x¦ + 1. ∑v | v dvd c. Lambda v * Lambda (c div v) * psi ((natfloor ¦x¦ + 1) div c))) + O(%x. (¦x¦ + 1) * (1 + ln (¦x¦ + 1)))