]> matita.cs.unibo.it Git - helm.git/blob - nat/chebyshev_teta.ma
made executable again
[helm.git] / nat / chebyshev_teta.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        Matita is distributed under the terms of the          *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/nat/chebyshev_teta".
16
17 include "nat/binomial.ma".
18 include "nat/pi_p.ma".
19
20 (* This is chebishev teta function *)
21
22 definition teta: nat \to nat \def
23 \lambda n. pi_p (S n) primeb (\lambda p.p).
24
25 theorem lt_O_teta: \forall n. O < teta n.
26 intros.elim n
27   [apply le_n
28   |unfold teta.apply (bool_elim ? (primeb (S n1)));intro 
29     [rewrite > true_to_pi_p_Sn
30       [rewrite > (times_n_O O).
31        apply lt_times
32         [apply lt_O_S
33         |assumption
34         ]
35       |assumption
36       ]
37     |rewrite > false_to_pi_p_Sn;assumption
38     ]
39   ]
40 qed.
41
42 definition M \def \lambda m.bc (S(2*m)) m.
43
44 theorem lt_M: \forall m. O < m \to M m < exp 2 (2*m).
45 intros.
46 apply (lt_times_to_lt 2)
47   [apply lt_O_S
48   |change in ⊢ (? ? %) with (exp 2 (S(2*m))).
49    change in ⊢ (? ? (? % ?)) with (1+1).
50    rewrite > exp_plus_sigma_p.
51    apply (le_to_lt_to_lt ? (sigma_p (S (S (2*m))) (λk:nat.orb (eqb k m) (eqb k (S m)))
52             (λk:nat.bc (S (2*m)) k*(1)\sup(S (2*m)-k)*(1)\sup(k))))
53     [rewrite > (sigma_p_gi ? ? m)
54       [rewrite > (sigma_p_gi ? ? (S m))
55         [rewrite > (false_to_eq_sigma_p O (S(S(2*m))))
56           [simplify in ⊢ (? ? (? ? (? ? %))).
57            simplify in ⊢ (? % ?).
58            rewrite < exp_SO_n.rewrite < exp_SO_n.
59            rewrite < exp_SO_n.rewrite < exp_SO_n.
60            rewrite < times_n_SO.rewrite < times_n_SO.
61            rewrite < times_n_SO.rewrite < times_n_SO.
62            apply le_plus
63             [unfold M.apply le_n
64             |apply le_plus_l.unfold M.
65              change in \vdash (? ? %) with (fact (S(2*m))/(fact (S m)*(fact ((2*m)-m)))).
66              simplify in \vdash (? ? (? ? (? ? (? (? % ?))))).
67              rewrite < plus_n_O.rewrite < minus_plus_m_m.
68              rewrite < sym_times in \vdash (? ? (? ? %)).
69              change in \vdash (? % ?) with (fact (S(2*m))/(fact m*(fact (S(2*m)-m)))).
70              simplify in \vdash (? (? ? (? ? (? (? (? %) ?)))) ?).
71              rewrite < plus_n_O.change in \vdash (? (? ? (? ? (? (? % ?)))) ?) with (S m + m).
72              rewrite < minus_plus_m_m.
73              apply le_n
74             ]
75           |apply le_O_n
76           |intros.
77            elim (eqb i m);elim (eqb i (S m));reflexivity
78           ]
79         |apply le_S_S.apply le_S_S.
80          apply le_times_n.
81          apply le_n_Sn
82         |rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S m))).
83          rewrite > (not_eq_to_eqb_false (S m) m)
84           [reflexivity
85           |intro.apply (not_eq_n_Sn m).
86            apply sym_eq.assumption
87           ]
88         ]
89       |apply le_S.apply le_S_S.
90        apply le_times_n.
91        apply le_n_Sn
92       |rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S m))).
93        reflexivity
94       ]
95     |rewrite > (bool_to_nat_to_eq_sigma_p (S(S(2*m))) ? (\lambda k.true) ? 
96       (\lambda k.bool_to_nat (eqb k m\lor eqb k (S m))*(bc (S (2*m)) k*(1)\sup(S (2*m)-k)*(1)\sup(k))))
97      in \vdash (? % ?)
98       [apply lt_sigma_p
99         [intros.elim (eqb i m\lor eqb i (S m))
100           [rewrite > sym_times.rewrite < times_n_SO.apply le_n
101           |apply le_O_n
102           ]
103         |apply (ex_intro ? ? O).
104          split
105           [split[apply lt_O_S|reflexivity]
106           |rewrite > (not_eq_to_eqb_false ? ? (not_eq_O_S m)).
107            rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H)).
108            simplify in \vdash (? % ?).
109            rewrite < exp_SO_n.rewrite < exp_SO_n.
110            rewrite > bc_n_O.simplify.
111            apply le_n
112           ]
113         ]
114       |intros.rewrite > sym_times in \vdash (? ? ? %).
115        rewrite < times_n_SO.
116        reflexivity
117       ]
118     ]
119   ]
120 qed.
121       
122 theorem divides_fact_to_divides: \forall p,n. prime p \to divides p n! \to 
123 \exists m.O < m \land m \le n \land divides p m.  
124 intros 3.elim n
125   [apply False_ind.elim H.
126    apply (lt_to_not_le ? ? H2).
127    apply divides_to_le[apply le_n|assumption]
128   |rewrite > factS in H2.
129    elim (divides_times_to_divides ? ? ? H H2)
130     [apply (ex_intro ? ? (S n1)).split
131       [split
132         [apply lt_O_S
133         |apply le_n
134         ]
135       |assumption
136       ]
137     |elim (H1 H3).elim H4.elim H5.
138      apply (ex_intro ? ? a).split
139       [split
140         [assumption
141         |apply le_S.assumption
142         ]
143       |assumption
144       ]
145     ]
146   ]
147 qed.
148       
149 theorem divides_fact_to_le: \forall p,n. prime p \to divides p n! \to 
150 p \le n.  
151 intros.
152 elim (divides_fact_to_divides p n H H1).
153 elim H2.elim H3.
154 apply (trans_le ? a)
155   [apply divides_to_le;assumption
156   |assumption
157   ]
158 qed.
159      
160 theorem prime_to_divides_M: \forall m,p. prime p \to S m < p \to p \le S(2*m) \to
161 divides p (M m).      
162 intros.unfold M.
163 elim (bc2 (S(2*m)) m)
164   [unfold bc.rewrite > H3.
165    rewrite > sym_times.
166    rewrite > lt_O_to_div_times
167     [elim (divides_times_to_divides p (m!*(S (2*m)-m)!) n2)
168       [apply False_ind.
169        elim (divides_times_to_divides p (m!) (S (2*m)-m)!)
170         [apply (lt_to_not_le ? ? (lt_to_le ? ? H1)).
171          apply divides_fact_to_le;assumption
172         |apply (lt_to_not_le ? ? H1).
173          apply divides_fact_to_le
174           [assumption
175           |cut (S m = S(2*m)-m)
176             [rewrite > Hcut.assumption
177             |simplify in ⊢ (? ? ? (? (? %) ?)).
178              rewrite < plus_n_O.
179              change in ⊢ (? ? ? (? % ?)) with (S m + m).
180              apply minus_plus_m_m
181             ]
182           ]
183         |assumption
184         |assumption
185         ]
186       |assumption
187       |assumption
188       |rewrite < H3.
189        apply divides_fact
190         [apply prime_to_lt_O.assumption
191         |assumption
192         ]
193       ]
194     |rewrite > (times_n_O O).
195      apply lt_times;apply lt_O_fact
196     ]
197   |simplify in ⊢ (? ? (? %)).
198    rewrite < plus_n_O.
199    change in ⊢ (? ? %) with (S m + m).
200    apply le_plus_n
201   ]
202 qed.
203              
204 theorem divides_pi_p_M1: \forall m.\forall i. i \le (S(S(2*m))) \to 
205 divides (pi_p i (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p)) (M m).
206 intros 2.
207 elim i
208   [simplify.apply (witness ? ? (M m)).rewrite > sym_times.apply times_n_SO
209   |apply (bool_elim ? (leb (S (S m)) n \land primeb n));intro
210     [rewrite > true_to_pi_p_Sn
211       [apply divides_to_divides_times
212         [apply primeb_true_to_prime.
213          apply (andb_true_true_r ? ? H2).
214         |cut (\forall p.prime p \to n \le p \to ¬p∣pi_p n (λp:nat.leb (S (S m)) p∧primeb p) (λp:nat.p))
215           [apply Hcut
216             [apply primeb_true_to_prime.
217              apply (andb_true_true_r ? ? H2)
218             |apply le_n
219             ]
220           |intros 2.
221            elim n
222             [simplify.intro.elim H3.apply (lt_to_not_le ? ? H6).
223              apply divides_to_le
224               [apply le_n
225               |assumption
226               ]
227             |apply (bool_elim ? (leb (S (S m)) n1∧primeb n1));intro
228               [rewrite > true_to_pi_p_Sn
229                 [intro.elim (divides_times_to_divides ? ? ? H3 H7)
230                   [apply (le_to_not_lt ? ? H5).
231                    apply le_S_S.
232                    apply divides_to_le
233                     [apply prime_to_lt_O.
234                      apply primeb_true_to_prime.
235                      apply (andb_true_true_r ? ? H6)
236                     |assumption
237                     ]
238                   |apply H4
239                     [apply lt_to_le.assumption
240                     |assumption
241                     ]
242                   ]
243                 |assumption
244                 ]
245               |rewrite > false_to_pi_p_Sn
246                 [apply H4.
247                  apply lt_to_le.assumption
248                 |assumption
249                 ]
250               ]
251             ]
252           ]
253         |apply prime_to_divides_M
254           [apply primeb_true_to_prime.
255            apply (andb_true_true_r ? ? H2)
256           |apply leb_true_to_le.
257            apply (andb_true_true ? ? H2)
258           |apply le_S_S_to_le.assumption
259           ]
260         |apply H.
261          apply lt_to_le.
262          assumption
263         ]
264       |assumption
265       ]
266     |rewrite > false_to_pi_p_Sn
267       [apply H.
268        apply lt_to_le.
269        assumption
270       |assumption
271       ]
272     ]
273   ]
274 qed.
275
276 theorem divides_pi_p_M:\forall m.
277 divides (pi_p (S(S(2*m))) (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p)) (M m).
278 intros. 
279 apply divides_pi_p_M1.
280 apply le_n.
281 qed.  
282
283 theorem teta_pi_p_teta: \forall m. teta (S (2*m))
284 =pi_p (S (S (2*m))) (λp:nat.leb (S (S m)) p∧primeb p) (λp:nat.p)*teta (S m).
285 intro.unfold teta.
286 rewrite > (eq_pi_p1 ? (\lambda p.leb p (S m) \land primeb p) ? (\lambda p.p) (S(S m)))
287   [rewrite < (false_to_eq_pi_p (S(S m)) (S(S(2*m))))
288     [generalize in match (S(S(2*m))).intro.
289      elim n
290       [simplify.reflexivity
291       |apply (bool_elim ? (primeb n1));intro
292         [rewrite > true_to_pi_p_Sn
293           [apply (bool_elim ? (leb n1 (S m))); intro
294             [rewrite > false_to_pi_p_Sn
295               [rewrite > true_to_pi_p_Sn
296                 [rewrite < assoc_times.
297                  rewrite > sym_times in ⊢ (? ? ? (? % ?)).
298                  rewrite > assoc_times.
299                  apply eq_f.
300                  assumption
301                 |apply true_to_true_to_andb_true;assumption
302                 ]
303               |rewrite > lt_to_leb_false
304                 [reflexivity
305                 |apply le_S_S.
306                  apply leb_true_to_le.
307                  assumption
308                 ]
309               ]
310             |rewrite > true_to_pi_p_Sn
311               [rewrite > false_to_pi_p_Sn
312                 [rewrite > assoc_times.
313                  apply eq_f.
314                  assumption
315                 |rewrite > H2.reflexivity
316                 ]
317               |rewrite > H1.
318                rewrite > le_to_leb_true
319                 [reflexivity
320                 |apply not_le_to_lt.
321                  apply leb_false_to_not_le.
322                  assumption
323                 ]
324               ]
325             ]
326           |assumption 
327           ]
328         |rewrite > false_to_pi_p_Sn
329           [rewrite > false_to_pi_p_Sn
330             [rewrite > false_to_pi_p_Sn
331               [assumption
332               |rewrite > H1.
333                rewrite > andb_sym.
334                reflexivity
335               ]
336             |rewrite > H1.
337              rewrite > andb_sym.
338              reflexivity
339             ]
340           |assumption
341           ]
342         ]
343       ]
344     |apply le_S_S.apply le_S_S.
345      apply le_times_n.
346      apply le_n_Sn
347     |intros.
348      rewrite > lt_to_leb_false
349       [reflexivity
350       |assumption
351       ]
352     ]
353   |intros.
354    rewrite > le_to_leb_true
355     [reflexivity
356     |apply le_S_S_to_le.
357      assumption
358     ]
359   |intros.reflexivity
360   ]
361 qed.                  
362
363 theorem div_teta_teta: \forall m. 
364 teta (S(2*m))/teta (S m) = pi_p (S(S(2*m))) (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p).
365 intros.apply (div_mod_spec_to_eq ? ? ? ? ? O (div_mod_spec_div_mod ? ? ? ))
366   [apply lt_O_teta
367   |apply div_mod_spec_intro
368     [apply lt_O_teta
369     |rewrite < plus_n_O.
370      apply teta_pi_p_teta
371     ]
372   ]
373 qed.
374                      
375 theorem le_teta_M_teta: \forall m. 
376 teta (S(2*m)) \le (M m)*teta (S m).  
377 intro.
378 rewrite > teta_pi_p_teta. 
379 apply le_times_l.
380 apply divides_to_le
381   [unfold M.apply lt_O_bc.apply lt_to_le.
382    apply le_S_S.apply le_times_n.
383    apply le_n_Sn
384   |apply divides_pi_p_M
385   ]
386 qed.
387
388 theorem lt_O_to_le_teta_M_teta: \forall m. O < m\to
389 teta (S(2*m)) < exp 2 (2*m)*teta (S m). 
390 intros. 
391 apply (le_to_lt_to_lt ? (M m*teta (S m)))
392   [apply le_teta_M_teta
393   |apply lt_times_l1
394     [apply lt_O_teta
395     |apply lt_M.
396      assumption
397     ]
398   ]
399 qed.
400
401   
402