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