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