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 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "nat/sqrt.ma".
16 include "nat/chebyshev_teta.ma".
17 include "nat/chebyshev.ma".
19 definition not_bertrand \def \lambda n.
20 \forall p.n < p \to p \le 2*n \to \not (prime p).
23 theorem divides_pi_p_to_divides: \forall p,n,b,g.prime p \to
24 divides p (pi_p n b g) \to \exists i. (i < n \and (b i = true \and
29 apply (le_to_not_lt p 1)
36 |apply (bool_elim ? (b n1));intro
37 [rewrite > (true_to_pi_p_Sn ? ? ? H3) in H2.
38 elim (divides_times_to_divides ? ? ? H1 H2)
39 [apply (ex_intro ? ? n1).
46 apply (ex_intro ? ? a).
48 [apply lt_to_le.apply le_S_S.assumption
52 |rewrite > (false_to_pi_p_Sn ? ? ? H3) in H2.
55 apply (ex_intro ? ? a).
57 [apply lt_to_le.apply le_S_S.assumption
64 theorem divides_B: \forall n,p.prime p \to p \divides (B n) \to
65 p \le n \land \exists i.mod (n /(exp p (S i))) 2 \neq O.
68 elim (divides_pi_p_to_divides ? ? ? ? H H1).
71 elim (divides_pi_p_to_divides ? ? ? ? H H5).clear H5.
76 [rewrite > Hcut.apply le_S_S_to_le.assumption
77 |apply (ex_intro ? ? a1).
80 change in H7:(? ? %) with (exp a ((n/(exp a (S a1))) \mod 2)).
84 [apply divides_to_le[apply lt_O_S|assumption]
85 |apply lt_to_not_le.elim H.assumption
88 |apply (divides_exp_to_eq ? ? ? H ? H7).
89 apply primeb_true_to_prime.
95 definition k \def \lambda n,p.
96 sigma_p (log p n) (λi:nat.true) (λi:nat.((n/(exp p (S i))\mod 2))).
98 theorem le_k: \forall n,p. k n p \le log p n.
99 intros.unfold k.elim (log p n)
101 |rewrite > true_to_sigma_p_Sn
102 [rewrite > plus_n_SO.
103 rewrite > sym_plus in ⊢ (? ? %).
116 \lambda n. pi_p (S n) primeb (\lambda p.(exp p (k n p))).
118 theorem eq_B_B1: \forall n. B n = B1 n.
119 intros.unfold B.unfold B1.
127 definition B_split1 \def \lambda n.
128 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb (k n p) 1)* (k n p)))).
130 definition B_split2 \def \lambda n.
131 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb 2 (k n p))* (k n p)))).
133 theorem eq_B1_times_B_split1_B_split2: \forall n.
134 B1 n = B_split1 n * B_split2 n.
135 intro.unfold B1.unfold B_split1.unfold B_split2.
136 rewrite < times_pi_p.
139 |intros.apply (bool_elim ? (leb (k n x) 1));intro
140 [rewrite > (lt_to_leb_false 2 (k n x))
141 [simplify.rewrite < plus_n_O.
142 rewrite < times_n_SO.reflexivity
143 |apply le_S_S.apply leb_true_to_le.assumption
145 |rewrite > (le_to_leb_true 2 (k n x))
146 [simplify.rewrite < plus_n_O.
147 rewrite < plus_n_O.reflexivity
148 |apply not_le_to_lt.apply leb_false_to_not_le.assumption
154 lemma lt_div_to_times: \forall n,m,q. O < q \to n/q < m \to n < q*m.
158 intro.apply (lt_to_not_le ? ? H1).
159 apply le_times_to_le_div;assumption
160 |apply (ltn_to_ltO ? ? H1)
164 lemma lt_to_div_O:\forall n,m. n < m \to n / m = O.
166 apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n)
167 [apply div_mod_spec_div_mod.
168 apply (ltn_to_ltO ? ? H)
169 |apply div_mod_spec_intro
176 (* the value of n could be smaller *)
177 lemma k1: \forall n,p. 18 \le n \to p \le n \to 2*n/ 3 < p\to k (2*n) p = O.
181 |rewrite > true_to_sigma_p_Sn
186 cut (2*n/p = 2) as H4
187 [rewrite > H4.reflexivity
188 |apply lt_to_le_times_to_lt_S_to_div
189 [apply (ltn_to_ltO ? ? H2)
190 |rewrite < sym_times.
193 |rewrite > sym_times in ⊢ (? ? %).
194 apply lt_div_to_times
200 |cut (2*n/(p)\sup(S (S n2)) = O) as H4
201 [rewrite > H4.reflexivity
203 apply (le_to_lt_to_lt ? (exp ((2*n)/3) 2))
204 [apply (le_times_to_le (exp 3 2))
205 [apply leb_true_to_le.reflexivity
206 |rewrite > sym_times in ⊢ (? ? %).
208 apply (trans_le ? (exp n 2))
209 [rewrite < assoc_times.
210 rewrite > exp_SSO in ⊢ (? ? %).
213 |apply monotonic_exp1.
214 apply (le_plus_to_le 3).
215 change in ⊢ (? ? %) with ((S(2*n/3))*3).
216 apply (trans_le ? (2*n))
217 [simplify in ⊢ (? ? %).
220 apply (trans_le ? 18 ? ? H).
221 apply leb_true_to_le.reflexivity
228 |apply (lt_to_le_to_lt ? (exp p 2))
234 [apply (ltn_to_ltO ? ? H2)
235 |apply le_S_S.apply le_S_S.apply le_O_n
246 theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to
247 B_split1 (2*n) \le teta (2 * n / 3).
248 intros.unfold B_split1.unfold teta.
249 apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
250 [apply le_pi_p.intros.
252 [apply prime_to_lt_O.apply primeb_true_to_prime.assumption
253 |apply (bool_elim ? (leb (k (2*n) i) 1));intro
254 [elim (le_to_or_lt_eq ? ? (leb_true_to_le ? ? H4))
255 [lapply (le_S_S_to_le ? ? H5) as H6.
256 apply (le_n_O_elim ? H6).
259 |rewrite > (eq_to_eqb_true ? ? H5).
260 rewrite > H5.apply le_n
265 |apply (trans_le ? (pi_p (S (2*n/3)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
266 [apply (eq_ind ? ? ? (le_n ?)).
267 apply or_false_eq_SO_to_eq_pi_p
269 apply le_times_to_le_div2
271 |rewrite > sym_times in ⊢ (? ? %).
273 apply leb_true_to_le.reflexivity
276 unfold not_bertrand in H1.
277 elim (decidable_le (S n) i)
279 apply not_prime_to_primeb_false.
282 |apply le_S_S_to_le.assumption
289 apply not_le_to_lt.assumption
294 |apply le_pi_p.intros.
295 elim (eqb (k (2*n) i) 1)
296 [rewrite < exp_n_SO.apply le_n
297 |simplify.apply prime_to_lt_O.
298 apply primeb_true_to_prime.
305 theorem le_B_split2_exp: \forall n. exp 2 7 \le n \to
306 B_split2 (2*n) \le exp (2*n) (pred(sqrt(2*n)/2)).
307 intros.unfold B_split2.
309 [apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb
310 (λp:nat.(p)\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p))))
311 [apply (eq_ind ? ? ? (le_n ?)).
312 apply or_false_eq_SO_to_eq_pi_p
316 apply (bool_elim ? (leb 2 (k (2*n) i)));intro
318 apply (lt_to_not_le ? ? H1).unfold sqrt.
320 [apply le_S_S_to_le.assumption
321 |apply le_to_leb_true.
323 apply not_lt_to_le.intro.
324 apply (le_to_not_lt 2 (log i (2*n)))
325 [apply (trans_le ? (k (2*n) i))
326 [apply leb_true_to_le.assumption
329 |apply le_S_S.unfold log.apply f_false_to_le_max
330 [apply (ex_intro ? ? O).split
332 |apply le_to_leb_true.simplify.
338 |intros.apply lt_to_leb_false.
339 apply (lt_to_le_to_lt ? (exp i 2))
342 [apply (ltn_to_ltO ? ? H1)
352 |apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb (λp:nat.2*n)))
353 [apply le_pi_p.intros.
354 apply (trans_le ? (exp i (log i (2*n))))
356 [apply prime_to_lt_O.
357 apply primeb_true_to_prime.
359 |apply (bool_elim ? (leb 2 (k (2*n) i)));intro
360 [simplify in ⊢ (? (? % ?) ?).
362 rewrite < times_n_SO.
368 rewrite > (times_n_O O) in ⊢ (? % ?).
374 |apply (trans_le ? (exp (2*n) (prim(sqrt (2*n)))))
376 apply (eq_ind ? ? ? (le_n ?)).
379 [rewrite > (times_n_O O) in ⊢ (? % ?).
387 [apply (trans_le ? (2*(exp 2 7)))
388 [apply leb_true_to_le.reflexivity
389 |apply le_times_r.assumption
391 |apply le_to_leb_true.
392 apply (trans_le ? (2*(exp 2 7)))
393 [apply leb_true_to_le.reflexivity
394 |apply le_times_r.assumption
401 |apply (lt_to_le_to_lt ? ? ? ? H).
402 apply leb_true_to_le.reflexivity
406 theorem not_bertrand_to_le_B:
407 \forall n.exp 2 7 \le n \to not_bertrand n \to
408 B (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
411 rewrite > eq_B1_times_B_split1_B_split2.
413 [apply (trans_le ? (teta ((2*n)/3)))
414 [apply le_B_split1_teta
415 [apply (trans_le ? ? ? ? H).
416 apply leb_true_to_le.reflexivity
421 |apply le_B_split2_exp.
427 theorem not_bertrand_to_le1:
428 \forall n.18 \le n \to not_bertrand n \to
429 exp 2 (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (S(sqrt(2*n)))).
432 theorem le_times_div_m_m: \forall n,m. O < m \to n/m*m \le n.
434 rewrite > (div_mod n m) in ⊢ (? ? %)
440 theorem not_bertrand_to_le1:
441 \forall n.exp 2 7 \le n \to not_bertrand n \to
442 (exp 2 (2*n / 3)) \le (exp (2*n) (sqrt(2*n)/2)).
444 apply (le_times_to_le (exp 2 (2*(2 * n / 3))))
445 [apply lt_O_exp.apply lt_O_S
446 |rewrite < exp_plus_times.
447 apply (trans_le ? (exp 2 (2*n)))
451 change in ⊢ (? % ?) with (3*(2*n/3)).
453 apply le_times_div_m_m.
457 rewrite < distr_times_plus.
459 apply (trans_le ? ((2*n + n)/3))
460 [apply le_plus_div.apply lt_O_S
462 change in ⊢ (? (? % ?) ?) with (3*n).
464 rewrite > lt_O_to_div_times
470 |apply (trans_le ? (2*n*B(2*n)))
472 apply (trans_le ? ? ? ? H).
473 apply leb_true_to_le.reflexivity
474 |rewrite > S_pred in ⊢ (? ? (? ? (? ? %)))
476 rewrite < assoc_times.
477 rewrite < sym_times in ⊢ (? ? (? % ?)).
478 rewrite > assoc_times in ⊢ (? ? %).
480 apply not_bertrand_to_le_B;assumption
481 |apply le_times_to_le_div
483 |apply (trans_le ? (sqrt (exp 2 8)))
484 [apply leb_true_to_le.reflexivity
485 |apply monotonic_sqrt.
486 change in ⊢ (? % ?) with (2*(exp 2 7)).
497 theorem not_bertrand_to_le2:
498 \forall n.exp 2 7 \le n \to not_bertrand n \to
499 2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)).
501 rewrite < (eq_log_exp 2)
502 [apply (trans_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2)))))
505 |apply not_bertrand_to_le1;assumption
515 theorem tech: \forall n. 2*(3*(S(log 2 (2*n)))/4) < sqrt (2*n) \to
516 (sqrt(2*n)/2)*S(log 2 (2*n)) < 2*n / 3.