Theory Chebyshev3

(*  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 (simp add: prime_not_divide_less);
  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)}");
  apply (simp add: finite_subset);
  apply (auto simp add: prime_dvd_binomial);
  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 (simp add: primes_always_ge_2);
  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 (simp add: two_is_prime);
  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 (simp add: lt_one_minus);
  apply (simp add: lt_one_minus);
  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 (simp add: finite_subset);
  apply force+;
  apply (subgoal_tac "{p::nat. p : prime & y + (2::nat) <= p & p <= Suc ((2::nat) * y)} <= {0..Suc(2*y)}");
  apply (simp add: finite_subset);
  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 (subst power_add [THEN sym]);
  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 (auto simp add: finite_subset);
      apply (rule finite_subset [of _ "{0..n}"]);
      apply force+;
      apply (auto simp add: prime_def);
      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 (simp add: theta_zero);
  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 (simp add: powr_add [THEN sym]);
  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 (simp add: func_plus);
    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);
    apply (simp add: func_times);
    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 (subst add_commute);
  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 (simp add: powr_add [THEN sym]);
  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))";
    by (simp add: func_times);
  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))";
    by (simp add: set_times_plus_distribs func_times);
  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 (simp add: func_times);
    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 (subst powr_add);
    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 (rule real_of_nat_floor_add_one_gt);
      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 (simp add: lprime_def);
      apply auto;
      apply (frule primes_always_ge_1);
      apply force;
      apply (rule setsum_cong);
      apply force;
      apply auto;
      apply (simp add: lprime_def);
      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 (subst add_divide_distrib [THEN sym]);
      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)";
      apply (auto simp add: mult_commute);
      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 add_left_mono);
      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 (subst add_left_cancel);
      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;
      apply (simp add: mult_commute);
      done;
    also have "... = (theta x / (real x))*(d / (1 - d)) + (2::real) / ((1 - d) * d) * (real x) powr (- d / 2)";
      apply (subst add_left_cancel);
      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 (simp add: theta_pi_rel6_aux2);
      apply (rule real_ge_zero_div_gt_zero);
      apply (auto simp add: theta_geq_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 (simp add: theta_pi_aux1);
      apply force+;
      apply (rule real_ge_zero_div_gt_zero);
      apply (auto simp add: theta_geq_zero);
      apply (auto simp add: times_ac1);
      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);
    apply (simp add: prems);
    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;
  apply (rule add_le_less_mono);
  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