# Theory Chebyshev3

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

theory Chebyshev3 = Chebyshev2 + BigO:

```(*  Title:      Chebyshev3.thy
Author:     Paul Raff and Jeremy Avigad
*)

theory Chebyshev3 = Chebyshev2 + BigO:;

subsection {* theta(x) = O(x) and psi(x) = O(x) *}

(* Most of the following involves Section 8.1 in Nathanson's book *)

lemma prime_dvd_binomial: "m + 2 <= p ==> p <= Suc(2*m) ==> 1 <= m ==> p : prime ==> p dvd (Suc(2*m) choose m)";
apply (simp only: binomial_odd_def);
apply (rule dvd_div);
apply force;
apply (simp only: prime_divides_product);
apply (subst factorial_setprod_def [THEN sym]);
apply (subgoal_tac "m+2 = Suc(m+1)");
apply (erule ssubst);
apply (subgoal_tac "setprod id {1..m} = setprod id {1..(Suc(2*m) - (m+1))}");
apply (erule ssubst);
apply (simp only: binomial_setprod_mod);
apply force+;
done;

lemma product_dvd_M: " 1 <= m ==> setprod id {p. p: prime & m+2 <= p & p <= Suc(2*m)} dvd (Suc(2*m) choose m)";
apply (rule prime_product_dvd);
apply (subgoal_tac "{p::nat. p : prime & m + (2::nat) <= p & p <= Suc ((2::nat) * m)} <= {1..Suc(2*m)}");
done;

lemma product_lt_M: " 1 <= m  ==> setprod id {p. p: prime & m+2 <= p & p <= Suc(2*m)} <= (Suc(2*m) choose m)";
apply (rule dvd_imp_le);
apply (simp only: product_dvd_M);
apply simp;
done;

lemma product_lt_4_to_m: "1 <= m ==> setprod id {p. p: prime & m+2 <= p & p <= Suc(2*m)} < (4::nat)^m";
apply (rule le_less_trans [of "setprod id {p. p: prime & m+2 <= p & p <= Suc(2*m)}" "(Suc(2*m) choose m)" "4^m"]);
apply (simp only: product_lt_M);
apply (simp only: binomial_sum_lemma_4);
done;

lemma product_primes_induction_step: "ALL m < n. (setprod id {p. p : prime & p <= (Suc m)} < 4^(Suc m))
==> setprod id {p. p : prime & p <= Suc n} < 4^(Suc n)";
apply (case_tac "n = 0");
apply (erule ssubst);
apply (subgoal_tac "{p::nat. p : prime & p <= Suc 0} = {}");
apply (erule ssubst);
apply force+;
apply clarsimp;
apply (subgoal_tac "2 <= x");
apply force;
apply (case_tac "n = 1");
apply (erule ssubst);
apply (subgoal_tac "{p::nat. p : prime & p <= Suc 1} = {2}");
apply (erule ssubst);
apply force;
apply clarsimp;
apply auto;
apply (subgoal_tac "2 <= x");
apply (force intro: le_anti_sym);
apply (force intro: primes_always_ge_2);
apply (subgoal_tac "2 <= n");
apply auto;
apply (case_tac "even (Suc n)");
apply (subgoal_tac "Suc n ~: prime");
apply (subgoal_tac "{p::nat. p : prime & p <= Suc n} = {p::nat. p : prime & p <= Suc (n - 1)}");
apply (erule ssubst);
apply (frule_tac x = "n - 1" in spec);
apply (frule mp);
apply force;
apply (subgoal_tac "4 * 4^(n - 1) <= 4 * 4 ^ n");
apply (erule order_less_le_trans);
apply assumption+;
apply (rule mult_left_mono);
apply (rule power_increasing);
apply force+;
apply auto;
apply (case_tac "x = Suc n");
apply (frule only_even_prime);
apply simp;
apply arith;
(* at this point, all we have is the odd case - time to use the IH *)
(*  apply (subgoal_tac "odd(Suc n)");
prefer 2;
apply simp;
apply (simp only: odd_nat_equiv_def2);
*)
apply (subgoal_tac "EX y. n = Suc(Suc 0) * y");
apply (erule exE);
apply (subgoal_tac "Suc y <= n");
apply (subgoal_tac "1 <= y");
apply (erule ssubst);
(*
apply (subgoal_tac "y = Suc(y - 1)");
prefer 2;
apply force;
*)
apply (subgoal_tac "{p::nat. p : prime & p <= Suc(Suc (Suc 0) * y)} =
{p::nat. p : prime & p <= Suc y} Un {p::nat. p : prime & (y+2) <= p & p <= Suc(2*y)}");
apply (erule ssubst);
apply (subst setprod_Un_disjoint);
apply (subgoal_tac "{p::nat. p : prime & p <= Suc y} <= {0..Suc y}");
apply force+;
apply (subgoal_tac "{p::nat. p : prime & y + (2::nat) <= p & p <= Suc ((2::nat) * y)} <= {0..Suc(2*y)}");
apply force+;
apply (frule_tac x = "y" in spec);
apply (frule mp);
apply force;
apply (subgoal_tac "setprod id {p::nat. p : prime & y + (2::nat) <= p & p <= Suc ((2::nat) * y)} < 4^y");
apply (subgoal_tac "0 < (4::nat) ^ Suc y");
apply (subgoal_tac "0 <= setprod id {p::nat. p : prime & y + (2::nat) <= p & p <= Suc ((2::nat) * y)}");
apply (subgoal_tac "4 * 4^(Suc (Suc 0) * y) = 4^Suc y * 4^y");
apply (erule ssubst);
apply (rule mult_strict_mono);
apply (subst power_Suc);
apply assumption+;
apply auto;
apply force;
apply (subgoal_tac "Suc (Suc y) = y+2");
apply (erule ssubst);
apply (simp only: product_lt_4_to_m);
apply force+;
apply (simp only: even_nat_equiv_def2);
apply auto;
done;

lemma product_primes_lt_4_to_n_aux: "setprod id {p. p: prime & p <= Suc n} < 4^(Suc n)";
apply (rule nat_less_induct [of _ n]);
apply (erule product_primes_induction_step);
done;

lemma product_primes_lt_4_to_n [rule_format]: "1 <= n ==> setprod id {p. p : prime & p <= n} < 4^n";
apply (subgoal_tac "n = Suc (n - 1)");
apply (erule ssubst);
apply (rule product_primes_lt_4_to_n_aux);
apply simp;
done;

lemma theta_bound: "1 <= n ==> theta n < real(n) * ln(4)";
proof-;
assume n: "1 <= n";
have "theta n = ln (real (setprod id {p::nat. p : prime & p <= n}))";
apply (rule theta_def_2);
done;
also have step1: "... < ln (real ((4::nat)^n))";
apply (subgoal_tac "0 < real (setprod id {p::nat. p : prime & p <= n})");
apply (subgoal_tac "0 < real ((4::nat)^n)");
apply (simp only:  ln_less_cancel_iff);
apply (simp only: real_of_nat_less_iff);
apply (rule product_primes_lt_4_to_n);
apply (rule n);
apply (subgoal_tac "0 < (4::nat)^n");
apply (simp only: real_of_nat_less_iff [THEN sym]);
apply force;
apply (subgoal_tac "0 < setprod id {p::nat. p : prime & p <= n}");
apply (simp only: real_of_nat_less_iff [THEN sym]);
apply (case_tac "n = 0");
apply (subgoal_tac "1 <= n");
apply force;
apply (rule n);
apply (case_tac "n = 1");
apply (simp);
apply (subgoal_tac "{p::nat. p : prime & p <= Suc (0::nat)} = {}");
apply (erule ssubst);back;
apply force;
apply auto;
apply (subgoal_tac "2 <= x");
apply force;
apply (erule primes_always_ge_2);
apply (subgoal_tac "2 <= n");
apply (subst setprod_gt_0_iff);
apply (rule finite_subset [of _ "{0..n}"]);
apply force+;
done;
also have "... = real n * ln(4::real)";
apply (subst realpow_real_of_nat [THEN sym]);
apply (subst ln_realpow);
apply force;
apply force;
done;
finally show ?thesis;.;
qed;

lemma theta_bound2: "theta n <= ln 4 * real n";
apply (case_tac "n = 0");
apply (subst mult_commute);
apply (rule order_less_imp_le);
apply (rule theta_bound);
apply auto;
done;

lemma theta_bigo: "theta =o O(%x. real x)";
apply (rule bigo_bounded_alt);
apply (rule allI);
apply (rule theta_geq_zero);
apply (rule allI);
apply (rule theta_bound2);
done;

lemma psi_bigo_aux:
"(%x. real((x::nat) + 1) powr (1/2) * ln(real(x + 1)) * ln(real(x + 1))) =o
O(%x. real (x + 1))";
apply (rule bigo_bounded_alt);
apply (rule allI);
apply (rule nonneg_times_nonneg)+;
apply (rule order_less_imp_le);
apply force+;
apply (rule allI);
apply (subgoal_tac "real (x + 1) powr (1 / 2) * ln (real (x + 1)) *
ln (real (x + 1)) <=
(real (x + 1) powr (1 / 2)) * ((real (x + 1) powr (1 / 4)) / (1 / 4)) *
((real (x + 1) powr (1 / 4)) / (1 / 4))");
apply (rule mult_mono)+;
apply force;
apply (rule ln_powr_bound);
apply force+;
apply (rule ln_powr_bound);
apply force+;
apply (rule nonneg_times_nonneg);
apply force+;
done;

lemma psi_bigo_aux2: "(%x. psi (x + 1)) =o O(%x. real (x + 1))";
proof -;
have "(%x. psi (x + 1)) =o O((%x. theta(x + 1)) +
(%x. real(x + 1) powr (1/2) * ln(real(x + 1)) * ln(real(x + 1)) / ln 2))";
apply (rule bigo_bounded);
apply (rule allI);
apply (rule psi_ge_zero);
apply (rule allI);
apply (rule psi_theta_bound_for_real);
apply force;
done;
also have "... <= O(%x. real(x + 1)) + O(%x. real(x + 1))";
apply (rule subset_trans);
apply (rule bigo_plus_subset);
apply (rule set_plus_mono2);
apply (rule bigo_elt_subset);
apply (rule bigo_compose1 [OF theta_bigo]);
apply (rule bigo_elt_subset);
apply (rule subsetD);
apply (subgoal_tac "(%x. 1 / ln 2) *o O(%x. real(x + 1)) <=
O(%x. real(x + 1))");
apply assumption;
apply (rule bigo_const_mult6);
apply (subgoal_tac "(%x. real (x + 1) powr (1 / 2) *
ln (real (x + 1)) * ln (real (x + 1)) / ln 2) = (%x. 1 / ln 2) *
(%x. real (x + 1) powr (1 / 2) * ln (real (x + 1)) *
ln (real (x + 1)))");
apply (erule ssubst);
apply (rule set_times_intro2);
apply (rule psi_bigo_aux);
done;
also have "... = O(%x. real(x + 1))";
by simp;
finally show ?thesis;.;
qed;

lemma psi_bigo: "psi =o O(%x. real x)";
apply (rule bigo_fix2);
apply (rule psi_bigo_aux2);
apply (rule psi_zero);
done;

lemma theta_le_psi: "theta x <= psi x";
apply (unfold theta_def);
apply (unfold psi_def);
apply (rule sumr_le_cong);
apply (unfold lprime_def);
apply (case_tac "y : prime");
apply simp;
apply (subgoal_tac "Lambda y = Lambda (y^1)");
apply (erule ssubst);
apply (subst Lambda_eq);
apply auto;
apply (rule Lambda_ge_zero);
done;

lemma psi_theta_lim1: "(%x. psi (x + 1)) =o (%x. theta(x + 1)) +o
O(%x. real(x + 1) powr (1/2) * ln(real(x + 1)) * ln(real(x + 1)) / ln 2)";
apply (rule set_minus_imp_plus);
apply (subst func_diff);
apply (rule bigo_bounded);
apply (rule allI);
apply simp;
apply (rule theta_le_psi);
apply (rule allI);
apply (simp only: compare_rls);
apply (rule psi_theta_bound_for_real);
apply force;
done;

lemma psi_theta_lim2:
"O(%x::nat. real(x + 1) powr (1/2) * ln(real(x + 1)) * ln(real(x + 1))
/ ln 2) <= O(%x. real(x + 1) powr (3 / 4))";
apply (rule bigo_elt_subset);
apply (rule bigo_bounded_alt);
apply (rule allI);
apply (rule real_ge_zero_div_gt_zero);
apply (rule nonneg_times_nonneg)+;
apply (rule order_less_imp_le);
apply force+;
apply (rule allI);
apply (subgoal_tac "real (x + 1) powr (1 / 2) * ln (real (x + 1)) *
ln (real (x + 1)) / ln 2 <=
(real (x + 1) powr (1 / 2)) * ((real (x + 1) powr (1 / 8)) / (1 / 8)) *
((real (x + 1) powr (1 / 8)) / (1 / 8)) / ln 2");
apply (subgoal_tac "64 * real (Suc x) powr (1 / 2 + 1 / 4) / ln 2 =
(64 / ln 2) * real (Suc x) powr (3 / 4)");
apply (erule subst);
apply assumption;
apply (subgoal_tac "(1::real) / 2 + 1 / 4 = 3 / 4");
apply (erule ssubst);
apply simp;
apply simp;
apply (rule divide_right_mono)
apply (rule mult_mono)+;
apply force;
apply (rule ln_powr_bound);
apply force+;
apply (rule ln_powr_bound);
apply force+;
apply (rule nonneg_times_nonneg);
apply force+;
done;

lemma psi_theta_lim3: "(%x. psi (x + 1) / real (x + 1)) =o
(%x. theta (x + 1) / real(x + 1)) +o O(%x. real(x + 1) powr (- (1 / 4)))";
proof -;
have "(%x. psi(x + 1) / real (x + 1)) =
(%x. 1 / (real (x + 1))) * (%x. psi(x + 1))";
also have "... =o (%x. 1 / (real (x + 1))) *o ((%x. theta (x + 1)) +o
O(%x. real(x + 1) powr (3 / 4)))";
apply (rule set_times_intro2);
apply (rule subsetD);
prefer 2;
apply (rule psi_theta_lim1);
apply (rule set_plus_mono);
apply (rule psi_theta_lim2);
done;
also have "... = (%x. theta (x + 1) / real (x + 1)) +o
(%x. 1 / (real (x + 1))) *o O(%x. real(x + 1) powr (3 / 4))";
also have "... <= (%x. theta (x + 1) / real (x + 1)) +o
O(%x. real(x + 1) powr (- (1 / 4)))";
apply (rule set_plus_mono);
apply (rule subset_trans);
apply (rule bigo_mult2);
apply (subgoal_tac "(%x. real (Suc x) powr (3 / 4) / real (Suc x))
= (%x. real (Suc x) powr - (1 / 4))");
apply (erule ssubst);
apply (rule order_refl);
apply (rule ext);
apply (subst nonzero_divide_eq_eq);
apply force;
apply (subgoal_tac "3 / 4 = -(1 / 4) + 1");
apply (erule ssubst);
apply simp;
apply simp;
done;
finally show ?thesis;.;
qed;

lemma psi_theta_lim4: "(%x. psi x / real x) ----> 1 ==>
(%x. theta x / real x) ----> 1";
apply (subgoal_tac "(%x. theta (x + 1) / (real (x + 1))) ----> 1");
apply (erule LIMSEQ_offset);
apply (rule bigo_LIMSEQ2);
apply (rule psi_theta_lim3);
apply (rule LIMSEQ_ignore_initial_segment);
apply (rule LIMSEQ_neg_powr);
apply force;
apply (erule LIMSEQ_ignore_initial_segment);
done;

subsection {* theta and pi *}

lemma theta_pi_rel1: "1 <= x ==> 0 < (d::real) ==> d < 1 ==>
(1 - d)*pi(x) * ln(real(x)) - real(x) powr (1 - d) * ln(real(x)) <=   theta x";
proof-;
assume "1 <= x" and "0 < d" and "d < 1";
have "(1 - d)*pi(x) * ln(real(x)) - real(x) powr (1 - d) * ln(real(x)) <= (1 - d)*pi(x) * ln(real(x)) - (1 - d)*real(x) powr (1 - d) * ln(real(x))";
apply auto;
apply (subst times_ac1_one_right [THEN sym]);
apply (subst mult_commute);
apply (subst mult_assoc);
apply (rule mult_mono);
apply (insert prems, arith);
apply force+;
apply (subst zero_le_mult_iff);
apply (rule disjI1);
apply auto;
apply (insert powr_gt_zero [of "real x" "((1::real) - d)"]);
done;
also have "... <= (1 - d)*pi(x) * ln(real(x)) - (1 - d)*real(nat(floor(real(x) powr (1 - d)))) * ln(real(x))";
apply auto;
apply (rule mult_right_mono);
apply (rule mult_left_mono);
apply (rule real_nat_floor);
apply (rule order_less_imp_le);
apply (insert prems, auto);
done;
also have "... <= ((1::real) - d) * pi x * ln (real x) -
((1::real) - d) * pi (nat (floor (real x powr ((1::real) - d)))) * ln (real x)";
apply auto;
apply (rule mult_right_mono);
apply (rule mult_left_mono);
apply (rule pi_less);
apply (insert prems, auto);
done;
also have "... = (1 - d)*(pi(x) - pi(nat(floor(real x powr (1 - d)))))*ln (real x)";
apply (subst right_diff_distrib);
apply (subst left_diff_distrib);
apply simp;
done;
also have "... = setsum (%y. (1 - d)*ln (real x)) {z::nat. nat(floor(real x powr (1 - d))) < z & z <= x & z : prime}";
apply (subst pi_diff);
apply auto;
apply (subst real_of_nat_le_iff [THEN sym]);
apply (rule real_le_trans [of "real(nat(floor(real x powr (1-d))))" "real x powr (1 - d)" "real x"]);
apply (rule real_nat_floor);
apply (rule order_less_imp_le);
apply (rule powr_gt_zero);
apply (subgoal_tac "real x = real x powr 1");
apply (erule ssubst);back;
apply (case_tac "x = 1");
apply (erule ssubst);
apply force;
apply (subst powr_le_cancel_iff);
apply (insert prems, force+);
apply (subst mult_assoc);
apply (subst mult_commute);back;back;
apply (subst mult_assoc [THEN sym]);
apply (subst setsum_real);
apply (rule finite_subset [of _ "{0..x}"]);
apply force;
apply force;
apply simp;
apply (subst setsum_multiplier_real);
apply (rule finite_subset [of _ "{0..x}"]);
apply force+;
done;
also have "... = (∑y:{z. nat (floor (real x powr (1 - d))) < z & z <= x & z : prime}. ln (real x powr (1 - d)))";
apply (rule setsum_cong);
apply force;
apply (subst powr_def);
apply simp;
done;
also have "... <= (∑y:{z. nat (floor (real x powr (1 - d))) < z & z <= x & z : prime}. ln (real y))";
apply (rule setsum_le_cong);
apply auto;
apply (rule order_less_imp_le);
apply (rule order_less_le_trans [of _ "real (natfloor (real x powr (1 - d))) + 1" _]);
apply (simp only: natfloor_def);
done;
also have "... <= theta x";
apply (simp only: theta_setsum_pos_def);
apply (rule order_trans [of _ "setsum (%y. ln ( real y)) {z. 2 <= z & z <= x & z : prime}"]);
apply (rule setsum_subset);
apply (rule finite_subset [of _ "{0..x}"]);
apply force+;
apply auto;
apply (subgoal_tac "1 <= real xa");
apply force;
apply (frule primes_always_ge_2);
apply arith;
apply (subgoal_tac "(∑y:{z. 2 <= z & z <= x & z : prime}. ln (real y)) = (∑y:{z. 2 <= z & z <= x & z : prime}. (lprime y))");
apply (erule ssubst);
apply (rule setsum_subset);
apply (blast);
apply force+;
apply auto;
apply (frule primes_always_ge_1);
apply force;
apply (rule setsum_cong);
apply force;
apply auto;
done;
finally show ?thesis;.;
qed;

lemma theta_pi_rel2: "1 <= x ==> 0 < d ==> d < 1 ==> pi(x) * ln(real x) / (real x) <=
theta(x) / ((1 - d) * (real x)) + ln(real x) / ((1 - d) * (real x) powr d)";
proof-;
assume "1 <= x" and "0 < d" and "d < 1";
have step1: "(1 - d)*pi(x) * ln(real(x)) - real(x) powr (1 - d) * ln(real(x)) <=   theta x";
apply (rule theta_pi_rel1);
apply (insert prems, auto);
done;
then have step2: "(1 - d)*pi(x) * ln(real(x)) <= theta x + real(x) powr (1 - d) * ln(real(x))";
apply auto;
done;
then have step3: "(1 - d)*pi(x) * ln(real(x)) / ((1 - d) * real(x)) <= (theta x + real(x) powr (1 - d) * ln(real(x))) / ((1 - d) * real(x))";
apply (rule divide_right_mono);
apply (rule nonneg_times_nonneg);
apply (insert prems, auto);
done;
then have step4: "pi(x) * ln(real(x)) / real(x) <= (theta x + real(x) powr (1 - d) * ln(real(x))) / ((1 - d) * real(x))";
apply (insert prems, auto);
done;
then have step5: "(1 - d)*pi(x) * ln(real(x)) / ((1 - d) * real(x)) <= theta x / ((1 - d) * real(x)) + real(x) powr (1 - d) * ln(real(x)) / ((1 - d) * real(x))";
apply auto;
done;
then have step6: "(1 - d)*pi(x) * ln(real(x)) / ((1 - d) * real(x)) <= theta x / ((1 - d) * real(x)) + real(x) powr (1 - d) * ln(real(x)) / ((1 - d) * (real(x) powr 1))";
apply (insert prems, auto);
done;
then have step7: "(1 - d)*pi(x) * ln(real(x)) / ((1 - d) * real(x)) <= theta x / ((1 - d) * real(x)) + ln(real(x)) / ((1 - d) * (real(x) powr d))";
apply (subgoal_tac "ln (real x) / ((1 - d) * real x powr d) = (ln (real x) / (1 - d)) * (real x powr (1 - d) / real x powr 1)");
apply (erule ssubst);
apply (insert prems, simp add: mult_commute);
apply (simp only: powr_divide_denom);
apply simp;
done;
then show ?thesis;
apply (insert prems, simp);
done;
qed;

lemma theta_pi_rel3: "1 <= x ==> 0 < d ==> d < 1 ==> pi x * ln (real x) / real x - theta(x) / (real x) <= (theta x / (real x))*(d / (1 - d)) + ln (real x) / ((1 - d) * real x powr d)";
proof-;
assume "1 <= x" and "0 < d" and "d < 1";
have "pi(x) * ln(real x) / (real x) <=
theta(x) / ((1 - d) * (real x)) + ln(real x) / ((1 - d) * (real x) powr d)";
by (insert prems, simp only: theta_pi_rel2);
then have step1: "pi(x) * ln(real x) / (real x) - theta(x) / (real x) <=
theta(x) / ((1 - d) * (real x)) - theta(x) / (real x) + ln(real x) / ((1 - d) * (real x) powr d)";
apply (insert prems, arith);
done;
then have step2: "pi(x) * ln(real x) / (real x) - theta(x) / (real x) <=
(theta(x) - ((1 - d) * theta(x))) / ((1 - d) * (real x)) + ln(real x) / ((1 - d) * (real x) powr d)";
apply (subst diff_divide_distrib);
apply (subst mult_divide_cancel_left);
apply (insert prems, force);
apply simp;
done;
then have step3: "pi(x) * ln(real x) / (real x) - theta(x) / (real x) <=
(theta(x)*(1  - (1 - d))) / ((1 - d) * (real x)) + ln(real x) / ((1 - d) * (real x) powr d)";
apply (subst right_diff_distrib);
apply (subst times_ac1_one_right);
apply (simp only: mult_commute);
done;
then have step4: "pi(x) * ln(real x) / (real x) - theta(x) / (real x) <=
(theta(x)*d) / ((1 - d) * (real x)) + ln(real x) / ((1 - d) * (real x) powr d)";
apply (auto);
done;
then have step5: "pi(x) * ln(real x) / (real x) - theta(x) / (real x) <=
(theta(x) / real x)*(d / (1 - d)) + ln(real x) / ((1 - d) * (real x) powr d)";
done;
then show ?thesis;.;
qed;

lemma theta_pi_rel4: "1 <= x ==> 0 < d ==> d < 1 ==> pi x * ln (real x) / real x - theta(x) / (real x) <= (theta x / (real x))*(d / (1 - d)) + (2::real) / ((1 - d)*d) * (real x) powr (- d / 2)";
proof-;
assume "1 <= x" and "0 < d" and "d < 1";
have "pi x * ln (real x) / real x - theta(x) / (real x) <= (theta x / (real x))*(d / (1 - d)) + ln (real x) / ((1 - d) * real x powr d)";
by (rule theta_pi_rel3);
also have "... <= (theta x / (real x))*(d / (1 - d)) + ((real x) powr (d / 2)/(d/2)) / ((1 - d) * real x powr d)";
apply (rule divide_right_mono);
apply (rule ln_powr_bound);
apply (insert prems, auto);
apply (rule nonneg_times_nonneg);
apply (auto);
done;
also have "... = (theta x / (real x))*(d / (1 - d)) + ((2::real) * (real x) powr (d / 2)) / ((1 - d) * d * real x powr d)";
apply auto;
apply (subgoal_tac "d * ((1 - d) * real x powr d) = (1 - d) * d * real x powr d");
apply (erule ssubst);
apply (rule fun_cong);back;
apply auto;
done;
also have "... = (theta x / (real x))*(d / (1 - d)) + (2::real) / ((1 - d) * d) * (real x) powr (- d / 2)";
apply (insert prems, auto);
apply (subgoal_tac "2 * real x powr (d / 2) / ((1 - d) * d * real x powr d) = (2 / ((1 - d) * d)) * (real x powr (d/2) / real x powr d)");
apply (erule ssubst);
apply (subst powr_divide2);
apply clarsimp;
apply (subgoal_tac "d / 2 - d = - (d / 2)");
apply (erule ssubst);
apply force+;
done;
finally show ?thesis;.;
qed;

lemma theta_pi_rel5: "1 <= x ==> 0 < d ==> d < 1 ==> abs (pi x * ln (real x) / real x - theta(x) / (real x)) <= (theta x / (real x))*(d / (1 - d)) + (2::real) / ((1 - d)*d) * (real x) powr (- d / 2)";
apply (subst abs_eqI1);
apply simp;
apply (rule divide_right_mono);
apply (subst l.sum_over_F2 [THEN sym]);
apply (subst pi_setsum_def);
apply (subst setsum_real);
apply (rule finite_subset [of _ "{0..x}"]);
apply force+;
apply (subst mult_commute);
apply (subst setsum_multiplier_real);
apply (rule finite_subset [of _ "{0..x}"]);
apply force+;
apply simp;
apply (subgoal_tac "{p. p : prime & p <= x} = {y. y <= x & y : prime}");
apply (erule ssubst);
apply (rule setsum_le_cong);
apply (subst ln_le_cancel_iff);
apply clarify;
apply (frule primes_always_ge_2);
apply arith;
apply clarify;
apply (frule primes_always_ge_2);
apply arith;
apply clarify;
apply blast;
apply arith;
apply (simp only: theta_pi_rel4);
done;

lemma theta_pi_rel6_aux1: "0 < (d::real) ==> d < 1/2 ==> d < 1 - d";
apply arith;
done;

lemma theta_pi_rel6_aux2: "0 < (d::real) ==> d < 1/2 ==> (d / (1 - d)) < 1";
apply (subgoal_tac "0 < (1 - d)");
apply (frule theta_pi_rel6_aux1);
apply simp;
apply (frule divide_strict_right_mono [of "d" "1 - d" "1 - d"]);
apply force+;
done;

lemma theta_pi_rel6_aux3: "0 < (d::real) ==> d < 1/2 ==> 2 / (d * (1 - d)) < 4 / d";
apply (subst pos_divide_less_eq);
apply (rule real_mult_order);
apply force+;
done;

lemma theta_pi_aux1: "0 < (d::real) ==> d < 1/2 ==> 1 / (1 - d) < 2";
apply (subst pos_divide_less_eq);
apply force+;
done;

lemma theta_pi_rel6: "1 <= x ==> 0 < d ==> d < 1/2 ==> abs (pi x * ln (real x) / real x - theta(x) / (real x)) <= theta(x) / real x + 4 / d * (real x) powr (- d / 2)";
proof-;
assume "1 <= x" and "0 < d" and "d < 1/2";
have lt: "d < 1";
apply (insert prems, auto);
done;
have "abs (pi x * ln (real x) / real x - theta(x) / (real x)) <= (theta x / (real x))*(d / (1 - d)) + (2::real) / ((1 - d)*d) * (real x) powr (- d / 2)";
apply (insert prems lt);
by (simp only: theta_pi_rel5);
also have "...  <= (theta x / (real x)) + (2::real) / ((1 - d)*d) * (real x) powr (- d / 2)";
apply simp;
apply (subgoal_tac "theta x * d / (real x * (1 - d)) = (theta x / real x) * (d / (1 - d))");
apply (erule ssubst);
apply (subgoal_tac "theta x / real x = (theta x / real x) * 1");
apply (erule ssubst);back;
apply (rule mult_left_mono);
apply (rule order_less_imp_le);
apply (insert prems);
apply (rule real_ge_zero_div_gt_zero);
done;
also have "... <= (theta x / (real x)) + (4 / d) * (real x) powr (- d / 2)";
apply simp;
apply (subgoal_tac "2 * real x powr - (d / 2) / ((1 - d) * d) = (2 / (d * (1 - d))) * real x powr - (d / 2)");
apply (erule ssubst);
apply (subgoal_tac "4 * real x powr - (d / 2) / d = (4 / d) * real x powr - (d / 2)");
apply (erule ssubst);
apply (insert prems);
apply (rule mult_right_mono);
apply (rule order_less_imp_le);
apply (simp only: theta_pi_rel6_aux3);
apply (rule order_less_imp_le);
apply force+;
done;
finally show ?thesis;.;
qed;

lemma theta_pi_rel7: "1 <= x ==> 0 < d ==> d < 1/2 ==> abs (pi x * ln (real x) / real x - theta(x) / (real x)) <= ln 4 + 4 / d * (real x) powr (- d / 2)";
proof-;
assume "1 <= x" and "0 < d" and "d < 1/2";
have "abs (pi x * ln (real x) / real x - theta(x) / (real x)) <= theta(x) / real x + 4 / d * (real x) powr (- d / 2)";
apply (insert prems);
apply (rule theta_pi_rel6);
apply auto;
done;
also have "... <= ln 4 + 4 / d * (real x) powr (- d / 2)";
apply simp;
apply (insert prems, auto);
apply (subst pos_divide_le_eq);
apply force;
apply (subst mult_commute);
apply (rule order_less_imp_le);
apply (rule theta_bound);
apply auto;
done;
finally show ?thesis;.;
qed;

lemma theta_pi_rel8: "1 <= x ==> 0 < d ==> d < 1/2 ==> abs (pi x * ln (real x) / real x - theta(x) / (real x)) <= 2 * d * theta(x) / real x + 4 / d * (real x) powr (- d / 2)";
proof-;
assume "1 <= x" and "0 < d" and "d < 1/2";
have lt: "d < 1";
apply (insert prems, auto);
done;
have "abs (pi x * ln (real x) / real x - theta(x) / (real x)) <= (theta x / (real x))*(d / (1 - d)) + (2::real) / ((1 - d)*d) * (real x) powr (- d / 2)";
apply (insert prems lt);
by (simp only: theta_pi_rel5);
also have "...  <= 2 * d * (theta x / (real x)) + (2::real) / ((1 - d)*d) * (real x) powr (- d / 2)";
apply simp;
apply (subgoal_tac "theta x * d / (real x * (1 - d)) = (1 / (1 - d)) * d * (theta x / real x)");
apply (erule ssubst);
apply (subgoal_tac "2 * d * theta x / real x = 2 * d * (theta x / real x)");
apply (erule ssubst);
apply (rule mult_right_mono);
apply (rule order_less_imp_le);
apply (insert prems);
apply auto;
apply (subgoal_tac "d / (1 - d) = (1 / (1 - d)) * d");
apply (erule ssubst);
apply (rule mult_strict_right_mono);
apply force+;
apply (rule real_ge_zero_div_gt_zero);
done;
also have "... <= 2 * d * (theta x / (real x)) + (4 / d) * (real x) powr (- d / 2)";
apply simp;
apply (subgoal_tac "2 * real x powr - (d / 2) / ((1 - d) * d) = (2 / (d * (1 - d))) * real x powr - (d / 2)");
apply (erule ssubst);
apply (subgoal_tac "4 * real x powr - (d / 2) / d = (4 / d) * real x powr - (d / 2)");
apply (erule ssubst);
apply (insert prems);
apply (rule mult_right_mono);
apply (rule order_less_imp_le);
apply (simp only: theta_pi_rel6_aux3);
apply (rule order_less_imp_le);
apply force+;
done;
finally show ?thesis;
apply simp;
done;
qed;

lemma theta_pi_rel9: "1 <= x ==> 0 < d ==> d < 1 / 2 ==>
abs (pi x * ln (real x) / real x - theta(x) / (real x)) <=
2 * d * ln 4 + 4 / d * (real x) powr (- d / 2)";
proof-;
assume "1 <= x" and "0 < d" and "d < 1/2";
have "abs (pi x * ln (real x) / real x - theta(x) / (real x)) <= 2 * d * theta(x) / real x + 4 / d * (real x) powr (- d / 2)";
apply (insert prems, simp only: theta_pi_rel8);
done;
also have "... <= 2 * d * ln 4 + 4 / d * (real x) powr (- d / 2)";
apply auto;
apply (subgoal_tac "2 * d * theta x / real x = 2 * d * (theta x / real x)");
apply (erule ssubst);
apply (insert prems);
apply (rule mult_left_mono)+;
apply (subst pos_divide_le_eq);
apply force;
apply (subst mult_commute);
apply (rule order_less_imp_le);
apply (rule theta_bound);
apply auto;
done;
finally show ?thesis;.;
qed;

(*
lemma temp: "1 <= x ==> 0 < d ==> d < 1 / 2 ==>
abs (pi x * ln (real x) / real x - theta(x) / (real x)) <=
2 * ln 4 * d + (4::real) / d * (real x) powr (- d / 2)"
sorry;
*)

lemma aux: "0 < d ==> 0 < r ==> EX (no::nat). ALL n. (no <= n -->
(4::real) / d * (real n) powr (- d / 2) < r)";
proof -;
assume "0 < d" and "0 < r";
have "(%x. (real x) powr (- (d / 2))) ----> 0";
apply (rule LIMSEQ_neg_powr);
done;
then have "(%x. (4::real) / d * (real x) powr (- d / 2)) ---->
4 / d * 0";
apply (intro LIMSEQ_mult);
apply (rule LIMSEQ_const);
apply simp;
done;
also have "4 / d * 0 = 0";
by simp;
finally show ?thesis;
apply (unfold LIMSEQ_def);
apply (drule_tac x = r in spec);
apply (drule mp);
apply (rule prems);
apply clarsimp;
apply (rule_tac x = "no" in exI);
apply clarify;
apply (drule_tac x = n in spec);
apply clarify;
apply (subgoal_tac "abs (4 * real n powr - (d / 2) / d)
= 4 * real n powr - (d / 2) / d");
apply (erule subst);
apply assumption;
apply (subst abs_nonneg);
apply (rule real_ge_zero_div_gt_zero);
apply (rule nonneg_times_nonneg);
apply force;
apply (rule order_less_imp_le);
apply force;
apply (rule prems);
apply (rule refl);
done;
qed;

lemma aux2: "(%x. (pi x * ln(real x) / (real x)) -
(theta x / (real x))) ----> 0";
apply (unfold LIMSEQ_def);
apply clarsimp;
apply (subgoal_tac  "EX (no::nat). ALL n. (no <= n -->
(4::real) / (min (min (1 / 3) (r / 2)) (r / (4 * ln 4))) *
(real n) powr (- (min (min (1 / 3) (r / 2)) (r / (4 * ln 4))) / 2)
< r / 2)");
apply (erule exE);
apply (rule_tac x = "max no 1" in exI);
apply clarify;
apply (drule_tac x = n in spec);
apply (drule mp);
apply simp;
apply (rule order_le_less_trans);
apply (rule theta_pi_rel9);
apply simp;
prefer 4;
apply (rule aux);
apply simp;
apply (rule real_mult_less_imp_less_div_pos);
apply simp;
apply simp;
apply simp;
prefer 3;
apply (rule order_less_le_trans);
prefer 2;
apply (subgoal_tac "r / 2 + r / 2 <= r");
apply assumption;
apply simp;
prefer 2;
apply assumption;
apply simp;
apply (rule order_trans);
prefer 2;
apply (subgoal_tac "4 * (ln 4 * (r / (4 * ln 4))) <= r");
apply assumption;
apply simp;
apply (rule mult_left_mono);
apply (subst mult_commute);
apply (rule mult_right_mono);
apply (simp split: split_min);
apply force;
apply force;
apply (simp split: split_min);
apply (rule real_mult_less_imp_less_div_pos);
apply force;
apply force;
apply (rule order_le_less_trans);
prefer 2;
apply (subgoal_tac "1 / 3 < 1 / 2");
apply assumption;
apply arith;
apply (subst min_le_iff_disj)+;
apply simp;
done;

lemma theta_limit_imp_pi_limit: "(%x. theta x / (real x)) ----> 1 ==>
(%x. pi x * ln (real x) / (real x)) ----> 1";
apply (erule LIMSEQ_diff_approach_zero);
apply (rule aux2);
done;

end
```

