X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fchebyshev.ma;h=ff7db61cc241eaeaebcd241f06ceceafecb08ceb;hb=063523ae5f8da7e6458232f4afb6744ec86dc8bd;hp=2a3695e8e99c401322e4491248d62c6442c4d7ef;hpb=9edc9828ff3c3d074ccc5547a53eadf092c186d8;p=helm.git diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma index 2a3695e8e..ff7db61cc 100644 --- a/helm/software/matita/library/nat/chebyshev.ma +++ b/helm/software/matita/library/nat/chebyshev.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/chebishev". - include "nat/log.ma". include "nat/pi_p.ma". include "nat/factorization.ma". @@ -22,7 +20,204 @@ include "nat/factorial2.ma". definition prim: nat \to nat \def \lambda n. sigma_p (S n) primeb (\lambda p.(S O)). -(* This is chebishev psi funcion *) +theorem le_prim_n: \forall n. prim n \le n. +intros.unfold prim. elim n + [apply le_n + |apply (bool_elim ? (primeb (S n1)));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > sym_plus. + rewrite < plus_n_Sm. + rewrite < plus_n_O. + apply le_S_S.assumption + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [apply le_S.assumption + |assumption + ] + ] + ] +qed. + +theorem not_prime_times_SSO: \forall n. 1 < n \to \lnot prime (2*n). +intros.intro.elim H1. +absurd (2 = 2*n) + [apply H3 + [apply (witness ? ? n).reflexivity + |apply le_n + ] + |apply lt_to_not_eq. + rewrite > times_n_SO in ⊢ (? % ?). + apply lt_times_r. + assumption + ] +qed. + +theorem eq_prim_prim_pred: \forall n. 1 < n \to +(prim (2*n)) = (prim (pred (2*n))). +intros.unfold prim. +rewrite < S_pred + [rewrite > false_to_sigma_p_Sn + [reflexivity + |apply not_prime_to_primeb_false. + apply not_prime_times_SSO. + assumption + ] + |apply (trans_lt ? (2*1)) + [simplify.apply lt_O_S + |apply lt_times_r. + assumption + ] + ] +qed. + +theorem le_prim_n1: \forall n. 4 \le n \to prim (S(2*n)) \le n. +intros.unfold prim. elim H + [simplify.apply le_n + |cut (sigma_p (2*S n1) primeb (λp:nat.1) = sigma_p (S (2*S n1)) primeb (λp:nat.1)) + [apply (bool_elim ? (primeb (S(2*(S n1)))));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > sym_plus. + rewrite < plus_n_Sm. + rewrite < plus_n_O. + apply le_S_S. + rewrite < Hcut. + rewrite > times_SSO. + assumption + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [apply le_S. + rewrite < Hcut. + rewrite > times_SSO. + assumption + |assumption + ] + ] + |apply sym_eq.apply (eq_prim_prim_pred (S n1)). + apply le_S_S.apply (trans_le ? 4) + [apply leb_true_to_le.reflexivity + |assumption + ] + ] + ] +qed. + +(* usefull to kill a successor in bertrand *) +theorem le_prim_n2: \forall n. 7 \le n \to prim (S(2*n)) \le pred n. +intros.unfold prim. elim H + [apply leb_true_to_le.reflexivity. + |cut (sigma_p (2*S n1) primeb (λp:nat.1) = sigma_p (S (2*S n1)) primeb (λp:nat.1)) + [apply (bool_elim ? (primeb (S(2*(S n1)))));intro + [rewrite > true_to_sigma_p_Sn + [rewrite > sym_plus. + rewrite < plus_n_Sm. + rewrite < plus_n_O. + simplify in ⊢ (? ? %). + rewrite > S_pred in ⊢ (? ? %) + [apply le_S_S. + rewrite < Hcut. + rewrite > times_SSO. + assumption + |apply (ltn_to_ltO ? ? H1) + ] + |assumption + ] + |rewrite > false_to_sigma_p_Sn + [simplify in ⊢ (? ? %). + apply (trans_le ? ? ? ? (le_pred_n n1)). + rewrite < Hcut. + rewrite > times_SSO. + assumption + |assumption + ] + ] + |apply sym_eq.apply (eq_prim_prim_pred (S n1)). + apply le_S_S.apply (trans_le ? 4) + [apply leb_true_to_le.reflexivity + |apply (trans_le ? ? ? ? H1). + apply leb_true_to_le.reflexivity + ] + ] + ] +qed. + +(* da spostare *) +theorem le_pred: \forall n,m. n \le m \to pred n \le pred m. +apply nat_elim2;intros + [apply le_O_n + |apply False_ind.apply (le_to_not_lt ? ? H). + apply lt_O_S + |simplify.apply le_S_S_to_le.assumption + ] +qed. + +(* si dovrebbe poter migliorare *) +theorem le_prim_n3: \forall n. 15 \le n \to +prim n \le pred (n/2). +intros. +elim (or_eq_eq_S (pred n)). +elim H1 + [cut (n = S (2*a)) + [rewrite > Hcut. + apply (trans_le ? (pred a)) + [apply le_prim_n2. + apply (le_times_to_le 2) + [apply le_n_Sn + |apply le_S_S_to_le. + rewrite < Hcut. + assumption + ] + |apply le_pred. + apply le_times_to_le_div + [apply lt_O_S + |apply le_n_Sn + ] + ] + |rewrite < H2. + apply S_pred. + apply (ltn_to_ltO ? ? H) + ] + |cut (n=2*(S a)) + [rewrite > Hcut. + rewrite > eq_prim_prim_pred + [rewrite > times_SSO in ⊢ (? % ?). + change in ⊢ (? (? %) ?) with (S (2*a)). + rewrite > sym_times in ⊢ (? ? (? (? % ?))). + rewrite > lt_O_to_div_times + [apply (trans_le ? (pred a)) + [apply le_prim_n2. + apply le_S_S_to_le. + apply (lt_times_to_lt 2) + [apply le_n_Sn + |apply le_S_S_to_le. + rewrite < Hcut. + apply le_S_S. + assumption + ] + |apply le_pred. + apply le_n_Sn + ] + |apply lt_O_S + ] + |apply le_S_S. + apply not_lt_to_le.intro. + apply (le_to_not_lt ? ? H). + rewrite > Hcut. + lapply (le_S_S_to_le ? ? H3) as H4. + apply (le_n_O_elim ? H4). + apply leb_true_to_le.reflexivity + ] + |rewrite > times_SSO. + rewrite > S_pred + [apply eq_f.assumption + |apply (ltn_to_ltO ? ? H) + ] + ] + ] +qed. + +(* This is chebishev psi function *) definition A: nat \to nat \def \lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)). @@ -944,6 +1139,30 @@ pi_p (S n) primeb (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))). +theorem B_SSSO: B 3 = 6. +reflexivity. +qed. + +theorem B_SSSSO: B 4 = 6. +reflexivity. +qed. + +theorem B_SSSSSO: B 5 = 30. +reflexivity. +qed. + +theorem B_SSSSSSO: B 6 = 20. +reflexivity. +qed. + +theorem B_SSSSSSSO: B 7 = 140. +reflexivity. +qed. + +theorem B_SSSSSSSSO: B 8 = 70. +reflexivity. +qed. + theorem eq_fact_B:\forall n.S O < n \to fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n). intros. unfold B. @@ -975,8 +1194,90 @@ apply le_exp ] qed. +theorem le_B_A4: \forall n. O < n \to (S(S O))* B ((S(S(S(S O))))*n) \le A ((S(S(S(S O))))*n). +intros.unfold B. +rewrite > eq_A_A'. +unfold A'. +cut ((S(S O)) < (S ((S(S(S(S O))))*n))) + [cut (O (pi_p_gi ? ? (S(S O))) + [rewrite > (pi_p_gi ? ? (S(S O))) in ⊢ (? ? %) + [rewrite < assoc_times. + apply le_times + [rewrite > (pi_p_gi ? ? O) + [rewrite > (pi_p_gi ? ? O) in ⊢ (? ? %) + [rewrite < assoc_times. + apply le_times + [rewrite < exp_n_SO. + change in ⊢ (? (? ? (? ? (? (? (? % ?) ?) ?))) ?) + with ((S(S O))*(S(S O))). + rewrite > assoc_times. + rewrite > sym_times in ⊢ (? (? ? (? ? (? (? % ?) ?))) ?). + rewrite > lt_O_to_div_times + [rewrite > divides_to_mod_O + [apply le_n + |apply lt_O_S + |apply (witness ? ? n).reflexivity + ] + |apply lt_O_S + ] + |apply le_pi_p.intros. + rewrite > exp_n_SO in ⊢ (? ? %). + apply le_exp + [apply lt_O_S + |apply le_S_S_to_le. + apply lt_mod_m_m. + apply lt_O_S + ] + ] + |assumption + |reflexivity + ] + |assumption + |reflexivity + ] + |apply le_pi_p.intros. + apply le_pi_p.intros. + rewrite > exp_n_SO in ⊢ (? ? %). + apply le_exp + [apply prime_to_lt_O. + apply primeb_true_to_prime. + apply (andb_true_true ? ? H2) + |apply le_S_S_to_le. + apply lt_mod_m_m. + apply lt_O_S + ] + ] + |assumption + |reflexivity + ] + |assumption + |reflexivity + ] + |apply lt_O_log + [rewrite > (times_n_O (S(S(S(S O))))) in ⊢ (? % ?). + apply lt_times_r1 + [apply lt_O_S + |assumption + ] + |rewrite > times_n_SO in ⊢ (? % ?). + apply le_times + [apply le_S.apply le_S.apply le_n + |assumption + ] + ] + ] + |apply le_S_S. + rewrite > times_n_SO in ⊢ (? % ?). + apply le_times + [apply le_S.apply le_n_Sn + |assumption + ] + ] +qed. + theorem le_fact_A:\forall n.S O < n \to -fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n). +fact (2*n) \le exp (fact n) 2 * A (2*n). intros. rewrite > eq_fact_B [apply le_times_r. @@ -986,7 +1287,7 @@ rewrite > eq_fact_B qed. theorem lt_SO_to_le_B_exp: \forall n.S O < n \to -B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n). +B (2*n) \le exp 2 (pred (2*n)). intros. apply (le_times_to_le (exp (fact n) (S(S O)))) [apply lt_O_exp. @@ -1002,17 +1303,34 @@ apply (le_times_to_le (exp (fact n) (S(S O)))) qed. theorem le_B_exp: \forall n. -B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n). +B (2*n) \le exp 2 (pred (2*n)). intro.cases n [apply le_n |cases n1 - [simplify.apply le_S.apply le_S.apply le_n + [simplify.apply le_n |apply lt_SO_to_le_B_exp. apply le_S_S.apply lt_O_S. ] ] qed. +theorem lt_SSSSO_to_le_B_exp: \forall n.4 < n \to +B (2*n) \le exp 2 ((2*n)-2). +intros. +apply (le_times_to_le (exp (fact n) (S(S O)))) + [apply lt_O_exp. + apply lt_O_fact + |rewrite < eq_fact_B + [rewrite < sym_times in ⊢ (? ? %). + rewrite > exp_SSO. + rewrite < assoc_times. + apply lt_SSSSO_to_fact.assumption + |apply lt_to_le.apply lt_to_le. + apply lt_to_le.assumption + ] + ] +qed. + theorem lt_SO_to_le_exp_B: \forall n. S O < n \to exp (S(S O)) ((S(S O))*n) \le (S(S O)) * n * B ((S(S O))*n). intros. @@ -1213,32 +1531,104 @@ intros.cases n qed. theorem le_A_exp: \forall n. -A((S(S O))*n) \le (exp (S(S O)) ((S(S O)*n)))*A n. +A(2*n) \le (exp 2 (pred (2*n)))*A n. intro. -apply (trans_le ? (B((S(S O))*n)*A n)) +apply (trans_le ? (B(2*n)*A n)) [apply le_A_BA |apply le_times_l. apply le_B_exp ] qed. +theorem lt_SSSSO_to_le_A_exp: \forall n. 4 < n \to +A(2*n) \le exp 2 ((2*n)-2)*A n. +intros. +apply (trans_le ? (B(2*n)*A n)) + [apply le_A_BA + |apply le_times_l. + apply lt_SSSSO_to_le_B_exp.assumption + ] +qed. + +theorem times_SSO_pred: \forall n. 2*(pred n) \le pred (2*n). +intro.cases n + [apply le_n + |simplify.apply le_plus_r. + apply le_n_Sn + ] +qed. + +theorem le_S_times_SSO: \forall n. O < n \to S n \le 2*n. +intros. +elim H + [apply le_n + |rewrite > times_SSO. + apply le_S_S. + apply (trans_le ? (2*n1)) + [assumption + |apply le_n_Sn + ] + ] +qed. + theorem le_A_exp1: \forall n. -A(exp (S(S O)) n) \le (exp (S(S O)) ((S(S O))*(exp (S(S O)) n))). +A(exp 2 n) \le (exp 2 ((2*(exp 2 n)-(S(S n))))). intro.elim n - [simplify.apply le_S_S.apply le_O_n - |change with (A ((S(S O))*((S(S O)))\sup n1)≤ ((S(S O)))\sup((S(S O))*((S(S O))\sup(S n1)))). - apply (trans_le ? ((exp (S(S O)) ((S(S O)*(exp (S(S O)) n1))))*A (exp (S(S O)) n1))) + [simplify.apply le_n + |change in ⊢ (? % ?) with (A(2*(exp 2 n1))). + apply (trans_le ? ((exp 2 (pred(2*(exp (S(S O)) n1))))*A (exp (S(S O)) n1))) [apply le_A_exp - |apply (trans_le ? ((S(S O))\sup((S(S O))*((S(S O)))\sup(n1))*(S(S O))\sup((S(S O))*((S(S O)))\sup(n1)))) + |apply (trans_le ? ((2)\sup(pred (2*(2)\sup(n1)))*(2)\sup(2*(2)\sup(n1)-S (S n1)))) [apply le_times_r. assumption |rewrite < exp_plus_times. - simplify.rewrite < plus_n_O in ⊢ (? ? (? ? (? ? %))). - apply le_n + apply le_exp + [apply lt_O_S + |cut (S(S n1) \le 2*(exp 2 n1)) + [apply le_S_S_to_le. + change in ⊢ (? % ?) with (S(pred (2*(2)\sup(n1)))+(2*(2)\sup(n1)-S (S n1))). + rewrite < S_pred + [rewrite > eq_minus_S_pred in ⊢ (? ? %). + rewrite < S_pred + [rewrite < eq_minus_plus_plus_minus + [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?). + apply le_n + |assumption + ] + |apply lt_to_lt_O_minus. + apply (lt_to_le_to_lt ? (2*(S(S n1)))) + [rewrite > times_n_SO in ⊢ (? % ?). + rewrite > sym_times. + apply lt_times_l1 + [apply lt_O_S + |apply le_n + ] + |apply le_times_r. + assumption + ] + ] + |unfold.rewrite > times_n_SO in ⊢ (? % ?). + apply le_times + [apply le_n_Sn + |apply lt_O_exp. + apply lt_O_S + ] + ] + |elim n1 + [apply le_n + |apply (trans_le ? (2*(S(S n2)))) + [apply le_S_times_SSO. + apply lt_O_S + |apply le_times_r. + assumption + ] + ] + ] + ] ] ] ] -qed. +qed. theorem monotonic_A: monotonic nat le A. unfold.intros. @@ -1276,7 +1666,8 @@ elim H ] ] qed. - + +(* theorem le_A_exp2: \forall n. O < n \to A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)). intros. @@ -1298,6 +1689,7 @@ apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n))))) ] ] qed. +*) (* example *) theorem A_SO: A (S O) = S O. @@ -1316,26 +1708,10 @@ theorem A_SSSSO: A (S(S(S(S O)))) = S(S(S(S(S(S(S(S(S(S(S(S O))))))))))). reflexivity. qed. -(* da spostare *) -theorem or_eq_eq_S: \forall n.\exists m. -n = (S(S O))*m \lor n = S ((S(S O))*m). -intro.elim n - [apply (ex_intro ? ? O). - left.reflexivity - |elim H.elim H1 - [apply (ex_intro ? ? a). - right.apply eq_f.assumption - |apply (ex_intro ? ? (S a)). - left.rewrite > H2. - apply sym_eq. - apply times_SSO - ] - ] -qed. - +(* (* a better result *) theorem le_A_exp3: \forall n. S O < n \to -A(n) \le exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n)). +A(n) \le exp (pred n) (2*(exp 2 (2 * n)). intro. apply (nat_elim1 n). intros. @@ -1450,6 +1826,123 @@ elim H2 ] ] ] + |rewrite < H4 in H3.simplify in H3. + apply False_ind. + apply (lt_to_not_le ? ? H1). + rewrite > H3. + apply le_ + ] + ] +qed. +*) + +theorem le_A_exp4: \forall n. S O < n \to +A(n) \le (pred n)*exp 2 ((2 * n) -3). +intro. +apply (nat_elim1 n). +intros. +elim (or_eq_eq_S m). +elim H2 + [elim (le_to_or_lt_eq (S O) a) + [rewrite > H3 in ⊢ (? % ?). + apply (trans_le ? (exp 2 (pred(2*a))*A a)) + [apply le_A_exp + |apply (trans_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3)))) + [apply le_times_r. + apply H + [rewrite > H3. + rewrite > times_n_SO in ⊢ (? % ?). + rewrite > sym_times. + apply lt_times_l1 + [apply lt_to_le.assumption + |apply le_n + ] + |assumption + ] + |rewrite < H3. + rewrite < assoc_times. + rewrite > sym_times in ⊢ (? (? % ?) ?). + rewrite > assoc_times. + apply le_times + [rewrite > H3. + elim a[apply le_n|simplify.apply le_plus_n_r] + |rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |apply (trans_le ? (m+(m-3))) + [apply le_plus_l. + cases m[apply le_n|apply le_n_Sn] + |simplify.rewrite < plus_n_O. + rewrite > eq_minus_plus_plus_minus + [apply le_n + |rewrite > H3. + apply (trans_le ? (2*2)) + [simplify.apply (le_n_Sn 3) + |apply le_times_r.assumption + ] + ] + ] + ] + ] + ] + ] + |rewrite > H3.rewrite < H4.simplify. + apply le_S_S.apply lt_O_S + |apply not_lt_to_le.intro. + apply (lt_to_not_le ? ? H1). + rewrite > H3. + apply (le_n_O_elim a) + [apply le_S_S_to_le.assumption + |apply le_O_n + ] + ] + |elim (le_to_or_lt_eq O a (le_O_n ?)) + [apply (trans_le ? (A ((S(S O))*(S a)))) + [apply monotonic_A. + rewrite > H3. + rewrite > times_SSO. + apply le_n_Sn + |apply (trans_le ? ((exp 2 (pred(2*(S a))))*A (S a))) + [apply le_A_exp + |apply (trans_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3))))) + [apply le_times_r. + apply H + [rewrite > H3. + apply le_S_S. + apply le_S_times_SSO. + assumption + |apply le_S_S.assumption + ] + |rewrite > H3. + change in ⊢ (? ? (? % ?)) with (2*a). + rewrite > times_SSO. + change in ⊢ (? (? (? ? %) ?) ?) with (S(2*a)). + rewrite > minus_Sn_m + [change in ⊢ (? (? ? (? ? %)) ?) with (2*(exp 2 (S(2*a)-3))). + rewrite < assoc_times in ⊢ (? (? ? %) ?). + rewrite < assoc_times. + rewrite > sym_times in ⊢ (? (? % ?) ?). + rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?). + rewrite > assoc_times. + apply le_times_r. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |rewrite < eq_minus_plus_plus_minus + [rewrite > plus_n_O in ⊢ (? (? (? ? %) ?) ?). + apply le_n + |apply le_S_S. + apply O_lt_const_to_le_times_const. + assumption + ] + ] + |apply le_S_S. + apply O_lt_const_to_le_times_const. + assumption + ] + ] + ] + ] |rewrite < H4 in H3.simplify in H3. apply False_ind. apply (lt_to_not_le ? ? H1). @@ -1459,6 +1952,138 @@ elim H2 ] qed. +theorem le_n_SSSSSSSSO_to_le_A_exp: +\forall n. n \le 8 \to A(n) \le exp 2 ((2 * n) -3). +intro.cases n + [intro.apply le_n + |cases n1 + [intro.apply le_n + |cases n2 + [intro.apply le_n + |cases n3 + [intro.apply leb_true_to_le.reflexivity + |cases n4 + [intro.apply leb_true_to_le.reflexivity + |cases n5 + [intro.apply leb_true_to_le.reflexivity + |cases n6 + [intro.apply leb_true_to_le.reflexivity + |cases n7 + [intro.apply leb_true_to_le.reflexivity + |cases n8 + [intro.apply leb_true_to_le.reflexivity + |intro.apply False_ind. + apply (lt_to_not_le ? ? H). + apply leb_true_to_le.reflexivity + ] + ] + ] + ] + ] + ] + ] + ] + ] +qed. + +theorem le_A_exp5: \forall n. A(n) \le exp 2 ((2 * n) -3). +intro. +apply (nat_elim1 n). +intros. +elim (decidable_le 9 m) + [elim (or_eq_eq_S m). + elim H2 + [rewrite > H3 in ⊢ (? % ?). + apply (trans_le ? (exp 2 (pred(2*a))*A a)) + [apply le_A_exp + |apply (trans_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3)))) + [apply le_times_r. + apply H. + rewrite > H3. + apply lt_m_nm + [apply (trans_lt ? 4) + [apply lt_O_S + |apply (lt_times_to_lt 2) + [apply lt_O_S + |rewrite < H3.assumption + ] + ] + |apply le_n + ] + |rewrite < H3. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |simplify.rewrite < plus_n_O. + rewrite > eq_minus_plus_plus_minus + [apply le_plus_l. + apply le_pred_n + |apply (trans_le ? 9) + [apply leb_true_to_le. reflexivity + |assumption + ] + ] + ] + ] + ] + |apply (trans_le ? (A (2*(S a)))) + [apply monotonic_A. + rewrite > H3. + rewrite > times_SSO. + apply le_n_Sn + |apply (trans_le ? ((exp 2 ((2*(S a))-2))*A (S a))) + [apply lt_SSSSO_to_le_A_exp. + apply le_S_S. + apply (le_times_to_le 2) + [apply le_n_Sn. + |apply le_S_S_to_le.rewrite < H3.assumption + ] + |apply (trans_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3)))) + [apply le_times_r. + apply H. + rewrite > H3. + apply le_S_S. + apply lt_m_nm + [apply (lt_to_le_to_lt ? 4) + [apply lt_O_S + |apply (le_times_to_le 2) + [apply lt_O_S + |apply le_S_S_to_le. + rewrite < H3.assumption + ] + ] + |apply le_n + ] + |rewrite > times_SSO. + rewrite < H3. + rewrite < exp_plus_times. + apply le_exp + [apply lt_O_S + |cases m + [apply le_n + |cases n1 + [apply le_n + |simplify. + rewrite < minus_n_O. + rewrite < plus_n_O. + rewrite < plus_n_Sm. + simplify.rewrite < minus_n_O. + rewrite < plus_n_Sm. + apply le_n + ] + ] + ] + ] + ] + ] + ] + |apply le_n_SSSSSSSSO_to_le_A_exp. + apply le_S_S_to_le. + apply not_le_to_lt. + assumption + ] +qed. + theorem eq_sigma_pi_SO_n: \forall n. sigma_p n (\lambda i.true) (\lambda i.S O) = n. intro.elim n @@ -1489,6 +2114,16 @@ assumption. qed. +theorem le_prim_log : \forall n,b.S O < b \to +log b (A n) \leq prim n * (S (log b n)). +intros;apply (trans_le ? ? ? ? (log_exp1 ? ? ? ?)) + [apply le_log + [assumption + |apply le_Al] + |assumption] +qed. + + (* the inequalities *) theorem le_exp_priml: \forall n. O < n \to exp (S(S O)) ((S(S O))*n) \le exp ((S(S O))*n) (S(prim ((S(S O))*n))). @@ -1504,8 +2139,35 @@ apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n)))))) ] qed. +theorem le_exp_prim4l: \forall n. O < n \to +exp 2 (S(4*n)) \le exp (4*n) (S(prim (4*n))). +intros. +apply (trans_le ? (2*(4*n*(B (4*n))))) + [change in ⊢ (? % ?) with (2*(exp 2 (4*n))). + apply le_times_r. + cut (4*n = 2*(2*n)) + [rewrite > Hcut. + apply le_exp_B. + apply lt_to_le.unfold. + rewrite > times_n_SO in ⊢ (? % ?). + apply le_times_r.assumption + |rewrite < assoc_times. + reflexivity + ] + |change in ⊢ (? ? %) with ((4*n)*(4*n)\sup (prim (4*n))). + rewrite < assoc_times. + rewrite > sym_times in ⊢ (? (? % ?) ?). + rewrite > assoc_times. + apply le_times_r. + apply (trans_le ? (A (4*n))) + [apply le_B_A4.assumption + |apply le_Al + ] + ] +qed. + theorem le_priml: \forall n. O < n \to -(S(S O))*n \le (S (log (S(S O)) ((S(S O))*n)))*S(prim ((S(S O))*n)). +2*n \le (S (log 2 (2*n)))*S(prim (2*n)). intros. rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?) [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n))))))) @@ -1521,24 +2183,82 @@ rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?) ] qed. -theorem le_exp_primr: \forall n. S O < n \to -exp n (prim n) \le exp (pred n) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * n)). +theorem le_exp_primr: \forall n. +exp n (prim n) \le exp 2 (2*(2*n-3)). intros. -apply (trans_le ? (exp (A n) (S(S O)))) +apply (trans_le ? (exp (A n) 2)) [change in ⊢ (? ? %) with ((A n)*((A n)*(S O))). rewrite < times_n_SO. apply leA_r2 - |apply (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * n))) (S(S O)))) - [apply monotonic_exp1. - apply le_A_exp3. + |rewrite > sym_times. + rewrite < exp_exp_times. + apply monotonic_exp1. + apply le_A_exp5 + ] +qed. + +(* bounds *) +theorem le_primr: \forall n. 1 < n \to prim n \le 2*(2*n-3)/log 2 n. +intros. +apply le_times_to_le_div + [apply lt_O_log + [apply lt_to_le.assumption + |assumption + ] + |apply (trans_le ? (log 2 (exp n (prim n)))) + [rewrite > sym_times. + apply log_exp2 + [apply le_n + |apply lt_to_le.assumption + ] + |rewrite < (eq_log_exp 2) in ⊢ (? ? %) + [apply le_log + [apply le_n + |apply le_exp_primr + ] + |apply le_n + ] + ] + ] +qed. + +theorem le_priml1: \forall n. O < n \to +2*n/((log 2 n)+2) - 1 \le prim (2*n). +intros. +apply le_plus_to_minus. +apply le_times_to_le_div2 + [rewrite > sym_plus. + simplify.apply lt_O_S + |rewrite > sym_times in ⊢ (? ? %). + rewrite < plus_n_Sm. + rewrite < plus_n_Sm in ⊢ (? ? (? ? %)). + rewrite < plus_n_O. + rewrite < sym_plus. + rewrite < log_exp + [simplify in ⊢ (? ? (? (? (? ? (? % ?))) ?)). + apply le_priml. assumption - |rewrite < times_exp. - rewrite > exp_exp_times. - rewrite > exp_exp_times. - rewrite > sym_times in ⊢ (? (? ? (? ? %)) ?). - rewrite < assoc_times in ⊢ (? (? ? (? ? %)) ?). - apply le_n + |apply le_n + |assumption ] ] qed. +(* +theorem prim_SSSSSSO: \forall n.30\le n \to O < prim (8*n) - prim n. +intros. +apply lt_to_lt_O_minus. +change in ⊢ (? ? (? (? % ?))) with (2*4). +rewrite > assoc_times. +apply (le_to_lt_to_lt ? (2*(2*n-3)/log 2 n)) + [apply le_primr.apply (trans_lt ? ? ? ? H). + apply leb_true_to_le.reflexivity + |apply (lt_to_le_to_lt ? (2*(4*n)/((log 2 (4*n))+2) - 1)) + [elim H + [ +normalize in ⊢ (%);simplify. + |apply le_priml1. +*) + + +