Up to index of Isabelle/HOL/HOL-Complex/NumberTheory
theory PrimeNumberTheorem = Error:(* Title: PrimeNumberTheorem.thy
Author: Jeremy Avigad
*)
header {* The prime number theorem *}
theory PrimeNumberTheorem = Error:;
lemma PNT1_aux1: "0 < C ==> 0 <= D ==>
EX C0. ALL eps. 0 < eps --> eps < 1 -->
(ALL K. exp (C0 / eps) < K -->
2 < K & D < ln K & C / (ln K - D) < eps)";
proof;
assume a: "0 < C" and b: "0 <= D";
let ?C0 = "3 * max (max C D) (ln 2)"
show "ALL eps. 0 < eps --> eps < 1 -->
(ALL K. exp (?C0 / eps) < K -->
2 < K & D < ln K & C / (ln K - D) < eps)";
proof (clarify);
fix eps::"real";
fix K::"real";
assume "0 < eps" and "eps < 1";
assume "exp (?C0 / eps) < K";
show "2 < K & D < ln K & C / (ln K - D) < eps";
apply (rule conjI);
apply (rule order_le_less_trans);
prefer 2;
apply (rule prems);
apply (subgoal_tac "2 = exp (ln 2)");
apply (erule ssubst);
apply (subst exp_le_cancel_iff);
apply (subst pos_le_divide_eq);
apply (rule prems);
apply (rule order_trans);
apply (subgoal_tac "ln 2 * eps <= ln 2 * 1");
apply assumption;
apply (rule mult_left_mono);
apply (rule order_less_imp_le);
apply (rule prems);
apply force;
apply (subst mult_commute);
apply (rule mult_mono);
apply simp;
apply (rule le_maxI2);
apply force;
apply simp;
apply (rule order_trans);
prefer 2;
apply (rule le_maxI2);
apply auto;
apply (rule order_le_less_trans);
prefer 2;
apply (subgoal_tac "ln (exp (?C0 / eps)) < ln K");
apply assumption;
apply (subst ln_less_cancel_iff);
apply force;
apply (rule order_less_trans);
prefer 2;
apply (rule prems);
apply force;
apply (rule prems);
apply simp;
apply (rule order_trans);
apply (subgoal_tac "D <= 3 * D");
apply assumption;
apply simp;
apply (rule prems)+;
apply (subst pos_le_divide_eq);
apply (rule prems);
apply simp;
apply (rule order_trans);
apply (subgoal_tac "D * eps <= D * 1");
apply assumption;
apply (rule mult_left_mono);
apply (rule order_less_imp_le);
apply (rule prems);
apply (rule prems);
apply simp;
apply (rule order_trans);
apply (rule le_maxI2);
apply (rule le_maxI1);
apply (subst pos_divide_less_eq);
apply simp;
apply (rule order_le_less_trans);
prefer 2;
apply (subgoal_tac "ln (exp (?C0 / eps)) < ln K");
apply assumption;
apply (subst ln_less_cancel_iff);
apply force;
apply (rule order_less_trans);
prefer 2;
apply (rule prems);
apply force;
apply (rule prems);
apply simp;
apply (rule order_trans);
apply (subgoal_tac "D <= 3 * D");
apply assumption;
apply simp;
apply (rule prems)+;
apply (subst pos_le_divide_eq);
apply (rule prems);
apply simp;
apply (rule order_trans);
apply (subgoal_tac "D * eps <= D * 1");
apply assumption;
apply (rule mult_left_mono);
apply (rule order_less_imp_le);
apply (rule prems);
apply (rule prems);
apply simp;
apply (rule order_trans);
apply (rule le_maxI2);
apply (rule le_maxI1);
apply (subgoal_tac "C = eps * (C / eps)");
apply (erule ssubst);
apply (rule mult_strict_left_mono);
apply (simp add: compare_rls);
apply (rule order_less_le_trans);
prefer 2;
apply (subst ln_le_cancel_iff);
prefer 3;
apply (rule order_less_imp_le);
apply (rule prems);
apply force;
apply (rule order_less_trans);
prefer 2;
apply (rule prems);
apply force;
apply simp;
apply (subgoal_tac "C / eps <= max (max C D) (ln 2) / eps");
apply (subgoal_tac "D <= max (max C D) (ln 2) / eps");
apply (subgoal_tac "0 < max (max C D) (ln 2) / eps");
apply (subgoal_tac "3 * max (max C D) (ln 2) / eps =
2 * (max (max C D) (ln 2) / eps) + max (max C D) (ln 2) / eps");
apply (erule ssubst);
apply arith;
apply (subgoal_tac "3 = 2 + 1");
apply (erule ssubst);
apply (simp only: ring_eq_simps add_divide_distrib);
apply simp+;
apply (subst pos_less_divide_eq);
apply (rule prems);
apply simp;
apply (rule order_less_le_trans);
apply (rule a);
apply (rule order_trans);
apply (rule le_maxI1);
apply (rule le_maxI1);
apply (subst pos_le_divide_eq);
apply (rule prems);
apply (rule order_trans);
apply (subgoal_tac "D * eps <= D * 1");
apply assumption;
apply (rule mult_left_mono);
apply (rule order_less_imp_le);
apply (rule prems)+;
apply simp;
apply (rule order_trans);
apply (rule le_maxI2);
apply (rule le_maxI1);
apply (rule divide_right_mono);
apply (rule order_trans);
apply (rule le_maxI1);
apply (rule le_maxI1);
apply (rule order_less_imp_le);
apply (rule prems)+;
apply (subgoal_tac "eps ~= 0");
apply simp;
apply (rule less_imp_neq [THEN not_sym]);
apply (rule prems);
done;
qed;
qed;
lemma PNT1_aux2: "EX C. ALL x. abs(ln (abs x + 1) -
(∑ i = 1..natfloor (abs x) + 1. 1 / real i)) < C";
apply (insert ln_sum_real2);
apply (drule set_plus_imp_minus);
apply (simp only: func_diff);
apply (simp only: bigo_alt_def);
apply clarsimp;
apply (rule_tac x = "c + c" in exI);
apply (rule allI);
apply (drule_tac x = x in spec);
apply (erule order_le_less_trans);
apply arith;
done;
lemma PNT1_aux3: "EX C. ALL x. (1 <= x --> abs(ln x -
(∑ i = 1..natfloor x. 1 / real i)) < C)";
apply (insert PNT1_aux2);
apply clarsimp;
apply (rule_tac x = C in exI);
apply (rule allI);
apply (rule impI);
apply (subgoal_tac "ln x = ln((x - 1) + 1)");
apply (erule ssubst);
apply (subgoal_tac "natfloor x = natfloor (x - 1) + 1");
apply (erule ssubst);
apply (subgoal_tac "x - 1 = abs(x - 1)");
apply (erule ssubst);
apply (erule spec);
apply (subst abs_nonneg);
apply auto;
apply (subst natfloor_add [THEN sym]);
apply auto;
done;
lemma PNT1_aux4: "EX C. ALL x. (1 <= x --> abs(ln x -
(∑ i = 1..natfloor x. 1 / real (i + 1))) < C)";
apply (insert PNT1_aux3);
apply clarify;
apply (rule_tac x = "C + 1" in exI);
apply clarify;
apply (drule_tac x = x in spec);
apply (subgoal_tac
"(∑ i = 2..natfloor x + 1. 1 / real i) =
(∑ i = 1..natfloor x. 1 / real (i + 1))");
prefer 2;
apply (rule setsum_reindex_cong');
apply force;
apply (subgoal_tac "inj_on (%x. x + 1) ?t");
apply assumption;
apply (simp add: inj_on_def);
apply (clarsimp simp add: image_def);
apply (rule equalityI);
apply clarify;
apply (rule_tac x = "xa - 1" in bexI);
apply force;
apply clarsimp;
apply (rule conjI);
apply arith;
apply arith;
apply clarsimp;
apply (rule refl);
apply (erule subst);
apply (subgoal_tac "ln x - (∑ i = 2..natfloor x + 1. 1 / real i) =
(ln x - (∑ i = 1..natfloor x. 1 / real i)) +
(1 - 1 / real (natfloor x + 1))");
apply (erule ssubst);
apply (rule order_le_less_trans);
apply (rule abs_triangle_ineq);
apply (rule real_add_less_le_mono);
apply (erule mp);
apply assumption;
apply (subst abs_nonneg);
apply simp;
apply (subst pos_divide_le_eq);
apply force;
apply force;
apply simp;
apply (simp add: compare_rls);
apply (subgoal_tac "(∑ i = 2..natfloor x + 1. 1 / real i) =
(∑ i = 1..natfloor x. 1 / real i) -
(∑ i : {1::nat}. 1 / real i) +
(∑ i : {natfloor x + 1}. 1 / real i)");
apply (erule ssubst);
apply simp;
apply (simp only: compare_rls);
apply (subst setsum_Un_disjoint [THEN sym]);
apply force;
apply force;
apply force;
apply (subst setsum_Un_disjoint [THEN sym]);
apply force;
apply force;
apply force;
apply (rule setsum_cong);
apply force;
apply (rule refl);
done;
lemma PNT1_aux5: "EX D. ALL x. ALL K. 1 <= x --> 1 <= K -->
abs (ln K -
(∑ n | natfloor x < n & n <= natfloor (K * x). 1 / real (n + 1)))
<= D";
proof -;
obtain C where "ALL x. (1 <= x --> abs(ln x -
(∑ i = 1..natfloor x. 1 / real (i + 1))) < C)";
by (insert PNT1_aux4, auto);
show ?thesis;
proof;
show "ALL x. ALL K. 1 <= x --> 1 <= K -->
abs (ln K -
(∑ n | natfloor x < n & n <= natfloor (K * x). 1 / real (n + 1)))
<= C + C";
proof (clarify);
fix x::"real"; fix K::"real";
assume "1 <= x" and "1 <= K";
have a: "(∑ n | natfloor x < n & n <= natfloor (K * x).
1 / real (n + 1)) =
(∑n=1..natfloor (K * x). 1 / real (n + 1)) -
(∑n=1..natfloor x. 1 / real (n + 1))"
(is "?LHS1 = ?RHS1a - ?RHS1b");
apply (simp add: compare_rls);
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule bounded_nat_set_is_finite);
apply clarsimp;
apply (subgoal_tac "i < natfloor (K * x) + 1");
apply assumption;
apply arith;
apply force;
apply force;
apply (rule setsum_cong);
apply auto;
apply (rule order_trans);
prefer 2;
apply (subgoal_tac "natfloor (1 * ?x) <= natfloor (K * ?x)");
apply assumption;
apply (rule natfloor_mono);
apply (rule mult_right_mono);
apply (rule prems);
apply (insert prems, arith);
apply simp;
done;
have b: "ln K = ln (K * x) - ln x"
apply (subst ln_mult);
apply (insert prems);
apply auto;
done;
have "ln K - ?LHS1 = (ln (K * x) - ?RHS1a) + (?RHS1b - ln x)"
by (simp only: a b compare_rls);
then have "abs(ln K - ?LHS1) = abs(...)";
by simp;
also have "... <= abs(ln (K * x) - ?RHS1a) + abs(?RHS1b - ln x)";
by (rule abs_triangle_ineq);
also have "... <= C + C";
apply (rule add_mono);
apply (insert prems);
apply (drule_tac x = "K * x" in spec);
apply (subgoal_tac "1 <= K * x");
apply force;
apply (subgoal_tac "1 * 1 <= K * x");
apply simp;
apply (rule mult_mono);
apply assumption+;
apply arith;
apply force;
apply (subst abs_diff);
apply (drule_tac x = x in spec);
apply force;
done;
finally; show "abs (ln K -
(∑ n | natfloor x < n & n <= natfloor (K * x). 1 / real (n + 1)))
<= C + C";.;
qed;
qed;
qed;
lemma PNT1_aux6: "EX D. ALL x. ALL K. 1 <= x --> 1 <= K --> ln K - D <=
(∑ n | natfloor x < n & n <= natfloor (K * x). 1 / real (n + 1))";
apply (insert PNT1_aux5);
apply (erule exE);
apply (rule_tac x = D in exI);
apply (clarsimp);
apply (drule_tac x = x in spec);
apply clarsimp;
apply (drule_tac x = K in spec);
apply clarsimp;
apply (frule abs_le_D1);
apply auto;
done;
lemma PNT1_aux7: "0 < C ==> EX C0. ALL eps. 0 < eps --> eps < 1 -->
(ALL K. ALL x. 1 <= x --> exp (C0 / eps) < K -->
2 < K &
C / (∑ n | natfloor x < n & n <= natfloor (K * x).
1 / real (n + 1)) < eps)";
proof -;
assume a: "0 < C";
obtain D where d: "ALL x. ALL K. 1 <= K --> 1 <= x --> ln K - D <=
(∑ n | natfloor x < n & n <= natfloor (K * x). 1 / real (n + 1))";
by (insert PNT1_aux6, auto);
let ?D = "max D 0";
have "EX C0. ALL eps. 0 < eps --> eps < 1 -->
(ALL K. exp (C0 / eps) < K -->
2 < K & ?D < ln K & C / (ln K - ?D) < eps)";
apply (rule PNT1_aux1);
apply (rule a);
apply (rule le_maxI2);
done;
then obtain C0 where C0: "ALL eps. 0 < eps --> eps < 1 -->
(ALL K. exp (C0 / eps) < K -->
2 < K & ?D < ln K & C / (ln K - ?D) < eps)";..;
show ?thesis;
proof;
show "ALL eps. 0 < eps --> eps < 1 -->
(ALL K. ALL x. 1 <= x --> exp (C0 / eps) < K --> 2 < K &
C / (∑ n | natfloor x < n & n <= natfloor (K * x).
1 / real (n + 1)) < eps)";
proof (clarify);
fix eps::"real"
fix K::"real";
fix x::"real";
assume "0 < eps";
assume "eps < 1";
assume "1 <= x";
assume "exp (C0 / eps) < K";
have c0: "ALL K. exp (C0 / eps) < K --> 2 < K & ?D < ln K &
C / (ln K - ?D) < eps";
by (insert C0 prems, blast);
show "2 < K &
C / (∑ n | natfloor x < n & n <= natfloor (K * x).
1 / real (n + 1)) < eps";
apply (rule conjI);
apply (insert c0);
apply (drule_tac x = K in spec);
apply (force simp add: prems);
apply (case_tac
"(∑ n | natfloor x < n & n <= natfloor (K * x).
1 / real (n + 1)) = 0");
apply (simp add: prems);
apply (subst pos_divide_less_eq);
apply (subgoal_tac "0 <=
(∑ n | natfloor x < n & n <= natfloor (K * x).
1 / real (n + 1))");
apply arith;
apply (rule setsum_nonneg');
apply force;
apply (rule order_less_le_trans);
apply (subgoal_tac "C < eps * (ln K - max D 0)");
apply assumption;
apply (subst pos_divide_less_eq [THEN sym]);
apply (simp add: compare_rls);
apply (insert d);
apply (drule_tac x = x in spec);
apply (drule_tac x = K in spec);
apply (clarsimp simp add: prems);
apply (insert c0);
apply (drule_tac x = K in spec);
apply (clarsimp simp add: prems);
apply (drule_tac x = K in spec);
apply (clarsimp simp add: prems);
apply (rule mult_left_mono);
apply (rule order_trans);
apply (subgoal_tac "ln K - max D 0 <= ln K - D");
apply assumption;
apply simp;
apply (rule le_maxI1);
apply (drule_tac x = x in spec);
apply (drule_tac x = K in spec);back;
apply (subgoal_tac "1 <= K");
apply (clarsimp simp add: prems);
apply (subgoal_tac "2 < K");
apply simp;
apply (force simp add: prems);
apply (rule order_less_imp_le);
apply (rule prems);
done;
qed;
qed;
qed;
lemma PNT1_aux8: "~((0 <= (x::real)) = (0 <= y)) ==> abs x <= abs (y - x)";
by auto;
lemma PNT1_aux9:
"(ALL k < (j::nat). ((0 <= (f(i + k)::real)) = (0 <= f(i + (k + 1))))) ==>
(ALL k <= j. (0 <= f(i + k))) | (ALL k <= j. (f(i + k) < 0))";
apply (case_tac "0 <= f i");
apply (rule disjI1);
apply (rule allI);
apply (induct_tac k);
apply force;
apply clarify;
apply (subgoal_tac "n <= j");
apply clarify;
apply (subgoal_tac "n < j");
apply (drule_tac x = n in spec);
apply (frule mp);
apply assumption;
apply (subgoal_tac "i + Suc n = i + (n + 1)");
apply (erule ssubst);back;
apply force;
apply simp;
apply arith;
apply arith;
apply (rule disjI2);
apply (rule allI);
apply (induct_tac k);
apply force;
apply clarify;
apply (subgoal_tac "n <= j");
apply clarify;
apply (subgoal_tac "n < j");
apply (drule_tac x = n in spec);
apply (frule mp);
apply assumption;
apply (subgoal_tac "i + Suc n = i + (n + 1)");
apply (erule ssubst);back;
apply force;
apply simp;
apply arith;
apply arith;
done;
lemma PNT1_aux10: "(i::nat) <= j ==> (ALL n. i < n & n <= j -->
(((0::real) <= f(n)) = (0 <= f(n+1)))) ==>
(ALL n. i < n & n <= j --> 0 <= f n) |
(ALL n. i < n & n <= j --> f n < 0)";
apply (subgoal_tac "
(ALL k <= j - i. (0 <= f((i + 1) + k))) |
(ALL k <= j - i. (f((i + 1) + k) < 0))");
apply (erule disjE);
apply (rule disjI1);
apply clarify;
apply (drule_tac x = "n - (i + 1)" in spec);back;
apply (subgoal_tac "n - (i + 1) <= j - i");
apply clarify;
apply (subgoal_tac "(i + 1) + (n - (i + 1)) = n");
apply simp;
apply arith+;
apply (rule disjI2);
apply clarify;
apply (drule_tac x = "n - (i + 1)" in spec);back;
apply (subgoal_tac "n - (i + 1) <= j - i");
apply clarify;
apply (subgoal_tac "(i + 1) + (n - (i + 1)) = n");
apply simp;
apply arith+;
apply (rule PNT1_aux9);
apply clarify;
apply (drule_tac x = "i + 1 + k" in spec);
apply (drule mp);
apply arith;
apply (simp add: add_ac);
done;
lemma PNT1_aux11: "EX C. ALL i. (1::nat) <= i -->
abs(∑n=1..i. R(real n) / ((real n) * (real (n + 1)))) <= C";
proof -;
have "EX C. ALL x. abs(∑ n=1..natfloor (abs x).
R(real n) / ((real n) * (real (n + 1)))) <= C";
apply (insert error1);
apply (unfold bigo_def);
apply clarsimp;
done;
thus ?thesis;
apply clarsimp;
apply (rule_tac x = C in exI);
apply (rule allI);
apply (rule impI);
apply (drule_tac x = "real i" in spec);
apply (subgoal_tac "abs(real i) = real i");
apply simp_all;
done;
qed;
lemma PNT1_aux12: "EX C. ALL (i::nat). ALL j. 1 <= i --> i <= j -->
abs (∑ n | i < n & n <= j. R(real n) / ((real n) * (real (n +
1)))) < C";
apply (insert PNT1_aux11);
apply (erule exE);
apply (rule_tac x = "C + C + 1" in exI);
apply clarify;
apply (rule order_le_less_trans);
prefer 2;
apply (subgoal_tac "C + C < C + C + 1");
apply assumption;
apply arith;
apply (subgoal_tac "(∑ n | i < n & n <= j.
R (real n) / (real n * real (n + 1))) =
(∑n=1..j. R(real n) / ((real n) * (real (n + 1)))) -
(∑n=1..i. R(real n) / ((real n) * (real (n + 1))))");
apply (erule ssubst);
apply (rule order_trans);
apply (rule abs_triangle_ineq4);
apply (rule add_mono);
apply force;
apply force;
apply (simp add: compare_rls);
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule bounded_nat_set_is_finite);
apply clarify;
apply (subgoal_tac "ia < j + 1");
apply assumption;
apply arith;
apply simp;
apply force;
apply (rule setsum_cong);
apply (auto simp only: atLeastAtMost_iff);
done;
lemma PNT1: "EX C0. ALL eps. 0 < eps --> eps < 1 --> (EX x0. ALL K x.
exp (C0 / eps) < K --> x0 < x --> (EX n.
natfloor x < n & n <= natfloor (K * x) &
abs(R(real n) / (real n)) < eps))";
proof -;
from PNT1_aux12 obtain C where C: "ALL (i::nat). ALL j.
1 <= i --> i <= j -->
abs (∑ n | i < n & n <= j. R(real n) / ((real n) * (real (n +
1)))) < C";..;
have "EX C0. ALL eps. 0 < eps --> eps < 1 -->
(ALL K. ALL x. 1 <= x --> exp (C0 / eps) < K -->
2 < K & C / (∑ n | natfloor x < n & n <= natfloor (K * x).
1 / real (n + 1)) < eps)";
apply (rule PNT1_aux7);
apply (insert prems);
apply (drule_tac x = 1 in spec)+;
apply (drule mp, simp)+;
apply arith;
done;
then obtain C0 where C0temp: "ALL eps. 0 < eps --> eps < 1 -->
(ALL K. ALL x. 1 <= x --> exp (C0 / eps) < K -->
2 < K & C / (∑ n | natfloor x < n & n <= natfloor (K * x).
1 / real (n + 1)) < eps)";..;
show ?thesis;
proof ((rule exI)+, clarify);
fix eps::"real";
assume "0 < eps";
assume "eps < 1";assume "eps < 1";
show "EX x0. ALL K x. exp (C0 / eps) < K --> x0 < x -->
(EX n. natfloor x < n & n <= natfloor (K * x) &
abs (R (real n) / real n) < eps)";
proof;
let ?x0 = "max (exp 2 + 1) (exp (4 / eps) + 1)";
show "ALL K x. exp (C0 / eps) < K --> ?x0 < x -->
(EX n. natfloor x < n & n <= natfloor (K * x) &
abs (R (real n) / real n) < eps)";
proof (clarify);
fix K::"real"; fix x::"real";
assume "exp (C0 / eps) < K";
assume "?x0 < x";
have C0: "ALL K. ALL x. 1 <= x --> exp (C0 / eps) < K -->
2 < K &
C / (∑ n | natfloor x < n & n <= natfloor (K * x).
1 / real (n + 1)) < eps";
by (insert C0temp prems, blast);
have a: "exp 2 + 1 <= x";
apply (intro order_less_imp_le);
apply (rule order_le_less_trans);
prefer 2;
apply assumption;
apply (rule le_maxI1);
done;
have b: "exp (4 / eps) + 1 <= x";
apply (intro order_less_imp_le);
apply (rule order_le_less_trans);
prefer 2;
apply (rule prems);
apply (rule le_maxI2);
done;
have d: "exp (4 / eps) <= real(natfloor x)";
apply (rule order_less_imp_le);
apply (rule ge_natfloor_plus_one_imp_gt);
apply (subst natfloor_add [THEN sym]);
apply (subgoal_tac "0 < exp (4 / eps)");
apply arith;
apply force;
apply simp;
apply (rule natfloor_mono);
apply (rule b);
done;
show "EX n. natfloor x < n &
n <= natfloor (K * x) & abs (R (real n) / real n) < eps";
proof (cases);
assume "EX n. natfloor x < n & n <= natfloor (K * x) &
~((0 <= R(real n)) = (0 <= R(real (n + 1))))";
then obtain n where c: "natfloor x < n & n <= natfloor (K * x) &
~((0 <= R(real n)) = (0 <= R(real (n + 1))))";..;
have c: "exp 2 < real n";
apply (rule ge_natfloor_plus_one_imp_gt);
apply (subgoal_tac "natfloor x < n");
apply (subgoal_tac "natfloor (exp 2) + 1 <= natfloor x");
apply arith;
apply (subst natfloor_add [THEN sym]);
apply force;
apply (rule natfloor_mono);
apply simp;
apply (rule a);
apply (insert prems, auto);
done;
have "abs (R(real n)) <= abs(R(real (n + 1)) - R(real n))";
by (insert prems, intro PNT1_aux8, simp);
also have "R(real(n + 1)) - R(real n) = psi(n + 1) - psi(n) - 1";
apply (unfold R_def);
apply simp;
apply (subgoal_tac "real n + 1 = real(n + 1)");
apply (erule ssubst);
apply (subst natfloor_real_id);
apply simp_all;
done;
also have "abs(...) < ln (real n)";
apply (subst psi_plus_one);
apply simp;
apply (case_tac "EX p a. p : prime & p ^ a = (n + 1) & 0 < a");
apply (clarsimp);
apply (subgoal_tac "n + 1 = p ^ a");
apply (erule ssubst);back;
apply (subst Lambda_eq);
apply assumption+;
apply (case_tac "real p < exp 1");
apply (rule order_le_less_trans);
apply (rule abs_triangle_ineq4);
apply simp;
apply (subst abs_nonneg);
apply (rule ln_ge_zero);
apply (subgoal_tac "real (1::nat) <= real p");
apply simp;
apply (rule le_imp_real_of_nat_le);
apply (erule primes_always_ge_1);
apply (rule order_less_le_trans);
apply (subgoal_tac "ln(real p) + 1 < ln (exp 1) + 1");
apply assumption;
apply (rule add_strict_right_mono);
apply (subst ln_less_cancel_iff);
apply (subgoal_tac "1 <= p");
apply arith;
apply (erule primes_always_ge_1);
apply force;
apply assumption;
apply simp;
apply (subgoal_tac "ln (exp 2) <= ln (real n)");
apply simp;
apply (subst ln_le_cancel_iff);
apply force;
apply (rule order_le_less_trans);
prefer 2;
apply (rule c);
apply force;
apply (rule order_less_imp_le);
apply (rule c);
apply (subst abs_nonneg);
apply simp;
apply (subgoal_tac "ln (exp 1) <= ln (real p)");
apply simp;
apply (subst ln_le_cancel_iff);
apply force;
apply (frule primes_always_ge_1);
apply arith;
apply arith;
apply (simp add: compare_rls);
apply (rule order_le_less_trans);
apply (subgoal_tac "ln (real p) <= ln(real (n + 1))");
apply assumption;
apply (subst ln_le_cancel_iff);
apply (frule primes_always_ge_1);
apply arith;
apply arith;
apply (rule le_imp_real_of_nat_le);
apply (erule subst);
apply (subgoal_tac "p^1 <= p^a");
apply simp;
apply (rule power_increasing);
apply arith;
apply (erule primes_always_ge_1);
apply simp;
apply (subgoal_tac "ln (real n + 1) - ln (real n) < 1");
apply simp;
apply (subst ln_div [THEN sym]);
apply force;
apply (rule order_le_less_trans);
prefer 2;
apply (rule c);
apply force;
apply (subgoal_tac "(real n + 1) / real n = 1 + 1 / real n");
apply (erule ssubst);back;
apply (rule order_le_less_trans);
apply (rule ln_add_one_self_le_self);
apply force;
apply (subst pos_divide_less_eq);
apply (rule order_le_less_trans);
prefer 2;
apply (rule c, force);
apply simp;
apply (rule order_le_less_trans);
prefer 2;
apply (rule c);
apply (subgoal_tac "exp 0 <= exp 2");
apply simp;
apply (subst exp_le_cancel_iff);
apply force;
apply (simp add: add_divide_distrib);
apply (subgoal_tac "0 < real n");
apply arith;
apply (rule order_le_less_trans);
prefer 2;
apply (rule c);
apply force;
apply simp;
apply (subst Lambda_eq2);
apply assumption;
apply simp;
apply (subgoal_tac "ln(exp 1) < ln(real n)");
apply simp;
apply (subst ln_less_cancel_iff);
apply force;
apply (rule order_le_less_trans);
prefer 2;
apply (rule c);
apply force;
apply (rule order_le_less_trans);
prefer 2;
apply (rule c);
apply simp;
done;
finally have "abs (R(real n)) < ln (real n)";.;
then have "abs (R(real n)) / (real n) < ln (real n) / (real n)";
apply (rule real_div_pos_less_mono);
apply (rule order_le_less_trans);
prefer 2;
apply (rule c);
apply force;
done;
also have "... <= ln (real (natfloor x)) / (real (natfloor x))";
apply (rule ln_x_over_x_mono);
apply (rule order_less_imp_le);
apply (rule ge_natfloor_plus_one_imp_gt);
apply (subst natfloor_add [THEN sym]);
apply force;
apply simp;
apply (rule natfloor_mono);
apply (rule order_trans);
prefer 2;
apply (rule a);
apply simp;
apply simp;
apply (rule order_less_imp_le);
apply (simp add: prems);
done;
also have "... <= ((real (natfloor x) powr (1 / 2)) / (1 / 2)) /
(real (natfloor x))";
apply (rule divide_right_mono);
apply (rule ln_powr_bound);
apply (rule order_less_imp_le);
apply (rule ge_natfloor_plus_one_imp_gt);
apply (subst natfloor_add [THEN sym]);
apply force;
apply simp;
apply (rule natfloor_mono);
apply (rule order_trans);
prefer 2;
apply (rule a);
apply simp;
apply (subgoal_tac "exp 0 <= exp 2");
apply simp;
apply force;
apply force;
apply simp;
done;
also have "... = 2 * ((real (natfloor x) powr (1 / 2)) /
real (natfloor x) powr 1)";
apply (simp add: mult_ac);
apply (rule sym);
apply (subst powr_one_gt_zero_iff);
apply simp;
apply (rule order_less_le_trans);
prefer 2;
apply (rule real_le_natfloor);
apply (subgoal_tac "real 1 <= x");
apply assumption;
apply simp;
apply (rule order_trans);
prefer 2;
apply (rule a);
apply simp;
apply simp;
done;
also have "... = 2 * (real (natfloor x) powr (1 / 2 - 1))";
apply (rule arg_cong);back;
apply (rule powr_divide2);
done;
also have "(1 / 2 - (1::real)) = - (1 / 2)";
by simp;
also have "2 * (real (natfloor x) powr - (1 / 2)) =
2 / (real (natfloor x) powr (1 / 2))";
apply (subst powr_minus_divide);
apply simp;
done;
also have "... <= 2 / (exp (4 / eps) powr (1 / 2))";
apply (rule divide_left_mono);
apply (rule power_mono2);
apply force;
apply force;
apply (rule d);
apply force;
apply (rule mult_pos);
apply force;
apply force;
done;
also have "... = 2 / (exp (2 / eps))";
by (simp add: powr_def);
also have "... < 2 / (2 / eps)";
apply (rule divide_strict_left_mono);
apply (rule order_less_le_trans);
prefer 2;
apply (rule exp_ge_add_one_self);
apply (rule real_ge_zero_div_gt_zero);
apply force;
apply (rule prems);
apply arith;
apply auto;
apply (rule pos_div_pos);
apply (rule mult_pos);
apply auto;
apply (rule prems);
done;
also have "... = eps";
by simp;
finally; show ?thesis;
apply (rule_tac x = n in exI);
apply (auto simp add: prems);
apply (subst abs_div [THEN sym]);
apply (subgoal_tac "0 < real n");
apply arith;
apply (rule order_le_less_trans);
prefer 2;
apply (rule c);
apply force;
apply simp;
done;
next assume no_sign_change:"~ (EX n. natfloor x < n &
n <= natfloor (K * x) &
~((0 <= R(real n)) = (0 <= R(real (n + 1)))))";
then have "
(ALL n. natfloor x < n & n <= natfloor (K * x) --> 0 <= R(real n)) |
(ALL n. natfloor x < n & n <= natfloor (K * x) --> R(real n) < 0)";
apply (intro PNT1_aux10);
apply (rule natfloor_mono);
apply (subgoal_tac "1 * x <= K * x");
apply simp;
apply (rule mult_right_mono);
apply (rule order_less_imp_le);
apply (insert C0);
apply (drule_tac x = K in spec);
apply (drule_tac x = 1 in spec);
apply (force simp add: prems);
apply (rule order_trans);
prefer 2;
apply (rule a);
apply (rule nonneg_plus_nonneg);
apply force;
apply force;
apply force;
done;
then have "(∑ n | natfloor x < n & n <= natfloor (K * x).
abs (R(real n)) / ((real n) * (real (n + 1)))) =
abs(∑ n | natfloor x < n & n <= natfloor (K * x).
R(real n) / ((real n) * (real (n + 1))))";
apply (elim disjE);
apply (subst abs_nonneg);
apply (rule setsum_nonneg');
apply clarify;
apply (rule real_ge_zero_div_gt_zero);
apply force;
apply (rule mult_pos);
apply (insert a);
apply (subgoal_tac "1 < exp 2 + 1");
apply arith;
apply force;
apply (insert a);
apply (subgoal_tac "1 < exp 2 + 1");
apply arith;
apply force;
apply (rule setsum_cong2);
apply (subst abs_nonneg);
apply force;
apply (rule refl);
apply (subst abs_nonpos);
apply (rule setsum_nonpos');
apply clarify;
apply (rule order_less_imp_le);
apply (subst pos_divide_less_eq);
apply (rule mult_pos);
apply (insert a);
apply (subgoal_tac "1 < exp 2 + 1");
apply arith;
apply force;
apply (insert a);
apply (subgoal_tac "1 < exp 2 + 1");
apply arith;
apply force;
apply force;
apply (subst setsum_negf' [THEN sym]);
apply (rule setsum_cong2);
apply (subst abs_nonpos);
apply force;
apply simp;
done;
also have "... < C";
apply (insert C);
apply (drule spec)+;
apply (drule mp);
prefer 2;
apply (drule mp);
prefer 2;
apply assumption;
apply (rule natfloor_mono);
apply (subgoal_tac "1 * x < K * x");
apply force;
apply (rule mult_strict_right_mono);
apply (insert C0);
apply (drule_tac x = K in spec);
apply (drule_tac x = 1 in spec);
apply (force simp add: prems);
apply (insert a);
apply (subgoal_tac "0 < exp 2");
apply arith;
apply force;
apply (rule real_le_natfloor);
apply (insert a);
apply (subgoal_tac "0 < exp 2");
apply arith;
apply force;
done;
finally; have e: "(∑ n | natfloor x < n & n <= natfloor (K * x).
abs (R (real n)) / (real n * real (n + 1))) < C";.;
have "~ (ALL n. natfloor x < n & n <= natfloor (K * x) -->
C / (∑ n | natfloor x < n & n <= natfloor (K * x).
1 / (real (n + 1))) <= abs (R (real n)) / (real n))";
proof;
assume f: "ALL n. natfloor x < n & n <= natfloor (K * x) -->
C / (∑ n | natfloor x < n & n <= natfloor (K * x).
1 / real (n + 1)) <= abs (R (real n)) / real n";
have "(∑ n | natfloor x < n & n <= natfloor (K * x).
abs (R (real n)) / (real n * real (n + 1))) =
(∑ n | natfloor x < n & n <= natfloor (K * x).
abs (R (real n)) / (real n) * (1 / real (n + 1)))";
apply (rule setsum_cong2);
apply simp;
done;
also have "(∑ n | natfloor x < n & n <= natfloor (K * x).
(C / (∑ n | natfloor x < n & n <= natfloor (K * x).
1 / real (n + 1))) * (1 / real (n + 1))) <= ..."
(is "?LHS <= ?RHS");
apply (rule setsum_le_cong);
apply (rule mult_right_mono);
apply (insert f);
apply auto;
done;
also have "?LHS = C";
apply (subst setsum_const_times);
apply simp;
apply (subgoal_tac "0 < (∑ n | natfloor x < n &
n <= natfloor (K * x). 1 / (real n + 1))");
apply force;
apply (subgoal_tac "(∑ n | natfloor x < n &
n <= natfloor (K * x). 1 / (real n + 1)) =
(∑ n : {natfloor x + 1}. 1 / (real n + 1)) +
(∑ n | natfloor x + 1 < n &
n <= natfloor (K * x). 1 / (real n + 1))");
apply (erule ssubst);
apply simp;
apply (rule order_less_le_trans);
prefer 2;
apply (rule setsum_nonneg');
apply force;
apply force;
apply (subst setsum_Un_disjoint [THEN sym]);
apply force;
apply (rule bounded_nat_set_is_finite);
apply clarify;
apply (subgoal_tac "i < natfloor (K * x) + 1");
apply assumption;
apply arith;
apply force;
apply (rule setsum_cong);
apply auto;
apply (subst natfloor_add [THEN sym]);
apply (rule order_trans);
prefer 2;
apply (rule a);
apply (subgoal_tac "0 < exp 2");
apply arith;
apply force;
apply simp;
apply (rule natfloor_mono);
apply (rule order_trans);
apply (subgoal_tac "x + 1 <= 2 * x");
apply assumption;
apply (insert a);
apply (subgoal_tac "0 < exp 2");
apply arith;
apply force;
apply (rule mult_right_mono);
apply (rule order_less_imp_le);
apply (insert C0);
apply (drule_tac x = K in spec);
apply (drule_tac x = 1 in spec);
apply (force simp add: prems);
apply (insert a);
apply (subgoal_tac "0 < exp 2");
apply arith;
apply force;
done;
finally show "False";
by (insert e, auto);
qed;
then have "EX n. natfloor x < n & n <= natfloor (K * x) &
abs (R (real n)) / real n < C /
(∑ n | natfloor x < n & n <= natfloor (K * x).
1 / real (n + 1))";
by auto;
then show "EX n. natfloor x < n & n <= natfloor (K * x) &
abs (R (real n) / real n) < eps";
apply auto;
apply (rule_tac x = n in exI);
apply auto;
apply (subst abs_div [THEN sym]);
apply force;
apply (subst abs_nonneg);
apply force;
apply (erule order_less_le_trans);
apply (insert C0);
apply (drule_tac x = K in spec);
apply (drule_tac x = x in spec);
apply (rule order_less_imp_le);
apply (subgoal_tac "1 <= x");
apply (force simp add: prems);
apply (insert a);
apply (subgoal_tac "0 < exp 2");
apply arith;
apply force;
done;
qed;
qed;
qed; qed; qed;
lemma PNT1a: "EX C0. ALL eps. 0 < eps --> eps < 1 --> (EX x0. ALL K x.
exp (C0 / eps) < K --> x0 < x --> (EX n::nat.
x < real n & real n <= K * x &
abs(R(real n) / (real n)) < eps))";
apply (insert PNT1);
apply clarify;
apply (rule_tac x = "C0" in exI);
apply clarify;
apply (drule_tac x = "eps" in spec);
apply clarify;
apply (rule_tac x = "max x0 0" in exI);
apply clarify;
apply (drule_tac x = K in spec);
apply (drule_tac x = x in spec);
apply clarify;
apply (subgoal_tac "x0 < x");
apply clarify;
apply (rule_tac x = n in exI);
apply (rule conjI);
apply (rule ge_natfloor_plus_one_imp_gt);
apply arith;
apply (rule conjI);
apply (rule nat_le_natfloor);
apply (rule nonneg_times_nonneg);
apply (rule order_less_imp_le);
apply (rule order_le_less_trans);
prefer 2;
apply assumption;
apply force;
apply arith;
apply assumption;
apply assumption;
apply simp;
done;
lemma PNT2_aux1: "EX C. ALL x. 1 <= x -->
abs (psi (natfloor x) * ln x + (∑ d = 1..natfloor x.
Lambda d * psi ((natfloor x) div d)) -
2 * x * ln x) <= C * x";
apply (insert Selberg4a);
apply (drule set_plus_imp_minus);
apply (simp add: func_plus func_diff);
apply (unfold bigo_def);
apply clarsimp;
apply (rule_tac x = c in exI);
apply clarify;
apply (drule_tac x = "x - 1" in spec);
apply (subgoal_tac "natfloor (abs(x - 1)) + 1 = natfloor (abs(x - 1) + 1)");
apply simp;
apply (subst natfloor_add [THEN sym]);
apply force;
apply simp;
done;
lemma PNT2_aux2: "EX C. ALL x y. 1 <= y --> y <= x -->
(psi (natfloor x) * ln x - psi (natfloor y) * ln y) <=
(2 * x * ln x - 2 * y * ln y) + C * x";
proof -;
from PNT2_aux1 obtain C where "ALL x. 1 <= x -->
abs (psi (natfloor x) * ln x + (∑ d = 1..natfloor x.
Lambda d * psi ((natfloor x) div d)) -
2 * x * ln x) <= C * x";..;
show ?thesis;
proof ((rule exI)+, clarify);
fix x; fix y;
assume "(1::real) <= y";
assume "y <= x";
show "(psi (natfloor x) * ln x - psi (natfloor y) * ln y) <=
(2 * x * ln x - 2 * y * ln y) + (C + C) * x";
proof -;
have a: "0 <= (∑ d = 1..natfloor x.
Lambda d * psi ((natfloor x) div d)) -
(∑ d = 1..natfloor y.
Lambda d * psi ((natfloor y) div d))"
(is "0 <= ?term1");
apply (subgoal_tac "
(∑ d = 1..natfloor x. Lambda d * psi (natfloor x div d)) =
(∑ d = 1..natfloor y.
Lambda d * psi (natfloor x div d)) +
(∑ d = natfloor y + 1..natfloor x.
Lambda d * psi (natfloor x div d))");
apply (erule ssubst);
apply (subgoal_tac "(∑ d = 1..natfloor y.
Lambda d * psi (natfloor y div d)) <=
(∑ d = 1..natfloor y.
Lambda d * psi (natfloor x div d))");
apply (subgoal_tac "0 <= (∑ d = natfloor y + 1..natfloor x.
Lambda d * psi (natfloor x div d))");
apply arith;
apply (rule setsum_nonneg');
apply clarsimp;
apply (rule nonneg_times_nonneg);
apply (rule Lambda_ge_zero);
apply (rule psi_ge_zero);
apply (rule setsum_le_cong);
apply (rule mult_left_mono);
apply (rule psi_mono);
apply (rule div_le_mono);
apply (rule natfloor_mono);
apply (rule prems);
apply (rule Lambda_ge_zero);
apply (subst setsum_Un_disjoint [THEN sym]);
apply force;
apply (rule bounded_nat_set_is_finite);
apply (rule ballI);
apply (subgoal_tac "i < natfloor x + 1");
apply assumption;
apply force;
apply force;
apply (rule setsum_cong);
apply auto;
apply (erule order_trans);
apply (rule natfloor_mono);
apply (rule prems);
done;
have "abs((psi (natfloor x) * ln x - psi (natfloor y) * ln y) + ?term1) -
abs(2 * x * ln x - 2 * y * ln y) <=
abs((psi (natfloor x) * ln x - psi (natfloor y) * ln y) + ?term1 -
(2 * x * ln x - 2 * y * ln y))";
by (rule abs_triangle_ineq2);
also have "... = abs((psi(natfloor x) * ln x +
(∑ d = 1..natfloor x. Lambda d * psi ((natfloor x) div d))
- 2 * x * ln x) -
(psi(natfloor y) * ln y +
(∑ d = 1..natfloor y. Lambda d * psi ((natfloor y) div d))
- 2 * y * ln y))";
apply (rule arg_cong); back;
apply (simp add: compare_rls);
done;
also have "... <= abs(psi(natfloor x) * ln x +
(∑ d = 1..natfloor x. Lambda d * psi ((natfloor x) div d))
- 2 * x * ln x) +
abs(psi(natfloor y) * ln y +
(∑ d = 1..natfloor y. Lambda d * psi ((natfloor y) div d))
- 2 * y * ln y)";
by (rule abs_triangle_ineq4);
also have "... <= C * x + C * y";
apply (rule add_mono);
apply (insert prems);
apply auto;
done;
also have "... <= C * x + C * x";
apply simp;
apply (rule mult_left_mono);
apply (rule prems);
apply (insert prems);
apply (drule_tac x = 1 in spec);
apply simp;
apply (rule order_trans);
prefer 2;
apply assumption;
apply (rule nonneg_times_nonneg);
apply auto;
done;
also have "... = (C + C) * x";
by (simp add: ring_eq_simps);
also; have "abs (psi (natfloor x) * ln x - psi (natfloor y) * ln y +
((∑ d = 1..natfloor x. Lambda d * psi (natfloor x div d)) -
(∑ d = 1..natfloor y. Lambda d * psi (natfloor y div d)))) =
psi (natfloor x) * ln x - psi (natfloor y) * ln y +
((∑ d = 1..natfloor x. Lambda d * psi (natfloor x div d)) -
(∑ d = 1..natfloor y. Lambda d * psi (natfloor y div d)))";
apply (rule abs_nonneg);
apply (rule nonneg_plus_nonneg);
apply simp;
apply (rule mult_mono);
apply (rule psi_mono);
apply (rule natfloor_mono);
apply (rule prems);
apply (subst ln_le_cancel_iff);
apply (insert prems, arith);
apply arith;
apply assumption;
apply (rule psi_ge_zero);
apply force;
apply (rule a);
done;
also; have "abs (2 * x * ln x - 2 * y * ln y) =
2 * x * ln x - 2 * y * ln y";
apply (rule abs_nonneg);
apply simp;
apply (rule mult_mono);
apply (rule prems);
apply (subst ln_le_cancel_iff);
apply (insert prems);
apply auto;
done;
finally show ?thesis;
by (insert a, arith);
qed;
qed;
qed;
lemma PNT2_aux3: "EX E. ALL x y. 1 <= y --> y < x --> x <= D * y -->
(psi(natfloor x) - psi(natfloor y)) <= 2 * (x - y) + E * (x / ln x)";
proof -;
from PNT2_aux2 obtain C where C: "ALL x y. 1 <= y --> y <= x -->
(psi (natfloor x) * ln x - psi (natfloor y) * ln y) <=
(2 * x * ln x - 2 * y * ln y) + C * x";..;
show ?thesis;
proof ((rule exI), clarify);;
fix x::"real";
fix y::"real";
assume "1 <= y";
assume "y < x";
assume "x <= D * y";
have "(psi (natfloor x) * ln x - psi (natfloor y) * ln y) <=
(2 * x * ln x - 2 * y * ln y) + C * x";
by (insert C prems, auto);
also have "psi(natfloor x) * ln x - psi(natfloor y) * ln y =
ln x * (psi(natfloor x) - psi(natfloor y)) +
psi (natfloor y) * (ln x - ln y)";
by (simp add: ring_eq_simps);
also have "(2 * x * ln x - 2 * y * ln y) =
2 * (x - y) * ln x + 2 * y * (ln x - ln y)";
by (simp add: ring_eq_simps);
also have "ln x - ln y = ln (x / y)";
apply (rule ln_div [THEN sym]);
apply (insert prems);
apply arith+;
done;
finally; have "ln x * (psi (natfloor x) - psi (natfloor y))
<= 2 * (x - y) * ln x + 2 * y * ln (x / y) + C * x";
apply (subgoal_tac "0 <= psi(natfloor y) * ln(x / y)");
apply arith;
apply (rule nonneg_times_nonneg);
apply (rule psi_ge_zero);
apply (rule ln_ge_zero);
apply (subst pos_le_divide_eq);
apply (insert prems, arith);
apply simp;
done;
also have "... <= 2 * (x - y) * ln x + 2 * x * ln D + C * x";
apply (rule add_right_mono);
apply (rule add_left_mono);
apply (rule mult_mono);
apply (rule mult_left_mono);
apply (rule order_less_imp_le, rule prems);
apply force;
apply (subst ln_le_cancel_iff);
apply (rule pos_div_pos);
apply (insert prems, arith);
apply arith;
prefer 2;
apply (subst pos_divide_le_eq);
apply arith;
apply assumption;
apply (rule order_less_le_trans);
apply (subgoal_tac "0 < x / y");
apply assumption;
apply (rule pos_div_pos);
apply arith;
apply arith;
apply (subst pos_divide_le_eq);
apply arith;
apply assumption;
apply arith;
apply (rule ln_ge_zero);
apply (subst pos_le_divide_eq);
apply arith;
apply simp;
done;
also have "... = 2 * (x - y) * ln x + (2 * ln D + C) * x";
by (simp add: ring_eq_simps);
finally have "ln x * (psi (natfloor x) - psi (natfloor y))
<= 2 * (x - y) * ln x + (2 * ln D + C) * x" (is "?LHS <= ?RHS");.;
then have "?LHS / ln x <= ?RHS / ln x";
apply (rule divide_right_mono);
apply (rule ln_ge_zero);
apply (insert prems, arith);
done;
also have "?LHS / ln x = (psi (natfloor x) - psi (natfloor y))";
apply (subgoal_tac "0 < ln x");
apply simp;
apply (rule ln_gt_zero);
apply (insert prems, arith);
done;
also have "?RHS / ln x = 2 * (x - y) + (2 * ln D + C) * (x / ln x)";
apply (subgoal_tac "0 < ln x");
apply (subst add_divide_distrib);
apply simp;
apply (rule ln_gt_zero);
apply (insert prems, arith);
done;
finally show "psi (natfloor x) - psi (natfloor y) <= 2 * (x - y) +
(2 * ln D + C) * (x / ln x)";.;
qed;
qed;
lemma PNT2_aux4: "EX C. ALL x. abs (R(x) / x) < C";
apply (insert error0);
apply (simp only: bigo_alt_def);
apply clarsimp;
apply (rule_tac x = "c + 1" in exI);
apply (rule allI);
apply (drule_tac x = x in spec);
apply (case_tac "x = 0");
apply simp;
apply (subst abs_divide);
apply (subst pos_divide_less_eq);
apply arith;
apply (simp add: ring_eq_simps);
apply arith;
done;
lemma PNT2_aux5: "0 < eps ==> EX x. ALL y. (x < y --> 1 / ln y < eps)";
apply (rule_tac x = "max 1 (exp (1 / eps))" in exI);
apply clarify;
apply (subst pos_divide_less_eq);
apply (rule ln_gt_zero);
apply force;
apply (subst mult_commute);
apply (subst pos_divide_less_eq [THEN sym]);
apply assumption;
apply (subgoal_tac "1 / eps = ln (exp (1 / eps))");
apply (erule ssubst);
apply (subst ln_less_cancel_iff);
apply auto;
done;
lemma PNT2: "EX lambda C1. 0 < lambda & lambda < 1 &
(ALL eps. 0 < eps --> eps < 1 --> (EX x1. ALL K x.
exp (C1 / eps) < K --> x1 < x --> (EX xstar.
x < xstar & (1 + lambda * eps) * xstar < K * x & (ALL u.
xstar <= u & u <= (1 + lambda * eps) * xstar -->
abs(R u) < eps * u))))" (is "EX lambda C1. ?P lambda C1");
proof -;
from PNT2_aux4 obtain Cstar where Cstar: "ALL x. abs (R(x) / x) < Cstar";..;
have Cstar0: "0 < Cstar";
apply (insert Cstar);
apply (drule_tac x = 0 in spec);
apply simp;
done;
let ?lambda = "1 / (3 * (Cstar + 3))";
have lambda0: "0 < ?lambda";
apply (rule pos_div_pos);
apply force;
apply (rule mult_pos);
apply force;
apply (rule pos_plus_pos);
apply (rule Cstar0);
apply force;
done;
have lambda1: "?lambda < 1";
apply (subst pos_divide_less_eq);
apply (rule mult_pos);
apply force;
apply (insert Cstar0, arith);
apply simp;
done;
from PNT1a obtain C0 where C0temp: "ALL eps. 0 < eps -->
eps < 1 --> (EX x0. ALL K x. exp (C0 / eps) < K -->
x0 < x --> (EX n::nat. x < real n &
real n <= K * x & abs (R (real n) / real n) < eps))";..;
let ?C1 = "3 * C0 + ln 2";
show ?thesis;
proof (rule exI)+;
show "?P ?lambda ?C1";
apply (rule conjI);
apply (rule lambda0);
apply (rule conjI);
apply (rule lambda1);
apply clarify;
proof -;
fix eps::"real";
assume eps0: "0 < eps";
assume eps1: "eps < 1";
have "EX x0. ALL K x.
exp (C0 / (eps / 3)) < K --> x0 < x --> (EX (n::nat).
x < real n & real n <= K * x &
abs(R(real n) / (real n)) < eps / 3)";
apply (insert eps0 eps1 C0temp);
apply (drule_tac x = "eps / 3" in spec);
apply (drule mp);
apply arith;
apply (drule mp);
apply arith;
apply assumption;
done;
then obtain x0 where C0x0: "ALL K x.
exp (C0 / (eps / 3)) < K --> x0 < x -->
(EX (n::nat). x < real n & real n <= K * x &
abs(R(real n) / (real n)) < eps / 3)"; by auto;
have C1: "!!K. exp (?C1 / eps) < K ==> 2 * exp (C0 / (eps / 3)) < K";
apply (rule order_le_less_trans);
prefer 2;
apply assumption;
apply (subgoal_tac "(3 * C0 + ln 2) / eps =
ln 2 / eps + (3 * C0 / eps)");
apply (erule ssubst);
apply (subst exp_add);
apply simp;
apply (rule mult_mono);
apply (subgoal_tac "2 = exp (ln 2)");
apply (erule ssubst);
apply (subst exp_le_cancel_iff);
apply simp;
apply (subst pos_le_divide_eq);
apply (rule eps0);
apply (subgoal_tac "ln 2 * eps <= ln 2 * 1");
apply simp;
apply (rule mult_left_mono);
apply (rule order_less_imp_le, rule eps1);
apply force;
apply simp;
apply (simp add: mult_ac);
apply force;
apply force;
apply (simp add: ring_eq_simps add_divide_distrib);
done;
from PNT2_aux3 obtain E where E: "ALL x y. 1 <= y --> y < x -->
x <= 2 * y --> (psi(natfloor x) - psi(natfloor y)) <=
2 * (x - y) + E * (x / ln x)"; ..;
let ?E2 = "max E 1";
have E2a: "0 < ?E2";
apply (subgoal_tac "1 <= ?E2");
apply arith;
apply (rule le_maxI2);
done;
have E2b: "ALL x y. 1 <= y --> y < x -->
x <= 2 * y --> (psi(natfloor x) - psi(natfloor y)) <=
2 * (x - y) + ?E2 * (x / ln x)";
apply (clarify);
apply (insert E);
apply (drule_tac x = x in spec);
apply (drule_tac x = y in spec);
apply clarify;
apply (subgoal_tac "E * (x / ln x) <= ?E2 * (x / ln x)");
apply arith;
apply (rule mult_right_mono);
apply (rule le_maxI1);
apply (rule order_less_imp_le);
apply (rule pos_div_pos);
apply arith;
apply (rule ln_gt_zero);
apply arith;
done;
have "EX x. ALL y. (x < y --> 1 / ln y <
eps / (3 * ?E2 * (1 + ?lambda * eps)))";
apply (rule PNT2_aux5);
apply (rule pos_div_pos);
apply (rule eps0);
apply (rule mult_pos);
apply (rule mult_pos);
apply force;
apply (rule E2a);
apply (rule pos_plus_pos);
apply force;
apply (rule mult_pos);
apply (rule lambda0);
apply (rule eps0);
done;
then obtain xtemp where xtemp:
"ALL y. (xtemp < y --> 1 / ln y <
eps / (3 * ?E2 * (1 + ?lambda * eps)))";..;
let ?x1 = "max (max xtemp x0) 1";
have x1a: "1 <= ?x1"; by (rule le_maxI2);
have x1b: "x0 <= ?x1";
apply (rule order_trans);
apply (rule le_maxI2);
apply (rule le_maxI1);
done;
have x1c: "xtemp <= ?x1";
apply (rule order_trans);
apply (rule le_maxI1);
apply (rule le_maxI1);
done;
show "EX x1. ALL K x. exp (?C1 / eps) < K --> x1 < x -->
(EX xstar. x < xstar &
(1 + 1 / (3 * (Cstar + 3)) * eps) * xstar < K * x &
(ALL u. xstar <= u &
u <= (1 + 1 / (3 * (Cstar + 3)) * eps) * xstar -->
abs (R u) < eps * u))" (is "EX x1. ?P x1");
proof ((rule exI)+, clarify);
fix K;
fix x;
assume K: "exp (?C1 / eps) < K";
assume x: "?x1 < x";
have xa: "1 < x";
apply (rule order_le_less_trans);
prefer 2;
apply (rule x);
apply (rule x1a);
done;
have xb: "x0 < x";
apply (rule order_le_less_trans);
prefer 2;
apply (rule x);
apply (rule x1b);
done;
have xc: "xtemp < x";
apply (rule order_le_less_trans);
prefer 2;
apply (rule x);
apply (rule x1c);
done;
have "EX (n::nat). x < real n & real n <= (K / 2) * x &
abs(R(real n) / (real n)) < eps / 3";
apply (insert C0x0);
apply (drule_tac x = "K / 2" in spec);
apply (drule_tac x = x in spec);
apply (drule mp);
apply (subst pos_less_divide_eq);
apply force;
apply (subst mult_commute);
apply (rule C1);
apply (rule K);
apply (drule mp);
apply (rule xb);
apply assumption;
done;
then obtain n::"nat" where n: "x < real n &
real n <= K / 2 * x & abs (R (real n) / real n) < eps / 3";..;
from n have n1: "x < real n";..;
from n have n2: "real n <= (K / 2) * x"; by auto;
from n have n3: "abs (R (real n) / real n) < eps / 3"; by auto;
show "EX xstar. x < xstar &
(1 + 1 / (3 * (Cstar + 3)) * eps) * xstar < K * x &
(ALL u. xstar <= u &
u <= (1 + 1 / (3 * (Cstar + 3)) * eps) * xstar -->
abs (R u) < eps * u)" (is "EX xstar. ?P xstar");
proof;
let ?xstar = "real n";
show "?P ?xstar";
apply (rule conjI);
apply (rule n1);
apply (rule conjI);
apply (rule order_le_less_trans);
apply (subgoal_tac "(1 + ?lambda * eps) * real n <=
(1 + ?lambda * eps) * ((K / 2) * x)");
apply assumption;
apply (rule mult_left_mono);
apply (rule n2);
apply (rule nonneg_plus_nonneg);
apply force;
apply (rule nonneg_times_nonneg);
apply (rule order_less_imp_le);
apply (rule pos_div_pos);
apply force;
apply (rule mult_pos);
apply force;
apply (rule pos_plus_pos);
apply (rule Cstar0);
apply force;
apply (rule order_less_imp_le);
apply (rule eps0);
apply (rule order_less_le_trans);
apply (subgoal_tac "(1 + ?lambda * eps) * (K / 2 * x) <
2 * (K / 2 * x)");
apply assumption;
apply (rule mult_strict_right_mono);
apply simp;
apply (subst pos_divide_less_eq);
apply (insert Cstar0, arith);
apply (insert eps1, simp);
apply (rule mult_pos);
apply (subgoal_tac "0 < K");
apply arith;
apply (rule order_le_less_trans);
prefer 2;
apply (rule prems);
apply force;
apply (insert xa, arith);
apply simp;
apply clarify;
proof -;
fix u;
assume xstar1: "?xstar <= u";
assume xstar2: "u <= (1 + ?lambda * eps) * ?xstar";
show "abs (R u) < eps * u";
proof -;
(* reset indentation for convenience, and rename xstar to n *)
let ?n = "?xstar";
have "abs (R(u) / u - R(?n) / ?n) = abs(R(u) * (1 / u - 1 / ?n) +
(R(u) - R(?n)) / ?n)";
apply (simp add: ring_eq_simps diff_divide_distrib);
done;
also have "... <= abs (R(u) * (1 / u - 1 / ?n)) + abs ((R(u) - R(?n)) / ?n)";
by (rule abs_triangle_ineq);
also have "abs (R(u) * (1 / u - 1 / ?n)) =
abs (R(u) / u) * abs (1 - u / ?n)";
apply (subst abs_mult [THEN sym]);
apply (rule arg_cong);back;
apply (simp add: ring_eq_simps);
apply (rule nonzero_mult_divide_cancel_left);
apply (insert n1 xa xstar1);
apply arith;
apply arith;
done;
also have "abs (1 - u / ?n) = u / ?n - 1";
apply (subst abs_nonpos);
apply simp;
apply (subst pos_le_divide_eq);
apply (insert n1 xa, arith);
apply (simp add: xstar1);
apply (simp add: ring_eq_simps);
done;
also have "abs ((R(u) - R(?n)) / ?n) = 1 / ?n * abs(R(u) - R(?n))";
apply (subst abs_divide);
apply simp;
done;
also have "R(u) - R(?n) = psi(natfloor(u)) - psi(natfloor(?n)) -
(u - ?n)";
by (simp add: R_def);
finally have "abs (R u / u - R ?n / ?n) <=
abs (R u / u) * (u / ?n - 1) +
1 / ?n * abs (psi (natfloor u) - psi (natfloor ?n) - (u - ?n))";.;
also have "... <= abs (R u / u) * (u / ?n - 1) +
1 / ?n * (abs (psi (natfloor u) - psi (natfloor ?n)) + abs(u - ?n))";
apply (rule add_left_mono);
apply (rule mult_left_mono);
apply (rule abs_triangle_ineq4);
apply (subst pos_le_divide_eq);
apply (insert n1 xa, arith);
apply simp;
done;
also have "1 / ?n * (abs (psi (natfloor u) - psi (natfloor ?n)) +
abs(u - ?n))
= (psi (natfloor u) - psi(natfloor ?n)) / ?n + (u / ?n - 1)";
apply (subst abs_nonneg);
apply (simp add: xstar1);
apply (subst abs_nonneg);
apply (simp del: natfloor_real_id);
apply (rule psi_mono);
apply (rule natfloor_mono);
apply (rule prems);
apply (simp add: ring_eq_simps diff_divide_distrib);
apply (insert prems, arith);
done;
also have "abs (R u / u) * (u / ?n - 1) +
((psi (natfloor u) - psi (natfloor ?n)) / ?n + (u / ?n - 1)) =
(u / ?n - 1) * (abs (R u / u) + 1) +
(psi (natfloor u) - psi (natfloor ?n)) / ?n";
by (simp add: ring_eq_simps);
finally have "abs (R u / u - R ?n / ?n) <=
(u / ?n - 1) * (abs (R u / u) + 1) +
(psi (natfloor u) - psi (natfloor ?n)) / ?n";.;
also have "... <= (u / ?n - 1) * (abs (R u / u) + 1) +
(2 * (u - ?n) + ?E2 * (u / ln u)) / ?n";
apply (rule add_left_mono);
apply (rule divide_right_mono);
apply (case_tac "u = ?n");
apply simp;
apply (rule order_less_imp_le);
apply (rule pos_div_pos);
apply (rule mult_pos);
apply (rule E2a);
apply (insert n1 xa, arith);
apply (rule ln_gt_zero);
apply arith;
apply (insert E2b);
apply (drule_tac x = u in spec);
apply (drule_tac x = ?n in spec);
apply (drule_tac mp);
apply (insert n1 xa, arith);
apply (drule_tac mp);
apply (insert xstar1, arith);
apply (drule_tac mp);
apply (rule order_trans);
apply (rule xstar2);
apply (rule mult_right_mono);
apply simp;
apply (subst pos_divide_le_eq);
apply (insert Cstar0, arith);
apply simp;
apply (insert eps1, arith);
apply arith;
apply assumption;
apply arith;
done;
also have "... = (u / ?n - 1) * (abs (R u / u) + 3) +
(?E2 * u / ?n) * (1 / ln u)" (is "?temp = ?term1 + ?term2");
apply (simp add: ring_eq_simps add_divide_distrib diff_divide_distrib);
apply auto;
apply (insert n1 xa, arith);
apply (subst add_divide_distrib [THEN sym]);
apply simp;
done;
also have "... <= ?term1 + (?E2 * (1 + ?lambda * eps) * x / x) *
(1 / ln x)";
apply (rule add_left_mono);
apply (rule mult_mono);
apply (subst times_divide_eq_right [THEN sym]);back;
apply (subst mult_assoc);
apply (subst times_divide_eq_right [THEN sym]);
apply (rule mult_left_mono);
apply (rule real_fraction_le);
apply (insert xa, arith);
apply (insert n, arith);
apply (simp only: times_ac1);
apply (subst mult_commute);back;back;back;back;
apply (rule mult_left_mono);
apply (subst mult_commute);
apply (subst mult_commute);back;
apply (rule xstar2);
apply arith;
apply (rule order_less_imp_le, rule E2a);
apply (rule real_one_div_le_anti_mono);
apply (rule ln_gt_zero);
apply assumption;
apply (subst ln_le_cancel_iff);
apply arith;
apply (insert xstar1 n1, arith);
apply arith;
apply (rule order_less_imp_le);
apply (rule pos_div_pos);
apply (rule mult_pos)+;
apply (rule E2a);
apply (rule pos_plus_pos);
apply force;
apply (rule mult_pos);
apply (rule pos_div_pos);
apply force;
apply simp;
apply (insert Cstar0, arith);
apply (rule eps0);
apply arith;
apply arith;
apply (rule order_less_imp_le);
apply (rule pos_div_pos);
apply force;
apply (rule ln_gt_zero);
apply arith;
done;
also have "... = ?term1 + (?E2 * (1 + ?lambda * eps)) * (1 / ln x)";
apply (subgoal_tac "x ~= 0");
apply simp;
apply (insert xa, arith);
done;
finally; have "abs (R u / u - R ?n / ?n)
<= (u / ?n - 1) * (abs (R u / u) + 3) +
max E 1 * (1 + 1 / (3 * (Cstar + 3)) * eps) * (1 / ln x)"
(is "?LHS <= ?RHS");.;
then have a: "?LHS + abs (R ?n / ?n) <= ?RHS + abs(R ?n / ?n)";
by (intro add_right_mono);
have "abs (R u / u) = abs (R u / u - R ?n / ?n + R ?n / ?n)";
by simp;
also have "... <= ?LHS + abs (R ?n / ?n)";
by (rule abs_triangle_ineq);
also note a;
also have "?RHS + abs(R ?n / ?n) < eps / 3 + eps / 3 + eps / 3";
apply (rule add_le_less_mono);
apply (rule add_mono);
apply (rule order_trans);
apply (subgoal_tac "(u / real n - 1) * (abs (R u / u) + 3) <=
(?lambda * eps) * (Cstar + 3)");
apply assumption;
apply (rule mult_mono);
apply (simp only: compare_rls);
apply (subst add_commute);
apply (subst pos_divide_le_eq);
apply (insert n1 xa, arith);
apply (rule prems);
apply simp;
apply (rule order_less_imp_le);
apply (insert Cstar);
apply (erule spec);
apply (rule nonneg_times_nonneg);
apply (rule order_less_imp_le);
apply (rule pos_div_pos);
apply force;
apply simp;
apply (insert Cstar0, arith);
apply (insert eps0, arith);
apply arith;
apply simp;
apply (subst pos_divide_le_eq);
apply arith;
apply (simp add: ring_eq_simps);
apply (rule order_trans);
apply (insert xtemp);
apply (drule_tac x = x in spec);back;
apply (drule mp);
apply (rule xc);
apply (rule mult_left_mono);
apply (rule order_less_imp_le);
apply assumption;
apply (rule nonneg_times_nonneg);
apply arith;
apply (rule nonneg_plus_nonneg);
apply force;
apply (rule nonneg_times_nonneg);
apply simp;
apply simp;
apply (subgoal_tac "?E2 ~= 0");
apply simp;
apply (subst pos_divide_le_eq);
apply (rule pos_plus_pos);
apply force;
apply (rule pos_div_pos);
apply arith;
apply arith;
apply (simp add: ring_eq_simps);
apply (insert E2a);
apply arith;
apply (rule n3);
done;
also have "... = eps";
apply simp;
apply (subst add_divide_distrib [THEN sym]);
apply simp;
done;
finally show ?thesis;
apply (simp add: abs_divide);
apply (subgoal_tac "abs u = u");
apply simp;
apply (subst pos_divide_less_eq [THEN sym]);
apply (insert xstar1 n1 xa, arith);
apply assumption;
apply (rule abs_nonneg);
apply arith;
done;
qed;qed;qed;qed;qed;qed;qed;
lemma PNT2a: "EX lambda C1. 0 < lambda & lambda < 1 & 1 <= C1 &
(ALL eps. 0 < eps --> eps < 1 --> (EX x1. 1 <= x1 & (ALL K x.
exp (C1 / eps) <= K --> x1 <= x --> (EX xstar.
x < xstar & (1 + lambda * eps) * xstar < K * x & (ALL u.
xstar <= u & u <= (1 + lambda * eps) * xstar -->
abs(R u) < eps * u)))))";
apply (insert PNT2);
apply (erule exE);
apply (erule exE);
apply (rule_tac x = lambda in exI);
apply (rule_tac x = "max C1 1 + 1" in exI);
apply clarify;
apply (rule conjI);
apply simp;
apply (rule order_trans);
prefer 2;
apply (rule le_maxI2);
apply force;
apply clarify;
apply (drule_tac x = eps in spec);
apply clarify;
apply (rule_tac x = "max (x1 + 1) 1" in exI);
apply (rule conjI);
apply (rule le_maxI2);
apply clarify;
apply (drule_tac x = K in spec);
apply (drule_tac x = x in spec);
apply (subgoal_tac "exp (C1 / eps) < K");
apply (subgoal_tac "x1 < x");
apply clarify;
apply (subgoal_tac "x1 + 1 <= x");
apply arith;
apply (rule order_trans);
prefer 2;
apply assumption;
apply (rule le_maxI1);
apply (rule order_less_le_trans);
prefer 2;
apply assumption;
apply (subst exp_less_cancel_iff);
apply (rule divide_strict_right_mono);
apply simp;
apply (rule order_le_less_trans);
apply (subgoal_tac "C1 <= max C1 1");
apply assumption;
apply (rule le_maxI1);
apply arith;
apply assumption;
done;
lemma PNT3_aux1: "EX C. ALL x. 1 <= x -->
abs (R (x)) * (ln x) ^ 2 <=
2 * (∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n)) +
C * abs (x * (1 + ln x))";
apply (insert bigo_lesso5 [OF error7]);
apply clarsimp;
apply (rule_tac x = C in exI);
apply (rule allI);
apply (drule_tac x = "x - 1" in spec);
apply clarsimp;
apply (subgoal_tac "natfloor (x - 1) + 1 = natfloor x");
apply simp;
apply (subst natfloor_add [THEN sym]);
apply simp;
apply simp;
done;
lemma PNT3_aux1a: "EX C. 0 <= C & (ALL x. 2 <= x -->
abs (R (x)) * (ln x) ^ 2 <=
2 * (∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n)) +
C * x * ln x)";
apply (insert PNT3_aux1);
apply clarsimp;
apply (subgoal_tac "0 <= C");
prefer 2;
apply (drule_tac x = 1 in spec);
apply simp;
apply (rule_tac x = "C + C / ln 2" in exI);
apply (rule conjI);
apply (rule nonneg_plus_nonneg);
apply assumption;
apply (subst pos_le_divide_eq);
apply force;
apply simp;
apply clarify;
apply (drule_tac x = x in spec);
apply clarsimp;
apply (erule order_trans);
apply (rule add_left_mono);
apply (subst abs_nonneg);
apply (subgoal_tac "0 <= ln x");
apply arith;
apply force;
apply (simp add: mult_ac);
apply (subst mult_left_commute);back;
apply (rule mult_left_mono);
apply (simp add: ring_eq_simps);
apply (subst pos_le_divide_eq);
apply force;
apply (rule mult_left_mono);
apply auto;
done;
lemma PNT3_aux2: "EX C. ALL x. 0 <= x --> abs (R x) <= C * x";
apply (insert R_bigo);
apply (clarsimp simp add: bigo_alt_def);
apply (rule_tac x = c in exI);
apply clarify;
apply (drule_tac x = x in spec);
apply simp;
done;
lemma PNT3_aux2a: "EX C. 0 < C & (ALL x. 0 <= x --> abs (R x) <= C * x)";
apply (insert PNT3_aux2);
apply clarify;
apply (rule_tac x = "C + 1" in exI);
apply (rule conjI);
apply (subgoal_tac "0 <= C");
apply simp;
apply (drule_tac x = 1 in spec);
apply clarsimp;
apply arith;
apply clarify;
apply (drule_tac x = x in spec);
apply (auto simp add: ring_eq_simps);
done;
lemma PNT3_aux3: "EX C. ALL x. 1 <= x -->
abs((∑ i = 1..natfloor x. ln (real i) / real i) -
(ln x) ^ 2 / 2) <= C";
apply (insert identity_four_real_b_cor);
apply (drule set_plus_imp_minus);
apply (simp only: func_diff);
apply (simp only: bigo_alt_def);
apply clarsimp;
apply (rule_tac x = c in exI);
apply (rule allI);
apply (drule_tac x = "(x - 1)" in spec);
apply clarify;
apply (subgoal_tac "natfloor (abs (x - 1)) + 1 = natfloor x");
apply (subgoal_tac "abs (x - 1) + 1 = x");
apply (simp only:);
apply (erule Selberg.aux2);
apply (erule Selberg.aux);
done;
lemma PNT3_aux4: "EX C. ALL x x2. 1 <= x2 --> x2 <= x -->
(∑ n = natfloor (x / x2) + 1..natfloor x.
ln (real n) / real n) <=
ln x2 * ln x + C";
proof -;
from PNT3_aux3 obtain C where C: "ALL x. 1 <= x -->
abs((∑ i = 1..natfloor x. ln (real i) / real i) -
(ln x) ^ 2 / 2) <= C";..;
show ?thesis;
proof (rule exI, clarify);
fix x::"real";
fix x2::"real";
assume a: "1 <= x2";
assume b: "x2 <= x";
show "(∑ n = natfloor (x / x2) + 1..natfloor x.
ln (real n) / real n) <=
ln x2 * ln x + (C + C)";
proof -;
let ?term1 = "(((ln x) ^ 2 / 2) - (ln (x / x2))^2 / 2)";
have "(∑n:{natfloor (x / x2) + 1..natfloor x}.
ln (real n) / real n) =
(∑n:{1..natfloor x}. ln (real n) / real n) -
(∑n:{1..natfloor (x / x2)}. ln (real n) / real n)";
apply (simp add: compare_rls);
apply (subst setsum_Un_disjoint [THEN sym]);
apply simp;
apply simp;
apply force;
apply (rule setsum_cong);
apply auto;
apply (erule order_trans);
apply (rule natfloor_mono);
apply (subst pos_divide_le_eq);
apply (insert a, arith);
apply (subgoal_tac "?x * 1 <= ?x * x2");
apply simp;
apply (rule mult_left_mono);
apply assumption;
apply (insert b, arith);
done;
then have "abs( ?term1 - (∑n:{natfloor (x / x2) + 1..natfloor x}.
ln (real n) / real n)) =
(abs (?term1 - ...))"; by simp;
also have "... = abs(
(ln x ^ 2 / 2 -
(∑ n = 1..natfloor x. ln(real n) / real n)) +
((∑ n = 1..natfloor (x / x2). ln (real n) / real n) -
ln (x / x2) ^ 2 / 2))";
by (simp add: ring_eq_simps);
also have "... <= abs((ln x ^ 2 / 2 -
(∑ n = 1..natfloor x. ln(real n) / real n))) +
abs((∑ n = 1..natfloor (x / x2). ln (real n) / real n) -
ln (x / x2) ^ 2 / 2)";
by (rule abs_triangle_ineq);
also have "... <= C + C";
apply (rule add_mono);
apply (subst abs_diff);
apply (insert prems, force);
apply (subgoal_tac "1 <= x / x2");
apply force;
apply (subst pos_le_divide_eq);
apply arith;
apply simp;
done;
also; have "?term1 = (2 * ln x * ln x2 - ln x2 ^ 2) / 2";
apply (subst ln_div);
apply (insert a b, arith);
apply arith;
apply (simp add: power2_eq_square diff_divide_distrib
ring_eq_simps);
done;
also have "... = ln x2 * (2 * ln x - ln x2) / 2";
by (simp add: ring_eq_simps power2_eq_square);
finally; have x: "
abs((∑ n = natfloor (x / x2) + 1..natfloor x. ln (real n) / real n) -
ln x2 * (2 * ln x - ln x2) / 2) <=
C + C";
apply (subst abs_diff);
apply assumption;
done;
have "(∑ n = natfloor (x / x2) + 1..natfloor x.
ln (real n) / real n) - ln x2 * (2 * ln x - ln x2) / 2 <=
C + C";
apply (rule order_trans);
prefer 2;
apply (rule x);
apply (rule abs_ge_self);
done;
then have "(∑ n = natfloor (x / x2) + 1..natfloor x.
ln (real n) / real n) <=
ln x2 * (2 * ln x - ln x2) / 2 + (C + C)";
by arith;
also have "ln x2 * (2 * ln x - ln x2) / 2 <= ln x2 * ln x";
apply (subst pos_divide_le_eq);
apply force;
apply (subst mult_assoc);
apply (rule mult_left_mono);
apply simp;
apply (insert a b, auto);
done;
finally; show ?thesis; by auto;
qed;qed;qed;
lemma PNT3_aux5: "EX C. 0 <= C & (ALL x. 1 <= x -->
(∑ i = 1..natfloor x. ln (real i) / real i) <=
(ln x) ^ 2 / 2 + C)";
apply (insert PNT3_aux3);
apply clarify;
apply (rule_tac x = C in exI);
apply (rule conjI);
apply (drule_tac x = 1 in spec);
apply simp;
apply clarify;
apply (drule_tac x = x in spec);
apply clarify;
apply (subgoal_tac "(∑ i = 1..natfloor x. ln (real i) / real i) -
ln x ^ 2 / 2 <= C");
apply arith;
apply (rule order_trans);
prefer 2;
apply assumption;
apply (rule abs_ge_self);
done;
lemma PNT3: "EX G. ALL x x2 S eps alpha.
0 < eps --> 0 < alpha --> alpha < c -->
2 <= x2 --> exp 1 <= x2 --> x2 <= x -->
(ALL x. x2 <= x --> abs(R x) <= alpha * x) -->
S <= {1..natfloor x} -->
(ALL n:S. abs(R(x / real n)) <= eps * (x / real n)) -->
abs (R x)
<= alpha * x -
2 * (alpha - eps) * x * (∑n:S. ln (real n) / real n) / ln x ^ 2 +
G * x * ln x2 / ln x";
proof -;
from PNT3_aux1a obtain C where C: "0 <= C & (ALL x. 2 <= x -->
abs (R (x)) * (ln x) ^ 2 <=
2 * (∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n)) +
C * x * ln x)";..;
then have C1: "ALL x. 2 <= x -->
abs (R (x)) * (ln x) ^ 2 <=
2 * (∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n)) +
C * x * ln x"; by blast;
from C have C2: "0 <= C"; by blast;
from PNT3_aux2 obtain D where D: "ALL x. 0 <= x --> abs (R x) <= D * x";..;
then have D': "0 <= D";
apply (drule_tac x = 1 in spec);
apply simp;
apply arith;
done;
from PNT3_aux4 obtain E where E: "ALL x x2. 1 <= x2 --> x2 <= x -->
(∑ n = natfloor (x / x2) + 1..natfloor x. ln (real n) / real n) <=
ln x2 * ln x + E";..;
then have E': "0 <= E";
apply (drule_tac x = 1 in spec);
apply (drule_tac x = 1 in spec);
apply simp;
done;
from PNT3_aux5 obtain F where F: "0 <= F & (ALL x. 1 <= x -->
(∑ i = 1..natfloor x. ln (real i) / real i) <=
(ln x) ^ 2 / 2 + F)";..;
then have F1: "ALL x. 1 <= x -->
(∑ i = 1..natfloor x. ln (real i) / real i) <=
(ln x) ^ 2 / 2 + F"; by blast;
from F have F2: "0 <= F" by blast;
show ?thesis;
proof ((rule exI)+, clarify);
fix eps::"real";
fix alpha::"real";
fix x::"real";
fix x2::"real";
fix S::"nat set";
assume a: "0 < eps";
assume aa: "0 < alpha";
assume aaa: "alpha < c";
assume b: "2 <= x2";
assume bb: "exp 1 <= x2";
assume c: "x2 <= x";
assume d: "ALL x. x2 <= x --> abs(R x) <= alpha * x";
assume e: "S <= {1..natfloor x}";
assume f: "ALL n:S. abs(R(x / real n)) <= eps * (x / real n)";
have "(∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n)) =
(∑ n:{1..natfloor x} Int S. abs (R (x / real n)) * ln (real n)) +
(∑ n:{1..natfloor x} - S. abs (R (x / real n)) * ln (real n))";
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule finite_subset);
apply (subgoal_tac "?t <= {1..natfloor x}");
apply assumption;
apply force;
apply force;
apply (rule finite_subset);
apply (subgoal_tac "?t <= {1..natfloor x}");
apply assumption;
apply force;
apply force;
apply force;
apply (rule setsum_cong);
apply force;
apply (rule refl);
done;
also have "
(∑n:{1..natfloor x} - S. abs (R (x / real n)) * ln (real n)) =
(∑n:{1..natfloor (x / x2)} - S.
abs (R (x / real n)) * ln (real n)) +
(∑n:{natfloor (x / x2) + 1..natfloor x} - S.
abs (R (x / real n)) * ln (real n))";
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule finite_subset);
apply (subgoal_tac "?t <= {1..natfloor (x / x2)}");
apply assumption;
apply force;
apply force;
apply (rule finite_subset);
apply (subgoal_tac "?t <= {natfloor (x / x2)..natfloor x}");
apply assumption;
apply force;
apply force;
apply force;
apply (rule setsum_cong);
apply auto;
apply (erule order_trans);
apply (rule natfloor_mono);
apply (subst pos_divide_le_eq);
apply (insert b, arith);
apply (subgoal_tac "?x * 1 <= ?x * x2");
apply simp;
apply (rule mult_left_mono);
apply (insert b, arith);
apply (insert c, arith);
done;
also have "
(∑ n:{1..natfloor x} Int S. abs (R (x / real n)) * ln (real n)) <=
(∑ n:{1..natfloor x} Int S. eps * (x / real n) * ln (real n))";
apply (rule setsum_le_cong);
apply (rule mult_right_mono);
apply (insert f, force);
apply force;
done;
also have "... = eps * x *
(∑ n:{1..natfloor x} Int S. ln (real n) / real n)";
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
done;
also have "(∑n:{1..natfloor (x / x2)} - S.
abs (R (x / real n)) * ln (real n)) <=
(∑n:{1..natfloor (x / x2)} - S.
alpha * (x / real n) * ln (real n))";
apply (rule setsum_le_cong);
apply (rule mult_right_mono);
apply clarsimp;
apply (insert d);
apply (drule spec);
apply (drule mp);
prefer 2;
apply (rule order_trans);
apply assumption;
apply simp;
apply (subst pos_le_divide_eq);
apply force;
apply (subst mult_commute);
apply (subst pos_le_divide_eq [THEN sym]);
apply (insert b, arith);
apply (rule nat_le_natfloor);
apply (rule order_less_imp_le);
apply (rule pos_div_pos);
apply (insert c, arith);
apply arith;
apply assumption;
apply simp;
apply force;
done;
also have "... = alpha * x * (∑n:{1..natfloor (x / x2)} - S.
ln (real n) / real n)";
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
done;
also; have "(∑n:{natfloor (x / x2) + 1..natfloor x} - S.
abs (R (x / real n)) * ln (real n)) <=
(∑n:{natfloor (x / x2) + 1..natfloor x}.
abs (R (x / real n)) * ln (real n))";
apply (rule setsum_le_cong2);
apply simp;
apply force;
apply (rule nonneg_times_nonneg);
apply auto;
done;
also; have "alpha * x *
(∑n:{1..natfloor (x / x2)} - S. ln (real n) / real n) <=
alpha * x *
(∑n:{1..natfloor x} - S. ln (real n) / real n)";
apply (rule mult_left_mono);
apply (rule setsum_le_cong2);
apply (rule finite_subset);
apply (subgoal_tac "{1..natfloor x} - S <= {1..natfloor x}");
apply assumption;
apply force;
apply simp;
apply clarsimp;
apply (erule order_trans);
apply (rule natfloor_mono);
apply (subst pos_divide_le_eq);
apply (insert b c, arith);
apply (subgoal_tac "?x * 1 <= ?x * x2");
apply simp;
apply (rule mult_left_mono);
apply arith;
apply simp;
apply (rule real_ge_zero_div_gt_zero);
apply force;
apply force;
apply (rule nonneg_times_nonneg);
apply (insert d);
apply (drule_tac x = x in spec);
apply clarsimp;
apply (rule order_trans);
apply (subgoal_tac "0 <= abs(R x) / x");
apply assumption;
apply (rule real_ge_zero_div_gt_zero);
apply force;
apply arith;
apply (subst pos_divide_le_eq);
apply arith;
apply assumption;
apply arith;
done;
finally; have
"(∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n))
<= eps * x * (∑n:{1..natfloor x} Int S. ln (real n) / real n) +
(alpha * x * (∑n:{1..natfloor x} - S. ln (real n) / real n) +
(∑ n = natfloor (x / x2) + 1..natfloor x.
abs (R (x / real n)) * ln (real n)))";
by arith;
also have "... =
alpha * x * (∑n:{1..natfloor x}. ln (real n) / real n)
- ((alpha - eps) * x *
(∑n:{1..natfloor x} Int S. ln (real n) / real n)) +
(∑ n = natfloor (x / x2) + 1..natfloor x.
abs (R (x / real n)) * ln (real n))";
apply (simp add: ring_eq_simps);
apply (subst right_distrib [THEN sym]);
apply (rule arg_cong);back;
apply (subst right_distrib [THEN sym]);
apply (rule arg_cong);back;
apply (subst setsum_Un_disjoint [THEN sym]);
apply (rule finite_subset);
apply (subgoal_tac "?t <= {1..natfloor x}");
apply assumption;
apply force;
apply simp;
apply (rule finite_subset);
apply (subgoal_tac "?t <= {1..natfloor x}");
apply assumption;
apply force;
apply simp;
apply force;
apply (rule setsum_cong);
apply force;
apply (rule refl);
done;
finally; have g: "
(∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n))
<= alpha * x * (∑ n = 1..natfloor x. ln (real n) / real n) -
(alpha - eps) * x *
(∑n:{1..natfloor x} Int S. ln (real n) / real n) +
(∑ n = natfloor (x / x2) + 1..natfloor x.
abs (R (x / real n)) * ln (real n))";.;
have "abs (R (x)) * (ln x) ^ 2 <=
2 * (∑ n = 1..natfloor x. abs (R (x / real n)) * ln (real n)) +
C * x * ln x";
by (insert C b c, auto);
also note g;
also; have "(∑ n = natfloor (x / x2) + 1..natfloor x.
abs (R (x / real n)) * ln (real n)) <=
(∑ n = natfloor (x / x2) + 1..natfloor x.
D * (x / real n) * ln (real n))";
apply (rule setsum_le_cong);
apply (rule mult_right_mono);
apply (insert D);
apply (subgoal_tac "0 <= ?x / real x");
apply force;
apply (subst pos_le_divide_eq);
apply simp;
apply arith;
apply (insert b c);
apply simp;
apply force;
done;
also have "... = D * x * (∑ n = natfloor (x / x2) + 1..natfloor x.
(ln (real n) / real n))";
apply (subst setsum_const_times [THEN sym]);
apply (rule setsum_cong2);
apply simp;
done;
also have "... <= D * x * (ln x2 * ln x + E)";
apply (rule mult_left_mono);
apply (insert E b c, force);
apply (rule nonneg_times_nonneg);
apply (rule D');
apply arith;
done;
also have "alpha * x * (∑ n = 1..natfloor x. ln (real n) / real n) <=
alpha * x * ((ln x)^2 / 2 + F)";
apply (rule mult_left_mono);
apply (insert F b c, force);
apply (rule nonneg_times_nonneg);
apply (insert aa, auto);
done;
also have "{1..natfloor x} Int S = S";
apply (insert e);
apply blast;
done;
finally; have "abs (R x) * ln x ^ 2
<= 2 *
(alpha * x * (ln x ^ 2 / 2 + F) -
(alpha - eps) * x *
(∑n:S. ln (real n) / real n) +
D * x * (ln x2 * ln x + E)) +
C * x * ln x"; by auto;
also have "... = alpha * x * ln x ^ 2 -
2 * (alpha - eps) * x * (∑n:S. ln (real n) / real n) +
(x * ln x * ((2 * D) * ln x2 + C) + x * ((2 * F) * alpha + 2 * D * E))";
by (simp add: ring_eq_simps);
also have "... <=
alpha * x * ln x ^ 2 -
2 * (alpha - eps) * x * (∑n:S. ln (real n) / real n) +
(x * ln x * ((2 * D) * ln x2 + C * ln x2) +
(x * ln x * ln x2) * ((2 * F) * c + 2 * D * E))";
apply (rule add_left_mono);
apply (rule add_mono);
apply (rule mult_left_mono);
apply (rule add_left_mono);
apply (subgoal_tac "C * ln (exp 1) <= C * ln x2");
apply simp;
apply (rule mult_left_mono);
apply (subst ln_le_cancel_iff);
apply force;
apply (insert a aa aaa b bb c);
apply arith;
apply (rule bb);
apply (rule C2);
apply (rule nonneg_times_nonneg);
apply arith;
apply (rule ln_ge_zero);
apply arith;
apply (rule mult_mono);
apply (subgoal_tac "x * ln (exp 1) * ln (exp 1) <= x * ln x * ln x2");
apply simp;
apply (rule mult_mono);
apply (rule mult_left_mono);
apply (subst ln_le_cancel_iff);
apply (force, force, force, force);
apply (subst ln_le_cancel_iff);
apply (force, force, force);
apply (rule nonneg_times_nonneg);
apply force;
apply (rule ln_ge_zero);
apply force;
apply force;
apply (rule add_right_mono);
apply (rule mult_left_mono);
apply (erule order_less_imp_le);
apply (rule nonneg_times_nonneg);
apply force;
apply (rule F2);
apply (rule nonneg_times_nonneg)+;
apply force;
apply (rule ln_ge_zero);
apply arith;
apply (rule ln_ge_zero);
apply arith;
apply (rule nonneg_plus_nonneg);
apply (rule nonneg_times_nonneg);
apply (rule nonneg_times_nonneg);
apply force;
apply (rule F2);
apply arith;
apply (rule nonneg_times_nonneg)+;
apply force;
apply (rule D');
apply (rule E');
done;
finally have x: "abs (R x) * ln x ^ 2
<= alpha * x * ln x ^ 2 -
2 * (alpha - eps) * x * (∑n:S. ln (real n) / real n) +
x * ln x * ln x2 * (2 * D + C + 2 * F * c + 2 * D * E)"
(is "?term1 <= ?term2 - ?term3 + ?term4 * ?term5");
by (simp add: ring_eq_simps);
have y: "ln x ~= 0";
apply (rule less_imp_neq [THEN not_sym]);
apply (rule ln_gt_zero);
apply (insert b c, arith);
done;
have z: "(ln x ^ 2) ~= 0";
apply (rule less_imp_neq [THEN not_sym]);
apply (subst power2_eq_square);
apply (rule mult_pos);
apply (rule ln_gt_zero);
apply (insert b c, arith);
apply (rule ln_gt_zero);
apply (insert b c, arith);
done;
from x have "?term1 / (ln x ^ 2) <=
(?term2 - ?term3 + ?term4 * ?term5) / (ln x ^ 2)";
apply (rule divide_right_mono);
apply force;
done;
also have "?term1 / (ln x^2) = abs (R x)";
by (insert y, simp);
also have "(?term2 - ?term3 + ?term4 * ?term5) / (ln x ^ 2) =
?term2 / (ln x ^ 2) - ?term3 / (ln x ^ 2) + ?term4 / (ln x ^ 2) * ?term5";
by (simp add: ring_eq_simps add_divide_distrib diff_divide_distrib);
also have "?term2 / (ln x ^ 2) = alpha * x";
by (insert z, simp);
also have "?term4 / (ln x ^ 2) * ?term5 = ?term5 * x * ln x2 / ln x";
by (simp add: power2_eq_square y);
finally; show "abs (R x)
<= alpha * x -
2 * (alpha - eps) * x * (∑n:S. ln (real n) / real n) / ln x ^ 2 +
?term5 * x * ln x2 / ln x";.;
qed;qed;
lemma PNT4_aux1: "1 < c2 ==> EX C. 0 < C & (ALL alpha.
0 < alpha --> alpha < c2 -->
(EX xlarge. ALL x. xlarge <= x -->
(EX S. S <= {1..natfloor x} &
(ALL n:S. abs(R(x / real n)) <= (alpha / c2) * (x / real n)) &
C * alpha^2 * (ln x)^2
<= (∑ n:S. ln(real n) / (real n)))))";
proof -;
assume c2_gt_1: "1 < c2";
from PNT2a obtain lambda c1 where lambdac1: "0 < lambda &
lambda < 1 & 1 <= c1 & (ALL eps. 0 < eps --> eps < 1 -->
(EX x1. 1 <= x1 & (ALL K x. exp (c1 / eps) <= K --> x1 <= x -->
(EX xstar. x < xstar &
(1 + lambda * eps) * xstar < K * x &
(ALL u. xstar <= u & u <= (1 + lambda * eps) * xstar -->
abs (R u) < eps * u)))))"; by blast;
from lambdac1 have lambda_gt_0: "0 < lambda" by blast;
from lambdac1 have lambda_le_1: "lambda < 1"; by blast;
from lambdac1 have c1_gt_1: "1 <= c1"; by blast;
show ?thesis;
proof;
let ?C = "lambda / (32 * c1 * c2 ^ 2)";
show "0 < ?C & (ALL alpha.
0 < alpha --> alpha < c2 -->
(EX xlarge. ALL x. xlarge <= x -->
(EX S. S <= {1..natfloor x} &
(ALL n:S. abs(R(x / real n)) <= (alpha / c2) * (x / real n)) &
?C * alpha^2 * (ln x)^2
<= (∑ n:S. ln(real n) / (real n)))))";
proof;
show "0 < ?C";
apply (rule pos_div_pos);
apply (rule lambda_gt_0);
apply (rule mult_pos);
apply (rule mult_pos);
apply force;
apply (insert c1_gt_1, arith);
apply (subst power2_eq_square);
apply (rule mult_pos);
apply (insert c2_gt_1, arith, arith);
done;
next show "ALL alpha.
0 < alpha --> alpha < c2 -->
(EX xlarge. ALL x. xlarge <= x -->
(EX S. S <= {1..natfloor x} &
(ALL n:S. abs(R(x / real n)) <= (alpha / c2) * (x / real n)) &
?C * alpha^2 * (ln x)^2
<= (∑ n:S. ln(real n) / (real n))))";
proof (clarify);
fix alpha::"real";
assume alpha_gt_0: "0 < (alpha::real)";
assume alpha_lt_c2: "alpha < c2";
let ?eps = "alpha / c2";
have eps_gt_0: "0 < ?eps";
apply (rule pos_div_pos);
apply (rule alpha_gt_0);
apply (insert c2_gt_1, arith);
done;
have eps_lt_1: "?eps < 1";
apply (subst pos_divide_less_eq);
apply (insert alpha_gt_0 alpha_lt_c2, arith);
apply simp;
done;
from lambdac1 eps_gt_0 eps_lt_1 have "EX x1. 1 <= x1 & (ALL K x.
exp (c1 / ?eps) <= K --> x1 <= x --> (EX xstar.
x < xstar & (1 + lambda * ?eps) * xstar < K * x & (ALL u.
xstar <= u & u <= (1 + lambda * ?eps) * xstar -->
abs(R u) < ?eps * u)))"; by blast;
then obtain x1 where x1c1: "1 <= x1 & (ALL K x.
exp (c1 / ?eps) <= K --> x1 <= x --> (EX xstar.
x < xstar & (1 + lambda * ?eps) * xstar < K * x & (ALL u.
xstar <= u & u <= (1 + lambda * ?eps) * xstar -->
abs(R u) < ?eps * u)))";..;
then have x1_ge_1: "1 <= x1"; by blast;
let ?K = "exp (c1 / ?eps)";
have K_gt_1: "1 < ?K";
apply (subgoal_tac "exp 0 < ?K");
apply simp;
apply (subst exp_less_cancel_iff);
apply (rule pos_div_pos);
apply (insert c1_gt_1, arith);
apply (insert eps_gt_0, arith);
done;
from x1c1 have x1K: "ALL x. x1 <= x --> (EX xstar.
x < xstar & (1 + lambda * ?eps) * xstar < ?K * x & (ALL u.
xstar <= u & u <= (1 + lambda * ?eps) * xstar -->
abs(R u) < ?eps * u))"
by auto;
let ?xlarge = "max (max (max (max (max (max (max
2 (?K powr 2)) (exp 2 + 1))
((2 / (1 - 1 / (1 + lambda * ?eps))) powr 2))
(exp ((alpha * (ln x1 * 2) + c1 * (c2 * 4)) / alpha)))
(exp (2 * (c1 * c2) / alpha)))
(x1 powr 8))
(exp (3 / (alpha / (8 * (c1 * c2)))))";
show "EX xlarge. ALL x. xlarge <= x --> (EX S<={1..natfloor x}.
(ALL n:S. abs (R (x / real n)) <= alpha / c2 * (x / real n)) &
?C * alpha ^ 2 * ln x ^ 2
<= (∑n:S. ln (real n) / real n))";
proof (rule exI, clarify);
fix x::"real";
assume xlarge: "?xlarge <= x";
then have x_gt_1: "1 < (x::real)" and
x_ge_K_squared: "?K powr 2 <= x" and
x_gt_exp2: "exp 2 < x" and
x_ge_blah: "(2 / (1 - 1 / (1 + lambda * ?eps))) powr 2 <= x" and
x_ge_blah2: "exp ((alpha * (ln x1 * 2) + c1 * (c2 * 4)) / alpha)
<= x" and
x_ge_blah3: "exp (2 * (c1 * c2) / alpha) <= x" and
x_ge_blah4: "x1 powr 8 <= x" and
x_ge_blah5: "exp (3 / (alpha / (8 * (c1 * c2)))) <= x";
by auto;
let ?jstar = "natfloor (ln x1 / ln ?K) + 1";
have jstar: "!!j. ?jstar < j ==> x1 <= ?K powr (real j)";
apply (subst ln_le_cancel_iff [THEN sym]);
apply simp;
apply (insert x1_ge_1, arith);
apply force;
apply (subst ln_pwr);
apply force;
apply arith;
apply (rule order_less_imp_le);
apply (subst pos_divide_less_eq [THEN sym]);
apply (rule ln_gt_zero);
apply (rule exp_gt_one);
apply (rule pos_div_pos);
apply (insert c1_gt_1, arith);
apply (rule eps_gt_0);
apply (rule ge_natfloor_plus_one_imp_gt);
apply (erule order_less_imp_le);
done;
let ?jhat = "natfloor (ln x / (2 * ln ?K)) - 1";
have jhat: "!!j. j <= ?jhat ==> ?K powr ((real j) + 1) <= x powr (1 / 2)";
apply (subst ln_le_cancel_iff [THEN sym]);
apply force;
apply (rule powr_gt_zero);
apply (subst ln_pwr);
apply (insert x_gt_1, arith);
apply simp;
apply (subst ln_pwr);
apply simp;
apply simp;
apply simp;
apply (subst pos_divide_le_eq);
apply (rule alpha_gt_0);
apply (subgoal_tac "real (j + 1) * (c1 * (c2 * 2)) <= alpha * ln x");
apply (simp add: ring_eq_simps compare_rls);
apply (subst pos_le_divide_eq [THEN sym]);
apply (rule mult_pos);
apply (insert c1_gt_1, arith);
apply (rule mult_pos);
apply (insert c2_gt_1, arith);
apply force;
apply (rule nat_le_natfloor);
apply (rule real_ge_zero_div_gt_zero);
apply (rule nonneg_times_nonneg);
apply (rule order_less_imp_le);
apply (rule alpha_gt_0);
apply (rule ln_ge_zero);
apply (rule order_less_imp_le);
apply (rule x_gt_1);
apply (rule mult_pos);
apply (insert c1_gt_1, arith);
apply arith;
apply (simp add: mult_ac);
apply (subgoal_tac "natfloor 1 <=
natfloor (alpha * ln x / (c1 * (c2 * 2)))");
apply simp;
apply arith;
apply (rule natfloor_mono);
apply (subst pos_le_divide_eq);
apply (simp add: pos_le_divide_eq mult_ac);
apply (rule mult_pos);
apply arith;
apply arith;
apply simp;
apply (insert x_ge_K_squared);
apply (subgoal_tac "2 * ln (exp (c1 / (alpha / c2))) <= ln x");
apply simp;
apply (subst mult_commute);
apply (subst pos_divide_le_eq [THEN sym]);
apply (rule alpha_gt_0);
apply (simp add: mult_ac);
apply (subst ln_pwr [THEN sym]);
apply auto;
done;
have xstar_aux: "!!j. ?jstar < j ==>
(EX xstar.
?K powr (real j) < xstar & (1 + lambda * ?eps) * xstar <
?K * (?K powr (real j)) & (ALL u.
xstar <= u & u <= (1 + lambda * ?eps) * xstar -->
abs(R u) < ?eps * u))";
apply (insert x1K);
apply (drule_tac x = "?K powr (real j)" in spec);
apply (drule mp);
apply (erule jstar);
apply assumption;
done;
have "EX xstar. ALL j. ?jstar < j -->
?K powr (real j) < xstar j & (1 + lambda * ?eps) *
xstar j < ?K * (?K powr (real j)) & (ALL u.
xstar j <= u & u <= (1 + lambda * ?eps) * xstar j -->
abs(R u) < ?eps * u)";
apply (rule exI);
apply (clarify);
apply (drule xstar_aux);
apply (erule someI_ex);
done;
then obtain xstar where xstar: "ALL j. ?jstar < j -->
?K powr (real j) < xstar j & (1 + lambda * ?eps) *
xstar j < ?K * (?K powr (real j)) & (ALL u.
xstar j <= u & u <= (1 + lambda * ?eps) * xstar j -->
abs(R u) < ?eps * u)";..;
then have xstar0: "!!j u. ?jstar < j ==> xstar j <= u ==>
u <= (1 + lambda * ?eps) * xstar j ==>
abs (R u) < ?eps * u"; by blast;
from xstar have xstar1: "!!j. ?jstar < j ==> ?K powr (real j) < xstar j";
by blast;
have xstar1a: "!!j. ?jstar < j ==> 0 < xstar j";
apply (rule order_le_less_trans);
prefer 2;
apply (erule xstar1);
apply force;
done;
from xstar have xstar2: "!!j. ?jstar < j ==>
(1 + lambda * ?eps) * xstar j < ?K * (?K powr (real j))"; by blast;
have xstar2a: "!!j. ?jstar < j ==>
xstar j < ?K powr (real j + 1)";
apply (rule order_less_trans);
prefer 2;
apply (subgoal_tac "?K powr (real j + 1) =
?K * (?K powr (real j))");
apply (erule ssubst);
apply (erule xstar2);
apply (simp add: powr_add);
apply (subgoal_tac "1 * xstar j < ?t");
apply simp;
apply (rule mult_strict_right_mono);
apply simp;
apply (rule pos_div_pos);
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule alpha_gt_0);
apply (insert c2_gt_1, arith);
apply (erule xstar1a);
done;
have xstar2b: "!!j. ?jstar < j ==> j <= ?jhat ==>
xstar j < x powr (1 / 2)";
apply (rule order_less_le_trans);
apply (erule xstar2a);
apply (erule jhat);
done;
have xstar2c: "!!j. ?jstar < j ==> j <= ?jhat ==>
x powr (1 / 2) < x / xstar j";
apply (subst pos_less_divide_eq);
apply (erule xstar1a);
apply (subst mult_commute);
apply (subst pos_less_divide_eq [THEN sym]);
apply force;
apply (subgoal_tac "x = x powr 1");
apply (erule ssubst); back;back;
apply (subst powr_divide2);
apply simp;
apply (rule xstar2b);
apply force;
apply force;
apply (rule sym);
apply (subst powr_one_gt_zero_iff);
apply (insert x_gt_1, arith);
done;
from xstar have xstar3: "!!j. ?jstar < j ==> xstar j <= u ==>
u <= (1 + lambda * ?eps) * xstar j ==> abs(R u) < ?eps * u"; by blast;
have xstar4_aux: "!!j n. ?jstar < j ==> xstar j <= x / real (n::nat) ==>
0 < real n";
apply (subgoal_tac "~(n = 0)");
apply arith;
apply (rule notI);
apply (frule xstar1a);
apply simp;
done;
have xstar4: "!!j n. ?jstar < j ==> xstar j <= x / real (n::nat) ==>
real n <= x / xstar j";
apply (subst pos_le_divide_eq);
apply (erule xstar1a);
apply (subst mult_commute);
apply (subst pos_le_divide_eq [THEN sym]);
apply (erule xstar4_aux);
apply assumption+;
done;
have xstar5: "!!j n. ?jstar < j ==> xstar j <= x / real (n::nat) ==>
real n < x / (?K powr (real j))";
apply (rule order_le_less_trans);
apply (erule xstar4);
apply assumption;
apply (rule divide_strict_left_mono);
apply (erule xstar1);
apply (insert x_gt_1, arith);
apply (rule mult_pos);
apply (erule xstar1a);
apply force;
done;
have xstar6: "!!j n. ?jstar < j ==>
xstar j <= x / real (n::nat) ==>
x / real n <= (1 + lambda * ?eps) * xstar j ==>
x / ((1 + lambda * ?eps) * xstar j) <= real n";
apply (subst pos_divide_le_eq);
apply (rule mult_pos);
apply (rule pos_plus_pos);
apply force;
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule eps_gt_0);
apply (erule xstar1a);
apply (subst mult_commute);
apply (subst pos_divide_le_eq [THEN sym]);
apply (elim xstar4_aux);
apply assumption+;
done;
have xstar7: "!!j n. ?jstar < j ==>
xstar j <= x / real (n::nat) ==>
x / real n <= (1 + lambda * ?eps) * xstar j ==>
x / (?K * (?K powr (real j))) < real n";
apply (rule order_less_le_trans);
prefer 2;
apply (erule xstar6);
apply (force, force);
apply (rule divide_strict_left_mono);
apply (erule xstar2);
apply (insert x_gt_1, arith);
apply (rule mult_pos);
apply (rule mult_pos);
apply force;
apply force;
apply (rule mult_pos);
apply (rule pos_plus_pos);
apply force;
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule eps_gt_0);
apply (erule xstar1a);
done;
have xstar8: "!!i j n. ?jstar < i ==> i < j ==>
xstar i <= x / real (n::nat) ==>
x / real n <= (1 + lambda * ?eps) * xstar i ==>
xstar j <= x / real (n::nat) ==> False";
apply (subgoal_tac "real n < x / (?K powr (real j))");
apply (subgoal_tac "x / (?K * (?K powr (real i))) < real n");
apply (subgoal_tac "x / (?K powr (real j)) <=
x / (?K * (?K powr (real i)))");
apply arith;
apply (subgoal_tac "?K * (?K powr (real i)) = ?K powr (real (i + 1))");
apply (erule ssubst);
apply (rule real_pos_div_le_mono);
apply (rule powr_gt_zero);
apply (rule powr_mono);
apply arith;
apply (insert K_gt_1, simp);
apply (insert x_gt_1, arith);
apply (simp add: powr_add);
apply (rule xstar7);
apply force;
apply force;
apply force;
apply (rule xstar5);
apply force;
apply force;
done;
let ?S = "UN j:{?jstar + 1..?jhat}.
{n::nat. xstar j <= x / real n &
x / real n <= (1 + lambda * ?eps) * xstar j}";
show "EX S<={1..natfloor x}.
(ALL n:S. abs (R (x / real n)) <= alpha / c2 * (x / real n)) &
?C * alpha ^ 2 * ln x ^ 2
<= (∑n:S. ln (real n) / real n)";
proof;
show "?S <= {1..natfloor x} &
(ALL n:?S. abs (R (x / real n)) <= alpha / c2 * (x / real n)) &
?C * alpha ^ 2 * ln x ^ 2 <= (∑n:?S. ln (real n) / real n)";
proof;
show "?S <= {1..natfloor x}";
apply clarsimp;
apply (rule conjI);
apply (subgoal_tac "0 < real x");
apply arith;
apply (rule xstar4_aux);
prefer 2;
apply assumption;
apply force;
apply (rule real_le_natfloor);
apply (rule order_trans);
apply (rule order_less_imp_le);
apply (rule xstar5);
prefer 2;
apply assumption;
apply force;
apply (subst pos_divide_le_eq);
apply force;
apply (subgoal_tac "?x * 1 <= ?x * exp (c1 / (alpha / c2)) powr real j");
apply simp;
apply (rule mult_left_mono);
apply (rule ge_one_powr_ge_zero);
apply (subgoal_tac "exp 0 <= exp (c1 / ?eps)");
apply simp;
apply (subst exp_le_cancel_iff);
apply (rule real_ge_zero_div_gt_zero);
apply (insert c1_gt_1, arith);
apply (rule eps_gt_0);
apply simp;
apply (insert x_gt_1, arith);
done;
next show "(ALL n:?S. abs (R (x / real n)) <= alpha / c2 * (x / real n)) &
?C * alpha ^ 2 * ln x ^ 2 <= (∑n:?S. ln (real n) / real n)";
proof;
show "(ALL n:?S. abs (R (x / real n)) <= alpha / c2 * (x / real n))";
apply clarify;
apply (rule order_less_imp_le);
apply (rule xstar0);
prefer 2;
apply assumption;
apply force;
apply assumption;
done;
next show "?C * alpha ^ 2 * ln x ^ 2 <= (∑n:?S. ln (real n) / real n)";
proof -;
have "(∑ n: ?S. ln (real n) / real n) =
(∑ j:{?jstar + 1..?jhat}.
(∑ n::nat | xstar j <= x / real n &
x / real n <= (1 + lambda * ?eps) * xstar j.
ln (real n) / real n))";
apply (rule setsum_UN_disjoint);
apply simp;
apply clarsimp;
apply (rule bounded_nat_set_is_finite);
apply clarsimp;
apply (subgoal_tac "i < natfloor (x / xstar j) + 1");
apply assumption;
apply (subgoal_tac "i <= natfloor (x / xstar j)");
apply arith;
apply (rule real_le_natfloor);
apply (rule xstar4);
apply force;
apply force;
apply (clarsimp simp add: Int_def);
apply (subgoal_tac "ja < j | j < ja");
apply (erule disjE);
apply (rule xstar8);
prefer 2;
apply assumption;
apply force;
apply force;
apply force;
apply force;
apply (rule xstar8);
prefer 2;
apply assumption;
apply auto;
done;
also have "(∑ j:{?jstar + 1..?jhat}.
(∑ n::nat | xstar j <= x / real n &
x / real n <= (1 + lambda * ?eps) * xstar j.
ln (x / xstar j) / (x / xstar j))) <= ..." (is "?term1 <= ?temp");
apply (rule setsum_le_cong);
apply (rule setsum_le_cong);
apply (rule ln_x_over_x_mono);
apply clarsimp;
apply (rule order_trans);
prefer 2;
apply (rule order_less_imp_le);
apply (rule xstar7);
prefer 2;
apply force;
apply force;
apply force;
apply (rule order_trans);
apply (subgoal_tac "exp 1 <= ?x powr (1 / 2)");
apply assumption;
apply (subst ln_le_cancel_iff [THEN sym]);
apply simp;
apply simp;
apply (simp add: powr_def);
apply (subst exp_le_cancel_iff [THEN sym]);
apply (subgoal_tac "exp (ln ?x) = ?x");
apply (erule ssubst);
apply (rule order_less_imp_le);
apply (rule x_gt_exp2);
apply (subst exp_ln_iff);
apply (insert x_gt_1, arith);
apply (subst pos_le_divide_eq);
apply (rule mult_pos);
apply (force, force);
apply (subst mult_commute);
apply (subst pos_le_divide_eq [THEN sym]);
apply force;
apply (subgoal_tac "?x / ?x powr (1 / 2) = ?x powr (1 / 2)");
apply (erule ssubst);
apply (rule order_trans);
prefer 2;
apply (rule jhat);
apply (subgoal_tac "x <= ?t");
apply assumption;
apply force;
apply (simp add: powr_add);
apply (subst nonzero_divide_eq_eq);
apply simp;
apply (simp add: powr_add [THEN sym]);
apply clarsimp;
apply (rule xstar4);
apply auto;
done;
also have "?term1 = (∑ j:{?jstar + 1..?jhat}. real (card
{n::nat. xstar j <= x / real n &
x / real n <= (1 + lambda * ?eps) * xstar j}) *
(ln (x / xstar j) / (x / xstar j)))";
apply (rule setsum_cong2);
apply (subst setsum_constant);
apply (rule bounded_nat_set_is_finite);
apply clarsimp;
apply (subgoal_tac "i <= natfloor (?x / xstar x)");
prefer 2;
apply (rule real_le_natfloor);
apply (rule xstar4);
apply force;
apply arith;
apply (subgoal_tac "i < Suc (natfloor (?x / xstar x))");
apply assumption;
apply (erule le_imp_less_Suc);
apply (subst real_eq_of_nat [THEN sym]);
apply (rule refl);
done;
also; have "(∑ j:{?jstar + 1..?jhat}. real (card
{natfloor (x / ((1 + lambda * ?eps) * xstar j))+1..
natfloor (x / xstar j)}) *
(ln (x / xstar j) / (x / xstar j))) <= ..."
(is "?term2 <= ?temp");
apply (rule setsum_le_cong);
apply (rule mult_right_mono);
apply (rule le_imp_real_of_nat_le);
apply (rule card_mono);
apply (rule bounded_nat_set_is_finite);
apply clarsimp;
apply (subgoal_tac "i <= natfloor (?x / xstar x)");
prefer 2;
apply (rule real_le_natfloor);
apply (rule xstar4);
apply force;
apply arith;
apply (subgoal_tac "i < Suc (natfloor (?x / xstar x))");
apply assumption;
apply (erule le_imp_less_Suc);
apply auto;
apply (subst pos_le_divide_eq);
apply simp;
apply (subst mult_commute);
apply (subst pos_le_divide_eq [THEN sym]);
apply (rule xstar1a);
apply force;
apply (rule nat_le_natfloor);
apply (rule order_less_imp_le);
apply (rule pos_div_pos);
apply (insert x_gt_1, arith);
apply (rule xstar1a);
apply force;
apply assumption;
apply (subst pos_divide_le_eq);
apply simp;
apply (subst mult_commute);
apply (subst pos_divide_le_eq [THEN sym]);
apply (rule mult_pos);
apply (rule pos_plus_pos);
apply force;
apply (rule pos_div_pos);
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule alpha_gt_0);
apply (insert c2_gt_1, arith);
apply (rule xstar1a);
apply force;
apply (rule order_less_imp_le);
apply (erule ge_natfloor_plus_one_imp_gt);
apply (rule real_ge_zero_div_gt_zero);
apply (rule nonneg_times_nonneg);
apply (rule ln_ge_zero);
apply (rule order_trans);
prefer 2;
apply (rule order_less_imp_le);
apply (rule xstar2c);
apply (force, force);
apply (subgoal_tac "1 powr (1 / 2) <= ?x powr (1 / 2)");
apply (simp add: powr_one_eq_one);
apply (rule power_mono2);
apply (force, force);
apply (rule order_less_imp_le);
apply (rule x_gt_1);
apply (rule order_less_imp_le);
apply (rule xstar1a);
apply force;
apply force;
done;
also (order_trans2); have "?term2 = (∑ j:{?jstar + 1..?jhat}.
(real (natfloor (x / xstar j)) -
real (natfloor (x / ((1 + lambda * alpha / c2) * xstar j)))) *
(ln (x / xstar j) / (x / xstar j)))";
apply (rule setsum_cong2);
apply (simp add: natfloor_plus_one);
apply (subgoal_tac "Suc (natfloor (?x / xstar x)) -
(natfloor (?x / ((1 + lambda * alpha / c2) * xstar x)) +
1) = natfloor (?x / xstar x) -
natfloor (?x / ((1 + lambda * alpha / c2) * xstar x))");
apply (erule ssubst);
apply (subst real_of_nat_diff);
apply (rule natfloor_mono);
apply (rule real_pos_div_le_mono);
apply (rule xstar1a);
apply force;
apply (simp add: ring_eq_simps);
apply (rule order_less_imp_le);
apply (rule pos_div_pos);
apply (rule mult_pos);
apply (rule alpha_gt_0);
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule xstar1a);
apply (simp add: mult_ac);
apply arith;
apply (insert c2_gt_1, simp);
apply (insert x_gt_1, simp);
apply simp;
apply arith;
done;
also; have "(∑ j:{?jstar + 1..?jhat}.
((x / xstar j - 1) -
(x / ((1 + lambda * ?eps) * xstar j))) *
(ln (x / xstar j) / (x / xstar j))) <= ...";
apply (rule setsum_le_cong);
apply (rule mult_right_mono);
apply (rename_tac xa);
apply (subgoal_tac "real (natfloor (x / ((1 + lambda * alpha / c2) *
xstar xa))) <= x / ((1 + lambda * ?eps) * xstar xa)");
apply (subgoal_tac "x / xstar xa <= real (natfloor (x / xstar xa)) + 1");
apply arith;
apply (rule real_natfloor_plus_one_ge);
apply (rule nat_le_natfloor);
apply (rule order_less_imp_le);
apply (rule pos_div_pos);
apply (insert x_gt_1, simp);
apply (rule mult_pos);
apply (rule pos_plus_pos);
apply force;
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule eps_gt_0);
apply (rule xstar1a);
apply force;
apply simp;
apply (rule real_ge_zero_div_gt_zero);
apply (rule ln_ge_zero);
apply (rule order_trans);
prefer 2;
apply (rule order_less_imp_le);
apply (rule xstar2c);
apply (force, force);
apply (rename_tac xa);
apply (subgoal_tac "1 powr (1 / 2) <= x powr (1 / 2)");
apply (simp add: powr_one_eq_one);
apply (rule power_mono2);
apply (force, force);
apply (rule order_less_imp_le);
apply (rule x_gt_1);
apply (rule pos_div_pos);
apply force;
apply (rule xstar1a);
apply force;
done;
also (order_trans2) have "(∑ j:{?jstar + 1..?jhat}. ((x / xstar j - 1) -
(x / ((1 + lambda * ?eps) * xstar j))) *
(ln (x / xstar j) / (x / xstar j))) =
(∑ j:{?jstar + 1..?jhat}.
((1 - 1 / (1 + lambda * ?eps)) * (x / xstar j) - 1) *
(ln (x / xstar j) / (x / xstar j)))";
apply (rule setsum_cong2);
apply (simp add: ring_eq_simps);
done;
also have "(∑ j:{?jstar + 1..?jhat}.
(1 / 2) * (1 - 1 / (1 + lambda * ?eps)) * (x / xstar j) *
(ln (x / xstar j) / (x / xstar j))) <= ...";
apply (rule setsum_le_cong);
apply (rule mult_right_mono);
apply (subst mult_assoc);
apply (subst times_divide_eq_left);
apply (subst pos_divide_le_eq);
apply simp;
apply (subst mult_commute);
apply (subst right_diff_distrib);
apply (rename_tac xa);
apply (subgoal_tac "2 * 1 <=
2 * ((1 - 1 / (1 + lambda * (alpha / c2))) * (x / xstar xa)) -
1 * ((1 - 1 / (1 + lambda * (alpha / c2))) * (x / xstar xa))");
apply (simp only: compare_rls);
apply (subst left_diff_distrib [THEN sym]);
apply simp;
apply (subst times_divide_eq_right [THEN sym]);
apply (subst mult_commute);
apply (subst pos_divide_le_eq [THEN sym]);
apply simp;
apply (subst pos_divide_less_eq);
apply (rule pos_plus_pos);
apply force;
apply (rule pos_div_pos);
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule alpha_gt_0);
apply (insert c2_gt_1, arith);
apply simp;
apply (rule pos_div_pos);
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule alpha_gt_0);
apply (insert c2_gt_1, arith);
apply (rule order_trans);
prefer 2;
apply (rule order_less_imp_le);
apply (rule xstar2c);
apply force;
apply force;
apply (subgoal_tac "2 / (1 - 1 / (1 + lambda * alpha / c2)) =
((2 / (1 - 1 / (1 + lambda * alpha / c2))) powr 2) powr (1 / 2)");
apply (erule ssubst);
apply (rule power_mono2);
apply force;
apply force;
apply (subst times_divide_eq_right [THEN sym]);
apply (rule x_ge_blah);
apply (simp add: powr_powr);
apply (rule sym);
apply (subst powr_one_gt_zero_iff);
apply (rule pos_div_pos);
apply force;
apply simp;
apply (subst pos_divide_less_eq);
apply (rule pos_plus_pos);
apply force;
apply (rule pos_div_pos);
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule alpha_gt_0);
apply (insert c2_gt_1, arith);
apply simp;
apply (rule pos_div_pos);
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule alpha_gt_0);
apply (insert c2_gt_1, arith);
apply (rule real_ge_zero_div_gt_zero);
apply (rule ln_ge_zero);
apply (rule order_trans);
prefer 2;
apply (rule order_less_imp_le);
apply (rule xstar2c);
apply (force, force);
apply (subgoal_tac "1 powr (1 / 2) <= ?x powr (1 / 2)");
apply (simp add: powr_one_eq_one);
apply (rule power_mono2);
apply (force, force);
apply (rule order_less_imp_le);
apply (rule x_gt_1);
apply (rule pos_div_pos);
apply (insert x_gt_1, arith);
apply (rule xstar1a);
apply auto;
done;
also (order_trans2); have "(∑ j:{?jstar + 1..?jhat}.
(1 / 2) * (1 - 1 / (1 + lambda * ?eps)) * (x / xstar j) *
(ln (x / xstar j) / (x / xstar j))) =
(∑ j:{?jstar + 1..?jhat}.
(1 / 2) * (1 - 1 / (1 + lambda * ?eps)) * (ln (x / xstar j)))";
apply (rule setsum_cong2);
apply (rename_tac xa);
apply (subgoal_tac "x / xstar xa ~= 0");
apply simp;
apply (subgoal_tac "0 < x / xstar xa");
apply arith;
apply (rule pos_div_pos);
apply (insert x_gt_1, arith);
apply (rule xstar1a);
apply auto;
done;
also have "(∑ j:{?jstar + 1..?jhat}.
(1 / 2) * (1 - 1 / (1 + lambda * ?eps)) * (ln (x powr (1 / 2)))) <= ...";
apply (rule setsum_le_cong);
apply (rule mult_left_mono);
apply (subst ln_le_cancel_iff);
apply force;
apply (rule pos_div_pos);
apply (insert x_gt_1, arith);
apply (rule xstar1a);
apply force;
apply (rule order_less_imp_le);
apply (rule xstar2c);
apply force;
apply force;
apply (rule nonneg_times_nonneg);
apply force;
apply simp;
apply (subst pos_divide_le_eq);
apply (rule pos_plus_pos);
apply force;
apply (rule pos_div_pos);
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule alpha_gt_0);
apply (insert c2_gt_1, arith);
apply simp;
apply (rule order_less_imp_le);
apply (rule pos_div_pos);
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule alpha_gt_0);
apply (insert c2_gt_1, arith);
done;
also (order_trans2); have "(∑ j:{?jstar + 1..?jhat}.
(1 / 2) * (1 - 1 / (1 + lambda * ?eps)) * (ln (x powr (1 / 2)))) =
(∑ j:{?jstar + 1..?jhat}.
(1 / 4) * (1 - 1 / (1 + lambda * ?eps)) * (ln x))";
apply (rule setsum_cong2);
apply (subst ln_pwr);
apply (insert x_gt_1, arith);
apply force;
apply simp;
done;
also have "... = (1 / 4) * (1 - 1 / (1 + lambda * ?eps)) * (ln x) *
real (card({?jstar + 1..?jhat}))";
apply (subst setsum_constant);
apply force;
apply (subst real_eq_of_nat [THEN sym]);
apply (rule mult_commute);
done;
also have "... = (1 / 4) * (1 - 1 / (1 + lambda * ?eps)) * (ln x) *
(real (natfloor (ln x / (2 * ln ?K))) -
real (natfloor (ln x1 / ln ?K)) - 2)";
apply (rule arg_cong); back;
apply simp;
apply (subgoal_tac "Suc (natfloor (ln x * alpha / (2 * (c1 * c2))) - 1)
= natfloor (ln x * alpha / (2 * (c1 * c2)))");
apply (erule ssubst);
apply (subst real_of_nat_diff);
apply (subst add_assoc);
apply (subst natfloor_add [THEN sym]);
apply (rule real_ge_zero_div_gt_zero);
apply (rule nonneg_times_nonneg);
apply (rule ln_ge_zero);
apply (rule x1_ge_1);
apply (rule order_less_imp_le, rule alpha_gt_0);
apply (rule mult_pos);
apply (insert c1_gt_1, arith);
apply (insert c2_gt_1, arith);
apply (rule natfloor_mono);
apply simp;
apply (subst pos_le_divide_eq);
apply (rule mult_pos);
apply force;
apply (rule mult_pos);
apply arith;
apply arith;
apply (simp add: ring_eq_simps);
apply (subgoal_tac "alpha * ln x = ln x * alpha");
apply (erule ssubst);
apply (subst pos_divide_le_eq [THEN sym]);
apply (rule alpha_gt_0);
apply (subst exp_le_cancel_iff [THEN sym]);
apply (subgoal_tac "exp (ln x) = x");
apply (erule ssubst);
apply (rule x_ge_blah2);
apply (subst exp_ln_iff);
apply (insert x_gt_1, arith);
apply (rule mult_commute);
apply arith;
apply (subgoal_tac "1 <= natfloor (ln x * alpha / (2 * (c1 * c2)))");
apply arith;
apply (subgoal_tac "1 = natfloor 1");
apply (erule ssubst);
apply (rule natfloor_mono);
apply (subst pos_le_divide_eq);
apply simp;
apply (rule mult_pos);
apply (insert c1_gt_1, arith);
apply (insert c2_gt_1, arith);
apply simp;
apply (subst pos_divide_le_eq [THEN sym]);
apply (rule alpha_gt_0);
apply (subst exp_le_cancel_iff [THEN sym]);
apply (subgoal_tac "exp (ln x) = x");
apply (erule ssubst);
apply (rule x_ge_blah3);
apply (subst exp_ln_iff);
apply (insert x_gt_1, arith);
apply simp;
done;
also have "(1 / 4) * (lambda * ?eps / 2) * (ln x) *
((1 / 4) * (ln x / ln ?K)) <= ...";
apply (rule mult_mono);
apply (rule mult_right_mono);
apply (rule mult_left_mono);
apply (subgoal_tac "1 - 1 / (1 + lambda * ?eps) = lambda * ?eps /
(1 + lambda * ?eps)");
apply (erule ssubst);
apply (rule divide_left_mono);
apply (subgoal_tac "lambda * ?eps <= 1 * 1");
apply simp;
apply (rule mult_mono);
apply (rule order_less_imp_le, rule lambda_le_1);
apply (rule order_less_imp_le, rule eps_lt_1);
apply force;
apply (rule order_less_imp_le, rule eps_gt_0);
apply (rule order_less_imp_le);
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule eps_gt_0);
apply (rule mult_pos);
apply force;
apply (rule pos_plus_pos);
apply force;
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule eps_gt_0);
apply (rule lemma_divide_rearrange);
apply (rule less_imp_neq [THEN not_sym]);
apply (rule pos_plus_pos);
apply force;
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule eps_gt_0);
apply simp;
apply force;
apply (rule ln_ge_zero);
apply (insert x_gt_1, arith);
apply (rule order_trans);
apply (subgoal_tac "1 / 4 * (ln x / ln (exp (c1 / (alpha / c2)))) <=
((ln x / (2 * ln ?K)) - (ln x1 / ln ?K) - 3)");
apply assumption;
prefer 2;
apply (subgoal_tac "(ln x / (2 * ln ?K)) <=
real (natfloor (ln x / (2 * ln ?K))) + 1");
apply (subgoal_tac "real (natfloor (ln x1 / ln ?K)) <=
(ln x1 / ln ?K)");
apply arith;
apply (rule real_natfloor_le);
apply simp;
apply (rule real_ge_zero_div_gt_zero);
apply (rule nonneg_times_nonneg);
apply (rule ln_ge_zero);
apply (rule x1_ge_1);
apply (rule order_less_imp_le);
apply (rule alpha_gt_0);
apply (rule mult_pos);
apply (insert c1_gt_1, arith);
apply (insert c2_gt_1, arith);
apply (rule real_natfloor_plus_one_ge);
prefer 2;
apply (rule nonneg_times_nonneg);
apply (rule nonneg_times_nonneg);
apply force;
apply simp;
apply (subst pos_divide_le_eq);
apply (rule pos_plus_pos);
apply force;
apply (rule pos_div_pos);
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule alpha_gt_0)
apply (insert c2_gt_1, arith)
apply simp;
apply (rule order_less_imp_le);
apply (rule pos_div_pos);
apply (rule mult_pos);
apply (rule lambda_gt_0);
apply (rule alpha_gt_0);
apply arith;
apply (rule ln_ge_zero);
apply (rule order_less_imp_le);
apply (rule x_gt_1);
apply (simp only: diff_minus);
apply (subgoal_tac "1 / 4 = 1 / 2 + - (1 / 8) + - (1 / 8)");
apply (erule ssubst);
apply (subst left_distrib);
apply (subst left_distrib);
apply (rule add_mono);
apply (rule add_mono);
apply simp;
apply (simp add: compare_rls);
apply (subst times_divide_eq_right [THEN sym]);
apply (subst pos_divide_le_eq [THEN sym]);
apply (rule pos_div_pos);
apply (rule alpha_gt_0);
apply (rule mult_pos);
apply force;
apply (rule mult_pos);
apply arith;
apply arith;
apply (subgoal_tac "alpha ~= 0");
apply simp;
apply (subst mult_commute);
apply (subst ln_pwr [THEN sym]);
apply (insert x1_ge_1, arith);
apply force;
apply (subst ln_le_cancel_iff);
apply force;
apply (insert x_gt_1, force);
apply (rule x_ge_blah4);
apply (rule less_imp_neq [THEN not_sym]);
apply (rule alpha_gt_0);
apply (simp add: compare_rls);
apply (subst times_divide_eq_right [THEN sym]);
apply (subst pos_divide_le_eq [THEN sym]);
apply (rule pos_div_pos);
apply (rule alpha_gt_0);
apply (rule mult_pos);
apply force;
apply (rule mult_pos);
apply arith;
apply arith;
apply (subst exp_le_cancel_iff [THEN sym]);
apply (subgoal_tac "exp (ln x) = x");
apply (erule ssubst);
apply (rule x_ge_blah5);
apply (subst exp_ln_iff);
apply arith;
apply simp;
apply simp;
apply (rule real_ge_zero_div_gt_zero);
apply (rule nonneg_times_nonneg);
apply (rule ln_ge_zero);
apply arith;
apply (rule order_less_imp_le);
apply (rule alpha_gt_0);
apply (rule mult_pos);
apply force;
apply (rule mult_pos);
apply arith;
apply arith;
done;
also (order_trans2) have "(1 / 4) * (lambda * ?eps / 2) * (ln x) *
((1 / 4) * (ln x / ln ?K)) =
(lambda * alpha^2 * (ln x)^2) / (32 * c1 * c2^2)";
by (simp add: mult_ac power2_eq_square);
finally; show "lambda / (32 * c1 * c2 ^ 2) * alpha ^ 2 * ln x ^ 2 <=
(∑ n:?S. ln (real n) / real n)";
by (simp add: ring_eq_simps);
qed;qed;qed;qed;qed;qed;qed;qed;qed;
lemma PNT4: "1 < (c2::real) ==> EX C. 0 < C & (ALL alpha1 x1. 0 < alpha1 -->
alpha1 < c2 --> (ALL x. x1 <= x --> abs (R x) <= alpha1 * x) -->
(EX x2. (ALL x. x2 <= x --> abs (R x) <= (alpha1 - C * alpha1^3) * x)))";
proof -;
assume c2_gt_1: "1 < (c2::real)";
have "EX C. 0 < C & (ALL alpha.
0 < alpha --> alpha < c2 -->
(EX xlarge. ALL x. xlarge <= x -->
(EX S. S <= {1..natfloor x} &
(ALL n:S. abs(R(x / real n)) <= (alpha / c2) * (x / real n)) &
C * alpha^2 * (ln x)^2
<= (∑ n:S. ln(real n) / (real n)))))";
apply (rule PNT4_aux1);
apply (rule prems);
done;
then obtain C where C_gt_0: "0 < C" and C': "(ALL alpha.
0 < alpha --> alpha < c2 -->
(EX xlarge. ALL x. xlarge <= x -->
(EX S. S <= {1..natfloor x} &
(ALL n:S. abs(R(x / real n)) <= (alpha / c2) * (x / real n)) &
C * alpha^2 * (ln x)^2
<= (∑ n:S. ln(real n) / (real n)))))"; by blast;
from PNT3 obtain G where G: "ALL x x2 S eps alpha.
0 < eps --> 0 < alpha --> alpha < c2 -->
2 <= x2 --> exp 1 <= x2 --> x2 <= x -->
(ALL x. x2 <= x --> abs(R x) <= alpha * x) -->
S <= {1..natfloor x} -->
(ALL n:S. abs(R(x / real n)) <= eps * (x / real n)) -->
abs (R x)
<= alpha * x -
2 * (alpha - eps) * x *
(∑n:S. ln (real n) / real n) / ln x ^ 2 +
G * x * ln x2 / ln x";..;
let ?C = "(1 - 1 / c2) * C";
show ?thesis;
proof;
show "0 < ?C & (ALL alpha1 x1. 0 < alpha1 -->
alpha1 < c2 --> (ALL x. x1 <= x --> abs (R x) <= alpha1 * x) -->
(EX x2. (ALL x. x2 <= x --> abs (R x) <= (alpha1 - ?C * alpha1^3) * x)))";
proof;
show "0 < ?C";
apply (rule mult_pos);
apply simp;
apply (subst pos_divide_less_eq);
apply (insert c2_gt_1, arith);
apply simp;
apply (rule C_gt_0);
done;
next show "(ALL alpha1 x1. 0 < alpha1 -->
alpha1 < c2 --> (ALL x. x1 <= x --> abs (R x) <= alpha1 * x) -->
(EX x2. (ALL x. x2 <= x --> abs (R x) <= (alpha1 - ?C * alpha1^3) * x)))";
proof (clarify);
fix alpha1::"real";
fix x1::"real";
assume alpha1_gt_0: "0 < alpha1"
assume alpha1_lt_c2: "alpha1 < c2";
assume x1_good: "ALL x. x1 <= x --> abs (R x) <= alpha1 * x";
have "EX xlarge. ALL x. xlarge <= x -->
(EX S. S <= {1..natfloor x} &
(ALL n:S. abs(R(x / real n)) <= (alpha1 / c2) * (x / real n)) &
C * alpha1^2 * (ln x)^2
<= (∑ n:S. ln(real n) / (real n)))";
by (insert C' alpha1_gt_0 alpha1_lt_c2, blast);
then obtain xlarge where xlarge: "ALL x. xlarge <= x -->
(EX S. S <= {1..natfloor x} &
(ALL n:S. abs(R(x / real n)) <= (alpha1 / c2) * (x / real n)) &
C * alpha1^2 * (ln x)^2
<= (∑ n:S. ln(real n) / (real n)))";..;
let ?x1' = "max x1 (max 2 (exp 1))";
have x1prime_ge_x1: "x1 <= ?x1'"; by arith;
have x1prime_ge_2: "2 <= ?x1'"; by arith;
have x1prime_ge_exp1: "exp 1 <= ?x1'"; by arith;
let ?messy_term = "exp (G * ln ?x1' /
(C * ((1 - 1 / c2) * alpha1 ^ 3)))";
let ?x2 = "max xlarge (max (max (max 2 (exp 1)) ?x1') ?messy_term)";
show "EX x2. ALL x. x2 <= x --> abs (R x) <= (alpha1 - ?C * alpha1 ^ 3) * x";
proof;
show "ALL x. ?x2 <= x --> abs (R x) <= (alpha1 - ?C * alpha1 ^ 3) * x";
proof (clarify);
fix x::"real";
assume x_ge_x2: "?x2 <= x";
have x_ge_xlarge: "xlarge <= x";
apply (rule order_trans);
prefer 2;
apply (rule x_ge_x2);
apply (rule le_maxI1);
done;
have x2_ge_2: "2 <= ?x2";
by arith;
have x2_ge_exp1: "exp 1 <= ?x2";
by arith;
have x2_ge_x1: "x1 <= ?x2";
by arith;
have x2_ge_x1prime: "?x1' <= ?x2";
apply auto;
apply arith;
apply arith;
apply arith;
done;
have messy_term: "?messy_term <= ?x2";
apply arith;
done;
have "EX S. S <= {1..natfloor x} &
(ALL n:S. abs(R(x / real n)) <= (alpha1 / c2) * (x / real n)) &
C * alpha1^2 * (ln x)^2
<= (∑ n:S. ln(real n) / (real n))";
apply (insert xlarge);
apply (drule_tac x = x in spec);
apply (insert x_ge_xlarge);
apply clarify;
done;
then obtain S where S1: "S <= {1..natfloor x}" and
S2: "(ALL n:S. abs(R(x / real n)) <= (alpha1 / c2) * (x / real n))" and
S3: "C * alpha1^2 * (ln x)^2 <= (∑ n:S. ln(real n) / (real n))";
by blast;
have "abs (R x) <= alpha1 * x -
2 * (alpha1 - alpha1 / c2) * x *
(∑n:S. ln (real n) / real n) / ln x ^ 2 +
G * x * ln ?x1' / ln x";
apply (insert G);
apply (drule_tac x = x in spec);
apply (drule_tac x = ?x1' in spec);
apply (drule_tac x = S in spec);
apply (drule_tac x = "(alpha1 / c2)" in spec);
apply (drule_tac x = alpha1 in spec);
apply (drule mp);
apply (rule pos_div_pos);
apply (rule alpha1_gt_0);
apply (insert c2_gt_1, arith);
apply (drule mp);
apply (rule alpha1_gt_0);
apply (drule mp);
apply (rule alpha1_lt_c2);
apply (drule mp);
apply (rule x1prime_ge_2);
apply (drule mp);
apply (rule x1prime_ge_exp1);
apply (drule mp);
apply (rule order_trans);
apply (rule x2_ge_x1prime);
apply (rule x_ge_x2);
apply (drule mp);
apply (rule allI);
apply (rename_tac xa);
apply (rule impI);
apply (insert x1_good);
apply (drule_tac x = xa in spec);
apply (drule mp);
apply arith;
apply assumption;
apply (drule mp);
apply (rule S1);
apply (drule mp);
apply (rule S2);
apply assumption;
done;
also have "... <= alpha1 * x -
2 * (alpha1 - alpha1 / c2) * x *
(C * alpha1 ^ 2 * ln x ^ 2) / ln x ^ 2 +
G * x * ln (?x1') / ln x";
apply (subst diff_minus)+;
apply (rule add_right_mono);
apply (rule add_left_mono);
apply (rule le_imp_neg_le);
apply (rule real_div_pos_le_mono);
apply (rule mult_left_mono);
apply (rule S3);
apply (rule nonneg_times_nonneg);
apply (rule nonneg_times_nonneg);
apply force;
apply simp;
apply (subst pos_divide_le_eq);
apply (insert c2_gt_1, arith);
apply (subgoal_tac "alpha1 * 1 <= alpha1 * c2");
apply simp;
apply (rule mult_left_mono);
apply (erule order_less_imp_le);
apply (insert alpha1_gt_0, arith);
apply (insert x_ge_x2 x2_ge_2, arith);
apply force;
done;
also have "... = x * (alpha1 - 2 * alpha1^3 * (1 - 1 / c2) * C +
(G * ln ?x1' / ln x))";
apply (subgoal_tac "ln x ~= 0");
apply (simp add: ring_eq_simps power3_eq_cube power2_eq_square
add_divide_distrib diff_divide_distrib);
apply (rule less_imp_neq [THEN not_sym]);
apply (rule ln_gt_zero);
apply (insert x_ge_x2 x2_ge_2, arith);
done;
also have "... <= x * (alpha1 - 2 * alpha1^3 * (1 - 1 / c2) * C +
alpha1^3 * (1 - 1 / c2) * C)";
apply (rule mult_left_mono);
apply simp;
apply (subst pos_divide_le_eq);
apply (rule ln_gt_zero);
apply (insert x_ge_x2 x2_ge_2, arith);
apply (subst mult_commute);
apply (subst pos_divide_le_eq [THEN sym]);
apply (rule mult_pos);
apply (rule C_gt_0);
apply (rule mult_pos);
apply simp;
apply (subst pos_divide_less_eq);
apply (insert c2_gt_1, arith);
apply simp;
apply (subst power3_eq_cube);
apply (rule mult_pos);
apply (rule mult_pos);
apply (rule alpha1_gt_0)+;
apply (subst exp_le_cancel_iff [THEN sym]);
apply (subgoal_tac "exp (ln x) = x");
apply (erule ssubst);
apply (rule order_trans);
apply (rule messy_term);
apply (rule x_ge_x2);
apply (subst exp_ln_iff);
apply (insert x_ge_x2 x2_ge_2, arith);
apply arith;
done;
also have "... = x * (alpha1 - alpha1 ^ 3 * (1 - 1 / c2) * C)";
by simp;
finally show "abs (R x) <= (alpha1 - (1 - 1 / c2) * C * alpha1 ^ 3) * x";
by (simp add: ring_eq_simps);
qed;qed;qed;qed;qed;qed;
constdefs
PNT_alpha0::"real"
"PNT_alpha0 == (SOME C. 0 < C & (ALL x. 0 <= x --> abs (R x) <= C * x))";
lemma PNT_alpha0: "0 < PNT_alpha0 &
(ALL x. 0 <= x --> abs (R x) <= PNT_alpha0 * x)";
apply (unfold PNT_alpha0_def);
apply (rule someI_ex);
apply (rule PNT3_aux2a);
done;
constdefs
PNT_C::"real"
"PNT_C == SOME C. 0 < C & (ALL alpha1 x1. 0 < alpha1 -->
alpha1 < max (PNT_alpha0 + 1) 2 -->
(ALL x. x1 <= x --> abs (R x) <= alpha1 * x) -->
(EX x2. (ALL x. x2 <= x --> abs (R x) <= (alpha1 - C * alpha1^3) * x)))";
lemma PNT_C: "0 < PNT_C & (ALL alpha1 x1. 0 < alpha1 -->
alpha1 < max (PNT_alpha0 + 1) 2 -->
(ALL x. x1 <= x --> abs (R x) <= alpha1 * x) -->
(EX x2. (ALL x. x2 <= x --> abs (R x) <=
(alpha1 - PNT_C * alpha1^3) * x)))";
apply (unfold PNT_C_def);
apply (rule someI_ex);
apply (rule PNT4);
apply arith;
done;
consts
PNT_alpha :: "nat => real"
primrec
PNT_alpha_0: "PNT_alpha 0 = PNT_alpha0"
PNT_alpha_Suc: "PNT_alpha (Suc n) = PNT_alpha n - PNT_C * (PNT_alpha n)^3";
lemma PNT5_aux1: "0 <= PNT_alpha n & PNT_alpha (Suc n) <= PNT_alpha n &
PNT_alpha n < max (PNT_alpha0 + 1) 2 &
(EX x2. (ALL x. x2 <= x --> abs (R x) <=
PNT_alpha n * x))";
apply (induct_tac n);
apply (rule conjI);
apply (rule order_less_imp_le);
apply (force simp add: PNT_alpha0);
apply (rule conjI);
apply simp;
apply (rule nonneg_times_nonneg);
apply (rule order_less_imp_le);
apply (force simp add: PNT_C);
apply (subgoal_tac "0 <= PNT_alpha0");
apply (subst power3_eq_cube);
apply (rule nonneg_times_nonneg)+;
apply assumption+;
apply (rule order_less_imp_le);
apply (force simp add: PNT_alpha0);
apply (rule conjI);
apply (rule order_less_le_trans);
prefer 2;
apply (rule le_maxI1);
apply simp;
apply (rule_tac x = 1 in exI);
apply simp;
apply (force simp add: PNT_alpha0);
apply (subgoal_tac "(EX x2. ALL x. x2 <= x -->
abs (R x) <= PNT_alpha (Suc n) * x)");
apply (subgoal_tac "0 <= PNT_alpha (Suc n)");
apply (rule conjI);
apply assumption;
apply (rule conjI);
apply (subst PNT_alpha_Suc);back;
apply (simp del: PNT_alpha_Suc);
apply (rule nonneg_times_nonneg);
apply (rule order_less_imp_le);
apply (force simp add: PNT_C);
apply (subst power3_eq_cube);
apply (rule nonneg_times_nonneg)+;
apply assumption+;
apply (rule conjI);
apply (rule order_le_less_trans);
apply clarify;
apply assumption;
apply force;
apply assumption;
apply clarify;
apply (drule_tac x = "max x2 1" in spec);
apply (drule mp);
apply arith;
apply (rule order_trans);
apply (subgoal_tac "0 <= abs (R (max x2 1)) / (max x2 1)");
apply assumption;back;
apply (rule real_ge_zero_div_gt_zero);
apply force;
apply arith;
apply (subst pos_divide_le_eq);
apply arith;
apply assumption;
apply simp;
apply (case_tac "PNT_alpha n = 0");
apply clarify;
apply (simp add: power3_eq_cube);
apply (rule_tac x = x2 in exI);
apply assumption;
apply (insert PNT_C);
apply clarify;
apply (drule_tac x = "PNT_alpha n" in spec);
apply (drule_tac x = x2 in spec);back;
apply (subgoal_tac "0 < PNT_alpha n");
apply clarify;
apply arith;
done;
lemma PNT5_aux2: "convergent PNT_alpha";
apply (rule Bseq_monoseq_convergent);
apply (unfold Bseq_def);
apply (insert PNT5_aux1);
apply (rule_tac x = "max (PNT_alpha0 + 1) 2" in exI);
apply (rule conjI);
apply arith;
apply (rule allI);
apply (subst abs_nonneg);
apply force;
apply (rule order_less_imp_le);
apply force;
apply (subst monoseq_Suc);
apply (rule disjI2);
apply force;
done;
lemma PNT5_aux3: "EX L. PNT_alpha ----> L";
apply (insert PNT5_aux2);
apply (unfold convergent_def);
apply assumption;
done;
lemma PNT5_aux4: "PNT_alpha ----> L ==> L = 0";
proof -;
assume a: "PNT_alpha ----> L";
then have b: "(%n. PNT_alpha (Suc n)) ----> L";
by (rule LIMSEQ_Suc);
have c: "(%n. PNT_alpha n -
PNT_C * PNT_alpha n * PNT_alpha n * PNT_alpha n) ---->
L - PNT_C * L * L * L";
apply (rule LIMSEQ_diff);
apply (rule a);
apply (rule LIMSEQ_mult)+;
apply (rule LIMSEQ_const);
apply (rule a)+;
done;
also have "(%n. PNT_alpha n -
PNT_C * PNT_alpha n * PNT_alpha n * PNT_alpha n) =
(%n. PNT_alpha (Suc n))";
by (rule ext, simp add: power3_eq_cube mult_ac);
finally have c: "(%n. PNT_alpha (Suc n)) ----> L - PNT_C * L * L * L";.;
then have "L - PNT_C * L * L * L = L";
apply (rule LIMSEQ_unique);
apply (rule b);
done;
then show "L = 0";
apply (subgoal_tac "PNT_C ~= 0");
apply simp;
apply (rule less_imp_neq [THEN not_sym]);
apply (insert PNT_C, force);
done;
qed;
lemma PNT5_aux5: "PNT_alpha ----> 0";
by (insert PNT5_aux3 PNT5_aux4, auto);
lemma PNT5: "ALL eps. (0 < eps -->
(EX z. ALL x. (z <= x --> abs (R x) < eps * x)))";
proof (clarify);
fix eps::"real";
assume "0 < eps";
have "EX n. PNT_alpha n < eps";
apply (insert PNT5_aux5);
apply (unfold LIMSEQ_def);
apply (drule_tac x = eps in spec);
apply (insert prems, clarify);
apply (rule_tac x = no in exI);
apply (drule_tac x = no in spec);
apply (subgoal_tac "abs(PNT_alpha no) = PNT_alpha no");
apply auto;
apply (rule abs_nonneg);
apply (insert PNT5_aux1, force);
done;
then obtain n where n: "PNT_alpha n < eps";..;
have "EX z. (ALL x. z <= x --> abs (R x) <=
PNT_alpha n * x)";
by (insert PNT5_aux1, force);
thus "EX z. ALL x. (z <= x --> abs (R x) < eps * x)";
apply clarify;
apply (rule_tac x = "max z 1" in exI);
apply clarify;
apply (drule_tac x = x in spec);
apply (subgoal_tac "z <= x");
apply clarify;
apply (erule order_le_less_trans);
apply (rule mult_strict_right_mono);
apply (rule n);
apply arith;
apply arith;
done;
qed;
lemma PrimeNumberTheorem1: "(%x. psi x / (real x)) ----> 1";
apply (rule R_bound_imp_PNT);
apply (rule PNT5);
done;
lemma PrimeNumberTheorem2: "(%x. theta x / (real x)) ----> 1";
apply (rule psi_theta_lim4);
apply (rule PrimeNumberTheorem1);
done;
lemma PrimeNumberTheorem: "(%x. pi x * ln (real x) / (real x)) ----> 1";
apply (rule theta_limit_imp_pi_limit);
apply (rule PrimeNumberTheorem2);
done;
end;
lemma PNT1_aux1:
[| 0 < C; 0 ≤ D |] ==> ∃C0. ∀eps. 0 < eps --> eps < 1 --> (∀K. exp (C0 / eps) < K --> 2 < K ∧ D < ln K ∧ C / (ln K - D) < eps)
lemma PNT1_aux2:
∃C. ∀x. ¦ln (¦x¦ + 1) - (∑i = 1..natfloor ¦x¦ + 1. 1 / real i)¦ < C
lemma PNT1_aux3:
∃C. ∀x. 1 ≤ x --> ¦ln x - (∑i = 1..natfloor x. 1 / real i)¦ < C
lemma PNT1_aux4:
∃C. ∀x. 1 ≤ x --> ¦ln x - (∑i = 1..natfloor x. 1 / real (i + 1))¦ < C
lemma PNT1_aux5:
∃D. ∀x K. 1 ≤ x --> 1 ≤ K --> ¦ln K - (∑n | natfloor x < n ∧ n ≤ natfloor (K * x). 1 / real (n + 1))¦ ≤ D
lemma PNT1_aux6:
∃D. ∀x K. 1 ≤ x --> 1 ≤ K --> ln K - D ≤ (∑n | natfloor x < n ∧ n ≤ natfloor (K * x). 1 / real (n + 1))
lemma PNT1_aux7:
0 < C ==> ∃C0. ∀eps. 0 < eps --> eps < 1 --> (∀K x. 1 ≤ x --> exp (C0 / eps) < K --> 2 < K ∧ C / (∑n | natfloor x < n ∧ n ≤ natfloor (K * x). 1 / real (n + 1)) < eps)
lemma PNT1_aux8:
(0 ≤ x) ≠ (0 ≤ y) ==> ¦x¦ ≤ ¦y - x¦
lemma PNT1_aux9:
∀k<j. (0 ≤ f (i + k)) = (0 ≤ f (i + (k + 1))) ==> (∀k≤j. 0 ≤ f (i + k)) ∨ (∀k≤j. f (i + k) < 0)
lemma PNT1_aux10:
[| i ≤ j; ∀n. i < n ∧ n ≤ j --> (0 ≤ f n) = (0 ≤ f (n + 1)) |] ==> (∀n. i < n ∧ n ≤ j --> 0 ≤ f n) ∨ (∀n. i < n ∧ n ≤ j --> f n < 0)
lemma PNT1_aux11:
∃C. ∀i. 1 ≤ i --> ¦∑n = 1..i. R (real n) / (real n * real (n + 1))¦ ≤ C
lemma PNT1_aux12:
∃C. ∀i j. 1 ≤ i --> i ≤ j --> ¦∑n | i < n ∧ n ≤ j. R (real n) / (real n * real (n + 1))¦ < C
lemma PNT1:
∃C0. ∀eps. 0 < eps --> eps < 1 --> (∃x0. ∀K x. exp (C0 / eps) < K --> x0 < x --> (∃n. natfloor x < n ∧ n ≤ natfloor (K * x) ∧ ¦R (real n) / real n¦ < eps))
lemma PNT1a:
∃C0. ∀eps. 0 < eps --> eps < 1 --> (∃x0. ∀K x. exp (C0 / eps) < K --> x0 < x --> (∃n. x < real n ∧ real n ≤ K * x ∧ ¦R (real n) / real n¦ < eps))
lemma PNT2_aux1:
∃C. ∀x. 1 ≤ x --> ¦psi (natfloor x) * ln x + (∑d = 1..natfloor x. Lambda d * psi (natfloor x div d)) - 2 * x * ln x¦ ≤ C * x
lemma PNT2_aux2:
∃C. ∀x y. 1 ≤ y --> y ≤ x --> psi (natfloor x) * ln x - psi (natfloor y) * ln y ≤ 2 * x * ln x - 2 * y * ln y + C * x
lemma PNT2_aux3:
∃E. ∀x y. 1 ≤ y --> y < x --> x ≤ D * y --> psi (natfloor x) - psi (natfloor y) ≤ 2 * (x - y) + E * (x / ln x)
lemma PNT2_aux4:
∃C. ∀x. ¦R x / x¦ < C
lemma PNT2_aux5:
0 < eps ==> ∃x. ∀y. x < y --> 1 / ln y < eps
lemma PNT2:
∃lambda C1. 0 < lambda ∧ lambda < 1 ∧ (∀eps. 0 < eps --> eps < 1 --> (∃x1. ∀K x. exp (C1 / eps) < K --> x1 < x --> (∃xstar. x < xstar ∧ (1 + lambda * eps) * xstar < K * x ∧ (∀u. xstar ≤ u ∧ u ≤ (1 + lambda * eps) * xstar --> ¦R u¦ < eps * u))))
lemma PNT2a:
∃lambda C1. 0 < lambda ∧ lambda < 1 ∧ 1 ≤ C1 ∧ (∀eps. 0 < eps --> eps < 1 --> (∃x1. 1 ≤ x1 ∧ (∀K x. exp (C1 / eps) ≤ K --> x1 ≤ x --> (∃xstar. x < xstar ∧ (1 + lambda * eps) * xstar < K * x ∧ (∀u. xstar ≤ u ∧ u ≤ (1 + lambda * eps) * xstar --> ¦R u¦ < eps * u)))))
lemma PNT3_aux1:
∃C. ∀x. 1 ≤ x --> ¦R x¦ * (ln x)² ≤ 2 * (∑n = 1..natfloor x. ¦R (x / real n)¦ * ln (real n)) + C * ¦x * (1 + ln x)¦
lemma PNT3_aux1a:
∃C. 0 ≤ C ∧ (∀x. 2 ≤ x --> ¦R x¦ * (ln x)² ≤ 2 * (∑n = 1..natfloor x. ¦R (x / real n)¦ * ln (real n)) + C * x * ln x)
lemma PNT3_aux2:
∃C. ∀x. 0 ≤ x --> ¦R x¦ ≤ C * x
lemma PNT3_aux2a:
∃C. 0 < C ∧ (∀x. 0 ≤ x --> ¦R x¦ ≤ C * x)
lemma PNT3_aux3:
∃C. ∀x. 1 ≤ x --> ¦(∑i = 1..natfloor x. ln (real i) / real i) - (ln x)² / 2¦ ≤ C
lemma PNT3_aux4:
∃C. ∀x x2. 1 ≤ x2 --> x2 ≤ x --> (∑n = natfloor (x / x2) + 1..natfloor x. ln (real n) / real n) ≤ ln x2 * ln x + C
lemma PNT3_aux5:
∃C. 0 ≤ C ∧ (∀x. 1 ≤ x --> (∑i = 1..natfloor x. ln (real i) / real i) ≤ (ln x)² / 2 + C)
lemma PNT3:
∃G. ∀x x2 S eps alpha. 0 < eps --> 0 < alpha --> alpha < c --> 2 ≤ x2 --> exp 1 ≤ x2 --> x2 ≤ x --> (∀x. x2 ≤ x --> ¦R x¦ ≤ alpha * x) --> S ⊆ {1..natfloor x} --> (∀n∈S. ¦R (x / real n)¦ ≤ eps * (x / real n)) --> ¦R x¦ ≤ alpha * x - 2 * (alpha - eps) * x * (∑n∈S. ln (real n) / real n) / (ln x)² + G * x * ln x2 / ln x
lemma PNT4_aux1:
1 < c2 ==> ∃C. 0 < C ∧ (∀alpha. 0 < alpha --> alpha < c2 --> (∃xlarge. ∀x. xlarge ≤ x --> (∃S≤{1..natfloor x}. (∀n∈S. ¦R (x / real n)¦ ≤ alpha / c2 * (x / real n)) ∧ C * alpha² * (ln x)² ≤ (∑n∈S. ln (real n) / real n))))
lemma PNT4:
1 < c2 ==> ∃C. 0 < C ∧ (∀alpha1 x1. 0 < alpha1 --> alpha1 < c2 --> (∀x. x1 ≤ x --> ¦R x¦ ≤ alpha1 * x) --> (∃x2. ∀x. x2 ≤ x --> ¦R x¦ ≤ (alpha1 - C * alpha1 ^ 3) * x))
lemma PNT_alpha0:
0 < PNT_alpha0 ∧ (∀x. 0 ≤ x --> ¦R x¦ ≤ PNT_alpha0 * x)
lemma PNT_C:
0 < PNT_C ∧ (∀alpha1 x1. 0 < alpha1 --> alpha1 < max (PNT_alpha0 + 1) 2 --> (∀x. x1 ≤ x --> ¦R x¦ ≤ alpha1 * x) --> (∃x2. ∀x. x2 ≤ x --> ¦R x¦ ≤ (alpha1 - PNT_C * alpha1 ^ 3) * x))
lemma PNT5_aux1:
0 ≤ PNT_alpha n ∧ PNT_alpha (Suc n) ≤ PNT_alpha n ∧ PNT_alpha n < max (PNT_alpha0 + 1) 2 ∧ (∃x2. ∀x. x2 ≤ x --> ¦R x¦ ≤ PNT_alpha n * x)
lemma PNT5_aux2:
convergent PNT_alpha
lemma PNT5_aux3:
∃L. PNT_alpha ----> L
lemma PNT5_aux4:
PNT_alpha ----> L ==> L = 0
lemma PNT5_aux5:
PNT_alpha ----> 0
lemma PNT5:
∀eps. 0 < eps --> (∃z. ∀x. z ≤ x --> ¦R x¦ < eps * x)
lemma PrimeNumberTheorem1:
(%x. psi x / real x) ----> 1
lemma PrimeNumberTheorem2:
(%x. theta x / real x) ----> 1
lemma PrimeNumberTheorem:
(%x. Chebyshev1.pi x * ln (real x) / real x) ----> 1