### theta(x) = O(x) and psi(x) = O(x)

lemma prime_dvd_binomial:

```  [| m + 2 ≤ p; p ≤ Suc (2 * m); 1 ≤ m; p ∈ prime |]
==> p dvd Suc (2 * m) choose m```

lemma product_dvd_M:

```  1 ≤ m
==> setprod id {p. p ∈ prime ∧ m + 2 ≤ p ∧ p ≤ Suc (2 * m)} dvd
Suc (2 * m) choose m```

lemma product_lt_M:

```  1 ≤ m
==> setprod id {p. p ∈ prime ∧ m + 2 ≤ p ∧ p ≤ Suc (2 * m)}
≤ Suc (2 * m) choose m```

lemma product_lt_4_to_m:

`  1 ≤ m ==> setprod id {p. p ∈ prime ∧ m + 2 ≤ p ∧ p ≤ Suc (2 * m)} < 4 ^ m`

lemma product_primes_induction_step:

```  ∀m<n. setprod id {p. p ∈ prime ∧ p ≤ Suc m} < 4 ^ Suc m
==> setprod id {p. p ∈ prime ∧ p ≤ Suc n} < 4 ^ Suc n```

lemma product_primes_lt_4_to_n_aux:

`  setprod id {p. p ∈ prime ∧ p ≤ Suc n} < 4 ^ Suc n`

