matita/library/nat/chebyshev_teta.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/binomial.ma".
  16 include "nat/pi_p.ma".
  17
  18 (* This is chebishev teta function *)
  19
  20 definition teta: nat \to nat \def
  21 \lambda n. pi_p (S n) primeb (\lambda p.p).
  22
  23 theorem lt_O_teta: \forall n. O < teta n.
  24 intros.elim n
  25   [apply le_n
  26   |unfold teta.apply (bool_elim ? (primeb (S n1)));intro
  27     [rewrite > true_to_pi_p_Sn
  28       [rewrite > (times_n_O O).
  29        apply lt_times
  30         [apply lt_O_S
  31         |assumption
  32         ]
  33       |assumption
  34       ]
  35     |rewrite > false_to_pi_p_Sn;assumption
  36     ]
  37   ]
  38 qed.
  39
  40 definition M \def \lambda m.bc (S(2*m)) m.
  41
  42 theorem lt_M: \forall m. O < m \to M m < exp 2 (2*m).
  43 intros.
  44 apply (lt_times_to_lt 2)
  45   [apply lt_O_S
  46   |change in ⊢ (? ? %) with (exp 2 (S(2*m))).
  47    change in ⊢ (? ? (? % ?)) with (1+1).
  48    rewrite > exp_plus_sigma_p.
  49    apply (le_to_lt_to_lt ? (sigma_p (S (S (2*m))) (λk:nat.orb (eqb k m) (eqb k (S m)))
  50             (λk:nat.bc (S (2*m)) k*(1)\sup(S (2*m)-k)*(1)\sup(k))))
  51     [rewrite > (sigma_p_gi ? ? m)
  52       [rewrite > (sigma_p_gi ? ? (S m))
  53         [rewrite > (false_to_eq_sigma_p O (S(S(2*m))))
  54           [simplify in ⊢ (? ? (? ? (? ? %))).
  55            simplify in ⊢ (? % ?).
  56            rewrite < exp_SO_n.rewrite < exp_SO_n.
  57            rewrite < exp_SO_n.rewrite < exp_SO_n.
  58            rewrite < times_n_SO.rewrite < times_n_SO.
  59            rewrite < times_n_SO.rewrite < times_n_SO.
  60            apply le_plus
  61             [unfold M.apply le_n
  62             |apply le_plus_l.unfold M.
  63              change in \vdash (? ? %) with (fact (S(2*m))/(fact (S m)*(fact ((2*m)-m)))).
  64              simplify in \vdash (? ? (? ? (? ? (? (? % ?))))).
  65              rewrite < plus_n_O.rewrite < minus_plus_m_m.
  66              rewrite < sym_times in \vdash (? ? (? ? %)).
  67              change in \vdash (? % ?) with (fact (S(2*m))/(fact m*(fact (S(2*m)-m)))).
  68              simplify in \vdash (? (? ? (? ? (? (? (? %) ?)))) ?).
  69              rewrite < plus_n_O.change in \vdash (? (? ? (? ? (? (? % ?)))) ?) with (S m + m).
  70              rewrite < minus_plus_m_m.
  71              apply le_n
  72             ]
  73           |apply le_O_n
  74           |intros.
  75            elim (eqb i m);elim (eqb i (S m));reflexivity
  76           ]
  77         |apply le_S_S.apply le_S_S.
  78          apply le_times_n.
  79          apply le_n_Sn
  80         |rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S m))).
  81          rewrite > (not_eq_to_eqb_false (S m) m)
  82           [reflexivity
  83           |intro.apply (not_eq_n_Sn m).
  84            apply sym_eq.assumption
  85           ]
  86         ]
  87       |apply le_S.apply le_S_S.
  88        apply le_times_n.
  89        apply le_n_Sn
  90       |rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S m))).
  91        reflexivity
  92       ]
  93     |rewrite > (bool_to_nat_to_eq_sigma_p (S(S(2*m))) ? (\lambda k.true) ?
  94       (\lambda k.bool_to_nat (eqb k m\lor eqb k (S m))*(bc (S (2*m)) k*(1)\sup(S (2*m)-k)*(1)\sup(k))))
  95      in \vdash (? % ?)
  96       [apply lt_sigma_p
  97         [intros.elim (eqb i m\lor eqb i (S m))
  98           [rewrite > sym_times.rewrite < times_n_SO.apply le_n
  99           |apply le_O_n
 100           ]
 101         |apply (ex_intro ? ? O).
 102          split
 103           [split[apply lt_O_S|reflexivity]
 104           |rewrite > (not_eq_to_eqb_false ? ? (not_eq_O_S m)).
 105            rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H)).
 106            simplify in \vdash (? % ?).
 107            rewrite < exp_SO_n.rewrite < exp_SO_n.
 108            rewrite > bc_n_O.simplify.
 109            apply le_n
 110           ]
 111         ]
 112       |intros.rewrite > sym_times in \vdash (? ? ? %).
 113        rewrite < times_n_SO.
 114        reflexivity
 115       ]
 116     ]
 117   ]
 118 qed.
 119
 120 theorem divides_fact_to_divides: \forall p,n. prime p \to divides p n! \to
 121 \exists m.O < m \land m \le n \land divides p m.
 122 intros 3.elim n
 123   [apply False_ind.elim H.
 124    apply (lt_to_not_le ? ? H2).
 125    apply divides_to_le[apply le_n|assumption]
 126   |rewrite > factS in H2.
 127    elim (divides_times_to_divides ? ? ? H H2)
 128     [apply (ex_intro ? ? (S n1)).split
 129       [split
 130         [apply lt_O_S
 131         |apply le_n
 132         ]
 133       |assumption
 134       ]
 135     |elim (H1 H3).elim H4.elim H5.
 136      apply (ex_intro ? ? a).split
 137       [split
 138         [assumption
 139         |apply le_S.assumption
 140         ]
 141       |assumption
 142       ]
 143     ]
 144   ]
 145 qed.
 146
 147 theorem divides_fact_to_le: \forall p,n. prime p \to divides p n! \to
 148 p \le n.
 149 intros.
 150 elim (divides_fact_to_divides p n H H1).
 151 elim H2.elim H3.
 152 apply (trans_le ? a)
 153   [apply divides_to_le;assumption
 154   |assumption
 155   ]
 156 qed.
 157
 158 theorem prime_to_divides_M: \forall m,p. prime p \to S m < p \to p \le S(2*m) \to
 159 divides p (M m).
 160 intros.unfold M.
 161 elim (bc2 (S(2*m)) m)
 162   [unfold bc.rewrite > H3.
 163    rewrite > sym_times.
 164    rewrite > lt_O_to_div_times
 165     [elim (divides_times_to_divides p (m!*(S (2*m)-m)!) n1)
 166       [apply False_ind.
 167        elim (divides_times_to_divides p (m!) (S (2*m)-m)!)
 168         [apply (lt_to_not_le ? ? (lt_to_le ? ? H1)).
 169          apply divides_fact_to_le;assumption
 170         |apply (lt_to_not_le ? ? H1).
 171          apply divides_fact_to_le
 172           [assumption
 173           |cut (S m = S(2*m)-m)
 174             [rewrite > Hcut.assumption
 175             |simplify in ⊢ (? ? ? (? (? %) ?)).
 176              rewrite < plus_n_O.
 177              change in ⊢ (? ? ? (? % ?)) with (S m + m).
 178              apply minus_plus_m_m
 179             ]
 180           ]
 181         |assumption
 182         |assumption
 183         ]
 184       |assumption
 185       |assumption
 186       |rewrite < H3.
 187        apply divides_fact
 188         [apply prime_to_lt_O.assumption
 189         |assumption
 190         ]
 191       ]
 192     |rewrite > (times_n_O O).
 193      apply lt_times;apply lt_O_fact
 194     ]
 195   |simplify in ⊢ (? ? (? %)).
 196    rewrite < plus_n_O.
 197    change in ⊢ (? ? %) with (S m + m).
 198    apply le_plus_n
 199   ]
 200 qed.
 201
 202 theorem divides_pi_p_M1: \forall m.\forall i. i \le (S(S(2*m))) \to
 203 divides (pi_p i (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p)) (M m).
 204 intros 2.
 205 elim i
 206   [simplify.apply (witness ? ? (M m)).rewrite > sym_times.apply times_n_SO
 207   |apply (bool_elim ? (leb (S (S m)) n \land primeb n));intro
 208     [rewrite > true_to_pi_p_Sn
 209       [apply divides_to_divides_times
 210         [apply primeb_true_to_prime.
 211          apply (andb_true_true_r ? ? H2).
 212         |cut (\forall p.prime p \to n \le p \to ¬p∣pi_p n (λp:nat.leb (S (S m)) p∧primeb p) (λp:nat.p))
 213           [apply Hcut
 214             [apply primeb_true_to_prime.
 215              apply (andb_true_true_r ? ? H2)
 216             |apply le_n
 217             ]
 218           |intros 2.
 219            elim n
 220             [simplify.intro.elim H3.apply (lt_to_not_le ? ? H6).
 221              apply divides_to_le
 222               [apply le_n
 223               |assumption
 224               ]
 225             |apply (bool_elim ? (leb (S (S m)) n1∧primeb n1));intro
 226               [rewrite > true_to_pi_p_Sn
 227                 [intro.elim (divides_times_to_divides ? ? ? H3 H7)
 228                   [apply (le_to_not_lt ? ? H5).
 229                    apply le_S_S.
 230                    apply divides_to_le
 231                     [apply prime_to_lt_O.
 232                      apply primeb_true_to_prime.
 233                      apply (andb_true_true_r ? ? H6)
 234                     |assumption
 235                     ]
 236                   |apply H4
 237                     [apply lt_to_le.assumption
 238                     |assumption
 239                     ]
 240                   ]
 241                 |assumption
 242                 ]
 243               |rewrite > false_to_pi_p_Sn
 244                 [apply H4.
 245                  apply lt_to_le.assumption
 246                 |assumption
 247                 ]
 248               ]
 249             ]
 250           ]
 251         |apply prime_to_divides_M
 252           [apply primeb_true_to_prime.
 253            apply (andb_true_true_r ? ? H2)
 254           |apply leb_true_to_le.
 255            apply (andb_true_true ? ? H2)
 256           |apply le_S_S_to_le.assumption
 257           ]
 258         |apply H.
 259          apply lt_to_le.
 260          assumption
 261         ]
 262       |assumption
 263       ]
 264     |rewrite > false_to_pi_p_Sn
 265       [apply H.
 266        apply lt_to_le.
 267        assumption
 268       |assumption
 269       ]
 270     ]
 271   ]
 272 qed.
 273
 274 theorem divides_pi_p_M:\forall m.
 275 divides (pi_p (S(S(2*m))) (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p)) (M m).
 276 intros.
 277 apply divides_pi_p_M1.
 278 apply le_n.
 279 qed.
 280
 281 theorem teta_pi_p_teta: \forall m. teta (S (2*m))
 282 =pi_p (S (S (2*m))) (λp:nat.leb (S (S m)) p∧primeb p) (λp:nat.p)*teta (S m).
 283 intro.unfold teta.
 284 rewrite > (eq_pi_p1 ? (\lambda p.leb p (S m) \land primeb p) ? (\lambda p.p) (S(S m)))
 285   [rewrite < (false_to_eq_pi_p (S(S m)) (S(S(2*m))))
 286     [generalize in match (S(S(2*m))).intro.
 287      elim n
 288       [simplify.reflexivity
 289       |apply (bool_elim ? (primeb n1));intro
 290         [rewrite > true_to_pi_p_Sn
 291           [apply (bool_elim ? (leb n1 (S m))); intro
 292             [rewrite > false_to_pi_p_Sn
 293               [rewrite > true_to_pi_p_Sn
 294                 [rewrite < assoc_times.
 295                  rewrite > sym_times in ⊢ (? ? ? (? % ?)).
 296                  rewrite > assoc_times.
 297                  apply eq_f.
 298                  assumption
 299                 |apply true_to_true_to_andb_true;assumption
 300                 ]
 301               |rewrite > lt_to_leb_false
 302                 [reflexivity
 303                 |apply le_S_S.
 304                  apply leb_true_to_le.
 305                  assumption
 306                 ]
 307               ]
 308             |rewrite > true_to_pi_p_Sn
 309               [rewrite > false_to_pi_p_Sn
 310                 [rewrite > assoc_times.
 311                  apply eq_f.
 312                  assumption
 313                 |rewrite > H2.reflexivity
 314                 ]
 315               |rewrite > H1.
 316                rewrite > le_to_leb_true
 317                 [reflexivity
 318                 |apply not_le_to_lt.
 319                  apply leb_false_to_not_le.
 320                  assumption
 321                 ]
 322               ]
 323             ]
 324           |assumption
 325           ]
 326         |rewrite > false_to_pi_p_Sn
 327           [rewrite > false_to_pi_p_Sn
 328             [rewrite > false_to_pi_p_Sn
 329               [assumption
 330               |rewrite > H1.
 331                rewrite > andb_sym.
 332                reflexivity
 333               ]
 334             |rewrite > H1.
 335              rewrite > andb_sym.
 336              reflexivity
 337             ]
 338           |assumption
 339           ]
 340         ]
 341       ]
 342     |apply le_S_S.apply le_S_S.
 343      apply le_times_n.
 344      apply le_n_Sn
 345     |intros.
 346      rewrite > lt_to_leb_false
 347       [reflexivity
 348       |assumption
 349       ]
 350     ]
 351   |intros.
 352    rewrite > le_to_leb_true
 353     [reflexivity
 354     |apply le_S_S_to_le.
 355      assumption
 356     ]
 357   |intros.reflexivity
 358   ]
 359 qed.
 360
 361 theorem div_teta_teta: \forall m.
 362 teta (S(2*m))/teta (S m) = pi_p (S(S(2*m))) (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p).
 363 intros.apply (div_mod_spec_to_eq ? ? ? ? ? O (div_mod_spec_div_mod ? ? ? ))
 364   [apply lt_O_teta
 365   |apply div_mod_spec_intro
 366     [apply lt_O_teta
 367     |rewrite < plus_n_O.
 368      apply teta_pi_p_teta
 369     ]
 370   ]
 371 qed.
 372
 373 theorem le_teta_M_teta: \forall m.
 374 teta (S(2*m)) \le (M m)*teta (S m).
 375 intro.
 376 rewrite > teta_pi_p_teta.
 377 apply le_times_l.
 378 apply divides_to_le
 379   [unfold M.apply lt_O_bc.apply lt_to_le.
 380    apply le_S_S.apply le_times_n.
 381    apply le_n_Sn
 382   |apply divides_pi_p_M
 383   ]
 384 qed.
 385
 386 theorem lt_O_to_le_teta_exp_teta: \forall m. O < m\to
 387 teta (S(2*m)) < exp 2 (2*m)*teta (S m).
 388 intros.
 389 apply (le_to_lt_to_lt ? (M m*teta (S m)))
 390   [apply le_teta_M_teta
 391   |apply lt_times_l1
 392     [apply lt_O_teta
 393     |apply lt_M.
 394      assumption
 395     ]
 396   ]
 397 qed.
 398
 399 theorem teta_pred: \forall n. S O < n \to teta (2*n) = teta (pred (2*n)).
 400 intros.unfold teta.
 401 rewrite > false_to_pi_p_Sn
 402   [rewrite < S_pred
 403     [reflexivity
 404     |rewrite > (times_n_O 2) in ⊢ (? % ?).
 405      apply lt_times_r.
 406      apply lt_to_le.assumption
 407     ]
 408   |apply not_prime_to_primeb_false.
 409    intro.
 410    elim H1.
 411    apply (lt_to_not_eq ? ? H).
 412    apply (injective_times_r 1).
 413    rewrite < times_n_SO.
 414    apply H3
 415     [apply (witness ? ? n).reflexivity
 416     |apply le_n
 417     ]
 418   ]
 419 qed.
 420
 421 theorem le_teta: \forall m.teta m \le exp 2 (2*m).
 422 intro.apply (nat_elim1 m).intros.
 423 elim (or_eq_eq_S m1).
 424 elim H1
 425   [rewrite > H2.
 426    generalize in match H2.
 427    cases a
 428     [intro.apply le_n
 429     |cases n;intros
 430       [apply leb_true_to_le.reflexivity
 431       |rewrite > teta_pred
 432         [rewrite > times_SSO.
 433          change in ⊢ (? (? %) ?) with (S (2*S n1)).
 434          apply (trans_le ? (exp 2 (2*(S n1))*teta (S (S n1))))
 435           [apply lt_to_le.
 436            apply lt_O_to_le_teta_exp_teta.
 437            apply lt_O_S
 438           |rewrite < times_SSO.
 439            change in ⊢ (? ? (? ? %)) with ((2*S (S n1))+((2*S (S n1)) + O)).
 440            rewrite < plus_n_O.
 441            rewrite > exp_plus_times.
 442            apply le_times
 443             [apply le_exp
 444               [apply lt_O_S
 445               |apply le_times_r.
 446                apply le_n_Sn
 447               ]
 448             |apply H.
 449              rewrite > H3.
 450              apply lt_m_nm
 451               [apply lt_O_S
 452               |apply le_n
 453               ]
 454             ]
 455           ]
 456         |apply le_S_S.apply lt_O_S
 457         ]
 458       ]
 459     ]
 460   |rewrite > H2.
 461    generalize in match H2.
 462    cases a;intro
 463     [apply leb_true_to_le.reflexivity
 464     |apply (trans_le ? (exp 2 (2*(S n))*teta (S (S n))))
 465       [apply lt_to_le.
 466        apply lt_O_to_le_teta_exp_teta.
 467        apply lt_O_S
 468       |change in ⊢ (? ? (? ? %)) with (S (2*S n) + (S (2*S n) +O)).
 469        rewrite < plus_n_O.
 470        rewrite < plus_n_Sm.
 471        rewrite < sym_plus.
 472        rewrite > plus_n_Sm.
 473        rewrite > exp_plus_times.
 474        apply le_times_r.
 475        rewrite < times_SSO.
 476        apply H.
 477        rewrite > H3.
 478        apply le_S_S.
 479        apply lt_m_nm
 480         [apply lt_O_S
 481         |apply le_n
 482         ]
 483       ]
 484     ]
 485   ]
 486 qed.
 487
 488 (*
 489 alias id "sqrt" = "cic:/matita/nat/sqrt/sqrt.con".
 490 alias id "not" = "cic:/matita/logic/connectives/Not.con".
 491 theorem absurd_bound: \forall n. exp 2 7 \le n \to
 492 (\forall p. n < p \to p < 2*n \to not (prime p)) \to
 493 bc (2*n) n < exp (2*n) (div (sqrt (2*n)) 2 - 1)*exp 4 (div (2*n) 3).
 494 intros.
 495 cut (O < n)
 496   [cut (sqrt (2*n) < div (2*n) 3)
 497     [
 498   |
 499 *)
 500