X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fneper.ma;h=9378bd8dee4685787088fb23a6820134b6172753;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=644db0630e88b7d39ae36573a20a69f321e056c9;hpb=9475bcd66c14f82b84c27d4c759aa94783ec08d3;p=helm.git diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index 644db0630..9378bd8de 100644 --- a/helm/software/matita/library/nat/neper.ma +++ b/helm/software/matita/library/nat/neper.ma @@ -18,6 +18,7 @@ include "nat/iteration2.ma". include "nat/div_and_mod_diseq.ma". include "nat/binomial.ma". include "nat/log.ma". +include "nat/chebyshev.ma". theorem sigma_p_div_exp: \forall n,m. sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le @@ -294,8 +295,6 @@ intros. apply (trans_le ? (log p (((S(S(S O))))\sup(m/n)*((n)\sup(m))))) [apply le_log [assumption - |apply lt_O_exp. - apply lt_O_S |apply lt_to_le. apply lt_exp_Sn_m_SSSO;assumption ] @@ -311,11 +310,11 @@ apply (trans_le ? (log p (((S(S(S O))))\sup(m/n)*((n)\sup(m))))) ] qed. -theorem le_log_exp_Sn_log_exp_n: \forall a,b,n,p. S O < p \to -a \le b \to b \le n \to +theorem le_log_exp_fact_sigma_p: \forall a,b,n,p. S O < p \to +O < a \to a \le b \to b \le n \to log p (exp b n!) - log p (exp a n!) \le sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))). -intros 6. +intros 7. elim b [simplify. apply (lt_O_n_elim ? (lt_O_fact n)).intro. @@ -331,9 +330,285 @@ elim b apply le_log_exp_Sn_log_exp_n [apply lt_O_fact |assumption - | + |apply divides_fact; + [apply (trans_le ? ? ? H1);apply leb_true_to_le;assumption + |apply lt_to_le;assumption]] + |apply le_log + [assumption + |cut (O = exp O n!) + [rewrite > Hcut;apply monotonic_exp1;constructor 2; + apply leb_true_to_le;assumption + |elim n + [reflexivity + |simplify;rewrite > exp_plus_times;rewrite < H6; + rewrite > sym_times;rewrite < times_n_O;reflexivity]]]] + |apply le_log + [assumption + |apply monotonic_exp1;apply leb_true_to_le;assumption]] + |rewrite > sym_plus;rewrite > sym_plus in \vdash (? ? %);apply le_minus_to_plus; + rewrite < minus_plus_m_m;apply H3;apply lt_to_le;assumption] + |assumption] + |lapply (not_le_to_lt ? ? (leb_false_to_not_le ? ? H5)); + rewrite > eq_minus_n_m_O + [apply le_O_n + |apply le_log + [assumption + |apply monotonic_exp1;assumption]]]] +qed. + +theorem le_exp_div:\forall n,m,q. O < m \to +exp (n/m) q \le (exp n q)/(exp m q). +intros. +apply le_times_to_le_div + [apply lt_O_exp. + assumption + |rewrite > times_exp. + rewrite < sym_times. + apply monotonic_exp1. + rewrite > (div_mod n m) in ⊢ (? ? %) + [apply le_plus_n_r + |assumption + ] + ] +qed. + +theorem le_log_div_sigma_p: \forall a,b,n,p. S O < p \to +O < a \to a \le b \to b \le n \to +log p (b/a) \le +(sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))))/n!. +intros. +apply le_times_to_le_div + [apply lt_O_fact + |apply (trans_le ? (log p (exp (b/a) n!))) + [apply log_exp2 + [assumption + |apply le_times_to_le_div + [assumption + |rewrite < times_n_SO. + assumption + ] + ] + |apply (trans_le ? (log p ((exp b n!)/(exp a n!)))) + [apply le_log + [assumption + |apply le_exp_div.assumption + ] + |apply (trans_le ? (log p (exp b n!) - log p (exp a n!))) + [apply log_div + [assumption + |apply lt_O_exp. + assumption + |apply monotonic_exp1. + assumption + ] + |apply le_log_exp_fact_sigma_p;assumption + ] + ] + ] + ] +qed. + +theorem sigma_p_log_div1: \forall n,b. S O < b \to +sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p))) +\le sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n! +). +intros. +apply le_sigma_p.intros. +apply le_log_div_sigma_p + [assumption + |apply prime_to_lt_O. + apply primeb_true_to_prime. + apply (andb_true_true ? ? H2) + |apply le_S_S_to_le. + assumption + |apply le_n + ] +qed. + +theorem sigma_p_log_div2: \forall n,b. S O < b \to +sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p))) +\le +(sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!). +intros. +apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n! +))) + [apply sigma_p_log_div1.assumption + |apply le_times_to_le_div + [apply lt_O_fact + |rewrite > distributive_times_plus_sigma_p. + rewrite < sym_times in ⊢ (? ? %). + rewrite > distributive_times_plus_sigma_p. + apply le_sigma_p.intros. + apply (trans_le ? ((n!*(sigma_p n (λj:nat.leb i j) (λi:nat.S (n!/i*S (log b (S(S(S O)))))))/n!))) + [apply le_times_div_div_times. + apply lt_O_fact + |rewrite > sym_times. + rewrite > lt_O_to_div_times + [rewrite > distributive_times_plus_sigma_p. + apply le_sigma_p.intros. + rewrite < times_n_Sm in ⊢ (? ? %). + rewrite > plus_n_SO. + rewrite > sym_plus. + apply le_plus + [apply le_S_S.apply le_O_n + |rewrite < sym_times. + apply le_n + ] + |apply lt_O_fact + ] + ] + ] + ] +qed. + +theorem sigma_p_log_div: \forall n,b. S O < b \to +sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p))) +\le (sigma_p n (\lambda i.leb (S n) (i*i)) (\lambda i.(prim i)*S(n!/i)))*S(log b (S(S(S O))))/n! +. +intros. +apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!)) + [apply sigma_p_log_div2.assumption + |apply monotonic_div + [apply lt_O_fact + |apply le_times_l. + unfold prim. + cut + (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p)) + (λp:nat.sigma_p n (λi:nat.leb p i) (λi:nat.S (n!/i))) + = sigma_p n (λi:nat.leb (S n) (i*i)) + (λi:nat.sigma_p (S n) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i)))) + [rewrite > Hcut. + apply le_sigma_p.intros. + rewrite < sym_times. + rewrite > distributive_times_plus_sigma_p. + rewrite < times_n_SO. + cut + (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i)) + = sigma_p (S i) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i))) + [rewrite > Hcut1. + apply le_sigma_p1.intros. + rewrite < andb_sym. + rewrite < andb_sym in ⊢ (? (? (? (? ? %)) ?) ?). + apply (bool_elim ? (leb i1 i));intros + [apply (bool_elim ? (leb (S n) (i1*i1)));intros + [apply le_n + |apply le_O_n + ] + |apply le_O_n + ] + |apply or_false_to_eq_sigma_p + [apply le_S.assumption + |intros. + left.rewrite > (lt_to_leb_false i1 i) + [rewrite > andb_sym.reflexivity + |assumption + ] + ] + ] + |apply sigma_p_sigma_p.intros. + apply (bool_elim ? (leb x y));intros + [apply (bool_elim ? (leb (S n) (x*x)));intros + [rewrite > le_to_leb_true in ⊢ (? ? ? (? % ?)) + [reflexivity + |apply (trans_le ? (x*x)) + [apply leb_true_to_le.assumption + |apply le_times;apply leb_true_to_le;assumption + ] + ] + |rewrite < andb_sym in ⊢ (? ? (? % ?) ?). + rewrite < andb_sym in ⊢ (? ? ? (? ? (? % ?))). + rewrite < andb_sym in ⊢ (? ? ? %). + reflexivity + ] + |rewrite < andb_sym. + rewrite > andb_assoc in ⊢ (? ? ? %). + rewrite < andb_sym in ⊢ (? ? ? (? % ?)). + reflexivity + ] + ] + ] + ] +qed. + +theorem le_sigma_p_div_log_div_pred_log : \forall n,b,m. S O < b \to b*b \leq n \to +sigma_p (S n) (\lambda i.leb (S n) (i*i)) (\lambda i.m/(log b i)) +\leq ((S (S O)) * n * m)/(pred (log b n)). +intros. +apply (trans_le ? (sigma_p (S n) + (\lambda i.leb (S n) (i*i)) (\lambda i.(S (S O))*m/(pred (log b n))))) + [apply le_sigma_p;intros;apply le_times_to_le_div + [rewrite > minus_n_O in ⊢ (? ? (? %));rewrite < eq_minus_S_pred; + apply le_plus_to_minus_r;simplify; + rewrite < (eq_log_exp b ? H); + apply le_log; + [assumption + |simplify;rewrite < times_n_SO;assumption] + |apply (trans_le ? ((pred (log b n) * m)/log b i)) + [apply le_times_div_div_times;apply lt_O_log + [elim (le_to_or_lt_eq ? ? (le_O_n i)) + [assumption + |apply False_ind;apply not_eq_true_false;rewrite < H3;rewrite < H4; + reflexivity] + |apply (le_exp_to_le1 ? ? (S (S O))) + [apply lt_O_S; + |apply (trans_le ? (S n)) + [apply le_S;simplify;rewrite < times_n_SO;assumption + |rewrite > exp_SSO;apply leb_true_to_le;assumption]]] + |apply le_times_to_le_div2 + [apply lt_O_log + [elim (le_to_or_lt_eq ? ? (le_O_n i)) + [assumption + |apply False_ind;apply not_eq_true_false;rewrite < H3;rewrite < H4; + reflexivity] + |apply (le_exp_to_le1 ? ? (S (S O))) + [apply lt_O_S; + |apply (trans_le ? (S n)) + [apply le_S;simplify;rewrite < times_n_SO;assumption + |rewrite > exp_SSO;apply leb_true_to_le;assumption]]] + |rewrite > sym_times in \vdash (? ? %);rewrite < assoc_times; + apply le_times_l;rewrite > sym_times; + rewrite > minus_n_O in \vdash (? (? %) ?); + rewrite < eq_minus_S_pred;apply le_plus_to_minus; + simplify;rewrite < plus_n_O;apply (trans_le ? (log b (i*i))) + [apply le_log + [assumption + |apply lt_to_le;apply leb_true_to_le;assumption] + |rewrite > sym_plus;simplify;apply log_times;assumption]]]] + |rewrite > times_n_SO in \vdash (? (? ? ? (\lambda i:?.%)) ?); + rewrite < distributive_times_plus_sigma_p; + apply (trans_le ? ((((S (S O))*m)/(pred (log b n)))*n)) + [apply le_times_r;apply (trans_le ? (sigma_p (S n) (\lambda i:nat.leb (S O) (i*i)) (\lambda Hbeta1:nat.S O))) + [apply le_sigma_p1;intros;do 2 rewrite < times_n_SO; + apply (bool_elim ? (leb (S n) (i*i))) + [intro;cut (leb (S O) (i*i) = true) + [rewrite > Hcut;apply le_n + |apply le_to_leb_true;apply (trans_le ? (S n)) + [apply le_S_S;apply le_O_n + |apply leb_true_to_le;assumption]] + |intro;simplify in \vdash (? % ?);apply le_O_n] + |elim n + [simplify;apply le_n + |apply (bool_elim ? (leb (S O) ((S n1)*(S n1))));intro + [rewrite > true_to_sigma_p_Sn + [change in \vdash (? % ?) with (S (sigma_p (S n1) (\lambda i:nat.leb (S O) (i*i)) (\lambda Hbeta1:nat.S O))); + apply le_S_S;assumption + |assumption] + |rewrite > false_to_sigma_p_Sn + [apply le_S;assumption + |assumption]]]] + |rewrite > sym_times in \vdash (? % ?); + rewrite > sym_times in \vdash (? ? (? (? % ?) ?)); + rewrite > assoc_times; + apply le_times_div_div_times; + rewrite > minus_n_O in ⊢ (? ? (? %));rewrite < eq_minus_S_pred; + apply le_plus_to_minus_r;simplify; + rewrite < (eq_log_exp b ? H); + apply le_log; + [assumption + |simplify;rewrite < times_n_SO;assumption]]] +qed. -theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to +(* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to divides n m \to log p (exp n m) - log p (exp a m) \le sigma_p (S n) (\lambda i.leb (S a) i) (\lambda i.S((m/i)*S(log p (S(S(S O)))))). @@ -354,7 +629,7 @@ elim n apply le_log_exp_Sn_log_exp_n. -(* a generalization +* a generalization theorem le_exp_sigma_p_exp_m: \forall m,n. (exp (S m) n) \le sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)). intros.