From: Andrea Asperti Date: Thu, 13 Dec 2007 15:29:58 +0000 (+0000) Subject: Some inequalities. X-Git-Tag: make_still_working~5708 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2abee6f6b5f1cf989224c64e6ab9091624a34248;p=helm.git Some inequalities. --- diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma index 567e40ef6..fa935be03 100644 --- a/helm/software/matita/library/nat/chebyshev.ma +++ b/helm/software/matita/library/nat/chebyshev.ma @@ -676,13 +676,6 @@ apply (trans_eq ? ? [apply prime_to_lt_SO. apply primeb_true_to_prime. assumption - |apply (lt_to_le_to_lt ? x) - [apply prime_to_lt_O. - apply primeb_true_to_prime. - assumption - |apply leb_true_to_le. - assumption - ] |apply le_S_S_to_le. assumption ] @@ -900,7 +893,6 @@ apply eq_pi_p1;intros [apply prime_to_lt_SO. apply primeb_true_to_prime. assumption - |apply lt_to_le.assumption |apply le_times_n. apply lt_O_S ] @@ -1116,7 +1108,6 @@ cut ( [apply prime_to_lt_SO. apply primeb_true_to_prime. assumption - |assumption |simplify. apply le_plus_n_r ] @@ -1274,13 +1265,6 @@ elim H [apply prime_to_lt_SO. apply primeb_true_to_prime. assumption - |apply (lt_to_le_to_lt ? i) - [apply prime_to_lt_O. - apply primeb_true_to_prime. - assumption - |apply le_S_S_to_le. - assumption - ] |apply le_S.apply le_n ] ] @@ -1523,7 +1507,6 @@ rewrite < (eq_log_exp (S(S O))) in ⊢ (? % ?) [apply (trans_le ? ((log (S(S O)) (exp ((S(S O))*n) (S(prim ((S(S O))*n))))))) [apply le_log [apply le_n - |apply lt_O_exp.apply lt_O_S |apply le_exp_priml.assumption ] |rewrite > sym_times in ⊢ (? ? %). @@ -1555,513 +1538,3 @@ apply (trans_le ? (exp (A n) (S(S O)))) ] qed. - -(* da spostare *) -theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p. -intros.elim p - [reflexivity - |simplify.autobatch - ] -qed. - -theorem le_exp_log: \forall p,n. O < n \to -exp p ( -log n) \le n. -intros. -apply leb_true_to_le. -unfold log. -apply (f_max_true (\lambda x.leb (exp p x) n)). -apply (ex_intro ? ? O). -split - [apply le_O_n - |apply le_to_leb_true.simplify.assumption - ] -qed. - -theorem lt_log_n_n: \forall n. O < n \to log n < n. -intros. -cut (log n \le n) - [elim (le_to_or_lt_eq ? ? Hcut) - [assumption - |absurd (exp (S(S O)) n \le n) - [rewrite < H1 in ⊢ (? (? ? %) ?). - apply le_exp_log. - assumption - |apply lt_to_not_le. - apply lt_m_exp_nm. - apply le_n - ] - ] - |unfold log.apply le_max_n - ] -qed. - -theorem le_log_n_n: \forall n. log n \le n. -intro. -cases n - [apply le_n - |apply lt_to_le. - apply lt_log_n_n. - apply lt_O_S - ] -qed. - -theorem lt_exp_log: \forall n. n < exp (S(S O)) (S (log n)). -intro.cases n - [simplify.apply le_S.apply le_n - |apply not_le_to_lt. - apply leb_false_to_not_le. - apply (lt_max_to_false ? (S n1) (S (log (S n1)))) - [apply le_S_S.apply le_n - |apply lt_log_n_n.apply lt_O_S - ] - ] -qed. - -theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to -(\forall m. p < m \to f m = false) -\to max n f \le p. -intros. -apply not_lt_to_le.intro. -apply not_eq_true_false. -rewrite < (H1 ? H2). -apply sym_eq. -apply f_max_true. -assumption. -qed. - -theorem log_times1: \forall n,m. O < n \to O < m \to -log (n*m) \le S(log n+log m). -intros. -unfold in ⊢ (? (% ?) ?). -apply f_false_to_le_max - [apply (ex_intro ? ? O). - split - [apply le_O_n - |apply le_to_leb_true. - simplify. - rewrite > times_n_SO. - apply le_times;assumption - ] - |intros. - apply lt_to_leb_false. - apply (lt_to_le_to_lt ? ((exp (S(S O)) (S(log n)))*(exp (S(S O)) (S(log m))))) - [apply lt_times;apply lt_exp_log - |rewrite < exp_plus_times. - apply le_exp - [apply lt_O_S - |simplify. - rewrite < plus_n_Sm. - assumption - ] - ] - ] -qed. - -theorem log_times: \forall n,m.log (n*m) \le S(log n+log m). -intros. -cases n - [apply le_O_n - |cases m - [rewrite < times_n_O. - apply le_O_n - |apply log_times1;apply lt_O_S - ] - ] -qed. - -theorem log_exp: \forall n,m.O < m \to -log ((exp (S(S O)) n)*m)=n+log m. -intros. -unfold log in ⊢ (? ? (% ?) ?). -apply max_spec_to_max. -unfold max_spec. -split - [split - [elim n - [simplify. - rewrite < plus_n_O. - apply le_log_n_n - |simplify. - rewrite < plus_n_O. - rewrite > times_plus_l. - apply (trans_le ? (S((S(S O))\sup(n1)*m))) - [apply le_S_S.assumption - |apply (lt_O_n_elim ((S(S O))\sup(n1)*m)) - [rewrite > (times_n_O O) in ⊢ (? % ?). - apply lt_times - [apply lt_O_exp. - apply lt_O_S - |assumption - ] - |intro.simplify.apply le_S_S. - apply le_plus_n - ] - ] - ] - |simplify. - apply le_to_leb_true. - rewrite > exp_plus_times. - apply le_times_r. - apply le_exp_log. - assumption - ] - |intros. - simplify. - apply lt_to_leb_false. - apply (lt_to_le_to_lt ? ((exp (S(S O)) n)*(exp (S(S O)) (S(log m))))) - [apply lt_times_r1 - [apply lt_O_exp.apply lt_O_S - |apply lt_exp_log. - ] - |rewrite < exp_plus_times. - apply le_exp - [apply lt_O_S - |rewrite < plus_n_Sm. - assumption - ] - ] - ] -qed. - -theorem log_SSO: \forall n. O < n \to -log ((S(S O))*n) = S (log n). -intros. -change with (log ((exp (S(S O)) (S O))*n)=S (log n)). -rewrite > log_exp.reflexivity.assumption. -qed. - -theorem or_eq_S: \forall n.\exists m. -(n = (S(S O))*m) \lor (n = S((S(S O))*m)). -intro. -elim n - [apply (ex_intro ? ? O).left.apply times_n_O - |elim H.elim H1 - [apply (ex_intro ? ? a).right.apply eq_f.assumption - |apply (ex_intro ? ? (S a)).left. - rewrite > H2.simplify. - rewrite < plus_n_O. - rewrite < plus_n_Sm. - reflexivity - ] - ] -qed. - -theorem lt_O_to_or_eq_S: \forall n.O < n \to \exists m.m < n \land -((n = (S(S O))*m) \lor (n = S((S(S O))*m))). -intros. -elim (or_eq_S n). -elim H1 - [apply (ex_intro ? ? a).split - [rewrite > H2. - rewrite > times_n_SO in ⊢ (? % ?). - rewrite > sym_times. - apply lt_times_l1 - [apply (divides_to_lt_O a n ? ?) - [assumption - |apply (witness a n (S (S O))). - rewrite > sym_times. - assumption - ] - |apply le_n - ] - |left.assumption - ] - |apply (ex_intro ? ? a).split - [rewrite > H2. - apply (le_to_lt_to_lt ? ((S(S O))*a)) - [rewrite > times_n_SO in ⊢ (? % ?). - rewrite > sym_times. - apply le_times_l. - apply le_n_Sn - |apply le_n - ] - |right.assumption - ] - ] -qed. - -theorem factS: \forall n. fact (S n) = (S n)*(fact n). -intro.simplify.reflexivity. -qed. - -theorem exp_S: \forall n,m. exp m (S n) = m*exp m n. -intros.reflexivity. -qed. - -lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)). -intro.simplify.rewrite < plus_n_Sm.reflexivity. -qed. - -theorem fact1: \forall n. -fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n). -intro.elim n - [rewrite < times_n_O.apply le_n - |rewrite > times_SSO. - rewrite > factS. - rewrite > factS. - rewrite < assoc_times. - rewrite > factS. - apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1))))) - [apply le_times_l. - rewrite > times_SSO. - apply le_times_r. - apply le_n_Sn - |rewrite > assoc_times. - rewrite > assoc_times. - rewrite > assoc_times in ⊢ (? ? %). - rewrite > exp_S. - rewrite > assoc_times in ⊢ (? ? %). - apply le_times_r. - rewrite < assoc_times. - rewrite < assoc_times. - rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?). - rewrite > assoc_times. - rewrite > assoc_times. - rewrite > exp_S. - rewrite > assoc_times in ⊢ (? ? %). - apply le_times_r. - rewrite > sym_times in ⊢ (? ? %). - rewrite > assoc_times in ⊢ (? ? %). - rewrite > assoc_times in ⊢ (? ? %). - apply le_times_r. - rewrite < assoc_times in ⊢ (? ? %). - rewrite < assoc_times in ⊢ (? ? %). - rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)). - rewrite > assoc_times in ⊢ (? ? %). - rewrite > assoc_times in ⊢ (? ? %). - apply le_times_r. - rewrite > sym_times in ⊢ (? ? (? ? %)). - rewrite > sym_times in ⊢ (? ? %). - assumption - ] - ] -qed. - -theorem monotonic_log: monotonic nat le log. -unfold monotonic.intros. -elim (le_to_or_lt_eq ? ? H) 0 - [cases x;intro - [apply le_O_n - |apply lt_S_to_le. - apply (lt_exp_to_lt (S(S O))) - [apply le_n - |apply (le_to_lt_to_lt ? (S n)) - [apply le_exp_log. - apply lt_O_S - |apply (trans_lt ? y) - [assumption - |apply lt_exp_log - ] - ] - ] - ] - |intro.rewrite < H1.apply le_n - ] -qed. - -theorem lt_O_fact: \forall n. O < fact n. -intro.elim n - [simplify.apply lt_O_S - |rewrite > factS. - rewrite > (times_n_O O). - apply lt_times - [apply lt_O_S - |assumption - ] - ] -qed. - -theorem fact2: \forall n.O < n \to -(exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)). -intros.elim H - [simplify.apply le_S.apply le_n - |rewrite > times_SSO. - rewrite > factS. - rewrite > factS. - rewrite < assoc_times. - rewrite > factS. - rewrite < times_SSO in ⊢ (? ? %). - apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!))) - [rewrite > assoc_times in ⊢ (? ? %). - rewrite > exp_S. - rewrite > assoc_times. - rewrite > assoc_times. - rewrite > assoc_times. - apply lt_times_r. - rewrite > exp_S. - rewrite > assoc_times. - rewrite > sym_times in ⊢ (? ? %). - rewrite > assoc_times in ⊢ (? ? %). - rewrite > assoc_times in ⊢ (? ? %). - apply lt_times_r. - rewrite > sym_times. - rewrite > assoc_times. - rewrite > assoc_times. - apply lt_times_r. - rewrite < assoc_times. - rewrite < assoc_times. - rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?). - rewrite > assoc_times. - rewrite > assoc_times. - rewrite > sym_times in ⊢ (? ? %). - apply lt_times_r. - rewrite < assoc_times. - rewrite < sym_times. - rewrite < assoc_times. - assumption - |apply lt_times_l1 - [rewrite > (times_n_O O) in ⊢ (? % ?). - apply lt_times - [rewrite > (times_n_O O) in ⊢ (? % ?). - apply lt_times - [apply lt_O_S - |apply lt_O_S - ] - |apply lt_O_fact - ] - |apply le_n - ] - ] - ] -qed. - -theorem lt_O_log: \forall n. S O < n \to O < log n. -intros.elim H - [simplify.apply lt_O_S - |apply (lt_to_le_to_lt ? (log n1)) - [assumption - |apply monotonic_log. - apply le_n_Sn - ] - ] -qed. - -theorem log_fact_SSSO: log (fact (S(S(S O)))) = S (S O). -reflexivity. -qed. - -lemma exp_SSO_SSO: exp (S(S O)) (S(S O)) = S(S(S(S O))). -reflexivity. -qed. -(* -theorem log_fact_SSSSO: log (fact (S(S(S(S O))))) = S(S(S(S O))). -reflexivity. -qed. -*) -theorem log_fact_SSSSSO: log (fact (S(S(S(S(S O)))))) = S(S(S(S O))). -reflexivity. -qed. - -theorem bof_bof: \forall n.(S(S(S(S O)))) < n \to -n \le (S(S(S(S(S(S(S(S O)))))))) \to log (fact n) < n*log n - n. -intros. -elim H - [rewrite > factS in ⊢ (? (? %) ?). - rewrite > factS in ⊢ (? (? (? ? %)) ?). - rewrite < assoc_times in ⊢ (? (? %) ?). - rewrite < sym_times in ⊢ (? (? (? % ?)) ?). - rewrite > assoc_times in ⊢ (? (? %) ?). - change with (exp (S(S O)) (S(S O))) in ⊢ (? (? (? % ?)) ?). - -theorem bof: \forall n.(S(S(S(S O))))) < n \to log (fact n) < n*log n - n. -intro.apply (nat_elim1 n). -intros. -elim (lt_O_to_or_eq_S m) - [elim H2.clear H2. - elim H4.clear H4. - rewrite > H2. - apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a)))) - [apply monotonic_log. - apply fact1 - |rewrite > assoc_times in ⊢ (? (? %) ?). - rewrite > log_exp. - apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!))) - [apply le_plus_r. - apply log_times - |rewrite > plus_n_Sm. - rewrite > log_SSO. - rewrite < times_n_Sm. - apply (le_to_lt_to_lt ? ((S(S O))*a+(log a!+(a*log a-a)))) - [apply le_plus_r. - apply le_plus_r. - apply H.assumption - |apply (lt_to_le_to_lt ? ((S(S O))*a+((a*log a-a)+(a*log a-a)))) - [apply lt_plus_r. - apply lt_plus_l. - apply H. - assumption. - |rewrite > times_SSO_n. - rewrite > distr_times_minus. - rewrite > sym_plus. - rewrite > plus_minus - [rewrite > sym_plus. - rewrite < assoc_times. - apply le_n - |rewrite < assoc_times. - rewrite > times_n_SO in ⊢ (? % ?). - apply le_times - [apply le_n - |apply lt_O_log. - apply (lt_times_n_to_lt_r (S(S O))) - [apply lt_O_S - |rewrite < times_n_SO. - rewrite < H2. - assumption - ] - ] - ] - ] - - . - ] - | - rewrite < eq_plus_minus_minus_plus. - - rewrite > assoc_plus. - apply lt_plus_r. - rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?). - change with - (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)). - apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a)))) - [apply le_S_S. - apply lt_plus_r. - apply lt_times_r. - apply H. - assumption - | - -theorem stirling: \forall n,k.k \le n \to -log (fact n) < n*log n - n + k*log n. -intro. -apply (nat_elim1 n). -intros. -elim (lt_O_to_or_eq_S m) - [elim H2.clear H2. - elim H4.clear H4. - rewrite > H2. - apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a)))) - [apply monotonic_log. - apply fact1 - |rewrite > assoc_times in ⊢ (? (? %) ?). - rewrite > log_exp. - apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!))) - [apply le_plus_r. - apply log_times - |rewrite < plus_n_Sm. - rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?). - change with - (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)). - apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a)))) - [apply le_S_S. - apply lt_plus_r. - apply lt_times_r. - apply H. - assumption - | - - [ - - a*log a-a+k*log a - -*) \ No newline at end of file diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma index 53200b161..39d9b2ecd 100644 --- a/helm/software/matita/library/nat/log.ma +++ b/helm/software/matita/library/nat/log.ma @@ -159,6 +159,50 @@ cases n ] qed. +theorem log_times_l: \forall p,n,m.O < n \to O < m \to S O < p \to +log p n+log p m \le log p (n*m) . +intros. +unfold log in ⊢ (? ? (% ? ?)). +apply f_m_to_le_max + [elim H + [rewrite > log_SO + [simplify. + rewrite < plus_n_O. + apply le_log_n_n. + assumption + |assumption + ] + |elim H1 + [rewrite > log_SO + [rewrite < plus_n_O. + rewrite < times_n_SO. + apply le_log_n_n. + assumption + |assumption + ] + |apply (trans_le ? (S n1 + S n2)) + [apply le_plus;apply le_log_n_n;assumption + |simplify. + apply le_S_S. + rewrite < plus_n_Sm. + change in ⊢ (? % ?) with ((S n1)+n2). + rewrite > sym_plus. + apply le_plus_r. + change with (n1 < n1*S n2). + rewrite > times_n_SO in ⊢ (? % ?). + apply lt_times_r1 + [assumption + |apply le_S_S.assumption + ] + ] + ] + ] + |apply le_to_leb_true. + rewrite > exp_plus_times. + apply le_times;apply le_exp_log;assumption + ] +qed. + theorem log_exp: \forall p,n,m.S O < p \to O < m \to log p ((exp p n)*m)=n+log p m. intros. @@ -286,6 +330,30 @@ intros.elim H1 [constructor 1 |apply (trans_le ? ? ? H3);apply le_log_plus;assumption] qed. + +theorem log_div: \forall p,n,m. S O < p \to O < m \to m \le n \to +log p (n/m) \le log p n -log p m. +intros. +apply le_plus_to_minus_r. +apply (trans_le ? (log p ((n/m)*m))) + [apply log_times_l + [apply le_times_to_le_div + [assumption + |rewrite < times_n_SO. + assumption + ] + |assumption + |assumption + ] + |apply le_log + [assumption + |rewrite > (div_mod n m) in ⊢ (? ? %) + [apply le_plus_n_r + |assumption + ] + ] + ] +qed. theorem log_n_n: \forall n. S O < n \to log n n = S O. intros. diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma index 51f65ef4a..890d33c66 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 @@ -355,6 +356,123 @@ elim b |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_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 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_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 (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 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 (S n) (\lambda i.leb (S n) (i*i)) (\lambda i.(prim i)*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. +*) + + (* 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