From 7265c6e8e0d548f6f97885727653b24c209d83f5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 4 Feb 2008 08:55:10 +0000 Subject: [PATCH] Improved approximations for A and prim. --- helm/software/matita/library/nat/chebyshev.ma | 205 ++++++++++++++++-- 1 file changed, 189 insertions(+), 16 deletions(-) diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma index e4ca6587a..317a82d15 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". @@ -944,6 +942,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. @@ -1095,6 +1117,23 @@ intro.cases n ] 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. @@ -1304,6 +1343,16 @@ apply (trans_le ? (B(2*n)*A n)) ] 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 @@ -1723,6 +1772,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 @@ -1778,8 +1959,6 @@ apply (trans_le ? ((((S(S O))*n*(B ((S(S O))*n)))))) ] qed. -alias num (instance 0) = "natural number". - theorem le_exp_prim4l: \forall n. O < n \to exp 2 (S(4*n)) \le exp (4*n) (S(prim (4*n))). intros. @@ -1824,23 +2003,17 @@ 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) 2*(exp 2 (2*(2*n-3))). +theorem le_exp_primr: \forall n. +exp n (prim n) \le exp 2 (2*(2*n-3)). intros. 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 ((pred n)*(exp 2 (2*n - 3))) 2)) - [apply monotonic_exp1. - apply le_A_exp4. - assumption - |rewrite < times_exp. - rewrite > exp_exp_times. - apply le_times_r. - rewrite > sym_times. - apply le_n - ] + |rewrite > sym_times. + rewrite < exp_exp_times. + apply monotonic_exp1. + apply le_A_exp5 ] qed. -- 2.39.2