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