helm/software/matita/library/Z/moebius.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 "nat/factorization.ma".
  16 include "Z/sigma_p.ma".
  17
  18 let rec moebius_aux p n : Z \def
  19   match p with
  20   [ O \Rightarrow pos O
  21   | (S p1) \Rightarrow
  22     match p_ord n (nth_prime p1) with
  23     [ (pair q r) \Rightarrow
  24       match q with
  25       [ O \Rightarrow moebius_aux p1 r
  26       | (S q1) \Rightarrow
  27               match q1 with
  28               [ O \Rightarrow Zopp (moebius_aux p1 r)
  29         | (S q2) \Rightarrow OZ
  30         ]
  31       ]
  32     ]
  33   ]
  34 .
  35
  36 definition moebius : nat \to Z \def
  37 \lambda n.
  38   let p \def (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) in
  39   moebius_aux (S p) n.
  40
  41 (*
  42 theorem moebius_O : moebius O = pos O.
  43 simplify. reflexivity.
  44 qed.
  45
  46 theorem moebius_SO : moebius (S O) = pos O.
  47 simplify.reflexivity.
  48 qed.
  49
  50 theorem moebius_SSO : moebius (S (S O)) = neg O.
  51 simplify.reflexivity.
  52 qed.
  53
  54 theorem moebius_SSSO : moebius (S (S (S O))) = neg O.
  55 simplify.reflexivity.
  56 qed.
  57
  58 theorem moebius_SSSSO : moebius (S (S (S (S O)))) = OZ.
  59 simplify.reflexivity.
  60 qed.
  61 *)
  62
  63 theorem not_divides_to_eq_moebius_aux: \forall n,p,p1.p \le p1 \to
  64 (\forall i. p \le i \to i \le p1 \to Not (divides (nth_prime i) n))
  65 \to moebius_aux p n = moebius_aux p1 n.
  66 intros 4.
  67 elim H
  68   [reflexivity
  69   |simplify.
  70    rewrite > not_divides_to_p_ord_O
  71     [simplify.apply H2.intros.
  72      apply H3[assumption|apply le_S.assumption]
  73     |apply H3[assumption|apply le_n_Sn]
  74     ]
  75   ]
  76 qed.
  77
  78 theorem eq_moebius_moebius_aux: \forall n,p.
  79 max_prime_factor n < p \to p \le n \to
  80 moebius n = moebius_aux p n.
  81 intros.
  82 unfold moebius.
  83 change with
  84 (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n
  85 = moebius_aux p n).
  86 apply not_divides_to_eq_moebius_aux
  87   [assumption
  88   |intros.
  89    apply divides_b_false_to_not_divides.
  90    unfold divides_b.
  91    apply (lt_max_to_false ? n i)
  92     [assumption
  93     |apply (trans_le ? p)[assumption|assumption]
  94     ]
  95   ]
  96 qed.
  97
  98 theorem moebius_aux_SO: \forall p.moebius_aux p (S O) = pos O.
  99 intros.
 100 elim p
 101   [simplify.reflexivity
 102   |rewrite < H.
 103    apply sym_eq.
 104    apply not_divides_to_eq_moebius_aux
 105    [apply le_n_Sn
 106    |intros.unfold.intro.
 107     absurd (nth_prime i \le S O)
 108       [apply divides_to_le
 109         [apply le_n|assumption]
 110       |apply lt_to_not_le.
 111        apply lt_SO_nth_prime_n.
 112       ]
 113     ]
 114   ]
 115 qed.
 116
 117 theorem p_ord_SO_SO_to_moebius : \forall n,p.
 118   (S O) < n \to
 119   p = max_prime_factor n \to
 120   p_ord n (nth_prime p) = pair nat nat (S O) (S O) \to
 121   moebius n = Zopp (pos O).
 122 intros.
 123 change with
 124   (moebius_aux (S (max_prime_factor n)) n = neg O).
 125 rewrite < H1.simplify.
 126 rewrite > H2.simplify.
 127 rewrite > moebius_aux_SO.
 128 reflexivity.
 129 qed.
 130
 131 theorem p_ord_SO_r_to_moebius1 : \forall n,p,r.
 132   (S O) < n \to
 133   p = max_prime_factor n \to
 134   (S O) < r \to
 135   p_ord n (nth_prime p) = pair nat nat (S O) r \to
 136   moebius n = Zopp (moebius r).
 137 intros.
 138 change with
 139   (moebius_aux (S (max_prime_factor n)) n = -(moebius r)).
 140 rewrite < H1.simplify.
 141 rewrite > H3.simplify.
 142 apply eq_f.
 143 apply sym_eq.
 144 change with
 145  (moebius_aux (S (max_prime_factor r)) r = moebius_aux p r).
 146 apply not_divides_to_eq_moebius_aux
 147   [apply (p_ord_to_lt_max_prime_factor n p (S O) ? ? H1)
 148     [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
 149     |apply sym_eq. assumption
 150     |assumption
 151     ]
 152   |intros.
 153    lapply (decidable_le i r).
 154    elim Hletin
 155     [apply divides_b_false_to_not_divides.
 156      apply (lt_max_to_false ? r i)[assumption|assumption]
 157     |unfold.intro.apply H6.
 158      apply (trans_le ? (nth_prime i))
 159       [apply lt_to_le.
 160        apply lt_n_nth_prime_n
 161       |apply divides_to_le
 162         [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
 163         |assumption
 164         ]
 165       ]
 166     ]
 167   ]
 168 qed.
 169
 170 theorem p_ord_SO_r_to_moebius : \forall n,p,r.
 171   (S O) < n \to
 172   p = max_prime_factor n \to
 173   p_ord n (nth_prime p) = pair nat nat (S O) r \to
 174   moebius n = Zopp (moebius r).
 175 intros 5.
 176 apply (nat_case r);intro
 177   [apply False_ind.
 178    apply (p_ord_to_not_eq_O ? ? ? ? H H2).
 179    reflexivity
 180   |apply (nat_case m);intros
 181     [simplify.apply (p_ord_SO_SO_to_moebius ? ? H H1 H2)
 182     |apply (p_ord_SO_r_to_moebius1 ? ? ? H H1 ? H2).
 183      apply le_S_S.apply le_S_S.apply le_O_n
 184     ]
 185   ]
 186 qed.
 187
 188 theorem p_ord_SSq_r_to_moebius : \forall n,p,q,r.
 189   (S O) < n \to
 190   p = max_prime_factor n \to
 191   p_ord n (nth_prime p) = pair nat nat (S (S q)) r \to
 192   moebius n = OZ.
 193 intros.
 194 change with
 195   (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n =OZ).
 196 rewrite < H1.simplify.
 197 rewrite > H2.simplify.
 198 reflexivity.
 199 qed.
 200
 201 theorem moebius_exp: \forall p,q,r:nat. O < r \to
 202 r = (S O) \lor (max_prime_factor r) < p \to
 203 (* r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to *)
 204 sigma_p (S (S q)) (\lambda y.true) (\lambda y.moebius (r*(exp (nth_prime p) y))) = O.
 205 intros.
 206 elim q
 207   [rewrite > true_to_sigma_p_Sn
 208     [rewrite > true_to_sigma_p_Sn
 209       [rewrite > Zplus_z_OZ.
 210        rewrite < times_n_SO.
 211        rewrite > (p_ord_SO_r_to_moebius ? p r)
 212         [rewrite > sym_Zplus.
 213          rewrite > Zplus_Zopp.
 214          reflexivity
 215         |rewrite < exp_n_SO.
 216          rewrite > sym_times.
 217          rewrite > times_n_SO.
 218          apply lt_to_le_to_lt_times
 219           [apply lt_SO_nth_prime_n
 220           |assumption
 221           |assumption
 222           ]
 223         |apply eq_p_max
 224           [apply le_n|assumption|assumption]
 225         |apply p_ord_exp1
 226           [apply lt_O_nth_prime_n
 227           |apply lt_max_prime_factor_to_not_divides;assumption
 228           |apply sym_times
 229           ]
 230         ]
 231       |reflexivity
 232       ]
 233     |reflexivity
 234     ]
 235   |rewrite > true_to_sigma_p_Sn
 236     [rewrite > H2.
 237      rewrite > Zplus_z_OZ.
 238      apply (p_ord_SSq_r_to_moebius ? p n r)
 239       [rewrite > times_n_SO.
 240        rewrite > sym_times in \vdash (? ? %).
 241        apply lt_to_le_to_lt_times
 242         [apply (trans_lt ? (nth_prime p))
 243           [apply lt_SO_nth_prime_n
 244             |rewrite > exp_n_SO in \vdash (? % ?).
 245              apply lt_exp
 246               [apply lt_SO_nth_prime_n
 247               |apply le_S_S.apply le_S_S.apply le_O_n
 248               ]
 249             ]
 250           |assumption
 251           |assumption
 252           ]
 253         |apply eq_p_max
 254           [apply le_S_S.apply le_O_n|assumption|assumption]
 255         |apply p_ord_exp1
 256           [apply lt_O_nth_prime_n
 257           |apply lt_max_prime_factor_to_not_divides;assumption
 258           |apply sym_times
 259           ]
 260         ]
 261       |reflexivity
 262       ]
 263     ]
 264 qed.
 265
 266 theorem sigma_p_moebius1: \forall n,m,p:nat.O < n \to O < m \to
 267 n = (S O) \lor max_prime_factor n < p \to
 268 sigma_p (S (n*(exp (nth_prime p) m))) (\lambda y.divides_b y (n*(exp (nth_prime p) m))) moebius = O.
 269 intros.
 270 rewrite > sigma_p_divides_b
 271   [apply (trans_eq ? ? (sigma_p (S n) (\lambda x:nat.divides_b x n) (\lambda x:nat.OZ)))
 272     [apply eq_sigma_p1
 273       [intros.reflexivity
 274       |apply (lt_O_n_elim m H1).
 275        intros.apply moebius_exp
 276         [apply (divides_b_true_to_lt_O ? ? ? H4).
 277          assumption
 278         |elim H2
 279           [left.rewrite > H5 in H3.
 280            elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? H3))
 281             [apply False_ind.
 282              apply (lt_to_not_le O x)
 283               [apply (divides_b_true_to_lt_O n x H H4)
 284               |apply le_S_S_to_le.assumption
 285               ]
 286             |assumption
 287             ]
 288           |right.
 289            apply (le_to_lt_to_lt ? ? ? ? H5).
 290            apply (divides_to_max_prime_factor1 x n)
 291             [apply (divides_b_true_to_lt_O ? ? H H4)
 292             |assumption
 293             |apply divides_b_true_to_divides.
 294              assumption
 295             ]
 296           ]
 297         ]
 298       ]
 299     |generalize in match (\lambda x:nat.divides_b x n).
 300      intro.
 301      elim n
 302       [simplify.elim (f O);reflexivity
 303       |apply (bool_elim ? (f (S n1)))
 304         [intro.
 305          rewrite > true_to_sigma_p_Sn
 306           [rewrite > H3.reflexivity|assumption]
 307         |intro.
 308          rewrite > false_to_sigma_p_Sn
 309           [apply H3|assumption]
 310         ]
 311       ]
 312     ]
 313   |assumption
 314   |apply prime_nth_prime
 315   |apply lt_max_prime_factor_to_not_divides;assumption
 316   ]
 317 qed.
 318
 319 theorem sigma_p_moebius: \forall n. (S O) < n \to
 320 sigma_p (S n) (\lambda y.divides_b y n) moebius = O.
 321 intros.
 322 lapply (exp_ord (nth_prime (max_prime_factor n)) n)
 323   [rewrite > sym_times in Hletin.
 324    rewrite > Hletin.
 325    apply sigma_p_moebius1
 326     [apply lt_O_ord_rem
 327       [apply lt_SO_nth_prime_n
 328       |apply lt_to_le.assumption
 329       ]
 330     |unfold lt.
 331      change with
 332       (fst ? ? (pair ? ? (S O) (S O)) \leq ord n (nth_prime (max_prime_factor n))).
 333      rewrite < (p_ord_p (nth_prime (max_prime_factor n)))
 334       [apply (divides_to_le_ord ? (nth_prime (max_prime_factor n)) n)
 335         [apply lt_O_nth_prime_n
 336         |apply lt_to_le.assumption
 337         |apply prime_nth_prime
 338         |apply divides_max_prime_factor_n.
 339          assumption
 340         ]
 341       |apply lt_SO_nth_prime_n
 342       ]
 343     |lapply (lt_O_ord_rem (nth_prime (max_prime_factor n)) n)
 344       [elim (le_to_or_lt_eq ? ? Hletin1)
 345         [right.
 346          apply (p_ord_to_lt_max_prime_factor1 n (max_prime_factor n)
 347           (ord n (nth_prime (max_prime_factor n)))
 348           (ord_rem n (nth_prime (max_prime_factor n))))
 349           [apply lt_to_le.assumption
 350           |apply le_n
 351           |autobatch
 352           |assumption
 353           ]
 354         |left.apply sym_eq.assumption
 355         ]
 356       |apply lt_SO_nth_prime_n
 357       |apply lt_to_le.assumption
 358       ]
 359     ]
 360   |apply lt_SO_nth_prime_n
 361   |apply lt_to_le.assumption
 362   ]
 363 qed.
 364
 365
 366