helm/software/matita/library/nat/bertrand.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/sqrt.ma".
  16 include "nat/chebyshev_teta.ma".
  17 include "nat/chebyshev.ma".
  18
  19 definition not_bertrand \def \lambda n.
  20 \forall p.n < p \to p \le 2*n \to \not (prime p).
  21
  22 (* not used
  23 theorem divides_pi_p_to_divides: \forall p,n,b,g.prime p \to
  24 divides p (pi_p n b g) \to \exists i. (i < n \and (b i = true \and
  25 divides p (g i))).
  26 intros 2.elim n
  27   [simplify in H1.
  28    apply False_ind.
  29    apply (le_to_not_lt p 1)
  30     [apply divides_to_le
  31       [apply le_n
  32       |assumption
  33       ]
  34     |elim H.assumption
  35     ]
  36   |apply (bool_elim ? (b n1));intro
  37     [rewrite > (true_to_pi_p_Sn ? ? ? H3) in H2.
  38      elim (divides_times_to_divides ? ? ? H1 H2)
  39       [apply (ex_intro ? ? n1).
  40        split
  41         [apply le_n
  42         |split;assumption
  43         ]
  44       |elim (H ? ? H1 H4).
  45        elim H5.
  46        apply (ex_intro ? ? a).
  47        split
  48         [apply lt_to_le.apply le_S_S.assumption
  49         |assumption
  50         ]
  51       ]
  52     |rewrite > (false_to_pi_p_Sn ? ? ? H3) in H2.
  53      elim (H ? ? H1 H2).
  54      elim H4.
  55      apply (ex_intro ? ? a).
  56      split
  57       [apply lt_to_le.apply le_S_S.assumption
  58       |assumption
  59       ]
  60     ]
  61   ]
  62 qed.
  63
  64 theorem divides_B: \forall n,p.prime p \to p \divides (B n) \to
  65 p \le n \land \exists i.mod (n /(exp p (S i))) 2 \neq O.
  66 intros.
  67 unfold B in H1.
  68 elim (divides_pi_p_to_divides ? ? ? ? H H1).
  69 elim H2.clear H2.
  70 elim H4.clear H4.
  71 elim (divides_pi_p_to_divides ? ? ? ? H H5).clear H5.
  72 elim H4.clear H4.
  73 elim H6.clear H6.
  74 cut (p = a)
  75   [split
  76     [rewrite > Hcut.apply le_S_S_to_le.assumption
  77     |apply (ex_intro ? ? a1).
  78      rewrite > Hcut.
  79      intro.
  80      change in H7:(? ? %) with (exp a ((n/(exp a (S a1))) \mod 2)).
  81      rewrite > H6 in H7.
  82      simplify in H7.
  83      absurd (p \le 1)
  84       [apply divides_to_le[apply lt_O_S|assumption]
  85       |apply lt_to_not_le.elim H.assumption
  86       ]
  87     ]
  88   |apply (divides_exp_to_eq ? ? ? H ? H7).
  89    apply primeb_true_to_prime.
  90    assumption
  91   ]
  92 qed.
  93 *)
  94
  95 definition k \def \lambda n,p.
  96 sigma_p (log p n) (λi:nat.true) (λi:nat.((n/(exp p (S i))\mod 2))).
  97
  98 theorem le_k: \forall n,p. k n p \le log p n.
  99 intros.unfold k.elim (log p n)
 100   [apply le_n
 101   |rewrite > true_to_sigma_p_Sn
 102     [rewrite > plus_n_SO.
 103      rewrite > sym_plus in ⊢ (? ? %).
 104      apply le_plus
 105       [apply le_S_S_to_le.
 106        apply lt_mod_m_m.
 107        apply lt_O_S
 108       |assumption
 109       ]
 110     |reflexivity
 111     ]
 112   ]
 113 qed.
 114
 115 definition B1 \def
 116 \lambda n. pi_p (S n) primeb (\lambda p.(exp p (k n p))).
 117
 118 theorem eq_B_B1: \forall n. B n = B1 n.
 119 intros.unfold B.unfold B1.
 120 apply eq_pi_p
 121   [intros.reflexivity
 122   |intros.unfold k.
 123    apply exp_sigma_p1
 124   ]
 125 qed.
 126
 127 definition B_split1 \def \lambda n.
 128 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb (k n p) 1)* (k n p)))).
 129
 130 definition B_split2 \def \lambda n.
 131 pi_p (S n) primeb (\lambda p.(exp p (bool_to_nat (leb 2 (k n p))* (k n p)))).
 132
 133 theorem eq_B1_times_B_split1_B_split2: \forall n.
 134 B1 n = B_split1 n * B_split2 n.
 135 intro.unfold B1.unfold B_split1.unfold B_split2.
 136 rewrite < times_pi_p.
 137 apply eq_pi_p
 138   [intros.reflexivity
 139   |intros.apply (bool_elim ? (leb (k n x) 1));intro
 140     [rewrite > (lt_to_leb_false 2 (k n x))
 141       [simplify.rewrite < plus_n_O.
 142        rewrite < times_n_SO.reflexivity
 143       |apply le_S_S.apply leb_true_to_le.assumption
 144       ]
 145     |rewrite > (le_to_leb_true 2 (k n x))
 146       [simplify.rewrite < plus_n_O.
 147        rewrite < plus_n_O.reflexivity
 148       |apply not_le_to_lt.apply leb_false_to_not_le.assumption
 149       ]
 150     ]
 151   ]
 152 qed.
 153
 154 lemma lt_div_to_times: \forall n,m,q. O < q \to n/q < m \to n < q*m.
 155 intros.
 156 cut (O < m) as H2
 157   [apply not_le_to_lt.
 158    intro.apply (lt_to_not_le ? ? H1).
 159    apply le_times_to_le_div;assumption
 160   |apply (ltn_to_ltO ? ? H1)
 161   ]
 162 qed.
 163
 164 lemma lt_to_div_O:\forall n,m. n < m \to n / m = O.
 165 intros.
 166 apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n)
 167   [apply div_mod_spec_div_mod.
 168    apply (ltn_to_ltO ? ? H)
 169   |apply div_mod_spec_intro
 170     [assumption
 171     |reflexivity
 172     ]
 173   ]
 174 qed.
 175
 176 (* the value of n could be smaller *)
 177 lemma k1: \forall n,p. 18 \le n \to p \le n \to 2*n/ 3 < p\to k (2*n) p = O.
 178 intros.unfold k.
 179 elim (log p (2*n))
 180   [reflexivity
 181   |rewrite > true_to_sigma_p_Sn
 182     [rewrite > H3.
 183      rewrite < plus_n_O.
 184      cases n1
 185       [rewrite < exp_n_SO.
 186        cut (2*n/p = 2) as H4
 187         [rewrite > H4.reflexivity
 188         |apply lt_to_le_times_to_lt_S_to_div
 189           [apply (ltn_to_ltO ? ? H2)
 190           |rewrite < sym_times.
 191            apply le_times_r.
 192            assumption
 193           |rewrite > sym_times in ⊢ (? ? %).
 194            apply lt_div_to_times
 195             [apply lt_O_S
 196             |assumption
 197             ]
 198           ]
 199         ]
 200       |cut (2*n/(p)\sup(S (S n2)) = O) as H4
 201         [rewrite > H4.reflexivity
 202         |apply lt_to_div_O.
 203          apply (le_to_lt_to_lt ? (exp ((2*n)/3) 2))
 204           [apply (le_times_to_le (exp 3 2))
 205             [apply leb_true_to_le.reflexivity
 206             |rewrite > sym_times in ⊢ (? ? %).
 207              rewrite > times_exp.
 208              apply (trans_le ? (exp n 2))
 209               [rewrite < assoc_times.
 210                rewrite > exp_SSO in ⊢ (? ? %).
 211                apply le_times_l.
 212                assumption
 213               |apply monotonic_exp1.
 214                apply (le_plus_to_le 3).
 215                change in ⊢ (? ? %) with ((S(2*n/3))*3).
 216                apply (trans_le ? (2*n))
 217                 [simplify in ⊢ (? ? %).
 218                  rewrite < plus_n_O.
 219                  apply le_plus_l.
 220                  apply (trans_le ? 18 ? ? H).
 221                  apply leb_true_to_le.reflexivity
 222                 |apply lt_to_le.
 223                  apply lt_div_S.
 224                  apply lt_O_S
 225                 ]
 226               ]
 227             ]
 228           |apply (lt_to_le_to_lt ? (exp p 2))
 229             [apply lt_exp1
 230               [apply lt_O_S
 231               |assumption
 232               ]
 233             |apply le_exp
 234               [apply (ltn_to_ltO ? ? H2)
 235               |apply le_S_S.apply le_S_S.apply le_O_n
 236               ]
 237             ]
 238           ]
 239         ]
 240       ]
 241     |reflexivity
 242     ]
 243   ]
 244 qed.
 245
 246 theorem le_B_split1_teta:\forall n.18 \le n \to not_bertrand n \to
 247 B_split1 (2*n) \le teta (2 * n / 3).
 248 intros.unfold B_split1.unfold teta.
 249 apply (trans_le ? (pi_p (S (2*n)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
 250   [apply le_pi_p.intros.
 251    apply le_exp
 252     [apply prime_to_lt_O.apply primeb_true_to_prime.assumption
 253     |apply (bool_elim ? (leb (k (2*n) i) 1));intro
 254       [elim (le_to_or_lt_eq ? ? (leb_true_to_le ? ? H4))
 255         [lapply (le_S_S_to_le ? ? H5) as H6.
 256          apply (le_n_O_elim ? H6).
 257          rewrite < times_n_O.
 258          apply le_n
 259         |rewrite > (eq_to_eqb_true ? ? H5).
 260          rewrite > H5.apply le_n
 261         ]
 262       |apply le_O_n
 263       ]
 264     ]
 265   |apply (trans_le ? (pi_p (S (2*n/3)) primeb (λp:nat.(p)\sup(bool_to_nat (eqb (k (2*n) p) 1)))))
 266     [apply (eq_ind ? ? ? (le_n ?)).
 267      apply or_false_eq_SO_to_eq_pi_p
 268       [apply le_S_S.
 269        apply le_times_to_le_div2
 270         [apply lt_O_S
 271         |rewrite > sym_times in ⊢ (? ? %).
 272          apply le_times_n.
 273          apply leb_true_to_le.reflexivity
 274         ]
 275       |intros.
 276        unfold not_bertrand in H1.
 277        elim (decidable_le (S n) i)
 278         [left.
 279          apply not_prime_to_primeb_false.
 280          apply H1
 281           [assumption
 282           |apply le_S_S_to_le.assumption
 283           ]
 284         |right.
 285          rewrite > k1
 286           [reflexivity
 287           |assumption
 288           |apply le_S_S_to_le.
 289            apply not_le_to_lt.assumption
 290           |assumption
 291           ]
 292         ]
 293       ]
 294     |apply le_pi_p.intros.
 295      elim (eqb (k (2*n) i) 1)
 296       [rewrite < exp_n_SO.apply le_n
 297       |simplify.apply prime_to_lt_O.
 298        apply primeb_true_to_prime.
 299        assumption
 300       ]
 301     ]
 302   ]
 303 qed.
 304
 305 theorem le_B_split2_exp: \forall n. exp 2 7 \le n \to
 306 B_split2 (2*n) \le exp (2*n) (pred(sqrt(2*n)/2)).
 307 intros.unfold B_split2.
 308 cut (O < n)
 309   [apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb
 310         (λp:nat.(p)\sup(bool_to_nat (leb 2 (k (2*n) p))*k (2*n) p))))
 311     [apply (eq_ind ? ? ? (le_n ?)).
 312      apply or_false_eq_SO_to_eq_pi_p
 313       [apply le_S_S.
 314        apply le_sqrt_n_n
 315       |intros.
 316        apply (bool_elim ? (leb 2 (k (2*n) i)));intro
 317         [apply False_ind.
 318          apply (lt_to_not_le ? ? H1).unfold sqrt.
 319          apply f_m_to_le_max
 320           [apply le_S_S_to_le.assumption
 321           |apply le_to_leb_true.
 322            rewrite < exp_SSO.
 323            apply not_lt_to_le.intro.
 324            apply (le_to_not_lt 2 (log i (2*n)))
 325             [apply (trans_le ? (k (2*n) i))
 326               [apply leb_true_to_le.assumption
 327               |apply le_k
 328               ]
 329             |apply le_S_S.unfold log.apply f_false_to_le_max
 330               [apply (ex_intro ? ? O).split
 331                 [apply le_O_n
 332                 |apply le_to_leb_true.simplify.
 333                  apply (trans_le ? n)
 334                   [assumption.
 335                   |apply le_plus_n_r
 336                   ]
 337                 ]
 338               |intros.apply lt_to_leb_false.
 339                apply (lt_to_le_to_lt ? (exp i 2))
 340                 [assumption
 341                 |apply le_exp
 342                   [apply (ltn_to_ltO ? ? H1)
 343                   |assumption
 344                   ]
 345                 ]
 346               ]
 347             ]
 348           ]
 349         |right.reflexivity
 350         ]
 351       ]
 352     |apply (trans_le ? (pi_p (S (sqrt (2*n))) primeb (λp:nat.2*n)))
 353       [apply le_pi_p.intros.
 354        apply (trans_le ? (exp i (log i (2*n))))
 355         [apply le_exp
 356           [apply prime_to_lt_O.
 357            apply primeb_true_to_prime.
 358            assumption
 359           |apply (bool_elim ? (leb 2 (k (2*n) i)));intro
 360             [simplify in ⊢ (? (? % ?) ?).
 361              rewrite > sym_times.
 362              rewrite < times_n_SO.
 363              apply le_k
 364             |apply le_O_n
 365             ]
 366           ]
 367         |apply le_exp_log.
 368          rewrite > (times_n_O O) in ⊢ (? % ?).
 369          apply lt_times
 370           [apply lt_O_S
 371           |assumption
 372           ]
 373         ]
 374       |apply (trans_le ? (exp (2*n) (prim(sqrt (2*n)))))
 375         [unfold prim.
 376          apply (eq_ind ? ? ? (le_n ?)).
 377          apply exp_sigma_p
 378         |apply le_exp
 379           [rewrite > (times_n_O O) in ⊢ (? % ?).
 380            apply lt_times
 381             [apply lt_O_S
 382             |assumption
 383             ]
 384           |apply le_prim_n3.
 385            unfold sqrt.
 386            apply f_m_to_le_max
 387             [apply (trans_le ? (2*(exp 2 7)))
 388               [apply leb_true_to_le.reflexivity
 389               |apply le_times_r.assumption
 390               ]
 391             |apply le_to_leb_true.
 392              apply (trans_le ? (2*(exp 2 7)))
 393               [apply leb_true_to_le.reflexivity
 394               |apply le_times_r.assumption
 395               ]
 396             ]
 397           ]
 398         ]
 399       ]
 400     ]
 401   |apply (lt_to_le_to_lt ? ? ? ? H).
 402    apply leb_true_to_le.reflexivity
 403   ]
 404 qed.
 405
 406 theorem not_bertrand_to_le_B:
 407 \forall n.exp 2 7 \le n \to not_bertrand n \to
 408 B (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (pred(sqrt(2*n)/2))).
 409 intros.
 410 rewrite > eq_B_B1.
 411 rewrite > eq_B1_times_B_split1_B_split2.
 412 apply le_times
 413   [apply (trans_le ? (teta ((2*n)/3)))
 414     [apply le_B_split1_teta
 415       [apply (trans_le ? ? ? ? H).
 416        apply leb_true_to_le.reflexivity
 417       |assumption
 418       ]
 419     |apply le_teta
 420     ]
 421   |apply le_B_split2_exp.
 422    assumption
 423   ]
 424 qed.
 425
 426 (*
 427 theorem not_bertrand_to_le1:
 428 \forall n.18 \le n \to not_bertrand n \to
 429 exp 2 (2*n) \le (exp 2 (2*(2 * n / 3)))*(exp (2*n) (S(sqrt(2*n)))).
 430 *)
 431
 432 theorem le_times_div_m_m: \forall n,m. O < m \to n/m*m \le n.
 433 intros.
 434 rewrite > (div_mod n m) in ⊢ (? ? %)
 435   [apply le_plus_n_r
 436   |assumption
 437   ]
 438 qed.
 439
 440 theorem not_bertrand_to_le1:
 441 \forall n.exp 2 7 \le n \to not_bertrand n \to
 442 (exp 2 (2*n / 3)) \le (exp (2*n) (sqrt(2*n)/2)).
 443 intros.
 444 apply (le_times_to_le (exp 2 (2*(2 * n / 3))))
 445   [apply lt_O_exp.apply lt_O_S
 446   |rewrite < exp_plus_times.
 447    apply (trans_le ? (exp 2 (2*n)))
 448     [apply le_exp
 449       [apply lt_O_S
 450       |rewrite < sym_plus.
 451        change in ⊢ (? % ?) with (3*(2*n/3)).
 452        rewrite > sym_times.
 453        apply le_times_div_m_m.
 454        apply lt_O_S
 455       ]
 456 (* weaker form
 457        rewrite < distr_times_plus.
 458        apply le_times_r.
 459        apply (trans_le ? ((2*n + n)/3))
 460         [apply le_plus_div.apply lt_O_S
 461         |rewrite < sym_plus.
 462          change in ⊢ (? (? % ?) ?) with (3*n).
 463          rewrite < sym_times.
 464          rewrite > lt_O_to_div_times
 465           [apply le_n
 466           |apply lt_O_S
 467           ]
 468         ]
 469       ] *)
 470     |apply (trans_le ? (2*n*B(2*n)))
 471       [apply le_exp_B.
 472        apply (trans_le ? ? ? ? H).
 473        apply leb_true_to_le.reflexivity
 474       |rewrite > S_pred in ⊢ (? ? (? ? (? ? %)))
 475         [rewrite > exp_S.
 476          rewrite < assoc_times.
 477          rewrite < sym_times in ⊢ (? ? (? % ?)).
 478          rewrite > assoc_times in ⊢ (? ? %).
 479          apply le_times_r.
 480          apply not_bertrand_to_le_B;assumption
 481         |apply le_times_to_le_div
 482           [apply lt_O_S
 483           |apply (trans_le ? (sqrt (exp 2 8)))
 484             [apply leb_true_to_le.reflexivity
 485             |apply monotonic_sqrt.
 486              change in ⊢ (? % ?) with (2*(exp 2 7)).
 487              apply le_times_r.
 488              assumption
 489             ]
 490           ]
 491         ]
 492       ]
 493     ]
 494   ]
 495 qed.
 496
 497 theorem not_bertrand_to_le2:
 498 \forall n.exp 2 7 \le n \to not_bertrand n \to
 499 2*n / 3 \le (sqrt(2*n)/2)*S(log 2 (2*n)).
 500 intros.
 501 rewrite < (eq_log_exp 2)
 502   [apply (trans_le ? (log 2 ((exp (2*n) (sqrt(2*n)/2)))))
 503     [apply le_log
 504       [apply le_n
 505       |apply not_bertrand_to_le1;assumption
 506       ]
 507     |apply log_exp1.
 508      apply le_n
 509     ]
 510   |apply le_n
 511   ]
 512 qed.
 513
 514 (*
 515 theorem tech: \forall n. 2*(3*(S(log 2 (2*n)))/4) < sqrt (2*n) \to
 516 (sqrt(2*n)/2)*S(log 2 (2*n)) < 2*n / 3.
 517 intros.
 518  *)