2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/chebyshev/chebyshev_teta.ma".
14 (* include "nat/sqrt.ma".
15 include "nat/chebyshev_teta.ma".
16 include "nat/chebyshev.ma".
18 include "list/sort.ma".
20 include "nat/sieve.ma". *)
23 let rec list_divides l n \def
26 | cons (m:nat) (tl:list nat) ⇒ orb (divides_b m n) (list_divides tl n) ].
28 definition lprim : nat \to list nat \def
29 \lambda n.let rec aux m acc \def
32 | S m1 => match (list_divides acc (n-m1)) with
34 | false => aux m1 (n-m1::acc)]]
37 let rec checker l \def
40 | cons h1 t1 => match t1 with
42 | cons h2 t2 => (andb (checker t1) (leb h1 (2*h2))) ]].
44 lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true.
45 intros 2;simplify;intro;elim l in H ⊢ %
47 |change in H1 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
48 apply (andb_true_true ? ? H1)]
51 theorem checker_sound : \forall l1,l2,l,x,y.l = l1@(x::y::l2) \to
52 checker l = true \to x \leq 2*y.
54 [simplify;intros 5;rewrite > H;simplify;intro;
55 apply leb_true_to_le;apply (andb_true_true_r ? ? H1);
56 |simplify;intros;rewrite > H1 in H2;lapply (checker_cons ? ? H2);
57 apply (H l2 ? ? ? ? Hletin);reflexivity]
61 definition bertrand ≝ λn. ∃p.n < p ∧ p \le 2*n ∧ (prime p).
63 definition not_bertrand ≝ λn.∀p.n < p → p ≤ 2*n → \not (prime p).
65 lemma min_prim : ∀n.∃p. n < p ∧ prime p ∧
66 ∀q.prime q → q < p → q ≤ n.
67 #n cases (le_to_or_lt_eq ?? (le_O_n n)) #Hn
68 [%{(min (S (n!)) (S n) primeb)} %
70 |@primeb_true_to_prime @(f_min_true primeb)
71 cases (ex_prime n Hn) #p * * #ltnp #lep #primep
73 [% [@ltnp | whd >(plus_n_O p) >plus_n_Sm @le_plus //]
74 |@prime_to_primeb_true //
77 |#p #primep #ltp @not_lt_to_le % #ltnp
78 lapply (lt_min_to_false … ltnp ltp)
79 >(prime_to_primeb_true ? primep) #H destruct (H)
82 [%[<Hn @lt_O_S | @primeb_true_to_prime //]
83 |#p #primep #lt2 @False_ind @(absurd … lt2)
84 @le_to_not_lt @prime_to_lt_SO //
89 theorem list_of_primes_to_bertrand: \forall n,pn,l.0 < n \to prime pn \to n <pn \to
90 list_of_primes pn l \to
91 (\forall p. prime p \to p \le pn \to in_list nat p l) \to
92 (\forall p. in_list nat p l \to 2 < p \to
93 \exists pp. in_list nat pp l \land pp < p \land p \le 2*pp) \to bertrand n.
96 apply (ex_intro ? ? a).
97 elim H6.clear H6.elim H7.clear H7.
101 |elim (le_to_or_lt_eq ? ? (prime_to_lt_SO ? H9))
103 [elim H10.clear H10.elim H11.clear H11.
104 apply (trans_le ? ? ? H12).
114 |apply not_lt_to_le.intro.
115 apply (lt_to_not_le ? ? H2).
121 apply O_lt_const_to_le_times_const.
129 let rec check_list l \def
131 [ nil \Rightarrow true
132 | cons (hd:nat) tl \Rightarrow
134 [ nil \Rightarrow eqb hd 2
135 | cons hd1 tl1 \Rightarrow
136 (leb (S hd1) hd \land leb hd (2*hd1) \land check_list tl)
141 lemma check_list1: \forall n,m,l.(check_list (n::m::l)) = true \to
142 m < n \land n \le 2*m \land (check_list (m::l)) = true \land ((check_list l) = true).
144 change in ⊢ (? ? % ?→?) with (leb (S m) n \land leb n (2*m) \land check_list (m::l)).
146 lapply (andb_true_true ? ? H) as H1.
147 lapply (andb_true_true_r ? ? H) as H2.clear H.
148 lapply (andb_true_true ? ? H1) as H3.
149 lapply (andb_true_true_r ? ? H1) as H4.clear H1.
153 [apply leb_true_to_le.assumption
154 |apply leb_true_to_le.assumption
158 |generalize in match H2.
161 |change in ⊢ (? ? % ?→?) with (leb (S n1) m \land leb m (2*n1) \land check_list (n1::l1)).
163 lapply (andb_true_true_r ? ? H) as H2.
169 theorem check_list2: \forall l. check_list l = true \to
170 \forall p. in_list nat p l \to 2 < p \to
171 \exists pp. in_list nat pp l \land pp < p \land p \le 2*pp.
173 [intros.apply False_ind.apply (not_in_list_nil ? ? H1)
175 [lapply (in_list_singleton_to_eq ? ? ? H2) as H4.
177 apply (lt_to_not_eq ? ? H3).
178 apply sym_eq.apply eqb_true_to_eq.
179 rewrite > H4.apply H1
180 |elim (check_list1 ? ? ? H1).clear H1.
183 elim (in_list_cons_case ? ? ? ? H2)
184 [apply (ex_intro ? ? n).
187 [apply in_list_cons.apply in_list_head
188 |rewrite > H1.assumption
190 |rewrite > H1.assumption
192 |elim (H H6 p H1 H3).clear H.
193 apply (ex_intro ? ? a1).
198 [apply in_list_cons.assumption
208 (* qualcosa che non va con gli S *)
209 lemma le_to_bertrand : \forall n.O < n \to n \leq exp 2 8 \to bertrand n.
211 apply (list_of_primes_to_bertrand ? (S(exp 2 8)) (sieve (S(exp 2 8))))
213 |apply primeb_true_to_prime.reflexivity
214 |apply (le_to_lt_to_lt ? ? ? H1).
216 |lapply (sieve_sound1 (S(exp 2 8))) as H
218 |apply leb_true_to_le.reflexivity
220 |intros.apply (sieve_sound2 ? ? H3 H2)
226 lemma not_not_bertrand_to_bertrand1: \forall n.
227 \lnot (not_bertrand n) \to \forall x. n \le x \to x \le 2*n \to
228 (\forall p.x < p \to p \le 2*n \to \not (prime p))
229 \to \exists p.n < p \land p \le x \land (prime p).
231 [apply False_ind.apply H.assumption
232 |apply (bool_elim ? (primeb (S n1)));intro
233 [apply (ex_intro ? ? (S n1)).
236 [apply le_S_S.assumption
239 |apply primeb_true_to_prime.assumption
244 apply (ex_intro ? ? a).
248 |apply le_S.assumption
252 |apply lt_to_le.assumption
253 |elim (le_to_or_lt_eq ? ? H7)
256 apply primeb_false_to_not_prime.
264 theorem not_not_bertrand_to_bertrand: \forall n.
265 \lnot (not_bertrand n) \to bertrand n.
266 unfold bertrand.intros.
267 apply (not_not_bertrand_to_bertrand1 ? ? (2*n))
269 |apply le_times_n.apply le_n_Sn
271 |intros.apply False_ind.
272 apply (lt_to_not_le ? ? H1 H2)
278 definition k \def \lambda n,p.
279 sigma_p (log p n) (λi:nat.true) (λi:nat.((n/(exp p (S i))\mod 2))).
281 theorem le_k: \forall n,p. k n p \le log p n.
282 intros.unfold k.elim (log p n)
284 |rewrite > true_to_sigma_p_Sn
285 [rewrite > plus_n_SO.
286 rewrite > sym_plus in ⊢ (? ? %).
299 \lambda n. pi_p (S n) primeb (\lambda p.(exp p (k n p))).
301 theorem eq_B_B1: \forall n. B n = B1 n.
302 intros.unfold B.unfold B1.
310 definition B_split1 \def \lambda n.
311 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb (k n p) 1)* (k n p)))).
313 definition B_split2 \def \lambda n.
314 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb 2 (k n p))* (k n p)))).
316 theorem eq_B1_times_B_split1_B_split2: \forall n.
317 B1 n = B_split1 n * B_split2 n.
318 intro.unfold B1.unfold B_split1.unfold B_split2.
319 rewrite < times_pi_p.
322 |intros.apply (bool_elim ? (leb (k n x) 1));intro
323 [rewrite > (lt_to_leb_false 2 (k n x))
324 [simplify.rewrite < plus_n_O.
325 rewrite < times_n_SO.reflexivity
326 |apply le_S_S.apply leb_true_to_le.assumption
328 |rewrite > (le_to_leb_true 2 (k n x))
329 [simplify.rewrite < plus_n_O.
330 rewrite < plus_n_O.reflexivity
331 |apply not_le_to_lt.apply leb_false_to_not_le.assumption
337 lemma lt_div_to_times: \forall n,m,q. O < q \to n/q < m \to n < q*m.
341 intro.apply (lt_to_not_le ? ? H1).
342 apply le_times_to_le_div;assumption
343 |apply (ltn_to_ltO ? ? H1)
347 lemma lt_to_div_O:\forall n,m. n < m \to n / m = O.
349 apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n)
350 [apply div_mod_spec_div_mod.
351 apply (ltn_to_ltO ? ? H)
352 |apply div_mod_spec_intro
359 (* the value of n could be smaller *)
360 lemma k1: \forall n,p. 18 \le n \to p \le n \to 2*n/ 3 < p\to k (2*n) p = O.
364 |rewrite > true_to_sigma_p_Sn
369 cut (2*n/p = 2) as H4
370 [rewrite > H4.reflexivity
371 |apply lt_to_le_times_to_lt_S_to_div
372 [apply (ltn_to_ltO ? ? H2)
373 |rewrite < sym_times.
376 |rewrite > sym_times in ⊢ (? ? %).
377 apply lt_div_to_times
383 |cut (2*n/(p)\sup(S (S n2)) = O) as H4
384 [rewrite > H4.reflexivity
386 apply (le_to_lt_to_lt ? (exp ((2*n)/3) 2))
387 [apply (le_times_to_le (exp 3 2))
388 [apply leb_true_to_le.reflexivity
389 |rewrite > sym_times in ⊢ (? ? %).
391 apply (trans_le ? (exp n 2))
392 [rewrite < assoc_times.
393 rewrite > exp_SSO in ⊢ (? ? %).
396 |apply monotonic_exp1.
397 apply (le_plus_to_le 3).
398 change in ⊢ (? ? %) with ((S(2*n/3))*3).
399 apply (trans_le ? (2*n))
400 [simplify in ⊢ (? ? %).
403 apply (trans_le ? 18 ? ? H).
404 apply leb_true_to_le.reflexivity
411 |apply (lt_to_le_to_lt ? (exp p 2))
417 [apply (ltn_to_ltO ? ? H2)
418 |apply le_S_S.apply le_S_S.apply le_O_n
429 theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to
430 B_split1 (2*n) \le teta (2 * n / 3).
431 intros. unfold B_split1.unfold teta.
432 apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
433 [apply le_pi_p.intros.
435 [apply prime_to_lt_O.apply primeb_true_to_prime.assumption
436 |apply (bool_elim ? (leb (k (2*n) i) 1));intro
437 [elim (le_to_or_lt_eq ? ? (leb_true_to_le ? ? H4))
438 [lapply (le_S_S_to_le ? ? H5) as H6.
439 apply (le_n_O_elim ? H6).
442 |rewrite > (eq_to_eqb_true ? ? H5).
443 rewrite > H5.apply le_n
448 |apply (trans_le ? (pi_p (S (2*n/3)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
449 [apply (eq_ind ? ? ? (le_n ?)).
450 apply or_false_eq_SO_to_eq_pi_p
452 apply le_times_to_le_div2
454 |rewrite > sym_times in ⊢ (? ? %).
456 apply leb_true_to_le.reflexivity
459 unfold not_bertrand in H1.
460 elim (decidable_le (S n) i)
462 apply not_prime_to_primeb_false.
465 |apply le_S_S_to_le.assumption
472 apply not_le_to_lt.assumption
477 |apply le_pi_p.intros.
478 elim (eqb (k (2*n) i) 1)
479 [rewrite < exp_n_SO.apply le_n
480 |simplify.apply prime_to_lt_O.
481 apply primeb_true_to_prime.
488 theorem le_B_split2_exp: \forall n. exp 2 7 \le n \to
489 B_split2 (2*n) \le exp (2*n) (pred(sqrt(2*n)/2)).
490 intros.unfold B_split2.
492 [apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb
493 (λp:nat.(p)\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p))))
494 [apply (eq_ind ? ? ? (le_n ?)).
495 apply or_false_eq_SO_to_eq_pi_p
499 apply (bool_elim ? (leb 2 (k (2*n) i)));intro
501 apply (lt_to_not_le ? ? H1).unfold sqrt.
503 [apply le_S_S_to_le.assumption
504 |apply le_to_leb_true.
506 apply not_lt_to_le.intro.
507 apply (le_to_not_lt 2 (log i (2*n)))
508 [apply (trans_le ? (k (2*n) i))
509 [apply leb_true_to_le.assumption
512 |apply le_S_S.unfold log.apply f_false_to_le_max
513 [apply (ex_intro ? ? O).split
515 |apply le_to_leb_true.simplify.
521 |intros.apply lt_to_leb_false.
522 apply (lt_to_le_to_lt ? (exp i 2))
525 [apply (ltn_to_ltO ? ? H1)
535 |apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb (λp:nat.2*n)))
536 [apply le_pi_p.intros.
537 apply (trans_le ? (exp i (log i (2*n))))
539 [apply prime_to_lt_O.
540 apply primeb_true_to_prime.
542 |apply (bool_elim ? (leb 2 (k (2*n) i)));intro
543 [simplify in ⊢ (? (? % ?) ?).
545 rewrite < times_n_SO.
551 rewrite > (times_n_O O) in ⊢ (? % ?).
557 |apply (trans_le ? (exp (2*n) (prim(sqrt (2*n)))))
559 apply (eq_ind ? ? ? (le_n ?)).
562 [rewrite > (times_n_O O) in ⊢ (? % ?).
570 [apply (trans_le ? (2*(exp 2 7)))
571 [apply leb_true_to_le.reflexivity
572 |apply le_times_r.assumption
574 |apply le_to_leb_true.
575 apply (trans_le ? (2*(exp 2 7)))
576 [apply leb_true_to_le.reflexivity
577 |apply le_times_r.assumption
584 |apply (lt_to_le_to_lt ? ? ? ? H).
585 apply leb_true_to_le.reflexivity
589 theorem not_bertrand_to_le_B:
590 \forall n.exp 2 7 \le n \to not_bertrand n \to
591 B (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
594 rewrite > eq_B1_times_B_split1_B_split2.
596 [apply (trans_le ? (teta ((2*n)/3)))
597 [apply le_B_split1_teta
598 [apply (trans_le ? ? ? ? H).
599 apply leb_true_to_le.reflexivity
604 |apply le_B_split2_exp.
610 theorem not_bertrand_to_le1:
611 \forall n.18 \le n \to not_bertrand n \to
612 exp 2 (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (S(sqrt(2*n)))).
615 theorem le_times_div_m_m: \forall n,m. O < m \to n/m*m \le n.
617 rewrite > (div_mod n m) in ⊢ (? ? %)
623 theorem not_bertrand_to_le1:
624 \forall n.exp 2 7 \le n \to not_bertrand n \to
625 (exp 2 (2*n / 3)) \le (exp (2*n) (sqrt(2*n)/2)).
627 apply (le_times_to_le (exp 2 (2*(2 * n / 3))))
628 [apply lt_O_exp.apply lt_O_S
629 |rewrite < exp_plus_times.
630 apply (trans_le ? (exp 2 (2*n)))
634 change in ⊢ (? % ?) with (3*(2*n/3)).
636 apply le_times_div_m_m.
639 |apply (trans_le ? (2*n*B(2*n)))
641 apply (trans_le ? ? ? ? H).
642 apply leb_true_to_le.reflexivity
643 |rewrite > S_pred in ⊢ (? ? (? ? (? ? %)))
645 rewrite < assoc_times.
646 rewrite < sym_times in ⊢ (? ? (? % ?)).
647 rewrite > assoc_times in ⊢ (? ? %).
649 apply not_bertrand_to_le_B;assumption
650 |apply le_times_to_le_div
652 |apply (trans_le ? (sqrt (exp 2 8)))
653 [apply leb_true_to_le.reflexivity
654 |apply monotonic_sqrt.
655 change in ⊢ (? % ?) with (2*(exp 2 7)).
666 theorem not_bertrand_to_le2:
667 \forall n.exp 2 7 \le n \to not_bertrand n \to
668 2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)).
670 rewrite < (eq_log_exp 2)
671 [apply (trans_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2)))))
674 |apply not_bertrand_to_le1;assumption
683 theorem tech1: \forall a,b,c,d.O < b \to O < d \to
684 (a/b)*(c/d) \le (a*c)/(b*d).
686 apply le_times_to_le_div
687 [rewrite > (times_n_O O).
688 apply lt_times;assumption
689 |rewrite > assoc_times.
690 rewrite < assoc_times in ⊢ (? (? ? %) ?).
691 rewrite < sym_times in ⊢ (? (? ? (? % ?)) ?).
692 rewrite > assoc_times.
693 rewrite < assoc_times.
695 rewrite > sym_times;apply le_times_div_m_m;assumption
699 theorem tech: \forall n. 2*(S(log 2 (2*n))) \le sqrt (2*n) \to
700 (sqrt(2*n)/2)*S(log 2 (2*n)) \le 2*n / 4.
702 cut (4*(S(log 2 (2*n))) \le 2* sqrt(2*n))
703 [rewrite > sym_times.
704 apply le_times_to_le_div
706 |rewrite < assoc_times.
707 apply (trans_le ? (2*sqrt(2*n)*(sqrt (2*n)/2)))
708 [apply le_times_l.assumption
709 |apply (trans_le ? ((2*sqrt(2*n)*(sqrt(2*n))/2)))
710 [apply le_times_div_div_times.
712 |rewrite > assoc_times.
714 rewrite > lt_O_to_div_times.
720 |change in ⊢ (? (? % ?) ?) with (2*2).
721 rewrite > assoc_times.
727 theorem lt_div_S_div: \forall n,m. O < m \to exp m 2 \le n \to
730 apply lt_times_to_lt_div.
731 apply (lt_to_le_to_lt ? (S(n/m)*m))
732 [apply lt_div_S.assumption
733 |rewrite > sym_times in ⊢ (? ? %). simplify.
734 rewrite > sym_times in ⊢ (? ? (? ? %)).
736 apply le_times_to_le_div
744 theorem exp_plus_SSO: \forall a,b. exp (a+b) 2 = (exp a 2) + 2*a*b + (exp b 2).
747 rewrite > distr_times_plus.
748 rewrite > times_plus_l.
750 rewrite > assoc_plus.
751 rewrite > assoc_plus.
753 rewrite > times_plus_l.
755 rewrite < assoc_plus.
757 rewrite > plus_n_O in ⊢ (? ? (? (? ? %) ?) ?).
758 rewrite > assoc_times.
759 apply eq_f2;reflexivity.
762 theorem tech3: \forall n. (exp 2 8) \le n \to 2*(S(log 2 (2*n))) \le sqrt (2*n).
764 lapply (le_log 2 ? ? (le_n ?) H) as H1.
765 rewrite > exp_n_SO in ⊢ (? (? ? (? (? ? (? % ?)))) ?).
772 apply (trans_le ? (2*log 2 n))
773 [rewrite < times_SSO_n.
776 [apply leb_true_to_le.reflexivity
777 |rewrite < (eq_log_exp 2)
782 |apply (trans_le ? ? ? ? (le_exp_log 2 ? ? )).
783 apply le_times_SSO_n_exp_SSO_n.
784 apply (lt_to_le_to_lt ? ? ? ? H).
785 apply leb_true_to_le.reflexivity
787 |apply le_to_leb_true.
788 rewrite > assoc_times.
791 rewrite > assoc_times.
793 rewrite > exp_plus_SSO.
794 rewrite > distr_times_plus.
795 rewrite > distr_times_plus.
796 rewrite > assoc_plus.
797 apply (trans_le ? (4*exp (log 2 n) 2))
798 [change in ⊢ (? ? (? % ?)) with (2*2).
799 rewrite > assoc_times in ⊢ (? ? %).
800 rewrite < times_SSO_n in ⊢ (? ? %).
802 rewrite < times_SSO_n in ⊢ (? ? %).
804 [rewrite > sym_times in ⊢ (? (? ? %) ?).
805 rewrite < assoc_times.
806 rewrite < assoc_times.
807 change in ⊢ (? (? % ?) ?) with 8.
810 (* strange things here *)
811 rewrite < (eq_log_exp 2)
815 |apply (trans_le ? (log 2 n))
816 [change in ⊢ (? % ?) with 8.
817 rewrite < (eq_log_exp 2)
821 |rewrite > exp_n_SO in ⊢ (? % ?).
824 [apply (lt_to_le_to_lt ? ? ? ? H).
825 apply leb_true_to_le.reflexivity
826 |apply (lt_to_le_to_lt ? ? ? ? H).
827 apply leb_true_to_le.reflexivity
833 |change in ⊢ (? (? % ?) ?) with (exp 2 2).
834 apply (trans_le ? ? ? ? (le_exp_log 2 ? ?))
835 [apply le_times_exp_n_SSO_exp_SSO_n
837 |change in ⊢ (? % ?) with 8.
838 rewrite < (eq_log_exp 2)
843 |apply (lt_to_le_to_lt ? ? ? ? H).
844 apply leb_true_to_le.reflexivity
849 |apply (lt_to_le_to_lt ? ? ? ? H).
850 apply leb_true_to_le.reflexivity
854 theorem le_to_bertrand2:
855 \forall n. (exp 2 8) \le n \to bertrand n.
857 apply not_not_bertrand_to_bertrand.unfold.intro.
858 absurd (2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)))
859 [apply not_bertrand_to_le2
860 [apply (trans_le ? ? ? ? H).
868 apply (le_to_lt_to_lt ? ? ? ? (lt_div_S_div ? ? ? ?))
869 [apply tech.apply tech3.assumption
871 |apply (trans_le ? (2*exp 2 8))
872 [apply leb_true_to_le.reflexivity
873 |apply le_times_r.assumption
880 \forall n. O < n \to bertrand n.
881 intros;elim (decidable_le n 256)
882 [apply le_to_bertrand;assumption
883 |apply le_to_bertrand2;apply lt_to_le;apply not_le_to_lt;apply H1]
887 theorem mod_exp: eqb (mod (exp 2 8) 13) O = false.