matita/library/nat/neper.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 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "nat/iteration2.ma".
  18 include "nat/div_and_mod_diseq.ma".
  19 include "nat/binomial.ma".
  20 include "nat/log.ma".
  21 include "nat/chebyshev.ma".
  22
  23 theorem sigma_p_div_exp: \forall n,m.
  24 sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le
  25 ((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
  26 intros.
  27 elim n
  28   [apply le_O_n.
  29   |rewrite > true_to_sigma_p_Sn
  30     [apply (trans_le ? (m/(S(S O))\sup(n1)+((S(S O))*m*(S(S O))\sup(n1)-(S(S O))*m)/(S(S O))\sup(n1)))
  31       [apply le_plus_r.assumption
  32       |rewrite > assoc_times in ⊢ (? ? (? (? % ?) ?)).
  33        rewrite < distr_times_minus.
  34        change in ⊢ (? ? (? ? %)) with ((S(S O))*(exp (S(S O)) n1)).
  35        rewrite > sym_times in ⊢ (? ? (? % ?)).
  36        rewrite > sym_times in ⊢ (? ? (? ? %)).
  37        rewrite < lt_to_lt_to_eq_div_div_times_times
  38         [apply (trans_le ? ((m+((S(S O))*m*((S(S O)))\sup(n1)-(S(S O))*m))/((S(S O)))\sup(n1)))
  39           [apply le_plus_div.
  40            apply lt_O_exp.
  41            apply lt_O_S
  42           |change in ⊢ (? (? (? ? (? ? %)) ?) ?) with (m + (m +O)).
  43            rewrite < plus_n_O.
  44            rewrite < eq_minus_minus_minus_plus.
  45            rewrite > sym_plus.
  46            rewrite > sym_times in ⊢ (? (? (? (? (? (? % ?) ?) ?) ?) ?) ?).
  47            rewrite > assoc_times.
  48            rewrite < plus_minus_m_m
  49             [apply le_n
  50             |apply le_plus_to_minus_r.
  51              rewrite > plus_n_O in ⊢ (? (? ? %) ?).
  52              change in ⊢ (? % ?) with ((S(S O))*m).
  53              rewrite > sym_times.
  54              apply le_times_r.
  55              rewrite > times_n_SO in ⊢ (? % ?).
  56              apply le_times_r.
  57              apply lt_O_exp.
  58              apply lt_O_S
  59             ]
  60           ]
  61         |apply lt_O_S
  62         |apply lt_O_exp.
  63          apply lt_O_S
  64         ]
  65       ]
  66     |reflexivity
  67     ]
  68   ]
  69 qed.
  70
  71 theorem le_fact_exp: \forall i,m. i \le m \to m!≤ m \sup i*(m-i)!.
  72 intro.elim i
  73   [rewrite < minus_n_O.
  74    simplify.rewrite < plus_n_O.
  75    apply le_n
  76   |simplify.
  77    apply (trans_le ? ((m)\sup(n)*(m-n)!))
  78     [apply H.
  79      apply lt_to_le.assumption
  80     |rewrite > sym_times in ⊢ (? ? (? % ?)).
  81      rewrite > assoc_times.
  82      apply le_times_r.
  83      generalize in match H1.
  84      cases m;intro
  85       [apply False_ind.
  86        apply (lt_to_not_le ? ? H2).
  87        apply le_O_n
  88       |rewrite > minus_Sn_m.
  89        simplify.
  90        apply le_plus_r.
  91        apply le_times_l.
  92        apply le_minus_m.
  93        apply le_S_S_to_le.
  94        assumption
  95       ]
  96     ]
  97   ]
  98 qed.
  99
 100 theorem le_fact_exp1: \forall n. S O < n \to (S(S O))*n!≤ n \sup n.
 101 intros.elim H
 102   [apply le_n
 103   |change with ((S(S O))*((S n1)*(fact n1)) \le (S n1)*(exp (S n1) n1)).
 104    rewrite < assoc_times.
 105    rewrite < sym_times in ⊢ (? (? % ?) ?).
 106    rewrite > assoc_times.
 107    apply le_times_r.
 108    apply (trans_le ? (exp n1 n1))
 109     [assumption
 110     |apply monotonic_exp1.
 111      apply le_n_Sn
 112     ]
 113   ]
 114 qed.
 115
 116 theorem le_exp_sigma_p_exp: \forall n. (exp (S n) n) \le
 117 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
 118 intro.
 119 rewrite > exp_S_sigma_p.
 120 apply le_sigma_p.
 121 intros.unfold bc.
 122 apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
 123   [rewrite > sym_times.
 124    apply le_times_r.
 125    rewrite > sym_times.
 126    rewrite < eq_div_div_div_times
 127     [apply monotonic_div
 128       [apply lt_O_fact
 129       |apply le_times_to_le_div2
 130         [apply lt_O_fact
 131         |apply le_fact_exp.
 132          apply le_S_S_to_le.
 133          assumption
 134         ]
 135       ]
 136     |apply lt_O_fact
 137     |apply lt_O_fact
 138     ]
 139   |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
 140     [rewrite > exp_plus_times.
 141      apply le_times_div_div_times.
 142      apply lt_O_fact
 143     |apply le_S_S_to_le.
 144      assumption
 145     ]
 146   ]
 147 qed.
 148
 149 theorem lt_exp_sigma_p_exp: \forall n. S O < n \to
 150 (exp (S n) n) <
 151 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
 152 intros.
 153 rewrite > exp_S_sigma_p.
 154 apply lt_sigma_p
 155   [intros.unfold bc.
 156    apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
 157     [rewrite > sym_times.
 158      apply le_times_r.
 159      rewrite > sym_times.
 160      rewrite < eq_div_div_div_times
 161       [apply monotonic_div
 162         [apply lt_O_fact
 163         |apply le_times_to_le_div2
 164           [apply lt_O_fact
 165           |apply le_fact_exp.
 166            apply le_S_S_to_le.
 167            assumption
 168           ]
 169         ]
 170       |apply lt_O_fact
 171       |apply lt_O_fact
 172       ]
 173     |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
 174       [rewrite > exp_plus_times.
 175        apply le_times_div_div_times.
 176        apply lt_O_fact
 177       |apply le_S_S_to_le.
 178        assumption
 179       ]
 180     ]
 181   |apply (ex_intro ? ? n).
 182    split
 183     [split
 184       [apply le_n
 185       |reflexivity
 186       ]
 187     |rewrite < minus_n_n.
 188      rewrite > bc_n_n.
 189      simplify.unfold lt.
 190      apply le_times_to_le_div
 191       [apply lt_O_fact
 192       |rewrite > sym_times.
 193        apply le_fact_exp1.
 194        assumption
 195       ]
 196     ]
 197   ]
 198 qed.
 199
 200 theorem le_exp_SSO_fact:\forall n.
 201 exp (S(S O)) (pred n) \le n!.
 202 intro.elim n
 203   [apply le_n
 204   |change with ((S(S O))\sup n1 ≤(S n1)*n1!).
 205    apply (nat_case1 n1);intros
 206     [apply le_n
 207     |change in ⊢ (? % ?) with ((S(S O))*exp (S(S O)) (pred (S m))).
 208      apply le_times
 209       [apply le_S_S.apply le_S_S.apply le_O_n
 210       |rewrite < H1.assumption
 211       ]
 212     ]
 213   ]
 214 qed.
 215
 216 theorem lt_SO_to_lt_exp_Sn_n_SSSO: \forall n. S O < n \to
 217 (exp (S n) n) < (S(S(S O)))*(exp n n).
 218 intros.
 219 apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
 220   [apply lt_exp_sigma_p_exp.assumption
 221   |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
 222     [apply le_sigma_p.intros.
 223      apply le_times_to_le_div
 224       [apply lt_O_exp.
 225        apply lt_O_S
 226       |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
 227         [apply le_times_div_div_times.
 228          apply lt_O_fact
 229         |apply le_times_to_le_div2
 230           [apply lt_O_fact
 231           |rewrite < sym_times.
 232            apply le_times_r.
 233            apply le_exp_SSO_fact
 234           ]
 235         ]
 236       ]
 237     |rewrite > eq_sigma_p_pred
 238       [rewrite > div_SO.
 239        rewrite > sym_plus.
 240        change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
 241        apply le_plus_r.
 242        apply (trans_le ? (((S(S O))*(exp n n)*(exp (S(S O)) n) - (S(S O))*(exp n n))/(exp (S(S O)) n)))
 243         [apply sigma_p_div_exp
 244         |apply le_times_to_le_div2
 245           [apply lt_O_exp.
 246            apply lt_O_S.
 247           |apply le_minus_m
 248           ]
 249         ]
 250       |reflexivity
 251       ]
 252     ]
 253   ]
 254 qed.
 255
 256 theorem lt_exp_Sn_n_SSSO: \forall n.
 257 (exp (S n) n) < (S(S(S O)))*(exp n n).
 258 intro.cases n;intros
 259   [simplify.apply le_S.apply le_n
 260   |cases n1;intros
 261     [simplify.apply le_n
 262     |apply lt_SO_to_lt_exp_Sn_n_SSSO.
 263      apply le_S_S.apply le_S_S.apply le_O_n
 264     ]
 265   ]
 266 qed.
 267
 268 theorem lt_exp_Sn_m_SSSO: \forall n,m. O < m \to
 269 divides n m \to
 270 (exp (S n) m) < (exp (S(S(S O))) (m/n)) *(exp n m).
 271 intros.
 272 elim H1.rewrite > H2.
 273 rewrite < exp_exp_times.
 274 rewrite < exp_exp_times.
 275 rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?)).
 276 rewrite > lt_O_to_div_times
 277   [rewrite > times_exp.
 278    apply lt_exp1
 279     [apply (O_lt_times_to_O_lt ? n).
 280      rewrite > sym_times.
 281      rewrite < H2.
 282      assumption
 283     |apply lt_exp_Sn_n_SSSO
 284     ]
 285   |apply (O_lt_times_to_O_lt ? n2).
 286    rewrite < H2.
 287    assumption
 288   ]
 289 qed.
 290
 291 theorem le_log_exp_Sn_log_exp_n: \forall n,m,p. O < m \to S O < p \to
 292 divides n m \to
 293 log p (exp (S n) m) \le S((m/n)*S(log p (S(S(S O))))) + log p (exp n m).
 294 intros.
 295 apply (trans_le ? (log p (((S(S(S O))))\sup(m/n)*((n)\sup(m)))))
 296   [apply le_log
 297     [assumption
 298     |apply lt_to_le.
 299      apply lt_exp_Sn_m_SSSO;assumption
 300     ]
 301   |apply (trans_le ? (S(log p (exp (S(S(S O))) (m/n)) + log p (exp n m))))
 302     [apply log_times.
 303      assumption
 304     |change in ⊢ (? ? %) with (S (m/n*S (log p (S(S(S O))))+log p ((n)\sup(m)))).
 305      apply le_S_S.
 306      apply le_plus_l.
 307      apply log_exp1.
 308      assumption
 309     ]
 310   ]
 311 qed.
 312
 313 theorem le_log_exp_fact_sigma_p: \forall a,b,n,p. S O < p \to
 314 O < a \to a \le b \to b \le n \to
 315 log p (exp b n!) - log p (exp a n!) \le
 316 sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))).
 317 intros 7.
 318 elim b
 319   [simplify.
 320    apply (lt_O_n_elim ? (lt_O_fact n)).intro.
 321    apply le_n.
 322   |apply (bool_elim ? (leb a n1));intro
 323     [rewrite > true_to_sigma_p_Sn
 324       [apply (trans_le ? (S (n!/n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(n!))-log p ((a)\sup(n!)))))
 325         [rewrite > sym_plus.
 326          rewrite > plus_minus
 327           [apply le_plus_to_minus_r.
 328            rewrite < plus_minus_m_m
 329             [rewrite > sym_plus.
 330              apply le_log_exp_Sn_log_exp_n
 331               [apply lt_O_fact
 332               |assumption
 333               |apply divides_fact;
 334                  [apply (trans_le ? ? ? H1);apply leb_true_to_le;assumption
 335                  |apply lt_to_le;assumption]]
 336             |apply le_log
 337               [assumption
 338               |cut (O = exp O n!)
 339                  [rewrite > Hcut;apply monotonic_exp1;constructor 2;
 340                   apply leb_true_to_le;assumption
 341                  |elim n
 342                     [reflexivity
 343                     |simplify;rewrite > exp_plus_times;rewrite < H6;
 344                      rewrite > sym_times;rewrite < times_n_O;reflexivity]]]]
 345         |apply le_log
 346           [assumption
 347           |apply monotonic_exp1;apply leb_true_to_le;assumption]]
 348       |rewrite > sym_plus;rewrite > sym_plus in \vdash (? ? %);apply le_minus_to_plus;
 349        rewrite < minus_plus_m_m;apply H3;apply lt_to_le;assumption]
 350     |assumption]
 351   |lapply (not_le_to_lt ? ? (leb_false_to_not_le ? ? H5));
 352    rewrite > eq_minus_n_m_O
 353     [apply le_O_n
 354     |apply le_log
 355        [assumption
 356        |apply monotonic_exp1;assumption]]]]
 357 qed.
 358
 359 theorem le_exp_div:\forall n,m,q. O < m \to
 360 exp (n/m) q \le (exp n q)/(exp m q).
 361 intros.
 362 apply le_times_to_le_div
 363   [apply lt_O_exp.
 364    assumption
 365   |rewrite > times_exp.
 366    rewrite < sym_times.
 367    apply monotonic_exp1.
 368    rewrite > (div_mod n m) in ⊢ (? ? %)
 369     [apply le_plus_n_r
 370     |assumption
 371     ]
 372   ]
 373 qed.
 374
 375 theorem le_log_div_sigma_p: \forall a,b,n,p. S O < p \to
 376 O < a \to a \le b \to b \le n \to
 377 log p (b/a) \le
 378 (sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))))/n!.
 379 intros.
 380 apply le_times_to_le_div
 381   [apply lt_O_fact
 382   |apply (trans_le ? (log p (exp (b/a) n!)))
 383     [apply log_exp2
 384       [assumption
 385       |apply le_times_to_le_div
 386         [assumption
 387         |rewrite < times_n_SO.
 388          assumption
 389         ]
 390       ]
 391     |apply (trans_le ? (log p ((exp b n!)/(exp a n!))))
 392       [apply le_log
 393         [assumption
 394         |apply le_exp_div.assumption
 395         ]
 396       |apply (trans_le ? (log p (exp b n!) - log p (exp a n!)))
 397         [apply log_div
 398           [assumption
 399           |apply lt_O_exp.
 400            assumption
 401           |apply monotonic_exp1.
 402            assumption
 403           ]
 404         |apply le_log_exp_fact_sigma_p;assumption
 405         ]
 406       ]
 407     ]
 408   ]
 409 qed.
 410
 411 theorem sigma_p_log_div1: \forall n,b. S O < b \to
 412 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
 413 \le sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n!
 414 ).
 415 intros.
 416 apply le_sigma_p.intros.
 417 apply le_log_div_sigma_p
 418   [assumption
 419   |apply prime_to_lt_O.
 420    apply primeb_true_to_prime.
 421    apply (andb_true_true ? ? H2)
 422   |apply le_S_S_to_le.
 423    assumption
 424   |apply le_n
 425   ]
 426 qed.
 427
 428 theorem sigma_p_log_div2: \forall n,b. S O < b \to
 429 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
 430 \le
 431 (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!).
 432 intros.
 433 apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)*S(log b (S(S(S O)))))))/n!
 434 )))
 435   [apply sigma_p_log_div1.assumption
 436   |apply le_times_to_le_div
 437     [apply lt_O_fact
 438     |rewrite > distributive_times_plus_sigma_p.
 439      rewrite < sym_times in ⊢ (? ? %).
 440      rewrite > distributive_times_plus_sigma_p.
 441      apply le_sigma_p.intros.
 442      apply (trans_le ? ((n!*(sigma_p n (λj:nat.leb i j) (λi:nat.S (n!/i*S (log b (S(S(S O)))))))/n!)))
 443       [apply le_times_div_div_times.
 444        apply lt_O_fact
 445       |rewrite > sym_times.
 446        rewrite > lt_O_to_div_times
 447         [rewrite > distributive_times_plus_sigma_p.
 448          apply le_sigma_p.intros.
 449          rewrite < times_n_Sm in ⊢ (? ? %).
 450          rewrite > plus_n_SO.
 451          rewrite > sym_plus.
 452          apply le_plus
 453           [apply le_S_S.apply le_O_n
 454           |rewrite < sym_times.
 455            apply le_n
 456           ]
 457         |apply lt_O_fact
 458         ]
 459       ]
 460     ]
 461   ]
 462 qed.
 463
 464 theorem sigma_p_log_div: \forall n,b. S O < b \to
 465 sigma_p (S n) (\lambda p.(primeb p \land (leb (S n) (p*p)))) (\lambda p.(log b (n/p)))
 466 \le (sigma_p n (\lambda i.leb (S n) (i*i)) (\lambda i.(prim i)*S(n!/i)))*S(log b (S(S(S O))))/n!
 467 .
 468 intros.
 469 apply (trans_le ? (sigma_p (S n) (\lambda p.primeb p \land (leb (S n) (p*p))) (\lambda p.(sigma_p n (\lambda i.leb p i) (\lambda i.S((n!/i)))))*S(log b (S(S(S O))))/n!))
 470   [apply sigma_p_log_div2.assumption
 471   |apply monotonic_div
 472     [apply lt_O_fact
 473     |apply le_times_l.
 474      unfold prim.
 475      cut
 476      (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p))
 477       (λp:nat.sigma_p n (λi:nat.leb p i) (λi:nat.S (n!/i)))
 478      = sigma_p n (λi:nat.leb (S n) (i*i))
 479        (λi:nat.sigma_p (S n) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i))))
 480       [rewrite > Hcut.
 481        apply le_sigma_p.intros.
 482        rewrite < sym_times.
 483        rewrite > distributive_times_plus_sigma_p.
 484        rewrite < times_n_SO.
 485        cut
 486         (sigma_p (S n) (λp:nat.primeb p∧leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i))
 487          = sigma_p (S i) (\lambda p.primeb p \land leb (S n) (p*p) \land leb p i) (λp:nat.S (n!/i)))
 488         [rewrite > Hcut1.
 489          apply le_sigma_p1.intros.
 490          rewrite < andb_sym.
 491          rewrite < andb_sym in ⊢ (? (? (? (? ? %)) ?) ?).
 492          apply (bool_elim  ? (leb i1 i));intros
 493           [apply (bool_elim  ? (leb (S n) (i1*i1)));intros
 494             [apply le_n
 495             |apply le_O_n
 496             ]
 497           |apply le_O_n
 498           ]
 499         |apply or_false_to_eq_sigma_p
 500           [apply le_S.assumption
 501           |intros.
 502            left.rewrite > (lt_to_leb_false i1 i)
 503             [rewrite > andb_sym.reflexivity
 504             |assumption
 505             ]
 506           ]
 507         ]
 508       |apply sigma_p_sigma_p.intros.
 509        apply (bool_elim ? (leb x y));intros
 510         [apply (bool_elim ? (leb (S n) (x*x)));intros
 511           [rewrite > le_to_leb_true in ⊢ (? ? ? (? % ?))
 512             [reflexivity
 513             |apply (trans_le ? (x*x))
 514               [apply leb_true_to_le.assumption
 515               |apply le_times;apply leb_true_to_le;assumption
 516               ]
 517             ]
 518           |rewrite < andb_sym in ⊢ (? ? (? % ?) ?).
 519            rewrite < andb_sym in ⊢ (? ? ? (? ? (? % ?))).
 520            rewrite < andb_sym in ⊢ (? ? ? %).
 521            reflexivity
 522           ]
 523         |rewrite < andb_sym.
 524          rewrite > andb_assoc in ⊢ (? ? ? %).
 525          rewrite < andb_sym in ⊢ (? ? ? (? % ?)).
 526          reflexivity
 527         ]
 528       ]
 529     ]
 530   ]
 531 qed.
 532
 533 theorem le_sigma_p_div_log_div_pred_log : \forall n,b,m. S O < b \to b*b \leq n \to
 534 sigma_p (S n) (\lambda i.leb (S n) (i*i)) (\lambda i.m/(log b i))
 535 \leq ((S (S O)) * n * m)/(pred (log b n)).
 536 intros.
 537 apply (trans_le ? (sigma_p (S n)
 538              (\lambda i.leb (S n) (i*i)) (\lambda i.(S (S O))*m/(pred (log b n)))))
 539   [apply le_sigma_p;intros;apply le_times_to_le_div
 540      [rewrite > minus_n_O in ⊢ (? ? (? %));rewrite < eq_minus_S_pred;
 541       apply le_plus_to_minus_r;simplify;
 542       rewrite < (eq_log_exp b ? H);
 543       apply le_log;
 544           [assumption
 545           |simplify;rewrite < times_n_SO;assumption]
 546      |apply (trans_le ? ((pred (log b n) * m)/log b i))
 547         [apply le_times_div_div_times;apply lt_O_log
 548           [elim (le_to_or_lt_eq ? ? (le_O_n i))
 549             [assumption
 550             |apply False_ind;apply not_eq_true_false;rewrite < H3;rewrite < H4;
 551              reflexivity]
 552           |apply (le_exp_to_le1 ? ? (S (S O)))
 553             [apply lt_O_S;
 554             |apply (trans_le ? (S n))
 555                [apply le_S;simplify;rewrite < times_n_SO;assumption
 556                |rewrite > exp_SSO;apply leb_true_to_le;assumption]]]
 557         |apply le_times_to_le_div2
 558           [apply lt_O_log
 559             [elim (le_to_or_lt_eq ? ? (le_O_n i))
 560               [assumption
 561               |apply False_ind;apply not_eq_true_false;rewrite < H3;rewrite < H4;
 562                reflexivity]
 563           |apply (le_exp_to_le1 ? ? (S (S O)))
 564             [apply lt_O_S;
 565             |apply (trans_le ? (S n))
 566                [apply le_S;simplify;rewrite < times_n_SO;assumption
 567                |rewrite > exp_SSO;apply leb_true_to_le;assumption]]]
 568           |rewrite > sym_times in \vdash (? ? %);rewrite < assoc_times;
 569            apply le_times_l;rewrite > sym_times;
 570            rewrite > minus_n_O in \vdash (? (? %) ?);
 571            rewrite < eq_minus_S_pred;apply le_plus_to_minus;
 572            simplify;rewrite < plus_n_O;apply (trans_le ? (log b (i*i)))
 573              [apply le_log
 574                 [assumption
 575                 |apply lt_to_le;apply leb_true_to_le;assumption]
 576              |rewrite > sym_plus;simplify;apply log_times;assumption]]]]
 577         |rewrite > times_n_SO in \vdash (? (? ? ? (\lambda i:?.%)) ?);
 578          rewrite < distributive_times_plus_sigma_p;
 579          apply (trans_le ? ((((S (S O))*m)/(pred (log b n)))*n))
 580            [apply le_times_r;apply (trans_le ? (sigma_p (S n) (\lambda i:nat.leb (S O) (i*i)) (\lambda Hbeta1:nat.S O)))
 581              [apply le_sigma_p1;intros;do 2 rewrite < times_n_SO;
 582               apply (bool_elim ? (leb (S n) (i*i)))
 583                 [intro;cut (leb (S O) (i*i) = true)
 584                   [rewrite > Hcut;apply le_n
 585                   |apply le_to_leb_true;apply (trans_le ? (S n))
 586                      [apply le_S_S;apply le_O_n
 587                      |apply leb_true_to_le;assumption]]
 588                 |intro;simplify in \vdash (? % ?);apply le_O_n]
 589              |elim n
 590                 [simplify;apply le_n
 591                 |apply (bool_elim ? (leb (S O) ((S n1)*(S n1))));intro
 592                    [rewrite > true_to_sigma_p_Sn
 593                       [change in \vdash (? % ?) with (S (sigma_p (S n1) (\lambda i:nat.leb (S O) (i*i)) (\lambda Hbeta1:nat.S O)));
 594                        apply le_S_S;assumption
 595                       |assumption]
 596                    |rewrite > false_to_sigma_p_Sn
 597                       [apply le_S;assumption
 598                       |assumption]]]]
 599           |rewrite > sym_times in \vdash (? % ?);
 600            rewrite > sym_times in \vdash (? ? (? (? % ?) ?));
 601            rewrite > assoc_times;
 602            apply le_times_div_div_times;
 603            rewrite > minus_n_O in ⊢ (? ? (? %));rewrite < eq_minus_S_pred;
 604            apply le_plus_to_minus_r;simplify;
 605            rewrite < (eq_log_exp b ? H);
 606            apply le_log;
 607              [assumption
 608              |simplify;rewrite < times_n_SO;assumption]]]
 609 qed.
 610
 611 (* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to
 612 divides n m \to
 613 log p (exp n m) - log p (exp a m) \le
 614 sigma_p (S n) (\lambda i.leb (S a) i) (\lambda i.S((m/i)*S(log p (S(S(S O)))))).
 615 intros.
 616 elim n
 617   [rewrite > false_to_sigma_p_Sn.
 618    simplify.
 619    apply (lt_O_n_elim ? H).intro.
 620    simplify.apply le_O_n
 621   |apply (bool_elim ? (leb a n1));intro
 622     [rewrite > true_to_sigma_p_Sn
 623       [apply (trans_le ? (S (m/S n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(m))-log p ((a)\sup(m)))))
 624         [rewrite > sym_plus.
 625          rewrite > plus_minus
 626           [apply le_plus_to_minus_r.
 627            rewrite < plus_minus_m_m
 628             [rewrite > sym_plus.
 629              apply le_log_exp_Sn_log_exp_n.
 630
 631
 632 * a generalization
 633 theorem le_exp_sigma_p_exp_m: \forall m,n. (exp (S m) n) \le
 634 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
 635 intros.
 636 rewrite > exp_S_sigma_p.
 637 apply le_sigma_p.
 638 intros.unfold bc.
 639 apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
 640   [rewrite > sym_times.
 641    apply le_times_r.
 642    rewrite > sym_times.
 643    rewrite < eq_div_div_div_times
 644     [apply monotonic_div
 645       [apply lt_O_fact
 646       |apply le_times_to_le_div2
 647         [apply lt_O_fact
 648         |apply le_fact_exp.
 649          apply le_S_S_to_le.
 650          assumption
 651         ]
 652       ]
 653     |apply lt_O_fact
 654     |apply lt_O_fact
 655     ]
 656   |apply le_times_div_div_times.
 657    apply lt_O_fact
 658   ]
 659 qed.
 660
 661 theorem lt_exp_sigma_p_exp_m: \forall m,n. S O < n \to
 662 (exp (S m) n) <
 663 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
 664 intros.
 665 rewrite > exp_S_sigma_p.
 666 apply lt_sigma_p
 667   [intros.unfold bc.
 668    apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
 669     [rewrite > sym_times.
 670      apply le_times_r.
 671      rewrite > sym_times.
 672      rewrite < eq_div_div_div_times
 673       [apply monotonic_div
 674         [apply lt_O_fact
 675         |apply le_times_to_le_div2
 676           [apply lt_O_fact
 677           |apply le_fact_exp.
 678            apply le_S_S_to_le.
 679            assumption
 680           ]
 681         ]
 682       |apply lt_O_fact
 683       |apply lt_O_fact
 684       ]
 685     |apply le_times_div_div_times.
 686      apply lt_O_fact
 687     ]
 688   |apply (ex_intro ? ? n).
 689    split
 690     [split
 691       [apply le_n
 692       |reflexivity
 693       ]
 694     |rewrite < minus_n_n.
 695      rewrite > bc_n_n.
 696      simplify.unfold lt.
 697      apply le_times_to_le_div
 698       [apply lt_O_fact
 699       |rewrite > sym_times.
 700        rewrite < plus_n_O.
 701        apply le_fact_exp1.
 702        assumption
 703       ]
 704     ]
 705   ]
 706 qed.
 707
 708 theorem lt_SO_to_lt_exp_Sn_n_SSSO_bof: \forall m,n. S O < n \to
 709 (exp (S m) n) < (S(S(S O)))*(exp m n).
 710 intros.
 711 apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!))))
 712   [apply lt_exp_sigma_p_exp_m.assumption
 713   |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
 714     [apply le_sigma_p.intros.
 715      apply le_times_to_le_div
 716       [apply lt_O_exp.
 717        apply lt_O_S
 718       |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
 719         [apply le_times_div_div_times.
 720          apply lt_O_fact
 721         |apply le_times_to_le_div2
 722           [apply lt_O_fact
 723           |rewrite < sym_times.
 724            apply le_times_r.
 725            apply le_exp_SSO_fact
 726           ]
 727         ]
 728       ]
 729     |rewrite > eq_sigma_p_pred
 730       [rewrite > div_SO.
 731        rewrite > sym_plus.
 732        change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
 733        apply le_plus_r.
 734        apply (trans_le ? (((S(S O))*(exp n n)*(exp (S(S O)) n) - (S(S O))*(exp n n))/(exp (S(S O)) n)))
 735         [apply sigma_p_div_exp
 736         |apply le_times_to_le_div2
 737           [apply lt_O_exp.
 738            apply lt_O_S.
 739           |apply le_minus_m
 740           ]
 741         ]
 742       |reflexivity
 743       ]
 744     ]
 745   ]
 746 qed.
 747 *)