1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/chebyshev_thm/".
17 include "nat/neper.ma".
19 definition C \def \lambda n.pi_p (S n) primeb
20 (\lambda p.match (leb (p*p) n) with
22 | false => S (n/p) ]).
24 theorem asdasd : \forall n. exp n (prim n) \leq (A n)*(C n).
25 intro;unfold prim;rewrite < exp_sigma_p;unfold A;unfold C;rewrite < times_pi_p;
27 apply (bool_elim ? (leb (i*i) n));intro
28 [change in \vdash (? ? (? ? %)) with i;
29 rewrite > sym_times;change in \vdash (? ? %) with (exp i (S (log i n)));
30 apply lt_to_le;apply lt_exp_log;apply prime_to_lt_SO;
31 apply primeb_true_to_prime;assumption
32 |change in \vdash (? ? (? ? %)) with (S (n/i));
34 [rewrite > Hcut;rewrite < exp_n_SO;
35 apply lt_to_le;rewrite > sym_times;apply lt_div_S;apply prime_to_lt_O;
36 apply primeb_true_to_prime;assumption
37 |apply antisymmetric_le
38 [apply le_S_S_to_le;apply not_le_to_lt;intro;
39 apply (leb_false_to_not_le ? ? H2);apply (trans_le ? (exp i (log i n)))
40 [rewrite < exp_SSO;apply le_exp;
42 apply primeb_true_to_prime;assumption
44 |apply le_exp_log;apply (trans_le ? i)
45 [apply prime_to_lt_O;apply primeb_true_to_prime;assumption
46 |apply le_S_S_to_le;assumption]]
47 |apply (trans_le ? (log i i))
50 |apply prime_to_lt_SO;apply primeb_true_to_prime;assumption]
52 [apply prime_to_lt_SO;apply primeb_true_to_prime;assumption
53 |apply le_S_S_to_le;assumption]]]]]
56 definition theta_pi \def
57 \lambda n.pi_p (S n) primeb (\lambda p.p).
60 \lambda n. pi_p (S n) (\lambda x. (primeb x) \land (leb (x*x) n)) (\lambda p.p).
63 \lambda n. pi_p (S n) (\lambda x. (primeb x) \land (leb (S n) (x*x))) (\lambda p.S (n/p)).
66 theorem jj : \forall n.C n = C1 n * C2 n.
67 intro;unfold C;unfold C1;unfold C2;
68 cut (\forall m.pi_p (S n) primeb
70 .match leb (p*p) m in bool return λb:bool.nat with
71 [true⇒p|false⇒S (m/p)])
72 =pi_p (S n) (λx:nat.primeb x∧leb (x*x) m) (λp:nat.p)
73 *pi_p (S n) (λx:nat.primeb x∧leb (S m) (x*x)) (λp:nat.S (m/p)))
77 |intro;apply (bool_elim ? (primeb (S n1)))
78 [intros;rewrite > true_to_pi_p_Sn
79 [apply (bool_elim ? (leb ((S n1)*(S n1)) m))
80 [intro;rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? % ?))
81 [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %))
82 [rewrite > H1;rewrite > H2;rewrite < assoc_times;reflexivity
83 |rewrite > H;lapply (leb_true_to_le ? ? H2);
84 lapply (le_to_not_lt ? ? Hletin);
85 apply (bool_elim ? (leb (S m) (S n1 * S n1)))
86 [intro;apply False_ind;apply Hletin1;
87 apply leb_true_to_le;assumption
89 |rewrite > H2;rewrite > H;reflexivity]
90 |intro;rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? % ?))
91 [rewrite > true_to_pi_p_Sn in \vdash (? ? ? (? ? %))
92 [rewrite > H1;rewrite < assoc_times;
93 rewrite > sym_times in \vdash (? ? (? % ?) ?);
94 rewrite > assoc_times;reflexivity
96 change in \vdash (? ? % ?) with (leb (S m) (S n1* S n1));
97 apply le_to_leb_true;apply not_le_to_lt;
98 apply leb_false_to_not_le;assumption]
99 |rewrite > H;rewrite > H2;reflexivity]]
101 |intros;rewrite > false_to_pi_p_Sn
102 [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? % ?))
103 [rewrite > false_to_pi_p_Sn in \vdash (? ? ? (? ? %))
104 [rewrite > H1;reflexivity
105 |rewrite > H;elim (leb (S m) (S n1*S n1));simplify;reflexivity]
106 |rewrite > H;elim (leb (S n1*S n1) m);simplify;reflexivity]
110 theorem log_pi_p : \forall n,b,f,g.S O < b \to
111 log b (pi_p n f g) \leq
112 (sigma_p n f (\lambda x.S O)) + (sigma_p n f (\lambda x.log b (g x))).
114 [simplify;rewrite < times_n_SO;apply (leb_elim b (S O))
115 [intro;elim (lt_to_not_le ? ? H);assumption
116 |intro;simplify;apply le_n]
117 |apply (bool_elim ? (f n1))
118 [intro;rewrite > true_to_pi_p_Sn
119 [rewrite > true_to_sigma_p_Sn
120 [rewrite > true_to_sigma_p_Sn
121 [apply (trans_le ? (S ((log b (g n1)) + (log b (pi_p n1 f g)))))
122 [apply log_times;assumption
123 |rewrite > assoc_plus;
124 change in \vdash (? ? %) with (S (sigma_p n1 f (\lambda x.S O)+(log b (g n1)+sigma_p n1 f (\lambda x.log b (g x)))));
125 apply le_S_S;rewrite < assoc_plus;
126 rewrite > sym_plus in \vdash (? ? (? % ?));
127 rewrite > assoc_plus;apply le_plus;
130 |intro;rewrite > false_to_pi_p_Sn
131 [rewrite > false_to_sigma_p_Sn
132 [rewrite > false_to_sigma_p_Sn]]
136 axiom daemon : False.
138 lemma lt_log_to_lt : \forall b,m,n.S O < b \to log b m < log b n \to m < n.
139 intros;apply not_le_to_lt;intro;elim (le_to_not_lt ? ? (le_log ? ? ? H H2));
143 theorem ababbs: \forall n,a,b.S O < b \to O < n \to n < exp b a \to log b n < a.
144 intros;unfold log;apply not_le_to_lt;intro;apply (lt_to_not_le ? ? H2);
145 elim (le_to_or_lt_eq ? ? H3)
146 [apply lt_to_le;apply (lt_log_to_lt b ? ? H);rewrite > eq_log_exp;assumption
147 |apply (trans_le ? (exp b (log b n)))
148 [rewrite < H4;apply le_n
149 |apply le_exp_log;assumption]]
152 theorem exp_exp_to_log : \forall b,n,k.S O < b \to
153 exp b k \leq n \to n < exp b (S k) \to log b n = k.
154 intros;unfold log;lapply (ababbs ? ? ? H ? H2)
155 [apply (trans_le ? ? ? ? H1);apply lt_O_exp
156 |unfold log in Hletin;lapply (le_to_leb_true ? ? H1);
157 lapply (f_m_to_le_max (λx:nat.leb ((b)\sup(x)) n) n ? ? Hletin1)
159 elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? Hletin))
164 theorem xxx_log : \forall a,b.S O < b \to O < a \to log b (b*a) = S (log b a).
166 [elim (not_le_Sn_O ? H1);
171 theorem le_log_C2_sigma_p : \forall n,b. S O < b \to
173 (sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) +
174 (prim n + (((sigma_p n (\lambda x.leb (S n) (x*x)) (\lambda i.prim i * S (n!/i)))
175 *(S (log b 3)))/n!)).
177 apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λx:nat.1)
178 +sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x))
179 (λi.log b (S (n/i)))))
180 [apply log_pi_p;assumption
183 |apply (trans_le ? (sigma_p (S n) (λx:nat.primeb x∧leb (S n) (x*x)) (λi:nat.S (log b (n/i)))))
184 [apply le_sigma_p;intros;cut (log b (b*(n/i)) = S (log b (n/i)))
185 [rewrite < Hcut;apply le_log
188 [rewrite < times_SSO_n;change in \vdash (? % ?) with (S O + (n/i));
190 [apply le_times_to_le_div
191 [apply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2)));
192 |rewrite < times_n_SO;apply le_S_S_to_le;assumption]
194 |apply (trans_le ? ? ? H4);apply le_times_l;apply le_S;apply le_n]]
195 |rewrite > exp_n_SO in ⊢ (? ? (? ? (? % ?)) ?);
199 |apply le_times_to_le_div;
200 [apply (prime_to_lt_O i (primeb_true_to_prime ? (andb_true_true ? ? H2)));
201 |rewrite < times_n_SO;apply le_S_S_to_le;assumption]]]
202 |change in ⊢ (? (? ? ? (λi:?.%)) ?) with ((S O) + (log b (n/i)));
203 rewrite > (sigma_p_plus_1 ? (\lambda x.S O));
205 [unfold prim;apply le_sigma_p1;intros;elim (leb (S n) (i*i));
206 [rewrite > andb_sym;apply le_n
207 |rewrite > andb_sym;apply le_O_n]
208 |apply sigma_p_log_div;assumption]]]]
211 lemma le_prim_n_stima : \forall n,b. S O < b \to b \leq n \to
212 prim n \leq (S (((S (S (S (S O))))*(S (log b (pred n)))) +
213 ((S (S (S (S O))))*n)))/(log b n).
214 (* la stima del secondo addendo è ottenuta considerando che
215 logreale 2 è sempre <= 1 (si dimostra per casi: b = 2, b > 2) *)
216 intros;apply le_times_to_le_div;
218 [apply (trans_le ? b)
219 [apply lt_to_le;assumption
222 |apply (trans_le ? (log b (exp n (prim n))))
223 [rewrite > sym_times;apply log_exp2
225 |apply (trans_le ? b ? ? H1);apply lt_to_le;assumption]
226 |apply (trans_le ? (log b ((exp (pred n) (S (S (S (S O)))))
227 *(exp (S (S O)) ((S (S (S (S O))))*n)))))
230 |apply le_exp_primr;apply (trans_le ? ? ? H H1)]
231 |apply (trans_le ? (S ((log b (exp (pred n) (S (S (S (S O)))))) +
232 (log b (exp (S (S O)) ((S (S (S (S O))))*n))))))
233 [apply log_times;assumption
234 |apply le_S_S;apply le_plus
235 [apply log_exp1;assumption
237 [rewrite > times_n_SO in \vdash (? (? ? %) ?);
239 [rewrite < plus_n_O;apply le_n
242 |apply (trans_le ? (((S (S (S (S O))))*n)*(S (log (S m) (S (S O))))))
243 [apply log_exp1;apply le_S;assumption
244 |rewrite > times_n_SO in \vdash (? ? %);
245 apply le_times_r;apply le_S_S;
246 rewrite > lt_to_log_O
249 |apply le_S_S;assumption]]]]]]]]
252 theorem le_log_C2_stima : \forall n,b. S O < b \to b*b < n \to
254 (*(sigma_p (S n) (\lambda x.(primeb x) \land (leb (S n) (x*x))) (\lambda x.S O)) +*)
255 ((S (((S (S (S (S O))))*(S (log b (pred n)))) +
256 ((S (S (S (S O))))*n)))/(log b n)) +
257 (((S (((S (S (S (S O))))*(S (log b (pred n)))) +
258 ((S (S (S (S O))))*n)))/(log b n)) +
259 (((sigma_p n (\lambda x.leb (S n) (x*x))
260 (\lambda i.((S (((S (S (S (S O))))*(S (log b (pred i)))) +
261 ((S (S (S (S O))))*i)))/(log b i))* S (n!/i)))
262 *(S (log b (S (S (S O))))))/n!)).intros.
263 apply (trans_le ? ? ? (le_log_C2_sigma_p ? ? ?))
266 [apply (trans_le ? ? ? ? (le_prim_n_stima ? ? ? ?));
267 [unfold prim;apply le_sigma_p1;intros;
268 do 2 rewrite < times_n_SO;elim (primeb i)
269 [elim (leb (S n) (i*i));simplify [apply le_n|apply le_O_n]
270 |simplify;apply le_n]
272 |apply (trans_le ? ? ? ? H1);apply le_S;apply le_times_n;
273 apply lt_to_le;assumption]
275 [apply le_prim_n_stima;
277 |apply (trans_le ? (b*b))
278 [apply le_times_n;apply lt_to_le;assumption
279 |apply lt_to_le;assumption]]
282 |apply le_times_l;apply le_sigma_p;intros;apply le_times_l;
283 apply le_prim_n_stima
285 |apply (le_exp_to_le1 ? ? (S (S O)));
286 [apply le_S;apply le_n
287 |do 2 rewrite > exp_SSO;apply (trans_le ? n)
288 [apply lt_to_le;assumption
289 |apply lt_to_le;apply leb_true_to_le;assumption]]]]]]]
292 lemma log_interval : \forall b,k,n. S O < b \to exp b k \leq n \to n < exp b (S k) \to
295 [simplify in H2;rewrite < times_n_SO in H2;apply lt_to_log_O;assumption
296 |cut (log b n1 < S (S n))
298 [apply antisymmetric_le
299 [apply le_S_S_to_le;assumption
301 |apply (trans_le ? (log b (exp b (S n))))
302 [rewrite > eq_log_exp
305 |apply le_log;assumption]]
306 |apply le_S_S;apply (trans_le ? (log b (pred (exp b (S (S n))))))
309 |apply le_S_S_to_le;apply (trans_le ? ? ? H3);
310 rewrite > minus_n_O in \vdash (? ? (? (? %)));
311 rewrite < (eq_minus_S_pred (exp b (S (S n))) O);
312 rewrite > minus_n_O in \vdash (? % ?);
313 apply minus_le_S_minus_S]
314 |unfold log;apply f_false_to_le_max;
315 [apply (ex_intro ? ? (S n));split
316 [apply (trans_le ? (exp b (S n)));
317 [apply lt_to_le;apply lt_m_exp_nm;assumption
318 |rewrite > minus_n_O in ⊢ (? ? (? %));
319 rewrite < eq_minus_S_pred;apply le_plus_to_minus_r;
321 change in \vdash (? % ?) with (S (O + exp b (S n)));
322 apply lt_minus_to_plus;
323 change in ⊢ (? ? (? % ?)) with (b * (exp b (S n)));
324 rewrite > times_n_SO in \vdash (? ? (? ? %));
325 rewrite > sym_times in \vdash (? ? (? % ?));
326 rewrite < distributive_times_minus;unfold lt;
327 rewrite > times_n_SO in \vdash (? % ?);apply le_times
328 [apply lt_O_exp;apply (trans_le ? ? ? ? H1);
329 apply le_S;apply le_n
330 |apply le_plus_to_minus_r;simplify;assumption]]
331 |apply le_to_leb_true;
332 rewrite > minus_n_O in \vdash (? ? (? %));
333 rewrite < eq_minus_S_pred;apply le_plus_to_minus_r;
334 rewrite > sym_plus;change in \vdash (? % ?) with (S (exp b (S n)));
338 |intros;apply lt_to_leb_false;unfold lt;
339 rewrite > minus_n_O in \vdash (? (? (? %)) ?);
340 rewrite < eq_minus_S_pred;rewrite < minus_Sn_m
341 [rewrite > minus_S_S;rewrite < minus_n_O;apply le_exp;
342 [apply (trans_le ? ? ? ? H1);apply le_S;apply le_n
344 |apply lt_O_exp;apply (trans_le ? ? ? ? H1);apply le_S;apply le_n]]]]]
347 lemma log_strano : \forall b,i.S O < b \to S O < i \to
348 ((S (S (S (S O)))) * log b (pred i)) + (S (S (S (S (S O))))) \leq
350 alias num (instance 0) = "natural number".
351 cut (\forall b,i,k.S O < b \to S O < i \to
352 (exp b k) \leq i-1 \to i-1 < (exp b (S k)) \to
353 ((S (S (S (S O)))) * log b (pred i)) + (S (S (S (S (S O))))) \leq
355 [intros;apply (Hcut ? ? (log b (i-1)) H H1);
356 [apply le_exp_log;rewrite > (minus_n_n 1) in \vdash (? % ?);
357 apply lt_plus_to_lt_minus;
359 |rewrite < eq_minus_plus_plus_minus
360 [rewrite > sym_plus;rewrite > eq_minus_plus_plus_minus;
361 [rewrite < minus_n_n;rewrite < plus_n_O;assumption
363 |apply lt_to_le;assumption]]
364 |apply lt_exp_log;assumption]
365 |intros;rewrite > minus_n_O in ⊢ (? (? (? ? (? ? (? %))) ?) ?);
366 rewrite < eq_minus_S_pred;rewrite > (log_interval ? k)
367 [apply (trans_le ? (3*(exp b k) + 3))
368 [change in \vdash (? (? ? %) ?) with (2+3);
369 rewrite < assoc_plus;apply le_plus_l;
371 [simplify;apply le_S;apply le_n
372 |elim (decidable_eq_nat O n)
373 [rewrite < H5;apply (trans_le ? (3*(exp 2 1)));
375 |apply le_times_r;apply monotonic_exp1;assumption]
376 |rewrite < times_n_Sm;apply (trans_le ? (3*(exp b n) + 4))
377 [rewrite > assoc_plus;rewrite > sym_plus;apply le_plus_l;
379 |rewrite < sym_plus;change in \vdash (? % ?) with (S (3 + (3*(exp b n))));
380 apply lt_minus_to_plus;
381 change in ⊢ (? ? (? (? ? %) ?)) with (b*(exp b n));
382 rewrite > sym_times in \vdash (? ? (? (? ? %) ?));
383 rewrite < assoc_times;
384 rewrite > times_n_SO in ⊢ (? ? (? ? (? ? %)));
385 rewrite < assoc_times;rewrite < distr_times_minus;
386 apply (trans_le ? (3*2*1))
387 [simplify;apply le_S;apply le_S;apply le_n
389 [apply le_times_r;apply (trans_le ? (exp 2 n))
390 [rewrite > exp_n_SO in \vdash (? % ?);apply le_exp
391 [apply le_S;apply le_n
392 |generalize in match H5;cases n
393 [intro;elim H6;reflexivity
394 |intro;apply le_S_S;apply le_O_n]]
395 |apply monotonic_exp1;assumption]
396 |apply le_S_S_to_le;rewrite < minus_Sn_m;
397 [simplify;rewrite < minus_n_O;assumption
398 |apply lt_to_le;assumption]]]]]]
399 |rewrite > times_n_SO in \vdash (? (? ? %) ?);
400 rewrite < distr_times_plus;apply le_times_r;
401 rewrite < plus_n_SO;apply (trans_le ? (S (i-1)))
402 [apply le_S_S;assumption
403 |rewrite < minus_Sn_m
404 [simplify;rewrite < minus_n_O;apply le_n
405 |apply lt_to_le;assumption]]]
411 lemma eq_div_div_times : \forall x,y,z.O < z \to O < y \to x/y = (z*x)/(z*y).
412 intros.rewrite > (div_mod x y) in \vdash (? ? ? %);
413 [rewrite > distr_times_plus;rewrite > sym_times;rewrite > assoc_times;
414 rewrite > sym_times in ⊢ (? ? ? (? (? (? ? %) ?) ?));
415 rewrite > div_plus_times
417 |generalize in match H;cases z;intros
418 [elim (not_le_Sn_O ? H2)
419 |apply lt_times_r;apply lt_mod_m_m;assumption]]
423 alias num (instance 0) = "natural number".
424 lemma le_sigma_p_lemma1 : \forall n,b. S O < b \to b*b < n \to
425 (sigma_p n (\lambda x.leb (S n) (x*x))
426 (\lambda i.((S (((S (S (S (S O))))*(S (log b (pred i)))) +
427 ((S (S (S (S O))))*i)))/(log b i))* S (n!/i)))
428 \leq ((28 * n * n!)/(pred (log b n))).
429 intros.apply (trans_le ? (sigma_p n (\lambda x.leb (S n) (x*x)) (\lambda i. ((7*i)/(log b i))*(S (n!/i)))))
430 [apply le_sigma_p;intros;cut (b \leq i)
431 [cut (1 < i) [|apply (trans_le ? ? ? H Hcut)]
432 apply le_times_l;apply monotonic_div
434 [generalize in match H3;cases i
435 [simplify;intros;destruct H4
436 |intro;apply le_S_S;apply le_O_n]
438 |rewrite > sym_times;simplify in ⊢ (? (? (? % ?)) ?);
439 change in ⊢ (? % ?) with (1 + ((4 + (log b (pred i) * 4)) + 4*i));
440 rewrite > assoc_plus;rewrite < assoc_plus;
441 simplify in \vdash (? (? % ?) ?);rewrite < assoc_plus;
442 apply (trans_le ? (3*i + 4*i))
443 [apply le_minus_to_plus;rewrite > eq_minus_plus_plus_minus
444 [rewrite < minus_n_n;rewrite < plus_n_O;
445 rewrite > sym_plus;rewrite > sym_times;apply log_strano
447 |lapply (leb_true_to_le ? ? H3);apply (trans_le ? ? ? H);
448 apply (le_exp_to_le1 ? ? 2);
449 [apply le_S_S;apply le_O_n
450 |apply lt_to_le;do 2 rewrite > exp_SSO;apply (trans_le ? ? ? H1);
451 apply lt_to_le;assumption]]
453 |rewrite > sym_times in \vdash (? (? % ?) ?);
454 rewrite > sym_times in \vdash (? (? ? %) ?);
455 rewrite < distr_times_plus;rewrite > sym_times;apply le_n]]
456 |apply (le_exp_to_le1 ? ? 2);
457 [apply le_S_S;apply le_O_n
458 |apply lt_to_le;do 2 rewrite > exp_SSO;apply (trans_le ? ? ? H1);
459 apply (trans_le ? ? ? ? (leb_true_to_le ? ? H3));apply le_S;
461 |apply (trans_le ? (sigma_p n (λx:nat.leb (S n) (x*x)) (λi:nat.7*i/log b i*((2*(n!))/i))))
462 [apply le_sigma_p;intros;apply le_times_r;apply (trans_le ? (n!/i + n!/i))
463 [change in \vdash (? % ?) with (1 + n!/i);apply le_plus_l;
464 apply le_times_to_le_div
465 [generalize in match H3;cases i;simplify;intro
467 |apply le_S_S;apply le_O_n]
468 |generalize in match H2;cases n;intro
469 [elim (not_le_Sn_O ? H4)
470 |change in \vdash (? ? %) with ((S n1)*(n1!));apply le_times
471 [apply lt_to_le;assumption
473 |rewrite > plus_n_O in \vdash (? (? ? %) ?);
474 change in \vdash (? % ?) with (2 * (n!/i));
475 apply le_times_div_div_times;
476 generalize in match H3;cases i;simplify;intro
478 |apply le_S_S;apply le_O_n]]
479 |apply (trans_le ? (sigma_p n (\lambda x:nat.leb (S n) (x*x)) (\lambda i.((14*(n!))/log b i))))
480 [apply le_sigma_p;intros;
482 [|apply (le_exp_to_le1 ? ? 2);
483 [apply le_S_S;apply le_O_n
484 |apply lt_to_le;do 2 rewrite > exp_SSO;apply (trans_le ? ? ? H1);
485 apply (trans_le ? ? ? ? (leb_true_to_le ? ? H3));apply le_S;
488 [|apply (trans_le ? ? ? H Hcut)]
489 change in ⊢ (? ? (? % ?)) with ((7*2)*(n!));
490 rewrite > assoc_times in \vdash (? ? (? % ?));
491 apply (trans_le ? ? ? (le_times_div_div_times ? ? ? ?));
492 [apply lt_to_le;assumption
493 |rewrite > (eq_div_div_times ? ? 7)
494 [rewrite > sym_times in ⊢ (? (? (? ? %) ?) ?);
495 rewrite < assoc_times in \vdash (? (? % ?) ?);
496 apply (trans_le ? ? ? (le_div_times_m ? ? ? ? ?))
498 [apply lt_to_le;assumption
500 |unfold lt;rewrite > times_n_SO in \vdash (? % ?);
502 [apply le_S_S;apply le_O_n
503 |apply lt_to_le;assumption]
505 |apply le_S_S;apply le_O_n
506 |apply lt_to_le;assumption]]
507 |apply (trans_le ? (sigma_p (S n) (\lambda x.leb (S n) (x*x))
508 (\lambda i.14*n!/log b i)))
509 [apply (bool_elim ? (leb (S n) (n*n)));intro
510 [rewrite > true_to_sigma_p_Sn
511 [rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
512 apply le_plus_r;apply le_O_n
514 |rewrite > false_to_sigma_p_Sn
517 |apply (trans_le ? ? ? (le_sigma_p_div_log_div_pred_log ? ? ? ? ?));
519 |apply lt_to_le;assumption
520 |rewrite < assoc_times;
521 rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?);
522 rewrite < assoc_times;apply le_n]]]]]
525 theorem le_log_C2_stima2 : \forall n,b. S O < b \to b*b < n \to
528 ((((28*n*n!)/pred (log b n))
529 *(S (log b (S (S (S O))))))/n!).intros.
530 apply (trans_le ? ? ? (le_log_C2_stima ? ? H H1));
531 rewrite < assoc_plus in \vdash (? % ?);apply le_plus
532 [rewrite > times_SSO_n in \vdash (? % ?);
533 apply (trans_le ? ? ? (le_times_div_div_times ? ? ? ?))
535 [apply (trans_le ? (b*b))
536 [rewrite > times_n_SO;apply le_times;apply lt_to_le;assumption
537 |apply lt_to_le;assumption]
538 |apply (trans_le ? (b*b))
539 [rewrite > times_n_SO in \vdash (? % ?);apply le_times
540 [apply le_n|apply lt_to_le;assumption]
541 |apply lt_to_le;assumption]]
542 |change in \vdash (? ? (? (? % ?) ?)) with (2*7);
545 [apply (trans_le ? (b*b))
546 [rewrite > times_n_SO;apply le_times;apply lt_to_le;assumption
547 |apply lt_to_le;assumption]
548 |apply (trans_le ? (b*b))
549 [rewrite > times_n_SO in \vdash (? % ?);apply le_times
550 [apply le_n|apply lt_to_le;assumption]
551 |apply lt_to_le;assumption]]
552 |rewrite > assoc_times;apply le_times_r;
553 change in \vdash (? (? (? (? ? %) ?)) ?) with (1 + (log b (pred n)));
554 rewrite > distr_times_plus;
555 change in \vdash (? % ?) with (1 + (4*1+4*log b (pred n)+4*n));
556 do 2 rewrite < assoc_plus;simplify in ⊢ (? (? (? % ?) ?) ?);
557 change in ⊢ (? ? %) with ((3+4)*n);rewrite > sym_times in \vdash (? ? %);
558 rewrite > distr_times_plus;
559 rewrite > sym_times in \vdash (? ? (? % ?));
560 rewrite > sym_times in \vdash (? ? (? ? %));
561 apply le_plus_l;rewrite > sym_plus;apply log_strano
563 |apply (trans_le ? ? ? H);apply (trans_le ? (b*b))
564 [rewrite > times_n_SO in \vdash (? % ?);
565 apply le_times_r;apply lt_to_le;assumption
566 |apply lt_to_le;assumption]]]]
569 |apply le_times_l;apply (le_sigma_p_lemma1 ? ? H H1)]]
572 theorem le_log_C2_stima3 : \forall n,b. S O < b \to b*b < n \to
575 ((28*n)*(S (log b (S (S (S O)))))/pred (log b n)).intros.
576 apply (trans_le ? ? ? (le_log_C2_stima2 ? ? H H1));apply le_plus_r;
577 (*apply (trans_le ? ((28*n)*(28*n*n!/pred (log b n)*S (log b 3)/(28*n*n!))))
579 rewrite > (eq_div_div_times ? ? (28*n)) in \vdash (? % ?)
580 [rewrite > sym_times in ⊢ (? (? (? ? %) ?) ?);
581 rewrite < assoc_times;
582 apply le_div_times_m;
583 [apply (trans_le ? (pred (log b (b*b))))
584 [rewrite < exp_SSO;rewrite > eq_log_exp;
587 |rewrite < exp_SSO;rewrite > eq_log_exp;
588 [simplify;rewrite > minus_n_O in \vdash (? ? (? %));
589 rewrite < eq_minus_S_pred;
590 apply le_plus_to_minus_r;simplify;
591 rewrite < (eq_log_exp b 2);
594 |rewrite > exp_SSO;apply lt_to_le;assumption]
597 |unfold lt;rewrite > times_n_SO in \vdash (? % ?);apply le_times
598 [rewrite > times_n_SO in \vdash (? % ?);apply le_times
599 [apply le_S_S;apply le_O_n
600 |apply (trans_le ? ? ? ? H1);apply le_S_S;
601 rewrite > times_n_SO;apply le_times
603 |apply lt_to_le;assumption]]
605 |unfold lt;rewrite > times_n_SO in \vdash (? % ?);apply le_times
606 [apply le_S_S;apply le_O_n
607 |apply (trans_le ? ? ? ? H1);apply le_S_S;
608 rewrite > times_n_SO;apply le_times
610 |apply lt_to_le;assumption]]
614 lemma le_prim_log1: \forall n,b. S O < b \to O < n \to
615 (prim n)*(log b n) \leq
616 log b (A n) + log b (C1 n) + log b (C2 n) + 2.
617 intros.change in \vdash (? ? (? ? %)) with (1+1).
618 rewrite < assoc_plus;rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?)).
619 rewrite > assoc_plus in ⊢ (? ? (? % ?));
620 apply (trans_le ? (log b (A n) + (log b (C1 n * C2 n)) + 1));
621 [apply (trans_le ? (log b (A n * (C1 n * C2 n))))
622 [apply (trans_le ? (log b (exp n (prim n))))
623 [apply log_exp2;assumption
626 |rewrite < jj;apply asdasd]]
627 |rewrite > sym_plus;simplify;apply log_times;assumption]
628 |apply le_plus_l;apply le_plus_r;rewrite > sym_plus;simplify;apply log_times;
632 lemma le_log_A1 : \forall n,b. S O < b \to S O < n \to
633 log b (A n) \leq 2*(S (log b (pred n))) + (2*(pred n))*(S (log b 2)) + 1.
634 intros.apply (trans_le ? (log b ((exp (pred n) 2)*(exp 2 (2*(pred n))))))
637 |simplify in ⊢ (? ? (? (? % ?) ?));apply le_A_exp4;assumption]
638 |rewrite < sym_plus;apply (trans_le ? (1 + ((log b (exp (pred n) 2)) + (log b (exp 2 (2*(pred n)))))));
639 [change in \vdash (? ? %) with (S (log b ((pred n)\sup(2))+log b ((2)\sup(2*(pred n)))));
640 apply log_times;assumption
641 |apply le_plus_r;apply le_plus;apply log_exp1;assumption]]
644 lemma le_theta_pi_A : \forall n.theta_pi n \leq A n.
645 intro.unfold theta_pi.unfold A.apply le_pi_p.intros.
646 rewrite > exp_n_SO in \vdash (? % ?).
651 [apply (trans_le ? ? ? Hcut);apply le_S_S_to_le;assumption
652 |apply le_S_S_to_le;assumption]]
653 |apply prime_to_lt_O;apply primeb_true_to_prime;assumption]
657 \lambda n.max n (\lambda x.leb (x*x) n).
659 theorem le_sqrt_to_le_times_l : \forall m,n.n \leq sqrt m \to n*n \leq m.
660 intros;apply (trans_le ? (sqrt m * sqrt m))
661 [apply le_times;assumption
662 |apply leb_true_to_le;apply (f_max_true (λx:nat.leb (x*x) m) m);
663 apply (ex_intro ? ? O);split
665 |simplify;reflexivity]]
668 theorem lt_sqrt_to_le_times_l : \forall m,n.n < sqrt m \to n*n < m.
669 intros;apply (trans_le ? (sqrt m * sqrt m))
670 [apply (trans_le ? (S n * S n))
671 [simplify in \vdash (? ? %);apply le_S_S;apply (trans_le ? (n * S n))
672 [apply le_times_r;apply le_S;apply le_n
673 |rewrite > sym_plus;rewrite > plus_n_O in \vdash (? % ?);
674 apply le_plus_r;apply le_O_n]
675 |apply le_times;assumption]
676 |apply le_sqrt_to_le_times_l;apply le_n]
679 theorem le_sqrt_to_le_times_r : \forall m,n.sqrt m < n \to m < n*n.
680 intros;apply not_le_to_lt;intro;
681 apply ((leb_false_to_not_le ? ?
682 (lt_max_to_false (\lambda x.leb (x*x) m) m n H ?))
684 apply (trans_le ? ? ? ? H1);cases n
686 |rewrite > times_n_SO in \vdash (? % ?);rewrite > sym_times;apply le_times
687 [apply le_S_S;apply le_O_n
691 theorem eq_theta_pi_sqrt_C1 : \forall n. theta_pi (sqrt n) = C1 n.
692 intro;unfold theta_pi;unfold C1;rewrite > (false_to_eq_pi_p (S (sqrt n)) (S n))
693 [generalize in match (le_sqrt_to_le_times_l n);elim (sqrt n)
694 [simplify;reflexivity
695 |apply (bool_elim ? (primeb (S n1)))
696 [intro;rewrite > true_to_pi_p_Sn
697 [rewrite > true_to_pi_p_Sn in \vdash (? ? ? %)
700 |apply H;intros;apply H1;apply le_S;assumption]
701 |apply (andb_elim (primeb (S n1)) (leb (S n1 * S n1) n));
702 rewrite > H2;whd;apply le_to_leb_true;apply H1;apply le_n]
704 |intro;rewrite > false_to_pi_p_Sn
705 [rewrite > false_to_pi_p_Sn in \vdash (? ? ? %)
706 [apply H;intros;apply H1;apply le_S;assumption
707 |apply (andb_elim (primeb (S n1)) (leb (S n1 * S n1) n));
708 rewrite > H2;whd;reflexivity]
710 |apply le_S_S;unfold sqrt;apply le_max_n
711 |intros;apply (andb_elim (primeb i) (leb (i*i) n));elim (primeb i);simplify
712 [rewrite > lt_to_leb_false
714 |apply le_sqrt_to_le_times_r;assumption]
718 lemma le_sqrt_n_n : \forall n.sqrt n \leq n.
719 intro.unfold sqrt.apply le_max_n.
722 lemma le_prim_log_stima: \forall n,b. S O < b \to b < sqrt n \to
723 (prim n)*(log b n) \leq
724 2*S (log b (pred n))+2*(pred n)*S (log b 2)
725 +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))
726 +(14*n/log b n+28*n*S (log b 3)/pred (log b n))
729 [apply (trans_le ? ((2*(S (log b (pred n))) + (2*(pred n))*(S (log b 2)) + 1) +
730 (2*(S (log b (pred (sqrt n)))) + (2*(pred (sqrt n)))*(S (log b 2)) + 1) +
731 ((14*n/(log b n)) + ((28*n)*(S (log b (S (S (S O)))))/pred (log b n))) + 2))
732 [apply (trans_le ? ? ? (le_prim_log1 ? ? H ?))
733 [apply lt_to_le;assumption
734 |apply le_plus_l;apply le_plus
736 [apply le_log_A1;assumption
737 |rewrite < eq_theta_pi_sqrt_C1;apply (trans_le ? (log b (A (sqrt n))))
740 |apply le_theta_pi_A]
743 |apply (trans_le ? ? ? H);apply lt_to_le;assumption]]]
744 |apply le_log_C2_stima3;
746 |apply lt_sqrt_to_le_times_l;assumption]]]
747 |rewrite > assoc_plus in ⊢ (? (? % ?) ?);
748 rewrite > sym_plus in ⊢ (? (? (? ? %) ?) ?);
749 rewrite > assoc_plus in \vdash (? % ?);
750 rewrite > assoc_plus in ⊢ (? (? ? %) ?);
751 rewrite > assoc_plus in ⊢ (? (? % ?) ?);
752 rewrite > assoc_plus in \vdash (? % ?);
753 rewrite < assoc_plus in ⊢ (? (? ? %) ?);
754 rewrite > assoc_plus in ⊢ (? (? ? (? % ?)) ?);
755 rewrite > sym_plus in ⊢ (? (? ? (? (? ? %) ?)) ?);
756 rewrite < assoc_plus in ⊢ (? (? ? (? % ?)) ?);
757 rewrite < assoc_plus in \vdash (? % ?);
758 rewrite < assoc_plus in ⊢ (? (? % ?) ?);
759 rewrite > assoc_plus in \vdash (? % ?);
760 rewrite > sym_plus in ⊢ (? (? ? %) ?);
761 rewrite > assoc_plus in ⊢ (? (? ? %) ?);
762 rewrite > assoc_plus in ⊢ (? (? ? (? % ?)) ?);
763 rewrite > assoc_plus in ⊢ (? (? ? %) ?);
764 rewrite > assoc_plus in ⊢ (? (? ? (? ? %)) ?);
765 simplify in ⊢ (? (? ? (? ? (? ? %))) ?);
766 rewrite < assoc_plus in ⊢ (? (? ? %) ?);
767 rewrite < assoc_plus in ⊢ (? % ?);apply le_plus_l;
768 rewrite > assoc_plus in \vdash (? % ?);
769 rewrite > assoc_plus in ⊢ (? (? ? %) ?);
770 rewrite > sym_plus in ⊢ (? (? ? (? ? %)) ?);
771 rewrite < assoc_plus in ⊢ (? (? ? %) ?);
772 rewrite < assoc_plus in \vdash (? % ?);apply le_plus_l;
773 rewrite > assoc_plus in \vdash (? ? %);apply le_n]
774 |apply (trans_le ? ? ? H);apply lt_to_le;apply (trans_le ? ? ? H1);
778 lemma eq_div_div_div_times: \forall a,b,c. O < b \to O < c \to a/b/c = a/(b*c).
779 intros.rewrite > (div_mod a (b*c)) in \vdash (? ? % ?)
780 [rewrite > (div_mod (a \mod (b*c)) b)
781 [rewrite < assoc_plus;
782 rewrite > sym_times in ⊢ (? ? (? (? (? (? (? ? %) ?) ?) ?) ?) ?);
783 rewrite < assoc_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
784 rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
785 rewrite > sym_times in ⊢ (? ? (? (? (? (? ? %) ?) ?) ?) ?);
786 rewrite < distr_times_plus;rewrite < sym_times in ⊢ (? ? (? (? (? % ?) ?) ?) ?);
787 rewrite > (div_plus_times b)
788 [rewrite > (div_plus_times c)
790 |apply lt_times_to_lt_div;rewrite > sym_times in \vdash (? ? %);
791 apply lt_mod_m_m;unfold lt;rewrite > times_n_SO;apply le_times;assumption]
792 |apply lt_mod_m_m;assumption]
794 |unfold lt;rewrite > times_n_SO;apply le_times;assumption]
797 lemma le_prim_stima: \forall n,b. S O < b \to b < sqrt n \to
799 2*S (log b (pred n))/(log b n) + 2*(pred n)*S (log b 2)/(log b n)
800 +2*S (log b (pred (sqrt n)))/(log b n)+ 2*(pred (sqrt n))*S (log b 2)/(log b n)
801 + 14*n/(log b n * log b n) + 28*n*S (log b 3)/(pred (log b n) * log b n)
806 [apply lt_to_le;apply (trans_le ? ? ? H);apply (trans_le ? (sqrt n))
807 [apply lt_to_le;assumption
809 |apply (trans_le ? (sqrt n))
810 [apply lt_to_le;assumption
811 |apply le_sqrt_n_n]]]
812 apply (trans_le ? ((2*S (log b (pred n))+2*(pred n)*S (log b 2)
813 +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))
814 +(14*n/log b n+28*n*S (log b 3)/pred (log b n))
816 [apply le_times_to_le_div
818 |rewrite > sym_times;apply le_prim_log_stima;assumption]
819 |apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*(pred n)*S (log b 2)
820 +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))
821 +(14*n/log b n+28*n*S (log b 3)/pred (log b n))) 4 (log b n) ?))
823 |rewrite < plus_n_Sm;apply le_S_S;rewrite > assoc_plus in \vdash (? ? %);
824 rewrite > sym_plus in \vdash (? ? (? ? %));
825 rewrite < assoc_plus in \vdash (? ? %);
826 apply le_plus_l;apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*(pred n)*S (log b 2)
827 +(2*S (log b (pred (sqrt n)))+2*(pred (sqrt n))*S (log b 2))) (14*n/log b n+28*n*S (log b 3)/pred (log b n)) (log b n) ?));
829 |rewrite < plus_n_Sm in \vdash (? ? %);apply le_S_S;
830 change in \vdash (? ? (? ? %)) with (1+3);
831 rewrite < assoc_plus in \vdash (? ? %);
832 rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?));
833 rewrite > assoc_plus in ⊢ (? ? (? % ?));
834 rewrite > sym_plus in \vdash (? ? %);rewrite < assoc_plus in \vdash (? ? %);
835 rewrite > sym_plus in \vdash (? ? (? % ?));apply le_plus
836 [apply (trans_le ? ? ? (le_div_plus_S (2*S (log b (pred n))+2*pred n*S (log b 2)) (2*S (log b (pred (sqrt n)))+2*pred (sqrt n)*S (log b 2)) (log b n) ?))
838 |rewrite < plus_n_Sm;apply le_S_S;change in \vdash (? ? (? ? %)) with (1+1);
839 rewrite < assoc_plus in \vdash (? ? %);rewrite > assoc_plus in ⊢ (? ? (? (? % ?) ?));
840 rewrite > assoc_plus in ⊢ (? ? (? % ?));
841 rewrite > sym_plus in \vdash (? ? %);
842 rewrite < assoc_plus in \vdash (? ? %);
843 rewrite > sym_plus in \vdash (? ? (? % ?));
845 [rewrite < plus_n_Sm;rewrite < plus_n_O;apply le_div_plus_S;
847 |rewrite < plus_n_Sm;rewrite < plus_n_O;apply le_div_plus_S;
849 |rewrite < plus_n_Sm;rewrite < plus_n_O;apply (trans_le ? ? ? (le_div_plus_S ? ? ? ?));
851 |apply le_S_S;apply le_plus
852 [rewrite > eq_div_div_div_times;
855 |rewrite > eq_div_div_div_times
857 |rewrite > minus_n_O in \vdash (? ? (? %));
858 rewrite < eq_minus_S_pred;apply lt_to_lt_O_minus;
859 apply (trans_le ? (log b (sqrt n * sqrt n)))
867 lemma leq_sqrt_n : \forall n. sqrt n * sqrt n \leq n.
868 intro;unfold sqrt;apply leb_true_to_le;apply f_max_true;apply (ex_intro ? ? O);
871 |simplify;reflexivity]
874 lemma le_sqrt_log_n : \forall n,b. 2 < b \to sqrt n * log b n \leq n.
876 apply (trans_le ? ? ? ? (leq_sqrt_n ?));
877 apply le_times_r;unfold sqrt;
879 [apply le_log_n_n;apply lt_to_le;assumption
880 |apply le_to_leb_true;elim (le_to_or_lt_eq ? ? (le_O_n n))
881 [apply (trans_le ? (exp b (log b n)))
884 |simplify in \vdash (? ? %);
885 elim (le_to_or_lt_eq ? ? (le_O_n n1))
886 [elim (le_to_or_lt_eq ? ? H3)
887 [apply (trans_le ? (3*(n1*n1)));
888 [simplify in \vdash (? % ?);rewrite > sym_times in \vdash (? % ?);
889 simplify in \vdash (? % ?);
890 simplify;rewrite > sym_plus;
891 rewrite > plus_n_Sm;rewrite > sym_plus in \vdash (? (? % ?) ?);
892 rewrite > assoc_plus;apply le_plus_r;
895 apply lt_plus;rewrite > times_n_SO in \vdash (? % ?);
896 apply lt_times_r1;assumption;
900 |rewrite < H4;apply le_times
901 [apply lt_to_le;assumption
902 |apply lt_to_le;simplify;rewrite < times_n_SO;assumption]]
903 |rewrite < H3;simplify;rewrite < times_n_SO;do 2 apply lt_to_le;assumption]]
904 |simplify;apply le_exp_log;assumption]
905 |rewrite < H1;simplify;apply le_n]]
908 (* Bertrand weak, lavori in corso
910 theorem bertrand_weak : \forall n. 9 \leq n \to prim n < prim (4*n).
912 apply (trans_le ? ? ? (le_S_S ? ? (le_prim_stima ? 2 ? ?)))
914 |unfold sqrt;apply f_m_to_le_max
915 [do 6 apply lt_to_le;assumption
916 |apply le_to_leb_true;assumption]
917 |cut (pred ((4*n)/(S (log 2 (4*n)))) \leq prim (4*n))
918 [|apply le_S_S_to_le;rewrite < S_pred
919 [apply le_times_to_le_div2
921 |change in \vdash (? % (? (? (? %)) (? (? ? %)))) with (2*2*n);
922 rewrite > assoc_times in \vdash (? % (? (? (? %)) (? (? ? %))));
923 rewrite > sym_times in \vdash (? ? %);
924 apply le_priml;rewrite > (times_n_O O) in \vdash (? % ?);
927 |apply (trans_le ? ? ? ? H);apply le_S_S;apply le_O_n]]
928 |apply le_times_to_le_div;
930 |rewrite < times_n_SO;apply (trans_le ? (S (S (2 + (log 2 n)))))
931 [apply le_S_S;apply (log_times 2 4 n);apply le_S_S;apply le_n
932 |change in \vdash (? % ?) with (4 + log 2 n);
933 rewrite > S_pred in \vdash (? ? (? ? %));
934 [change in ⊢ (? ? (? ? %)) with (1 + pred n);
935 rewrite > distr_times_plus;apply le_plus_r;elim H
936 [simplify;do 3 apply le_S_S;apply le_O_n
937 |apply (trans_le ? (log 2 (2*n1)))
939 [apply le_S_S;apply le_n
940 |rewrite < times_SSO_n;
941 change in \vdash (? % ?) with (1 + n1);
942 apply le_plus_l;apply (trans_le ? ? ? ? H1);
944 |apply (trans_le ? (S (4*pred n1)))
945 [rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?);
947 [change in \vdash (? ? %) with (1 + (4*pred n1));
950 |apply le_S_S;apply le_n
951 |apply (trans_le ? ? ? ? H1);apply le_S_S;apply le_O_n]
952 |simplify in \vdash (? ? (? ? %));
953 rewrite > minus_n_O in \vdash (? (? (? ? (? %))) ?);
954 rewrite < eq_minus_S_pred;
955 rewrite > distr_times_minus;
956 change in \vdash (? % ?) with (1 + (4*n1 - 4));
957 rewrite > eq_plus_minus_minus_minus
958 [simplify;apply le_minus_m;
960 |rewrite > times_n_SO in \vdash (? % ?);
961 apply le_times_r;apply (trans_le ? ? ? ? H1);
963 |apply (trans_le ? ? ? ? H);apply lt_O_S]]]]]
964 apply (trans_le ? ? ? ? Hcut);