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