1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/neper".
17 include "nat/iteration2.ma".
18 include "nat/div_and_mod_diseq.ma".
19 include "nat/binomial.ma".
21 include "nat/chebyshev.ma".
23 theorem sigma_p_div_exp: \forall n,m.
24 sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le
25 ((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
29 |rewrite > true_to_sigma_p_Sn
30 [apply (trans_le ? (m/(S(S O))\sup(n1)+((S(S O))*m*(S(S O))\sup(n1)-(S(S O))*m)/(S(S O))\sup(n1)))
31 [apply le_plus_r.assumption
32 |rewrite > assoc_times in ⊢ (? ? (? (? % ?) ?)).
33 rewrite < distr_times_minus.
34 change in ⊢ (? ? (? ? %)) with ((S(S O))*(exp (S(S O)) n1)).
35 rewrite > sym_times in ⊢ (? ? (? % ?)).
36 rewrite > sym_times in ⊢ (? ? (? ? %)).
37 rewrite < lt_to_lt_to_eq_div_div_times_times
38 [apply (trans_le ? ((m+((S(S O))*m*((S(S O)))\sup(n1)-(S(S O))*m))/((S(S O)))\sup(n1)))
42 |change in ⊢ (? (? (? ? (? ? %)) ?) ?) with (m + (m +O)).
44 rewrite < eq_minus_minus_minus_plus.
46 rewrite > sym_times in ⊢ (? (? (? (? (? (? % ?) ?) ?) ?) ?) ?).
47 rewrite > assoc_times.
48 rewrite < plus_minus_m_m
50 |apply le_plus_to_minus_r.
51 rewrite > plus_n_O in ⊢ (? (? ? %) ?).
52 change in ⊢ (? % ?) with ((S(S O))*m).
55 rewrite > times_n_SO in ⊢ (? % ?).
71 theorem le_fact_exp: \forall i,m. i \le m \to m!≤ m \sup i*(m-i)!.
74 simplify.rewrite < plus_n_O.
77 apply (trans_le ? ((m)\sup(n)*(m-n)!))
79 apply lt_to_le.assumption
80 |rewrite > sym_times in ⊢ (? ? (? % ?)).
81 rewrite > assoc_times.
83 generalize in match H1.
86 apply (lt_to_not_le ? ? H2).
88 |rewrite > minus_Sn_m.
100 theorem le_fact_exp1: \forall n. S O < n \to (S(S O))*n!≤ n \sup n.
103 |change with ((S(S O))*((S n1)*(fact n1)) \le (S n1)*(exp (S n1) n1)).
104 rewrite < assoc_times.
105 rewrite < sym_times in ⊢ (? (? % ?) ?).
106 rewrite > assoc_times.
108 apply (trans_le ? (exp n1 n1))
110 |apply monotonic_exp1.
116 theorem le_exp_sigma_p_exp: \forall n. (exp (S n) n) \le
117 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
119 rewrite > exp_S_sigma_p.
122 apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
123 [rewrite > sym_times.
126 rewrite < eq_div_div_div_times
129 |apply le_times_to_le_div2
139 |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
140 [rewrite > exp_plus_times.
141 apply le_times_div_div_times.
149 theorem lt_exp_sigma_p_exp: \forall n. S O < n \to
151 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
153 rewrite > exp_S_sigma_p.
156 apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
157 [rewrite > sym_times.
160 rewrite < eq_div_div_div_times
163 |apply le_times_to_le_div2
173 |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
174 [rewrite > exp_plus_times.
175 apply le_times_div_div_times.
181 |apply (ex_intro ? ? n).
187 |rewrite < minus_n_n.
190 apply le_times_to_le_div
192 |rewrite > sym_times.
200 theorem le_exp_SSO_fact:\forall n.
201 exp (S(S O)) (pred n) \le n!.
204 |change with ((S(S O))\sup n1 ≤(S n1)*n1!).
205 apply (nat_case1 n1);intros
207 |change in ⊢ (? % ?) with ((S(S O))*exp (S(S O)) (pred (S m))).
209 [apply le_S_S.apply le_S_S.apply le_O_n
210 |rewrite < H1.assumption
216 theorem lt_SO_to_lt_exp_Sn_n_SSSO: \forall n. S O < n \to
217 (exp (S n) n) < (S(S(S O)))*(exp n n).
219 apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
220 [apply lt_exp_sigma_p_exp.assumption
221 |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
222 [apply le_sigma_p.intros.
223 apply le_times_to_le_div
226 |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
227 [apply le_times_div_div_times.
229 |apply le_times_to_le_div2
231 |rewrite < sym_times.
233 apply le_exp_SSO_fact
237 |rewrite > eq_sigma_p_pred
240 change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
242 apply (trans_le ? (((S(S O))*(exp n n)*(exp (S(S O)) n) - (S(S O))*(exp n n))/(exp (S(S O)) n)))
243 [apply sigma_p_div_exp
244 |apply le_times_to_le_div2
256 theorem lt_exp_Sn_n_SSSO: \forall n.
257 (exp (S n) n) < (S(S(S O)))*(exp n n).
259 [simplify.apply le_S.apply le_n
262 |apply lt_SO_to_lt_exp_Sn_n_SSSO.
263 apply le_S_S.apply le_S_S.apply le_O_n
268 theorem lt_exp_Sn_m_SSSO: \forall n,m. O < m \to
270 (exp (S n) m) < (exp (S(S(S O))) (m/n)) *(exp n m).
272 elim H1.rewrite > H2.
273 rewrite < exp_exp_times.
274 rewrite < exp_exp_times.
275 rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?)).
276 rewrite > lt_O_to_div_times
277 [rewrite > times_exp.
279 [apply (O_lt_times_to_O_lt ? n).
283 |apply lt_exp_Sn_n_SSSO
285 |apply (O_lt_times_to_O_lt ? n2).
291 theorem le_log_exp_Sn_log_exp_n: \forall n,m,p. O < m \to S O < p \to
293 log p (exp (S n) m) \le S((m/n)*S(log p (S(S(S O))))) + log p (exp n m).
295 apply (trans_le ? (log p (((S(S(S O))))\sup(m/n)*((n)\sup(m)))))
299 apply lt_exp_Sn_m_SSSO;assumption
301 |apply (trans_le ? (S(log p (exp (S(S(S O))) (m/n)) + log p (exp n m))))
304 |change in ⊢ (? ? %) with (S (m/n*S (log p (S(S(S O))))+log p ((n)\sup(m)))).
313 theorem le_log_exp_fact_sigma_p: \forall a,b,n,p. S O < p \to
314 O < a \to a \le b \to b \le n \to
315 log p (exp b n!) - log p (exp a n!) \le
316 sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))).
320 apply (lt_O_n_elim ? (lt_O_fact n)).intro.
322 |apply (bool_elim ? (leb a n1));intro
323 [rewrite > true_to_sigma_p_Sn
324 [apply (trans_le ? (S (n!/n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(n!))-log p ((a)\sup(n!)))))
327 [apply le_plus_to_minus_r.
328 rewrite < plus_minus_m_m
330 apply le_log_exp_Sn_log_exp_n
334 [apply (trans_le ? ? ? H1);apply leb_true_to_le;assumption
335 |apply lt_to_le;assumption]]
339 [rewrite > Hcut;apply monotonic_exp1;constructor 2;
340 apply leb_true_to_le;assumption
343 |simplify;rewrite > exp_plus_times;rewrite < H6;
344 rewrite > sym_times;rewrite < times_n_O;reflexivity]]]]
347 |apply monotonic_exp1;apply leb_true_to_le;assumption]]
348 |rewrite > sym_plus;rewrite > sym_plus in \vdash (? ? %);apply le_minus_to_plus;
349 rewrite < minus_plus_m_m;apply H3;apply lt_to_le;assumption]
351 |lapply (not_le_to_lt ? ? (leb_false_to_not_le ? ? H5));
352 rewrite > eq_minus_n_m_O
356 |apply monotonic_exp1;assumption]]]]
359 theorem le_exp_div:\forall n,m,q. O < m \to
360 exp (n/m) q \le (exp n q)/(exp m q).
362 apply le_times_to_le_div
365 |rewrite > times_exp.
367 apply monotonic_exp1.
368 rewrite > (div_mod n m) in ⊢ (? ? %)
375 theorem le_log_div_sigma_p: \forall a,b,n,p. S O < p \to
376 O < a \to a \le b \to b \le n \to
378 (sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))))/n!.
380 apply le_times_to_le_div
382 |apply (trans_le ? (log p (exp (b/a) n!)))
385 |apply le_times_to_le_div
387 |rewrite < times_n_SO.
391 |apply (trans_le ? (log p ((exp b n!)/(exp a n!))))
394 |apply le_exp_div.assumption
396 |apply (trans_le ? (log p (exp b n!) - log p (exp a n!)))
401 |apply monotonic_exp1.
404 |apply le_log_exp_fact_sigma_p;assumption
411 theorem sigma_p_log_div1: \forall n,b. S O < b \to
412 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
413 \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!
416 apply le_sigma_p.intros.
417 apply le_log_div_sigma_p
419 |apply prime_to_lt_O.
420 apply primeb_true_to_prime.
421 apply (andb_true_true ? ? H2)
428 theorem sigma_p_log_div2: \forall n,b. S O < b \to
429 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
431 (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!).
433 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!
435 [apply sigma_p_log_div1.assumption
436 |apply le_times_to_le_div
438 |rewrite > distributive_times_plus_sigma_p.
439 rewrite < sym_times in ⊢ (? ? %).
440 rewrite > distributive_times_plus_sigma_p.
441 apply le_sigma_p.intros.
442 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!)))
443 [apply le_times_div_div_times.
445 |rewrite > sym_times.
446 rewrite > lt_O_to_div_times
447 [rewrite > distributive_times_plus_sigma_p.
448 apply le_sigma_p.intros.
449 rewrite < times_n_Sm in ⊢ (? ? %).
453 [apply le_S_S.apply le_O_n
454 |rewrite < sym_times.
464 theorem sigma_p_log_div: \forall n,b. S O < b \to
465 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
466 \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!
469 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!))
470 [apply sigma_p_log_div2.assumption
476 (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p))
477 (λp:nat.sigma_p n (λi:nat.leb p i) (λi:nat.S (n!/i)))
478 = sigma_p n (λi:nat.leb (S n) (i*i))
479 (λ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))))
481 apply le_sigma_p.intros.
483 rewrite > distributive_times_plus_sigma_p.
484 rewrite < times_n_SO.
486 (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i))
487 = sigma_p (S i) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i)))
489 apply le_sigma_p1.intros.
491 rewrite < andb_sym in ⊢ (? (? (? (? ? %)) ?) ?).
492 apply (bool_elim ? (leb i1 i));intros
493 [apply (bool_elim ? (leb (S n) (i1*i1)));intros
499 |apply or_false_to_eq_sigma_p
500 [apply le_S.assumption
502 left.rewrite > (lt_to_leb_false i1 i)
503 [rewrite > andb_sym.reflexivity
508 |apply sigma_p_sigma_p.intros.
509 apply (bool_elim ? (leb x y));intros
510 [apply (bool_elim ? (leb (S n) (x*x)));intros
511 [rewrite > le_to_leb_true in ⊢ (? ? ? (? % ?))
513 |apply (trans_le ? (x*x))
514 [apply leb_true_to_le.assumption
515 |apply le_times;apply leb_true_to_le;assumption
518 |rewrite < andb_sym in ⊢ (? ? (? % ?) ?).
519 rewrite < andb_sym in ⊢ (? ? ? (? ? (? % ?))).
520 rewrite < andb_sym in ⊢ (? ? ? %).
524 rewrite > andb_assoc in ⊢ (? ? ? %).
525 rewrite < andb_sym in ⊢ (? ? ? (? % ?)).
533 theorem le_sigma_p_div_log_div_pred_log : \forall n,b,m. S O < b \to b*b \leq n \to
534 sigma_p (S n) (\lambda i.leb (S n) (i*i)) (\lambda i.m/(log b i))
535 \leq ((S (S O)) * n * m)/(pred (log b n)).
537 apply (trans_le ? (sigma_p (S n)
538 (\lambda i.leb (S n) (i*i)) (\lambda i.(S (S O))*m/(pred (log b n)))))
539 [apply le_sigma_p;intros;apply le_times_to_le_div
540 [rewrite > minus_n_O in ⊢ (? ? (? %));rewrite < eq_minus_S_pred;
541 apply le_plus_to_minus_r;simplify;
542 rewrite < (eq_log_exp b ? H);
545 |simplify;rewrite < times_n_SO;assumption]
546 |apply (trans_le ? ((pred (log b n) * m)/log b i))
547 [apply le_times_div_div_times;apply lt_O_log
548 [elim (le_to_or_lt_eq ? ? (le_O_n i))
550 |apply False_ind;apply not_eq_true_false;rewrite < H3;rewrite < H4;
552 |apply (le_exp_to_le1 ? ? (S (S O)))
554 |apply (trans_le ? (S n))
555 [apply le_S;simplify;rewrite < times_n_SO;assumption
556 |rewrite > exp_SSO;apply leb_true_to_le;assumption]]]
557 |apply le_times_to_le_div2
559 [elim (le_to_or_lt_eq ? ? (le_O_n i))
561 |apply False_ind;apply not_eq_true_false;rewrite < H3;rewrite < H4;
563 |apply (le_exp_to_le1 ? ? (S (S O)))
565 |apply (trans_le ? (S n))
566 [apply le_S;simplify;rewrite < times_n_SO;assumption
567 |rewrite > exp_SSO;apply leb_true_to_le;assumption]]]
568 |rewrite > sym_times in \vdash (? ? %);rewrite < assoc_times;
569 apply le_times_l;rewrite > sym_times;
570 rewrite > minus_n_O in \vdash (? (? %) ?);
571 rewrite < eq_minus_S_pred;apply le_plus_to_minus;
572 simplify;rewrite < plus_n_O;apply (trans_le ? (log b (i*i)))
575 |apply lt_to_le;apply leb_true_to_le;assumption]
576 |rewrite > sym_plus;simplify;apply log_times;assumption]]]]
577 |rewrite > times_n_SO in \vdash (? (? ? ? (\lambda i:?.%)) ?);
578 rewrite < distributive_times_plus_sigma_p;
579 apply (trans_le ? ((((S (S O))*m)/(pred (log b n)))*n))
580 [apply le_times_r;apply (trans_le ? (sigma_p (S n) (\lambda i:nat.leb (S O) (i*i)) (\lambda Hbeta1:nat.S O)))
581 [apply le_sigma_p1;intros;do 2 rewrite < times_n_SO;
582 apply (bool_elim ? (leb (S n) (i*i)))
583 [intro;cut (leb (S O) (i*i) = true)
584 [rewrite > Hcut;apply le_n
585 |apply le_to_leb_true;apply (trans_le ? (S n))
586 [apply le_S_S;apply le_O_n
587 |apply leb_true_to_le;assumption]]
588 |intro;simplify in \vdash (? % ?);apply le_O_n]
591 |apply (bool_elim ? (leb (S O) ((S n1)*(S n1))));intro
592 [rewrite > true_to_sigma_p_Sn
593 [change in \vdash (? % ?) with (S (sigma_p (S n1) (\lambda i:nat.leb (S O) (i*i)) (\lambda Hbeta1:nat.S O)));
594 apply le_S_S;assumption
596 |rewrite > false_to_sigma_p_Sn
597 [apply le_S;assumption
599 |rewrite > sym_times in \vdash (? % ?);
600 rewrite > sym_times in \vdash (? ? (? (? % ?) ?));
601 rewrite > assoc_times;
602 apply le_times_div_div_times;
603 rewrite > minus_n_O in ⊢ (? ? (? %));rewrite < eq_minus_S_pred;
604 apply le_plus_to_minus_r;simplify;
605 rewrite < (eq_log_exp b ? H);
608 |simplify;rewrite < times_n_SO;assumption]]]
611 (* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to
613 log p (exp n m) - log p (exp a m) \le
614 sigma_p (S n) (\lambda i.leb (S a) i) (\lambda i.S((m/i)*S(log p (S(S(S O)))))).
617 [rewrite > false_to_sigma_p_Sn.
619 apply (lt_O_n_elim ? H).intro.
620 simplify.apply le_O_n
621 |apply (bool_elim ? (leb a n1));intro
622 [rewrite > true_to_sigma_p_Sn
623 [apply (trans_le ? (S (m/S n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(m))-log p ((a)\sup(m)))))
626 [apply le_plus_to_minus_r.
627 rewrite < plus_minus_m_m
629 apply le_log_exp_Sn_log_exp_n.
633 theorem le_exp_sigma_p_exp_m: \forall m,n. (exp (S m) n) \le
634 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
636 rewrite > exp_S_sigma_p.
639 apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
640 [rewrite > sym_times.
643 rewrite < eq_div_div_div_times
646 |apply le_times_to_le_div2
656 |apply le_times_div_div_times.
661 theorem lt_exp_sigma_p_exp_m: \forall m,n. S O < n \to
663 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
665 rewrite > exp_S_sigma_p.
668 apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
669 [rewrite > sym_times.
672 rewrite < eq_div_div_div_times
675 |apply le_times_to_le_div2
685 |apply le_times_div_div_times.
688 |apply (ex_intro ? ? n).
694 |rewrite < minus_n_n.
697 apply le_times_to_le_div
699 |rewrite > sym_times.
708 theorem lt_SO_to_lt_exp_Sn_n_SSSO_bof: \forall m,n. S O < n \to
709 (exp (S m) n) < (S(S(S O)))*(exp m n).
711 apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!))))
712 [apply lt_exp_sigma_p_exp_m.assumption
713 |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
714 [apply le_sigma_p.intros.
715 apply le_times_to_le_div
718 |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
719 [apply le_times_div_div_times.
721 |apply le_times_to_le_div2
723 |rewrite < sym_times.
725 apply le_exp_SSO_fact
729 |rewrite > eq_sigma_p_pred
732 change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
734 apply (trans_le ? (((S(S O))*(exp n n)*(exp (S(S O)) n) - (S(S O))*(exp n n))/(exp (S(S O)) n)))
735 [apply sigma_p_div_exp
736 |apply le_times_to_le_div2