lemma product_primes_lt_4_to_n:

`  1 ≤ n ==> setprod id {p. p ∈ prime ∧ p ≤ n} < 4 ^ n`

lemma theta_bound:

`  1 ≤ n ==> theta n < real n * ln 4`

lemma theta_bound2:

`  theta n ≤ ln 4 * real n`

lemma theta_bigo:

`  theta ∈ O(real)`

lemma psi_bigo_aux:

```  (%x. real (x + 1) powr (1 / 2) * ln (real (x + 1)) * ln (real (x + 1)))
∈ O(%x. real (x + 1))```

lemma psi_bigo_aux2:

`  (%x. psi (x + 1)) ∈ O(%x. real (x + 1))`

lemma psi_bigo:

`  psi ∈ O(real)`

lemma theta_le_psi:

`  theta x ≤ psi x`

lemma psi_theta_lim1:

```  (%x. psi (x + 1))
∈ (%x. theta (x + 1)) +
O(%x. real (x + 1) powr (1 / 2) * ln (real (x + 1)) * ln (real (x + 1)) /
ln 2)```

lemma psi_theta_lim2:

```  O(%x. real (x + 1) powr (1 / 2) * ln (real (x + 1)) * ln (real (x + 1)) / ln 2)
⊆ O(%x. real (x + 1) powr (3 / 4))```

