]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/arithmetics/chebyshev/chebyshev_B.ma
- some additions and renaming ...
[helm.git] / matita / matita / lib / arithmetics / chebyshev / chebyshev_B.ma
1 (*
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.           
5     ||I||                                                            
6     ||T||  
7     ||A||  
8     \   /  This file is distributed under the terms of the       
9      \ /   GNU General Public License Version 2   
10       V_____________________________________________________________*)
11
12 include "arithmetics/chebyshev/chebyshev.ma".
13     
14 definition B ≝ λn.
15 ∏_{p < S n | primeb p} 
16   (∏_{i < log p n} (exp p (mod (n /(exp p (S i))) 2))).
17   
18 lemma Bdef : ∀n.B n = 
19   ∏_{p < S n | primeb p} 
20   (∏_{i < log p n} (exp p (mod (n /(exp p (S i))) 2))).
21 // qed-.
22
23 example B_SSSO: B 3 = 6. //
24 qed.
25
26 example B_SSSSO: B 4 = 6. //
27 qed.
28
29 example B_SSSSSO: B 5 = 30. //
30 qed.
31
32 example B_SSSSSSO: B 6 = 20. //
33 qed.
34
35 example B_SSSSSSSO: B 7 = 140. //
36 qed.
37
38 example B_SSSSSSSSO: B 8 = 70. //
39 qed.
40
41 theorem eq_fact_B:∀n. 1 < n →
42   (2*n)! = exp (n!) 2 * B(2*n).
43 #n #lt1n >fact_pi_p3 @eq_f2
44   [@sym_eq >pi_p_primeb5 [@exp_fact_2|//] |// ]
45 qed.
46
47 theorem le_B_A: ∀n. B n ≤ A n.
48 #n >eq_A_A' @le_pi #p #ltp #primep
49 @le_pi #i #lti #_ >(exp_n_1 p) in ⊢ (??%); @le_exp
50   [@prime_to_lt_O @primeb_true_to_prime //
51   |@le_S_S_to_le @lt_mod_m_m @lt_O_S
52   ]
53 qed.
54
55 theorem le_B_A4: ∀n. O < n → 2 * B (4*n) ≤ A (4*n).
56 #n #posn >eq_A_A'
57 cut (2 < (S (4*n)))
58   [@le_S_S >(times_n_1 2) in ⊢ (?%?); @le_times //] #H2
59 cut (O<log 2 (4*n))
60   [@lt_O_log [@le_S_S_to_le @H2 |@le_S_S_to_le @H2]] #Hlog
61 >Bdef >(bigop_diff ??? timesAC ? 2 ? H2) [2:%]
62 >Adef >(bigop_diff ??? timesAC ? 2 ? H2) in ⊢ (??%); [2:%]
63 <associative_times @le_times
64   [>(bigop_diff ??? timesAC ? 0 ? Hlog) [2://]
65    >(bigop_diff ??? timesAC ? 0 ? Hlog) in ⊢ (??%); [2:%]
66    <associative_times >timesACdef @le_times 
67     [<exp_n_1 cut (4=2*2) [//] #H4 >H4 >associative_times
68      >commutative_times in ⊢ (?(??(??(?(?%?)?)))?);
69      >div_times [2://] >divides_to_mod_O
70       [@le_n |%{n} // |@lt_O_S]
71     |@le_pi #i #lti #H >(exp_n_1 2) in ⊢ (??%);
72      @le_exp [@lt_O_S |@le_S_S_to_le @lt_mod_m_m @lt_O_S]
73     ]
74   |@le_pi #p #ltp #Hp @le_pi #i #lti #H
75    >(exp_n_1 p) in ⊢ (??%); @le_exp
76     [@prime_to_lt_O @primeb_true_to_prime @(andb_true_r ?? Hp)
77     |@le_S_S_to_le @lt_mod_m_m @lt_O_S
78     ]
79   ]
80 qed.
81
82 (* not usefull    
83 theorem le_fact_A:\forall n.S O < n \to
84 fact (2*n) \le exp (fact n) 2 * A (2*n).
85 intros.
86 rewrite > eq_fact_B
87   [apply le_times_r.
88    apply le_B_A
89   |assumption
90   ]
91 qed. *)
92
93 theorem lt_SO_to_le_B_exp: ∀n. 1 < n →
94   B (2*n) ≤ exp 2 (pred (2*n)).
95 #n #lt1n @(le_times_to_le (exp (fact n) 2))
96   [@lt_O_exp //
97   |<(eq_fact_B … lt1n) <commutative_times in ⊢ (??%);
98    >exp_2 <associative_times @fact_to_exp 
99   ]
100 qed.
101
102 theorem le_B_exp: ∀n.
103   B (2*n) ≤ exp 2 (pred (2*n)).
104 #n cases n
105   [@le_n|#n1 cases n1 [@le_n |#n2 @lt_SO_to_le_B_exp @le_S_S @lt_O_S]]
106 qed.
107
108 theorem lt_4_to_le_B_exp: ∀n.4 < n →
109   B (2*n) \le exp 2 ((2*n)-2).
110 #n #lt4n @(le_times_to_le (exp (fact n) 2))
111   [@lt_O_exp //
112   |<eq_fact_B
113     [<commutative_times in ⊢ (??%); >exp_2 <associative_times
114      @lt_4_to_fact //
115     |@lt_to_le @lt_to_le @lt_to_le //
116     ]
117   ]
118 qed.
119
120 theorem lt_1_to_le_exp_B: ∀n. 1 < n →
121   exp 2 (2*n) ≤ 2 * n * B (2*n).
122 #n #lt1n 
123 @(le_times_to_le (exp (fact n) 2))
124   [@lt_O_exp @le_1_fact
125   |<associative_times in ⊢ (??%); >commutative_times in ⊢ (??(?%?));
126    >associative_times in ⊢ (??%); <(eq_fact_B … lt1n)
127    <commutative_times; @exp_to_fact2 @lt_to_le // 
128   ]
129 qed.
130
131 theorem le_exp_B: ∀n. O < n →
132   exp 2 (2*n) ≤ 2 * n * B (2*n).
133 #n #posn cases posn
134   [@le_n |#m #lt1m @lt_1_to_le_exp_B @le_S_S // ]
135 qed.
136
137 let rec bool_to_nat b ≝ 
138   match b with [true ⇒ 1 | false ⇒ 0].
139   
140 theorem eq_A_2_n: ∀n.O < n →
141 A(2*n) =
142  ∏_{p <S (2*n) | primeb p}
143   (∏_{i <log p (2*n)} (exp p (bool_to_nat (leb (S n) (exp p (S i)))))) *A n.
144 #n #posn >eq_A_A' > eq_A_A' 
145 cut (
146  ∏_{p < S n | primeb p} (∏_{i <log p n} p)
147  = ∏_{p < S (2*n) | primeb p}
148      (∏_{i <log p (2*n)} (p\sup(bool_to_nat (¬ (leb (S n) (exp p (S i))))))))
149   [2: #Hcut >Adef in ⊢ (???%); >Hcut
150    <times_pi >Adef @same_bigop
151     [//
152     |#p #lt1p #primep <times_pi @same_bigop
153       [//
154       |#i #lt1i #_ cases (true_or_false (leb (S n) (exp p (S i)))) #Hc >Hc
155         [normalize <times_n_1 >plus_n_O //
156         |normalize <plus_n_O <plus_n_O //
157         ]
158       ]
159     ]
160   |@(trans_eq ?? 
161     (∏_{p < S n | primeb p} 
162       (∏_{i < log p n} (p \sup(bool_to_nat (¬leb (S n) (exp p (S i))))))))
163     [@same_bigop
164       [//
165       |#p #lt1p #primep @same_bigop
166         [//
167         |#i #lti#_ >lt_to_leb_false
168           [normalize @plus_n_O
169           |@le_S_S @(transitive_le ? (exp p (log p n)))
170             [@le_exp [@prime_to_lt_O @primeb_true_to_prime //|//]
171             |@le_exp_log //
172             ]
173           ]
174         ]
175       ]
176     |@(trans_eq ?? 
177       (∏_{p < S (2*n) | primeb p}
178        (∏_{i <log p n} (p \sup(bool_to_nat (¬leb (S n) (p \sup(S i))))))))
179       [@(pad_bigop_nil … timesA)
180         [@le_S_S //|#i #lti #upi %2 >lt_to_log_O //]
181       |@same_bigop 
182         [//
183         |#p #ltp #primep @(pad_bigop_nil … timesA)
184           [@le_log
185             [@prime_to_lt_SO @primeb_true_to_prime //|//]
186           |#i #lei #iup %2 >le_to_leb_true
187             [%
188             |@(lt_to_le_to_lt ? (exp p (S (log p n))))
189               [@lt_exp_log @prime_to_lt_SO @primeb_true_to_prime //
190               |@le_exp
191                 [@prime_to_lt_O @primeb_true_to_prime //
192                 |@le_S_S //
193                 ]
194               ]
195             ]
196           ]
197         ]
198       ]
199     ]
200   ]
201 qed.
202                
203 theorem le_A_BA1: ∀n. O < n → 
204   A(2*n) ≤ B(2*n)*A n.
205 #n #posn >(eq_A_2_n … posn) @le_times [2:@le_n]
206 >Bdef @le_pi #p #ltp #primep @le_pi #i #lti #_ @le_exp
207   [@prime_to_lt_O @primeb_true_to_prime //
208   |cases (true_or_false (leb (S n) (exp p (S i)))) #Hc >Hc
209     [whd in ⊢ (?%?);
210      cut (2*n/p\sup(S i) = 1) [2: #Hcut >Hcut @le_n]
211      @(div_mod_spec_to_eq (2*n) (exp p (S i)) 
212        ? (mod (2*n) (exp p (S i))) ? (minus (2*n) (exp p (S i))) )
213       [@div_mod_spec_div_mod @lt_O_exp @prime_to_lt_O @primeb_true_to_prime //
214       |cut (p\sup(S i)≤2*n)
215         [@(transitive_le ? (exp p (log p (2*n))))
216           [@le_exp [@prime_to_lt_O @primeb_true_to_prime // | //]
217           |@le_exp_log >(times_n_O O) in ⊢ (?%?); @lt_times // 
218           ]
219         ] #Hcut
220        @div_mod_spec_intro
221         [@lt_plus_to_minus
222           [// |normalize in ⊢ (? % ?); < plus_n_O @lt_plus @leb_true_to_le //]
223         |>commutative_plus >commutative_times in ⊢ (???(??%));
224          < times_n_1 @plus_minus_m_m //
225         ]
226       ]
227     |@le_O_n
228     ]
229   ]
230 qed.
231
232 theorem le_A_BA: ∀n. A(2*n) \le B(2*n)*A n.
233 #n cases n [@le_n |#m @le_A_BA1 @lt_O_S]
234 qed.
235
236 theorem le_A_exp: ∀n. A(2*n) ≤ (exp 2 (pred (2*n)))*A n.
237 #n @(transitive_le ? (B(2*n)*A n))
238   [@le_A_BA |@le_times [@le_B_exp |//]]
239 qed.
240
241 theorem lt_4_to_le_A_exp: ∀n. 4 < n →
242   A(2*n) ≤ exp 2 ((2*n)-2)*A n.
243 #n #lt4n @(transitive_le ? (B(2*n)*A n))
244   [@le_A_BA|@le_times [@(lt_4_to_le_B_exp … lt4n) |@le_n]]
245 qed.
246
247 (* two technical lemmas *)
248 lemma times_2_pred: ∀n. 2*(pred n) \le pred (2*n).
249 #n cases n
250   [@le_n|#m @monotonic_le_plus_r @le_n_Sn]
251 qed.
252
253 lemma le_S_times_2: ∀n. O < n → S n ≤ 2*n.
254 #n #posn elim posn
255   [@le_n
256   |#m #posm #Hind 
257    cut (2*(S m) = S(S(2*m))) [normalize <plus_n_Sm //] #Hcut >Hcut
258    @le_S_S @(transitive_le … Hind) @le_n_Sn
259   ]
260 qed.
261
262 theorem le_A_exp1: ∀n.
263   A(exp 2 n) ≤ exp 2 ((2*(exp 2 n)-(S(S n)))).
264 #n elim n
265   [@le_n
266   |#n1 #Hind whd in ⊢ (?(?%)?); >commutative_times 
267    @(transitive_le ??? (le_A_exp ?)) 
268    @(transitive_le ? (2\sup(pred (2*2^n1))*2^(2*2^n1-(S(S n1)))))
269     [@monotonic_le_times_r // 
270     |<exp_plus_times @(le_exp … (lt_O_S ?))
271      cut (S(S n1) ≤ 2*(exp 2 n1))
272       [elim n1
273         [@le_n
274         |#n2 >commutative_times in ⊢ (%→?); #Hind1 @(transitive_le ? (2*(S(S n2))))
275           [@le_S_times_2 @lt_O_S |@monotonic_le_times_r //] 
276         ]
277       ] #Hcut
278      @le_S_S_to_le cut(∀a,b. S a + b = S (a+b)) [//] #Hplus <Hplus >S_pred
279       [>eq_minus_S_pred in ⊢ (??%); >S_pred
280         [>plus_minus_commutative
281           [@monotonic_le_minus_l
282            cut (∀a. 2*a = a + a) [//] #times2 <times2 
283            @monotonic_le_times_r >commutative_times @le_n
284           |@Hcut
285           ]
286         |@lt_plus_to_minus_r whd in ⊢ (?%?);
287          @(lt_to_le_to_lt ? (2*(S(S n1))))
288           [>(times_n_1 (S(S n1))) in ⊢ (?%?); >commutative_times
289            @monotonic_lt_times_l [@lt_O_S |@le_n]
290           |@monotonic_le_times_r whd in ⊢ (??%); //
291           ]
292         ]
293       |whd >(times_n_1 1) in ⊢ (?%?); @le_times
294         [@le_n_Sn |@lt_O_exp @lt_O_S]
295       ]
296     ]
297   ]
298 qed.
299
300 theorem monotonic_A: monotonic nat le A.
301 #n #m #lenm elim lenm
302   [@le_n
303   |#n1 #len #Hind @(transitive_le … Hind)
304    cut (∏_{p < S n1 | primeb p}(p^(log p n1))
305           ≤∏_{p < S n1 | primeb p}(p^(log p (S n1))))
306     [@le_pi #p #ltp #primep @le_exp
307       [@prime_to_lt_O @primeb_true_to_prime //
308       |@le_log [@prime_to_lt_SO @primeb_true_to_prime // | //]
309       ]
310     ] #Hcut
311    >psi_def in ⊢ (??%); cases (true_or_false (primeb (S n1))) #Hc
312     [>bigop_Strue in ⊢ (??%); [2://]
313      >(times_n_1 (A n1)) >commutative_times @le_times
314       [@lt_O_exp @lt_O_S |@Hcut]
315     |>bigop_Sfalse in ⊢ (??%); // 
316     ]
317   ]
318 qed.
319
320 (*
321 theorem le_A_exp2: \forall n. O < n \to
322 A(n) \le (exp (S(S O)) ((S(S O)) * (S(S O)) * n)).
323 intros.
324 apply (trans_le ? (A (exp (S(S O)) (S(log (S(S O)) n)))))
325   [apply monotonic_A.
326    apply lt_to_le.
327    apply lt_exp_log.
328    apply le_n
329   |apply (trans_le ? ((exp (S(S O)) ((S(S O))*(exp (S(S O)) (S(log (S(S O)) n)))))))
330     [apply le_A_exp1
331     |apply le_exp
332       [apply lt_O_S
333       |rewrite > assoc_times.apply le_times_r.
334        change with ((S(S O))*((S(S O))\sup(log (S(S O)) n))≤(S(S O))*n).
335        apply le_times_r.
336        apply le_exp_log.
337        assumption
338       ]
339     ]
340   ]
341 qed.
342 *)
343
344 (* example *)
345 example A_1: A 1 = 1. // qed.
346
347 example A_2: A 2 = 2. // qed.
348
349 example A_3: A 3 = 6. // qed.
350
351 example A_4: A 4 = 12. // qed.
352
353 (*
354 (* a better result *)
355 theorem le_A_exp3: \forall n. S O < n \to
356 A(n) \le exp (pred n) (2*(exp 2 (2 * n)).
357 intro.
358 apply (nat_elim1 n).
359 intros.
360 elim (or_eq_eq_S m).
361 elim H2
362   [elim (le_to_or_lt_eq (S O) a)
363     [rewrite > H3 in ⊢ (? % ?).
364      apply (trans_le ? ((exp (S(S O)) ((S(S O)*a)))*A a))
365       [apply le_A_exp
366       |apply (trans_le ? (((S(S O)))\sup((S(S O))*a)*
367          ((pred a)\sup((S(S O)))*((S(S O)))\sup((S(S O))*a))))
368         [apply le_times_r.
369          apply H
370           [rewrite > H3.
371            rewrite > times_n_SO in ⊢ (? % ?).
372            rewrite > sym_times.
373            apply lt_times_l1
374             [apply lt_to_le.assumption
375             |apply le_n
376             ]
377           |assumption
378           ]
379         |rewrite > sym_times.
380          rewrite > assoc_times.
381          rewrite < exp_plus_times.
382          apply (trans_le ? 
383           (pred a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
384           [rewrite > assoc_times.
385            apply le_times_r.
386            rewrite < exp_plus_times.
387            apply le_exp
388             [apply lt_O_S
389             |rewrite < H3.
390              simplify.
391              rewrite < plus_n_O.
392              apply le_S.apply le_S.
393              apply le_n
394             ]
395           |apply le_times_l.
396            rewrite > times_exp.
397            apply monotonic_exp1.
398            rewrite > H3.
399            rewrite > sym_times.
400            cases a
401             [apply le_n
402             |simplify.
403              rewrite < plus_n_Sm.
404              apply le_S.
405              apply le_n
406             ]
407           ]
408         ]
409       ]
410     |rewrite < H4 in H3.
411      simplify in H3.
412      rewrite > H3.
413      simplify.
414      apply le_S_S.apply le_S_S.apply le_O_n
415     |apply not_lt_to_le.intro.
416      apply (lt_to_not_le ? ? H1).
417      rewrite > H3.
418      apply (le_n_O_elim a)
419       [apply le_S_S_to_le.assumption
420       |apply le_O_n
421       ]
422     ]
423   |elim (le_to_or_lt_eq O a (le_O_n ?))
424     [apply (trans_le ? (A ((S(S O))*(S a))))
425       [apply monotonic_A.
426        rewrite > H3.
427        rewrite > times_SSO.
428        apply le_n_Sn
429       |apply (trans_le ? ((exp (S(S O)) ((S(S O)*(S a))))*A (S a)))
430         [apply le_A_exp
431         |apply (trans_le ? (((S(S O)))\sup((S(S O))*S a)*
432            (a\sup((S(S O)))*((S(S O)))\sup((S(S O))*(S a)))))
433           [apply le_times_r.
434            apply H
435             [rewrite > H3.
436              apply le_S_S.
437              simplify.
438              rewrite > plus_n_SO.
439              apply le_plus_r.
440              rewrite < plus_n_O.
441              assumption
442             |apply le_S_S.assumption
443             ]
444           |rewrite > sym_times.
445            rewrite > assoc_times.
446            rewrite < exp_plus_times.
447            apply (trans_le ? 
448             (a\sup((S(S O)))*(S(S O))\sup(S(S O))*(S(S O))\sup((S(S O))*m)))
449             [rewrite > assoc_times.
450              apply le_times_r.
451              rewrite < exp_plus_times.
452              apply le_exp
453               [apply lt_O_S
454               |rewrite > times_SSO.
455                rewrite < H3.
456                simplify.
457                rewrite < plus_n_Sm.
458                rewrite < plus_n_O.
459                apply le_n
460               ]
461             |apply le_times_l.
462              rewrite > times_exp.
463              apply monotonic_exp1.
464              rewrite > H3.
465              rewrite > sym_times.
466              apply le_n
467             ]
468           ]
469         ]
470       ]
471     |rewrite < H4 in H3.simplify in H3.
472      apply False_ind.
473      apply (lt_to_not_le ? ? H1).
474      rewrite > H3.
475      apply le_
476     ]
477   ]
478 qed.
479 *)
480
481 theorem le_A_exp4: ∀n. 1 < n →
482   A(n) ≤ (pred n)*exp 2 ((2 * n) -3).
483 #n @(nat_elim1 n)
484 #m #Hind cases (even_or_odd m)
485 #a * #Hm >Hm #Hlt
486   [cut (0<a) 
487     [cases a in Hlt; 
488       [whd in ⊢ (??%→?); #lt10 @False_ind @(absurd ? lt10 (not_le_Sn_O 1))
489     |#b #_ //]
490     ] #Hcut 
491    cases (le_to_or_lt_eq … Hcut) #Ha
492     [@(transitive_le ? (exp 2 (pred(2*a))*A a))
493       [@le_A_exp
494       |@(transitive_le ? (2\sup(pred(2*a))*((pred a)*2\sup((2*a)-3))))
495         [@monotonic_le_times_r @(Hind ?? Ha)
496          >Hm >(times_n_1 a) in ⊢ (?%?); >commutative_times
497          @monotonic_lt_times_l [@lt_to_le // |@le_n]
498         |<Hm <associative_times >commutative_times in ⊢ (?(?%?)?);
499          >associative_times; @le_times
500           [>Hm cases a[@le_n|#b normalize @le_plus_n_r]
501           |<exp_plus_times @le_exp
502             [@lt_O_S
503             |@(transitive_le ? (m+(m-3)))
504               [@monotonic_le_plus_l // 
505               |normalize <plus_n_O >plus_minus_commutative
506                 [@le_n
507                 |>Hm @(transitive_le ? (2*2) ? (le_n_Sn 3))
508                  @monotonic_le_times_r //
509                 ]
510               ]
511             ]
512           ]
513         ]
514       ]
515     |<Ha normalize @le_n
516     ]
517   |cases (le_to_or_lt_eq O a (le_O_n ?)) #Ha
518     [@(transitive_le ? (A (2*(S a))))
519       [@monotonic_A >Hm normalize <plus_n_Sm @le_n_Sn
520       |@(transitive_le … (le_A_exp ?) ) 
521        @(transitive_le ? ((2\sup(pred (2*S a)))*(a*(exp 2 ((2*(S a))-3)))))
522         [@monotonic_le_times_r @Hind
523           [>Hm @le_S_S >(times_n_1 a) in ⊢ (?%?); >commutative_times
524            @monotonic_lt_times_l //
525           |@le_S_S //
526           ]
527         |cut (pred (S (2*a)) = 2*a) [//] #Spred >Spred
528          cut (pred (2*(S a)) = S (2 * a)) [normalize //] #Spred1 >Spred1
529          cut (2*(S a) = S(S(2*a))) [normalize <plus_n_Sm //] #times2 
530          cut (exp 2 (2*S a -3) = 2*(exp 2 (S(2*a) -3))) 
531           [>(commutative_times 2) in ⊢ (???%); >times2 >minus_Sn_m [%]
532            @le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha
533           ] #Hcut >Hcut
534          <associative_times in ⊢ (? (? ? %) ?); <associative_times
535          >commutative_times in ⊢ (? (? % ?) ?);
536          >commutative_times in ⊢ (? (? (? % ?) ?) ?);
537          >associative_times @monotonic_le_times_r
538          <exp_plus_times @(le_exp … (lt_O_S ?))
539          >plus_minus_commutative
540           [normalize >(plus_n_O (a+(a+0))) in ⊢ (?(?(??%)?)?); @le_n
541           |@le_S_S >(times_n_1 2) in ⊢ (?%?); @monotonic_le_times_r @Ha
542           ]
543         ]
544       ]
545     |@False_ind <Ha in Hlt; normalize #Hfalse @(absurd ? Hfalse) //
546     ]
547   ]
548 qed.
549
550 theorem le_n_8_to_le_A_exp: ∀n. n ≤ 8 → 
551   A(n) ≤ exp 2 ((2 * n) -3).
552 #n cases n
553   [#_ @le_n
554   |#n1 cases n1
555     [#_ @le_n
556     |#n2 cases n2
557       [#_ @le_n
558       |#n3 cases n3
559         [#_ @leb_true_to_le //
560         |#n4 cases n4
561           [#_ @leb_true_to_le //
562           |#n5 cases n5
563             [#_ @leb_true_to_le //
564             |#n6 cases n6
565               [#_ @leb_true_to_le //
566               |#n7 cases n7
567                 [#_ @leb_true_to_le //
568                 |#n8 cases n8
569                   [#_ @leb_true_to_le //
570                   |#n9 #H @False_ind @(absurd ?? (lt_to_not_le ?? H))
571                    @leb_true_to_le //
572                   ]
573                 ]
574               ]
575             ]
576           ]
577         ]
578       ]
579     ]
580   ]
581 qed.
582            
583 theorem le_A_exp5: ∀n. A(n) ≤ exp 2 ((2 * n) -3).
584 #n @(nat_elim1 n) #m #Hind
585 cases (decidable_le 9 m)
586   [#lem cases (even_or_odd m) #a * #Hm
587     [>Hm in ⊢ (?%?); @(transitive_le … (le_A_exp ?))
588      @(transitive_le ? (2\sup(pred(2*a))*(2\sup((2*a)-3))))
589       [@monotonic_le_times_r @Hind >Hm >(times_n_1 a) in ⊢ (?%?); 
590        >commutative_times @(monotonic_lt_times_l  … (le_n ?))
591        @(transitive_lt ? 3)
592         [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |<Hm @lt_to_le @lem]]
593       |<Hm <exp_plus_times @(le_exp … (lt_O_S ?))
594        whd in match (times 2 m); >commutative_times <times_n_1
595        <plus_minus_commutative
596         [@monotonic_le_plus_l @le_pred_n
597         |@(transitive_le … lem) @leb_true_to_le //
598         ]
599       ]
600     |@(transitive_le ? (A (2*(S a))))
601       [@monotonic_A >Hm normalize <plus_n_Sm @le_n_Sn
602       |@(transitive_le ? ((exp 2 ((2*(S a))-2))*A (S a)))
603         [@lt_4_to_le_A_exp @le_S_S
604          @(le_times_to_le 2)[@le_n_Sn|@le_S_S_to_le <Hm @lem]
605         |@(transitive_le ? ((2\sup((2*S a)-2))*(exp 2 ((2*(S a))-3))))
606           [@monotonic_le_times_r @Hind >Hm @le_S_S
607            >(times_n_1 a) in ⊢ (?%?); 
608            >commutative_times @(monotonic_lt_times_l  … (le_n ?))
609            @(transitive_lt ? 3)
610             [@lt_O_S |@(le_times_to_le 2) [@lt_O_S |@le_S_S_to_le <Hm @lem]]
611           |cut (∀a. 2*(S a) = S(S(2*a))) [normalize #a <plus_n_Sm //] #times2
612            >times2 <Hm <exp_plus_times @(le_exp … (lt_O_S ?))
613            cases m
614             [@le_n
615             |#n1 cases n1
616               [@le_n
617               |#n2 normalize <minus_n_O <plus_n_O <plus_n_Sm
618                normalize <minus_n_O <plus_n_Sm @le_n
619               ]
620             ]
621           ]
622         ]
623       ]
624     ]
625   |#H @le_n_8_to_le_A_exp @le_S_S_to_le @not_le_to_lt //
626   ]
627 qed.       
628
629 theorem le_exp_Al:∀n. O < n → exp 2 n ≤ A (2 * n).
630 #n #posn @(transitive_le ? ((exp 2 (2*n))/(2*n)))
631   [@le_times_to_le_div
632     [>(times_n_O O) in ⊢ (?%?); @lt_times [@lt_O_S|//]
633     |normalize in ⊢ (??(??%)); < plus_n_O >exp_plus_times
634      @le_times [2://] elim posn [//]
635      #m #le1m #Hind whd in ⊢ (??%); >commutative_times in ⊢ (??%);
636      @monotonic_le_times_r @(transitive_le … Hind) 
637      >(times_n_1 m) in ⊢ (?%?); >commutative_times 
638      @(monotonic_lt_times_l  … (le_n ?)) @le1m
639     ]
640   |@le_times_to_le_div2
641     [>(times_n_O O) in ⊢ (?%?); @lt_times [@lt_O_S|//]
642     |@(transitive_le ? ((B (2*n)*(2*n))))
643       [<commutative_times in ⊢ (??%); @le_exp_B //
644       |@le_times [@le_B_A|@le_n]
645       ]
646     ]
647   ]
648 qed.
649
650 theorem le_exp_A2:∀n. 1 < n → exp 2 (n / 2) \le A n.
651 #n #lt1n @(transitive_le ? (A(n/2*2)))
652   [>commutative_times @le_exp_Al
653    cases (le_to_or_lt_eq ? ? (le_O_n (n/2))) [//]
654    #Heq @False_ind @(absurd ?? (lt_to_not_le ?? lt1n))
655    >(div_mod n 2) <Heq whd in ⊢ (?%?);
656    @le_S_S_to_le @(lt_mod_m_m n 2) @lt_O_S
657   |@monotonic_A >(div_mod n 2) in ⊢ (??%); @le_plus_n_r
658   ]
659 qed.
660
661 theorem eq_sigma_pi_SO_n: ∀n.∑_{i < n} 1 = n.
662 #n elim n //
663 qed.
664
665 theorem leA_prim: ∀n.
666   exp n (prim n) \le A n * ∏_{p < S n | primeb p} p.
667 #n <(exp_sigma (S n) n primeb) <times_pi @le_pi
668 #p #ltp #primep @lt_to_le @lt_exp_log
669 @prime_to_lt_SO @primeb_true_to_prime //
670 qed.
671
672 theorem le_prim_log : ∀n,b. 1 < b →
673   log b (A n) ≤ prim n * (S (log b n)).
674 #n #b #lt1b @(transitive_le … (log_exp1 …)) [@le_log // | //]
675 qed.
676
677 (*********************** the inequalities ***********************)
678 lemma exp_Sn: ∀b,n. exp b (S n) = b * (exp b n).
679 normalize // 
680 qed.
681
682 theorem le_exp_priml: ∀n. O < n →
683   exp 2 (2*n) ≤ exp (2*n) (S(prim (2*n))).
684 #n #posn @(transitive_le ? (((2*n*(B (2*n))))))
685   [@le_exp_B // 
686   |>exp_Sn @monotonic_le_times_r @(transitive_le ? (A (2*n)))
687     [@le_B_A |@le_Al]
688   ]
689 qed.
690
691 theorem le_exp_prim4l: ∀n. O < n →
692   exp 2 (S(4*n)) ≤ exp (4*n) (S(prim (4*n))).
693 #n #posn @(transitive_le ? (2*(4*n*(B (4*n)))))
694   [>exp_Sn @monotonic_le_times_r
695    cut (4*n = 2*(2*n)) [<associative_times //] #Hcut
696    >Hcut @le_exp_B @lt_to_le whd >(times_n_1 2) in ⊢ (?%?);
697    @monotonic_le_times_r //
698   |>exp_Sn <associative_times >commutative_times in ⊢ (?(?%?)?);
699    >associative_times @monotonic_le_times_r @(transitive_le ? (A (4*n)))
700     [@le_B_A4 // |@le_Al]
701   ]
702 qed.
703
704 theorem le_priml: ∀n. O < n →
705   2*n ≤ (S (log 2 (2*n)))*S(prim (2*n)).
706 #n #posn <(eq_log_exp 2 (2*n) ?) in ⊢ (?%?);
707   [@(transitive_le ? ((log 2) (exp (2*n) (S(prim (2*n))))))
708     [@le_log [@le_n |@le_exp_priml //]
709     |>commutative_times in ⊢ (??%); @log_exp1 @le_n
710     ]
711   |@le_n
712   ]
713 qed.
714
715 theorem le_exp_primr: ∀n.
716   exp n (prim n) ≤ exp 2 (2*(2*n-3)).
717 #n @(transitive_le ? (exp (A n) 2))
718   [>exp_Sn >exp_Sn whd in match (exp ? 0); <times_n_1 @leA_r2
719   |>commutative_times <exp_exp_times @le_exp1 [@lt_O_S |@le_A_exp5]
720   ]
721 qed.
722
723 (* bounds *)
724 theorem le_primr: ∀n. 1 < n → prim n \le 2*(2*n-3)/log 2 n.
725 #n #lt1n @le_times_to_le_div
726   [@lt_O_log // 
727   |@(transitive_le ? (log 2 (exp n (prim n))))
728     [>commutative_times @log_exp2
729       [@le_n |@lt_to_le //]
730     |<(eq_log_exp 2 (2*(2*n-3))) in ⊢ (??%);
731       [@le_log [@le_n |@le_exp_primr]
732       |@le_n
733       ]
734     ]
735   ]
736 qed.
737      
738 theorem le_priml1: ∀n. O < n →
739   2*n/((log 2 n)+2) - 1 ≤ prim (2*n).
740 #n #posn @le_plus_to_minus @le_times_to_le_div2
741   [>commutative_plus @lt_O_S
742   |>commutative_times in ⊢ (??%); <plus_n_Sm <plus_n_Sm in ⊢ (??(??%));
743    <plus_n_O <commutative_plus <log_exp
744     [@le_priml // | //| @le_n]
745   ]
746 qed.
747
748
749
750