X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fneper.ma;h=9378bd8dee4685787088fb23a6820134b6172753;hb=018a168b0ca16c5951106162e515d7949366d754;hp=890d33c66043744e5be6df7db6b5cda72191ad44;hpb=2abee6f6b5f1cf989224c64e6ab9091624a34248;p=helm.git diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index 890d33c66..9378bd8de 100644 --- a/helm/software/matita/library/nat/neper.ma +++ b/helm/software/matita/library/nat/neper.ma @@ -408,7 +408,7 @@ apply le_times_to_le_div ] qed. -theorem sigma_p_log_div: \forall n,b. S O < b \to +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! ). @@ -425,14 +425,14 @@ apply le_log_div_sigma_p ] qed. -theorem sigma_p_log_div1: \forall n,b. S O < b \to +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_div.assumption + [apply sigma_p_log_div1.assumption |apply le_times_to_le_div [apply lt_O_fact |rewrite > distributive_times_plus_sigma_p. @@ -460,18 +460,153 @@ apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\ ] ] 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 (S n) (\lambda i.leb (S n) (i*i)) (\lambda i.(prim i)*n!/i))*S(log b (S(S(S O)))/n! -). +\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_div1 - |unfold prim. -*) + [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 divides n m \to