lemma psi_theta_lim3:

```  (%x. psi (x + 1) / real (x + 1))
∈ (%x. theta (x + 1) / real (x + 1)) + O(%x. real (x + 1) powr - (1 / 4))```

lemma psi_theta_lim4:

`  (%x. psi x / real x) ----> 1 ==> (%x. theta x / real x) ----> 1`

### theta and pi

lemma theta_pi_rel1:

```  [| 1 ≤ x; 0 < d; d < 1 |]
==> (1 - d) * Chebyshev1.pi x * ln (real x) - real x powr (1 - d) * ln (real x)
≤ theta x```

lemma theta_pi_rel2:

```  [| 1 ≤ x; 0 < d; d < 1 |]
==> Chebyshev1.pi x * ln (real x) / real x
≤ theta x / ((1 - d) * real x) + ln (real x) / ((1 - d) * real x powr d)```

lemma theta_pi_rel3:

```  [| 1 ≤ x; 0 < d; d < 1 |]
==> Chebyshev1.pi x * ln (real x) / real x - theta x / real x
≤ theta x / real x * (d / (1 - d)) + ln (real x) / ((1 - d) * real x powr d)```

lemma theta_pi_rel4:

```  [| 1 ≤ x; 0 < d; d < 1 |]
==> Chebyshev1.pi x * ln (real x) / real x - theta x / real x
≤ theta x / real x * (d / (1 - d)) +
2 / ((1 - d) * d) * real x powr (- d / 2)```

