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