From 018a168b0ca16c5951106162e515d7949366d754 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 29 Jan 2008 10:57:02 +0000 Subject: [PATCH] New approximtions. --- helm/software/matita/library/nat/chebyshev.ma | 121 +++++++++++++++++- 1 file changed, 116 insertions(+), 5 deletions(-) diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma index 1f50b3212..2c705635f 100644 --- a/helm/software/matita/library/nat/chebyshev.ma +++ b/helm/software/matita/library/nat/chebyshev.ma @@ -22,7 +22,7 @@ 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 *) +(* 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)). @@ -975,6 +975,88 @@ 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). intros. @@ -1594,7 +1676,6 @@ elim H2 ] qed. - theorem eq_sigma_pi_SO_n: \forall n. sigma_p n (\lambda i.true) (\lambda i.S O) = n. intro.elim n @@ -1624,6 +1705,7 @@ apply primeb_true_to_prime. 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 ? ? ? ?)) @@ -1649,6 +1731,35 @@ 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. +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)). intros. @@ -1667,15 +1778,15 @@ 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)). +exp n (prim n) \le exp (pred n) ((S(S O))*(S(S O)))*(exp (S(S O)) ((S(S O))*(S(S O)) * (pred n))). intros. apply (trans_le ? (exp (A n) (S(S O)))) [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 (trans_le ? (exp (exp (pred n) (S(S O))*(exp (S(S O)) ((S(S O)) * (pred n)))) (S(S O)))) [apply monotonic_exp1. - apply le_A_exp3. + apply le_A_exp4. assumption |rewrite < times_exp. rewrite > exp_exp_times. -- 2.39.2