lemma theta_pi_rel5:

```  [| 1 ≤ x; 0 < d; d < 1 |]
==> ¦Chebyshev1.pi x * ln (real x) / real x - theta x / real x¦
≤ theta x / real x * (d / (1 - d)) +
2 / ((1 - d) * d) * real x powr (- d / 2)```

lemma theta_pi_rel6_aux1:

`  [| 0 < d; d < 1 / 2 |] ==> d < 1 - d`

lemma theta_pi_rel6_aux2:

`  [| 0 < d; d < 1 / 2 |] ==> d / (1 - d) < 1`

lemma theta_pi_rel6_aux3:

`  [| 0 < d; d < 1 / 2 |] ==> 2 / (d * (1 - d)) < 4 / d`

lemma theta_pi_aux1:

`  [| 0 < d; d < 1 / 2 |] ==> 1 / (1 - d) < 2`

lemma theta_pi_rel6:

```  [| 1 ≤ x; 0 < d; d < 1 / 2 |]
==> ¦Chebyshev1.pi x * ln (real x) / real x - theta x / real x¦
≤ theta x / real x + 4 / d * real x powr (- d / 2)```

lemma theta_pi_rel7:

```  [| 1 ≤ x; 0 < d; d < 1 / 2 |]
==> ¦Chebyshev1.pi x * ln (real x) / real x - theta x / real x¦
≤ ln 4 + 4 / d * real x powr (- d / 2)```

lemma theta_pi_rel8:

```  [| 1 ≤ x; 0 < d; d < 1 / 2 |]
==> ¦Chebyshev1.pi x * ln (real x) / real x - theta x / real x¦
≤ 2 * d * theta x / real x + 4 / d * real x powr (- d / 2)```

lemma theta_pi_rel9:

```  [| 1 ≤ x; 0 < d; d < 1 / 2 |]
==> ¦Chebyshev1.pi x * ln (real x) / real x - theta x / real x¦
≤ 2 * d * ln 4 + 4 / d * real x powr (- d / 2)```

lemma aux:

`  [| 0 < d; 0 < r |] ==> ∃no. ∀n. no ≤ n --> 4 / d * real n powr (- d / 2) < r`

lemma aux2:

`  (%x. Chebyshev1.pi x * ln (real x) / real x - theta x / real x) ----> 0`

lemma theta_limit_imp_pi_limit:

```  (%x. theta x / real x) ----> 1
==> (%x. Chebyshev1.pi x * ln (real x) / real x) ----> 1```