From: Wilmer Ricciotti Date: Fri, 21 Dec 2007 16:09:59 +0000 (+0000) Subject: beginning proof of chebyshev's bound on prim. X-Git-Tag: make_still_working~5702 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c5f91917b06e323411981a22142bfedba996518;p=helm.git beginning proof of chebyshev's bound on prim. --- diff --git a/helm/software/matita/library/nat/chebyshev_thm.ma b/helm/software/matita/library/nat/chebyshev_thm.ma new file mode 100644 index 000000000..bf616a17c --- /dev/null +++ b/helm/software/matita/library/nat/chebyshev_thm.ma @@ -0,0 +1,345 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/chebyshev_thm/". + +include "nat/neper.ma". + +definition C \def \lambda n.pi_p (S n) primeb + (\lambda p.match (leb (p*p) n) with + [ true => p + | false => S (n/p) ]). + +theorem asdasd : \forall n. exp n (prim n) \leq (A n)*(C n). +intro;unfold prim;rewrite < exp_sigma_p;unfold A;unfold C;rewrite < times_pi_p; +apply le_pi_p;intros; +apply (bool_elim ? (leb (i*i) n));intro + [change in \vdash (? ? (? ? %)) with i; + rewrite > sym_times;change in \vdash (? ? %) with (exp i (S (log i n))); + apply lt_to_le;apply lt_exp_log;apply prime_to_lt_SO; + apply primeb_true_to_prime;assumption + |change in \vdash (? ? (? ? %)) with (S (n/i)); + cut (log i n = S O) + [rewrite > Hcut;rewrite < exp_n_SO; + apply lt_to_le;rewrite > sym_times;apply lt_div_S;apply prime_to_lt_O; + apply primeb_true_to_prime;assumption + |apply antisymmetric_le + [apply le_S_S_to_le;apply not_le_to_lt;intro; + apply (leb_false_to_not_le ? ? H2);apply (trans_le ? (exp i (log i n))) + [rewrite < exp_SSO;apply le_exp; + [apply prime_to_lt_O; + apply primeb_true_to_prime;assumption + |assumption] + |apply le_exp_log;apply (trans_le ? i) + [apply prime_to_lt_O;apply primeb_true_to_prime;assumption + |apply le_S_S_to_le;assumption]] + |apply (trans_le ? (log i i)) + [rewrite > log_n_n; + [apply le_n + |apply prime_to_lt_SO;apply primeb_true_to_prime;assumption] + |apply le_log + [apply prime_to_lt_SO;apply primeb_true_to_prime;assumption + |apply le_S_S_to_le;assumption]]]]] +qed. + +definition theta_pi \def + \lambda n.pi_p (S n) primeb (\lambda p.p). + +definition C1 \def + \lambda n. pi_p (S n) (\lambda x. (primeb x) \land (leb (x*x) n)) (\lambda p.p). + +definition C2 \def + \lambda n. pi_p (S n) (\lambda x. (primeb x) \land (leb (S n) (x*x))) (\lambda p.S (n/p)). + + +theorem jj : \forall n.C n = C1 n * C2 n. +intro;unfold C;unfold C1;unfold C2; +cut (\forall m.pi_p (S n) primeb +(λp:nat + .match leb (p*p) m in bool return λb:bool.nat with  + [true⇒p|false⇒S (m/p)]) +=pi_p (S n) (λx:nat.primeb x∧leb (x*x) m) (λp:nat.p) + *pi_p (S n) (λx:nat.primeb x∧leb (S m) (x*x)) (λp:nat.S (m/p))) + [apply Hcut; + |intro;elim n 0 + [simplify;reflexivity + |intro;apply (bool_elim ? (primeb (S n1))) + [intros;rewrite > true_to_pi_p_Sn + [apply (bool_elim ? (leb ((S n1)*(S n1)) m)) + [intro;rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? % ?)) + [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %)) + [rewrite > H1;rewrite > H2;rewrite < assoc_times;reflexivity + |rewrite > H;lapply (leb_true_to_le ? ? H2); + lapply (le_to_not_lt ? ? Hletin); + apply (bool_elim ? (leb (S m) (S n1 * S n1))) + [intro;apply False_ind;apply Hletin1; + apply leb_true_to_le;assumption + |intro;reflexivity]] + |rewrite > H2;rewrite > H;reflexivity] + |intro;rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? % ?)) + [rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? ? %)) + [rewrite > H1;rewrite < assoc_times; + rewrite > sym_times in \vdash (? ? (? % ?) ?); + rewrite > assoc_times;reflexivity + |rewrite > H; + change in \vdash (? ? % ?) with (leb (S m) (S n1* S n1)); + apply le_to_leb_true;apply not_le_to_lt; + apply leb_false_to_not_le;assumption] + |rewrite > H;rewrite > H2;reflexivity]] + |assumption] + |intros;rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? % ?)) + [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %)) + [rewrite > H1;reflexivity + |rewrite > H;elim (leb (S m) (S n1*S n1));simplify;reflexivity] + |rewrite > H;elim (leb (S n1*S n1) m);simplify;reflexivity] + |assumption]]]] +qed. + +theorem log_pi_p : \forall n,b,f,g.S O < b \to + log b (pi_p n f g) \leq + (sigma_p n f (\lambda x.S O)) + (sigma_p n f (\lambda x.log b (g x))). +intros;elim n + [simplify;rewrite < times_n_SO;apply (leb_elim b (S O)) + [intro;elim (lt_to_not_le ? ? H);assumption + |intro;simplify;apply le_n] + |apply (bool_elim ? (f n1)) + [intro;rewrite > true_to_pi_p_Sn + [rewrite > true_to_sigma_p_Sn + [rewrite > true_to_sigma_p_Sn + [apply (trans_le ? (S ((log b (g n1)) + (log b (pi_p n1 f g))))) + [apply log_times;assumption + |rewrite > assoc_plus; + change in \vdash (? ? %) with (S (sigma_p n1 f (\lambda x.S O)+(log b (g n1)+sigma_p n1 f (\lambda x.log b (g x))))); + apply le_S_S;rewrite < assoc_plus; + rewrite > sym_plus in \vdash (? ? (? % ?)); + rewrite > assoc_plus;apply le_plus; + [apply le_n]]]]] + assumption + |intro;rewrite > false_to_pi_p_Sn + [rewrite > false_to_sigma_p_Sn + [rewrite > false_to_sigma_p_Sn]] + assumption]] +qed. + +axiom daemon : False. +(* +lemma lt_log_to_lt : \forall b,m,n.S O < b \to log b m < log b n \to m < n. +intros;apply not_le_to_lt;intro;elim (le_to_not_lt ? ? (le_log ? ? ? H H2)); +assumption. +qed. + +theorem ababbs: \forall n,a,b.S O < b \to O < n \to n < exp b a \to log b n < a. +intros;unfold log;apply not_le_to_lt;intro;apply (lt_to_not_le ? ? H2); +elim (le_to_or_lt_eq ? ? H3) + [apply lt_to_le;apply (lt_log_to_lt b ? ? H);rewrite > eq_log_exp;assumption + |apply (trans_le ? (exp b (log b n))) + [rewrite < H4;apply le_n + |apply le_exp_log;assumption]] +qed. + +theorem exp_exp_to_log : \forall b,n,k.S O < b \to +exp b k \leq n \to n < exp b (S k) \to log b n = k. +intros;unfold log;lapply (ababbs ? ? ? H ? H2) + [apply (trans_le ? ? ? ? H1);apply lt_O_exp + |unfold log in Hletin;lapply (le_to_leb_true ? ? H1); + lapply (f_m_to_le_max (λx:nat.leb ((b)\sup(x)) n) n ? ? Hletin1) + [ + elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? Hletin)) + [unfold log in H3; +]]elim daemon. +qed. + +theorem xxx_log : \forall a,b.S O < b \to O < a \to log b (b*a) = S (log b a). +intros 3;elim a + [elim (not_le_Sn_O ? H1); + |apply (inj_exp_r b) + [assumption + |*) + +theorem le_log_C2_sigma_p : \forall n,b. S O < b \to +log b (C2 n) \leq +(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) + +(prim n + (((sigma_p n (\lambda x.leb (S n) (x*x)) (\lambda i.prim i * S (n!/i))) + *(S (log b 3)))/n!)). +intros;unfold C2; +apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λx:nat.1) ++sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) + (λi.log b (S (n/i))))) + [apply log_pi_p;assumption + |apply le_plus + [apply le_n + |apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λi:nat.S (log b (n/i))))) + [apply le_sigma_p;intros;cut (log b (b*(n/i)) = S (log b (n/i))) + [rewrite < Hcut;apply le_log + [assumption + |elim H + [rewrite < times_SSO_n;change in \vdash (? % ?) with (S O + (n/i)); + apply le_plus; + [apply le_times_to_le_div + [apply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2))); + |rewrite < times_n_SO;apply le_S_S_to_le;assumption] + |apply le_n] + |apply (trans_le ? ? ? H4);apply le_times_l;apply le_S;apply le_n]] + |rewrite > exp_n_SO in ⊢ (? ? (? ? (? % ?)) ?); + rewrite > log_exp; + [reflexivity + |assumption + |apply le_times_to_le_div; + [apply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2))); + |rewrite < times_n_SO;apply le_S_S_to_le;assumption]]] + |change in ⊢ (? (? ? ? (λi:?.%)) ?) with ((S O) + (log b (n/i))); + rewrite > (sigma_p_plus_1 ? (\lambda x.S O)); + apply le_plus + [unfold prim;apply le_sigma_p1;intros;elim (leb (S n) (i*i)); + [rewrite > andb_sym;apply le_n + |rewrite > andb_sym;apply le_O_n] + |apply sigma_p_log_div;assumption]]]] +qed. + +lemma le_prim_n_stima : \forall n,b. S O < b \to b \leq n \to +prim n \leq (S (((S (S (S (S O))))*(S (log b (pred n)))) + + ((S (S (S (S O))))*n)))/(log b n). +(* la stima del secondo addendo è ottenuta considerando che + logreale 2 è sempre <= 1 (si dimostra per casi: b = 2, b > 2) *) +intros;apply le_times_to_le_div; + [apply lt_O_log; + [apply (trans_le ? b) + [apply lt_to_le;assumption + |assumption] + |assumption] + |apply (trans_le ? (log b (exp n (prim n)))) + [rewrite > sym_times;apply log_exp2 + [assumption + |apply (trans_le ? b ? ? H1);apply lt_to_le;assumption] + |apply (trans_le ? (log b ((exp (pred n) (S (S (S (S O))))) + *(exp (S (S O)) ((S (S (S (S O))))*n))))) + [apply le_log + [assumption + |apply le_exp_primr;apply (trans_le ? ? ? H H1)] + |apply (trans_le ? (S ((log b (exp (pred n) (S (S (S (S O)))))) + + (log b (exp (S (S O)) ((S (S (S (S O))))*n)))))) + [apply log_times;assumption + |apply le_S_S;apply le_plus + [apply log_exp1;assumption + |cases H + [rewrite > times_n_SO in \vdash (? (? ? %) ?); + rewrite > log_exp + [rewrite < plus_n_O;apply le_n + |apply le_n + |apply le_n] + |apply (trans_le ? (((S (S (S (S O))))*n)*(S (log (S m) (S (S O)))))) + [apply log_exp1;apply le_S;assumption + |rewrite > times_n_SO in \vdash (? ? %); + apply le_times_r;apply le_S_S; + rewrite > lt_to_log_O + [apply le_n + |apply lt_O_S + |apply le_S_S;assumption]]]]]]]] +qed. + +(* + +theorem le_log_C2_stima : \forall n,b. S O < b \to +log b (C2 n) \leq +(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) + +(((S (((S (S (S (S O))))*(S (log b (pred n)))) + + ((S (S (S (S O))))*n)))/(log b n)) + + (((sigma_p n (\lambda x.leb (S n) (x*x)) + (\lambda i.((S (((S (S (S (S O))))*(S (log b (pred n)))) + + ((S (S (S (S O))))*n)))/(log b n))* S (n!/i))) + *(S (log b 3)))/n!)). +elim daemon. + +theorem le_log_C2_sigma_p : \forall n,b. S O < b \to +log b (C2 n) \leq +(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) + +(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) + (\lambda p.(sigma_p (n+p) (\lambda i.leb p i) + (\lambda i.S ((n+p)!/i*(S (log b 3)))))/(n+p)!)). +intros;unfold C2; +apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λx:nat.1) ++sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) + (λi.log b (S (n/i))))) + [apply log_pi_p;assumption + |apply le_plus + [apply le_n + |apply le_sigma_p;intros;cut (S (n/i) = (n+i)/i) + [rewrite > Hcut;apply le_log_div_sigma_p + [assumption + |apply prime_to_lt_O;apply primeb_true_to_prime; + elim (and_true ? ? H2);assumption + |apply le_plus_n + |apply le_n] + |lapply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2))) as H3; + apply (div_mod_spec_to_eq (n+i) i (S (n/i)) (n \mod i) ? ((n+i) \mod i)) + [constructor 1 + [apply lt_mod_m_m;assumption + |simplify;rewrite > assoc_plus;rewrite < div_mod; + [apply sym_plus + |assumption]] + |apply div_mod_spec_div_mod;assumption]]]] +qed. +*) + +definition sqrt \def + \lambda n.max n (\lambda x.leb (x*x) n). + +theorem le_sqrt_to_le_times_l : \forall m,n.n \leq sqrt m \to n*n \leq m. +intros;apply (trans_le ? (sqrt m * sqrt m)) + [apply le_times;assumption + |apply leb_true_to_le;apply (f_max_true (λx:nat.leb (x*x) m) m); + apply (ex_intro ? ? O);split + [apply le_O_n + |simplify;reflexivity]] +qed. + +theorem le_sqrt_to_le_times_r : \forall m,n.sqrt m < n \to m < n*n. +intros;apply not_le_to_lt;intro; +apply ((leb_false_to_not_le ? ? + (lt_max_to_false (\lambda x.leb (x*x) m) m n H ?)) + H1); +apply (trans_le ? ? ? ? H1);cases n + [apply le_n + |rewrite > times_n_SO in \vdash (? % ?);rewrite > sym_times;apply le_times + [apply le_S_S;apply le_O_n + |apply le_n]] +qed. + +theorem eq_theta_pi_sqrt_C1 : \forall n. theta_pi (sqrt n) = C1 n. +intro;unfold theta_pi;unfold C1;rewrite > (false_to_eq_pi_p (S (sqrt n)) (S n)) + [generalize in match (le_sqrt_to_le_times_l n);elim (sqrt n) + [simplify;reflexivity + |apply (bool_elim ? (primeb (S n1))) + [intro;rewrite > true_to_pi_p_Sn + [rewrite > true_to_pi_p_Sn in \vdash (? ? ? %) + [apply eq_f2 + [reflexivity + |apply H;intros;apply H1;apply le_S;assumption] + |apply (andb_elim (primeb (S n1)) (leb (S n1 * S n1) n)); + rewrite > H2;whd;apply le_to_leb_true;apply H1;apply le_n] + |assumption] + |intro;rewrite > false_to_pi_p_Sn + [rewrite > false_to_pi_p_Sn in \vdash (? ? ? %) + [apply H;intros;apply H1;apply le_S;assumption + |apply (andb_elim (primeb (S n1)) (leb (S n1 * S n1) n)); + rewrite > H2;whd;reflexivity] + |assumption]]] + |apply le_S_S;unfold sqrt;apply le_max_n + |intros;apply (andb_elim (primeb i) (leb (i*i) n));elim (primeb i);simplify + [rewrite > lt_to_leb_false + [reflexivity + |apply le_sqrt_to_le_times_r;assumption] + |reflexivity]] +qed. diff --git a/helm/software/matita/library/nat/iteration2.ma b/helm/software/matita/library/nat/iteration2.ma index 6dbbfd572..211df69d0 100644 --- a/helm/software/matita/library/nat/iteration2.ma +++ b/helm/software/matita/library/nat/iteration2.ma @@ -629,32 +629,33 @@ elim n qed. theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat. -sigma_p n (\lambda b:nat. true) (\lambda a:nat.(f a) + (g a)) = -sigma_p n (\lambda b:nat. true) f + sigma_p n (\lambda b:nat. true) g. +\forall p. +sigma_p n p (\lambda a:nat.(f a) + (g a)) = +sigma_p n p f + sigma_p n p g. intros. elim n [ simplify. reflexivity -| rewrite > true_to_sigma_p_Sn - [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) f) - [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) g) - [ rewrite > assoc_plus in \vdash (? ? ? %). - rewrite < assoc_plus in \vdash (? ? ? (? ? %)). - rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))). - rewrite > assoc_plus in \vdash (? ? ? (? ? %)). - rewrite < assoc_plus in \vdash (? ? ? %). - apply eq_f. - assumption - | reflexivity - ] - | reflexivity - ] - | reflexivity - ] -] +| apply (bool_elim ? (p n1)); intro; + [ rewrite > true_to_sigma_p_Sn + [ rewrite > (true_to_sigma_p_Sn n1 p f) + [ rewrite > (true_to_sigma_p_Sn n1 p g) + [ rewrite > assoc_plus in \vdash (? ? ? %). + rewrite < assoc_plus in \vdash (? ? ? (? ? %)). + rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))). + rewrite > assoc_plus in \vdash (? ? ? (? ? %)). + rewrite < assoc_plus in \vdash (? ? ? %). + apply eq_f. + assumption]]] + assumption + | rewrite > false_to_sigma_p_Sn + [ rewrite > (false_to_sigma_p_Sn n1 p f) + [ rewrite > (false_to_sigma_p_Sn n1 p g) + [assumption]]] + assumption +]] qed. - theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat. sigma_p (n*m) (\lambda x:nat.true) f = sigma_p m (\lambda x:nat.true)