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 set "baseuri" "cic:/matita/Z/moebius".
17 include "nat/factorization.ma".
18 include "Z/sigma_p.ma".
20 let rec moebius_aux p n : Z \def
24 match p_ord n (nth_prime p1) with
25 [ (pair q r) \Rightarrow
27 [ O \Rightarrow moebius_aux p1 r
30 [ O \Rightarrow Zopp (moebius_aux p1 r)
31 | (S q2) \Rightarrow OZ
38 definition moebius : nat \to Z \def
40 let p \def (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) in
43 theorem moebius_O : moebius O = pos O.
44 simplify. reflexivity.
47 theorem moebius_SO : moebius (S O) = pos O.
51 theorem moebius_SSO : moebius (S (S O)) = neg O.
55 theorem moebius_SSSO : moebius (S (S (S O))) = neg O.
60 theorem not_divides_to_p_ord_O: \forall n,i.
61 Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) =
65 [apply lt_O_nth_prime_n
71 theorem p_ord_O_to_not_divides: \forall n,i,r.
73 p_ord n (nth_prime i) = pair nat nat O r
74 \to Not (divides (nth_prime i) n).
76 lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
77 [apply lt_SO_nth_prime_n
87 theorem not_divides_to_eq_moebius_aux: \forall n,p,p1.p \le p1 \to
88 (\forall i. p \le i \to i \le p1 \to Not (divides (nth_prime i) n))
89 \to moebius_aux p n = moebius_aux p1 n.
94 rewrite > not_divides_to_p_ord_O
95 [simplify.apply H2.intros.
96 apply H3[assumption|apply le_S.assumption]
97 |apply H3[assumption|apply le_n_Sn]
102 theorem eq_moebius_moebius_aux: \forall n,p.
103 max_prime_factor n < p \to p \le n \to
104 moebius n = moebius_aux p n.
108 (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n
110 apply not_divides_to_eq_moebius_aux
113 apply divides_b_false_to_not_divides.
115 apply (lt_max_to_false ? n i)
117 |apply (trans_le ? p)[assumption|assumption]
122 theorem moebius_aux_SO: \forall p.moebius_aux p (S O) = pos O.
125 [simplify.reflexivity
128 apply not_divides_to_eq_moebius_aux
130 |intros.unfold.intro.
131 absurd (nth_prime i \le S O)
133 [apply le_n|assumption]
135 apply lt_SO_nth_prime_n.
141 theorem p_ord_to_not_eq_O : \forall n,p,q,r.
143 p_ord n (nth_prime p) = pair nat nat q r \to
148 [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
149 [apply lt_SO_nth_prime_n.
152 apply (lt_to_not_eq ? ? Hcut).
157 |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
161 theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r.
163 p = max_prime_factor n \to
164 p_ord n (nth_prime p) \neq pair nat nat O r.
165 intros.unfold Not.intro.
166 apply (p_ord_O_to_not_divides ? ? ? ? H2)
167 [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
169 apply divides_max_prime_factor_n.
174 theorem p_ord_SO_SO_to_moebius : \forall n,p.
176 p = max_prime_factor n \to
177 p_ord n (nth_prime p) = pair nat nat (S O) (S O) \to
178 moebius n = Zopp (pos O).
181 (moebius_aux (S (max_prime_factor n)) n = neg O).
182 rewrite < H1.simplify.
183 rewrite > H2.simplify.
184 rewrite > moebius_aux_SO.
188 theorem p_ord_SO_r_to_moebius1 : \forall n,p,r.
190 p = max_prime_factor n \to
192 p_ord n (nth_prime p) = pair nat nat (S O) r \to
193 moebius n = Zopp (moebius r).
196 (moebius_aux (S (max_prime_factor n)) n = -(moebius r)).
197 rewrite < H1.simplify.
198 rewrite > H3.simplify.
202 (moebius_aux (S (max_prime_factor r)) r = moebius_aux p r).
203 apply not_divides_to_eq_moebius_aux
204 [apply (p_ord_to_lt_max_prime_factor n p (S O) ? ? H1)
205 [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
206 |apply sym_eq. assumption
210 lapply (decidable_le i r).
212 [apply divides_b_false_to_not_divides.
213 apply (lt_max_to_false ? r i)[assumption|assumption]
214 |unfold.intro.apply H6.
215 apply (trans_le ? (nth_prime i))
217 apply lt_n_nth_prime_n
219 [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
227 theorem p_ord_SO_r_to_moebius : \forall n,p,r.
229 p = max_prime_factor n \to
230 p_ord n (nth_prime p) = pair nat nat (S O) r \to
231 moebius n = Zopp (moebius r).
233 apply (nat_case r);intro
235 apply (p_ord_to_not_eq_O ? ? ? ? H H2).
237 |apply (nat_case m);intros
238 [simplify.apply (p_ord_SO_SO_to_moebius ? ? H H1 H2)
239 |apply (p_ord_SO_r_to_moebius1 ? ? ? H H1 ? H2).
240 apply le_S_S.apply le_S_S.apply le_O_n
245 theorem p_ord_SSq_r_to_moebius : \forall n,p,q,r.
247 p = max_prime_factor n \to
248 p_ord n (nth_prime p) = pair nat nat (S (S q)) r \to
252 (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n =OZ).
253 rewrite < H1.simplify.
254 rewrite > H2.simplify.
258 lemma eq_p_max: \forall n,p,r:nat. O < n \to
260 r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to
261 p = max_prime_factor (r*(nth_prime p)\sup n).
264 unfold max_prime_factor.
265 apply max_spec_to_max.
268 [rewrite > times_n_SO in \vdash (? % ?).
273 apply (lt_to_le_to_lt ? (nth_prime p))
274 [apply lt_n_nth_prime_n
275 |rewrite > exp_n_SO in \vdash (? % ?).
277 [apply lt_O_nth_prime_n
282 |apply eq_to_eqb_true.
283 apply divides_to_mod_O
284 [apply lt_O_nth_prime_n
285 |apply (lt_O_n_elim ? H).
287 apply (witness ? ? (r*(nth_prime p \sup m))).
288 rewrite < assoc_times.
289 rewrite < sym_times in \vdash (? ? ? (? % ?)).
290 rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).
291 rewrite > assoc_times.
292 rewrite < exp_plus_times.
297 apply not_eq_to_eqb_false.
299 lapply (mod_O_to_divides ? ? ? H5)
300 [apply lt_O_nth_prime_n
301 |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n)))
303 [rewrite > H6 in Hletin.
305 rewrite < plus_n_O in Hletin.
306 apply Hcut.assumption
307 |elim (divides_times_to_divides ? ? ? ? Hletin)
308 [apply (lt_to_not_le ? ? H3).
310 apply (le_to_lt_to_lt ? ? ? ? H6).
312 [apply (trans_le ? (nth_prime i))
314 apply lt_n_nth_prime_n
315 |apply divides_to_le[assumption|assumption]
317 |apply eq_to_eqb_true.
318 apply divides_to_mod_O
319 [apply lt_O_nth_prime_n|assumption]
321 |apply prime_nth_prime
322 |apply Hcut.assumption
326 apply (lt_to_not_eq ? ? H3).
328 elim (prime_nth_prime p).
329 apply injective_nth_prime.
331 [apply (divides_exp_to_divides ? ? ? ? H6).
332 apply prime_nth_prime.
333 |apply lt_SO_nth_prime_n
340 lemma lt_max_prime_factor_to_not_divides: \forall n,p:nat.
341 O < n \to n=S O \lor max_prime_factor n < p \to
342 (nth_prime p \ndivides n).
343 intros.unfold Not.intro.
346 apply (le_to_not_lt (nth_prime p) (S O))
347 [apply divides_to_le[apply le_n|assumption]
348 |apply lt_SO_nth_prime_n
350 |apply (not_le_Sn_n p).
352 apply (le_to_lt_to_lt ? ? ? ? H3).
353 unfold max_prime_factor.
355 [apply (trans_le ? (nth_prime p))
357 apply lt_n_nth_prime_n
358 |apply divides_to_le;assumption
360 |apply eq_to_eqb_true.
361 apply divides_to_mod_O
362 [apply lt_O_nth_prime_n|assumption]
367 theorem moebius_exp: \forall p,q,r:nat. O < r \to
368 r = (S O) \lor (max_prime_factor r) < p \to
369 (* r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to *)
370 sigma_p (S (S q)) (\lambda y.true) (\lambda y.moebius (r*(exp (nth_prime p) y))) = O.
373 [rewrite > true_to_sigma_p_Sn
374 [rewrite > true_to_sigma_p_Sn
375 [rewrite > Zplus_z_OZ.
376 rewrite < times_n_SO.
377 rewrite > (p_ord_SO_r_to_moebius ? p r)
378 [rewrite > sym_Zplus.
379 rewrite > Zplus_Zopp.
383 rewrite > times_n_SO.
384 apply lt_to_le_to_lt_times
385 [apply lt_SO_nth_prime_n
390 [apply le_n|assumption|assumption]
392 [apply lt_O_nth_prime_n
393 |apply lt_max_prime_factor_to_not_divides;assumption
401 |rewrite > true_to_sigma_p_Sn
403 rewrite > Zplus_z_OZ.
404 apply (p_ord_SSq_r_to_moebius ? p n r)
405 [rewrite > times_n_SO.
406 rewrite > sym_times in \vdash (? ? %).
407 apply lt_to_le_to_lt_times
408 [apply (trans_lt ? (nth_prime p))
409 [apply lt_SO_nth_prime_n
410 |rewrite > exp_n_SO in \vdash (? % ?).
412 [apply lt_SO_nth_prime_n
413 |apply le_S_S.apply le_S_S.apply le_O_n
420 [apply le_S_S.apply le_O_n|assumption|assumption]
422 [apply lt_O_nth_prime_n
423 |apply lt_max_prime_factor_to_not_divides;assumption
432 theorem sigma_p_moebius1: \forall n,m,p:nat.O < n \to O < m \to
433 n = (S O) \lor max_prime_factor n < p \to
434 sigma_p (S (n*(exp (nth_prime p) m))) (\lambda y.divides_b y (n*(exp (nth_prime p) m))) moebius = O.
436 rewrite > sigma_p_divides_b
437 [apply (trans_eq ? ? (sigma_p (S n) (\lambda x:nat.divides_b x n) (\lambda x:nat.OZ)))
440 |apply (lt_O_n_elim m H1).
441 intros.apply moebius_exp
442 [apply (divides_b_true_to_lt_O ? ? ? H4).
445 [left.rewrite > H5 in H3.
446 elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? H3))
448 apply (lt_to_not_le O x)
449 [apply (divides_b_true_to_lt_O n x H H4)
450 |apply le_S_S_to_le.assumption
455 apply (le_to_lt_to_lt ? ? ? ? H5).
456 apply (divides_to_max_prime_factor1 x n)
457 [apply (divides_b_true_to_lt_O ? ? H H4)
459 |apply divides_b_true_to_divides.
465 |generalize in match (\lambda x:nat.divides_b x n).
468 [simplify.elim (f O);reflexivity
469 |apply (bool_elim ? (f (S n1)))
471 rewrite > true_to_sigma_p_Sn
472 [rewrite > H3.reflexivity|assumption]
474 rewrite > false_to_sigma_p_Sn
475 [apply H3|assumption]
480 |apply prime_nth_prime
481 |apply lt_max_prime_factor_to_not_divides;assumption
485 theorem sigma_p_moebius: \forall n. (S O) < n \to
486 sigma_p (S n) (\lambda y.divides_b y n) moebius = O.
488 lapply (exp_ord (nth_prime (max_prime_factor n)) n)
489 [rewrite > sym_times in Hletin.
491 apply sigma_p_moebius1
493 [apply lt_SO_nth_prime_n
494 |apply lt_to_le.assumption
498 (fst ? ? (pair ? ? (S O) (S O)) \leq ord n (nth_prime (max_prime_factor n))).
499 rewrite < (p_ord_p (nth_prime (max_prime_factor n)))
500 [apply (divides_to_le_ord ? (nth_prime (max_prime_factor n)) n)
501 [apply lt_O_nth_prime_n
502 |apply lt_to_le.assumption
503 |apply prime_nth_prime
504 |apply divides_max_prime_factor_n.
507 |apply lt_SO_nth_prime_n
509 |lapply (lt_O_ord_rem (nth_prime (max_prime_factor n)) n)
510 [elim (le_to_or_lt_eq ? ? Hletin1)
512 apply (p_ord_to_lt_max_prime_factor1 n (max_prime_factor n)
513 (ord n (nth_prime (max_prime_factor n)))
514 (ord_rem n (nth_prime (max_prime_factor n))))
515 [apply lt_to_le.assumption
520 |left.apply sym_eq.assumption
522 |apply lt_SO_nth_prime_n
523 |apply lt_to_le.assumption
526 |apply lt_SO_nth_prime_n
527 |apply lt_to_le.assumption