]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Z/inversion.ma
Proof of the moebius inversion theorem
[helm.git] / helm / software / matita / library / Z / inversion.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/Z/inversion".
16
17 include "Z/dirichlet_product.ma".
18 include "Z/moebius.ma".
19
20 definition sigma_div: (nat \to Z) \to nat \to Z \def
21 \lambda f.\lambda n. sigma_p (S n) (\lambda d.divides_b d n) f.
22
23 theorem sigma_div_moebius:
24 \forall n:nat. O < n \to sigma_div moebius n = is_one n.
25 intros.elim H
26   [reflexivity
27   |rewrite > is_one_OZ  
28     [unfold sigma_div.
29      apply sigma_p_moebius.
30      apply le_S_S.
31      assumption
32     |unfold Not.intro.
33      apply (lt_to_not_eq ? ? H1).
34      apply injective_S.
35      apply sym_eq.
36      assumption
37     ]
38   ]
39 qed.
40   
41 (* moebius inversion theorem *)
42 theorem inversion: \forall f:nat \to Z.\forall n:nat.O < n \to
43 dirichlet_product moebius (sigma_div f) n = f n.
44 intros.
45 rewrite > commutative_dirichlet_product
46   [apply (trans_eq ? ? (dirichlet_product (dirichlet_product f (\lambda n.Zone)) moebius n))
47     [unfold dirichlet_product.
48      apply eq_sigma_p1;intros
49       [reflexivity
50       |apply eq_f2
51         [apply sym_eq.
52          unfold sigma_div.
53          apply dirichlet_product_one_r.
54          apply (divides_b_true_to_lt_O ? ? H H2)
55         |reflexivity
56         ]
57       ]
58     |rewrite > associative_dirichlet_product
59       [apply (trans_eq ? ? (dirichlet_product f (sigma_div moebius) n))
60         [unfold dirichlet_product.
61          apply eq_sigma_p1;intros
62           [reflexivity
63           |apply eq_f2
64             [reflexivity
65             |unfold sigma_div.
66              apply dirichlet_product_one_l.
67              apply (lt_times_n_to_lt x)
68               [apply (divides_b_true_to_lt_O ? ? H H2)
69               |rewrite > divides_to_div
70                 [assumption
71                 |apply (divides_b_true_to_divides ? ? H2)
72                 ]
73               ]
74             ]
75           ]
76         |apply (trans_eq ? ? (dirichlet_product f is_one n))
77           [unfold dirichlet_product.
78            apply eq_sigma_p1;intros
79             [reflexivity
80             |apply eq_f2
81               [reflexivity
82               |apply sigma_div_moebius.
83                apply (lt_times_n_to_lt x)
84                 [apply (divides_b_true_to_lt_O ? ? H H2)
85                 |rewrite > divides_to_div
86                   [assumption
87                   |apply (divides_b_true_to_divides ? ? H2)
88                   ]
89                 ]
90               ]
91             ]
92           |apply dirichlet_product_is_one_r
93           ]
94         ]
95       |assumption
96       ]
97     ]
98   |assumption
99   ]
100 qed.
101