helm/software/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 set "baseuri" "cic:/matita/nat/neper".
  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
  22 theorem sigma_p_div_exp: \forall n,m.
  23 sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le
  24 ((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
  25 intros.
  26 elim n
  27   [apply le_O_n.
  28   |rewrite > true_to_sigma_p_Sn
  29     [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)))
  30       [apply le_plus_r.assumption
  31       |rewrite > assoc_times in ⊢ (? ? (? (? % ?) ?)).
  32        rewrite < distr_times_minus.
  33        change in ⊢ (? ? (? ? %)) with ((S(S O))*(exp (S(S O)) n1)).
  34        rewrite > sym_times in ⊢ (? ? (? % ?)).
  35        rewrite > sym_times in ⊢ (? ? (? ? %)).
  36        rewrite < lt_to_lt_to_eq_div_div_times_times
  37         [apply (trans_le ? ((m+((S(S O))*m*((S(S O)))\sup(n1)-(S(S O))*m))/((S(S O)))\sup(n1)))
  38           [apply le_plus_div.
  39            apply lt_O_exp.
  40            apply lt_O_S
  41           |change in ⊢ (? (? (? ? (? ? %)) ?) ?) with (m + (m +O)).
  42            rewrite < plus_n_O.
  43            rewrite < eq_minus_minus_minus_plus.
  44            rewrite > sym_plus.
  45            rewrite > sym_times in ⊢ (? (? (? (? (? (? % ?) ?) ?) ?) ?) ?).
  46            rewrite > assoc_times.
  47            rewrite < plus_minus_m_m
  48             [apply le_n
  49             |apply le_plus_to_minus_r.
  50              rewrite > plus_n_O in ⊢ (? (? ? %) ?).
  51              change in ⊢ (? % ?) with ((S(S O))*m).
  52              rewrite > sym_times.
  53              apply le_times_r.
  54              rewrite > times_n_SO in ⊢ (? % ?).
  55              apply le_times_r.
  56              apply lt_O_exp.
  57              apply lt_O_S
  58             ]
  59           ]
  60         |apply lt_O_S
  61         |apply lt_O_exp.
  62          apply lt_O_S
  63         ]
  64       ]
  65     |reflexivity
  66     ]
  67   ]
  68 qed.
  69
  70 theorem le_fact_exp: \forall i,m. i \le m \to m!≤ m \sup i*(m-i)!.
  71 intro.elim i
  72   [rewrite < minus_n_O.
  73    simplify.rewrite < plus_n_O.
  74    apply le_n
  75   |simplify.
  76    apply (trans_le ? ((m)\sup(n)*(m-n)!))
  77     [apply H.
  78      apply lt_to_le.assumption
  79     |rewrite > sym_times in ⊢ (? ? (? % ?)).
  80      rewrite > assoc_times.
  81      apply le_times_r.
  82      generalize in match H1.
  83      cases m;intro
  84       [apply False_ind.
  85        apply (lt_to_not_le ? ? H2).
  86        apply le_O_n
  87       |rewrite > minus_Sn_m.
  88        simplify.
  89        apply le_plus_r.
  90        apply le_times_l.
  91        apply le_minus_m.
  92        apply le_S_S_to_le.
  93        assumption
  94       ]
  95     ]
  96   ]
  97 qed.
  98
  99 theorem le_fact_exp1: \forall n. S O < n \to (S(S O))*n!≤ n \sup n.
 100 intros.elim H
 101   [apply le_n
 102   |change with ((S(S O))*((S n1)*(fact n1)) \le (S n1)*(exp (S n1) n1)).
 103    rewrite < assoc_times.
 104    rewrite < sym_times in ⊢ (? (? % ?) ?).
 105    rewrite > assoc_times.
 106    apply le_times_r.
 107    apply (trans_le ? (exp n1 n1))
 108     [assumption
 109     |apply monotonic_exp1.
 110      apply le_n_Sn
 111     ]
 112   ]
 113 qed.
 114
 115 theorem le_exp_sigma_p_exp: \forall n. (exp (S n) n) \le
 116 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
 117 intro.
 118 rewrite > exp_S_sigma_p.
 119 apply le_sigma_p.
 120 intros.unfold bc.
 121 apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
 122   [rewrite > sym_times.
 123    apply le_times_r.
 124    rewrite > sym_times.
 125    rewrite < eq_div_div_div_times
 126     [apply monotonic_div
 127       [apply lt_O_fact
 128       |apply le_times_to_le_div2
 129         [apply lt_O_fact
 130         |apply le_fact_exp.
 131          apply le_S_S_to_le.
 132          assumption
 133         ]
 134       ]
 135     |apply lt_O_fact
 136     |apply lt_O_fact
 137     ]
 138   |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
 139     [rewrite > exp_plus_times.
 140      apply le_times_div_div_times.
 141      apply lt_O_fact
 142     |apply le_S_S_to_le.
 143      assumption
 144     ]
 145   ]
 146 qed.
 147
 148 theorem lt_exp_sigma_p_exp: \forall n. S O < n \to
 149 (exp (S n) n) <
 150 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
 151 intros.
 152 rewrite > exp_S_sigma_p.
 153 apply lt_sigma_p
 154   [intros.unfold bc.
 155    apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
 156     [rewrite > sym_times.
 157      apply le_times_r.
 158      rewrite > sym_times.
 159      rewrite < eq_div_div_div_times
 160       [apply monotonic_div
 161         [apply lt_O_fact
 162         |apply le_times_to_le_div2
 163           [apply lt_O_fact
 164           |apply le_fact_exp.
 165            apply le_S_S_to_le.
 166            assumption
 167           ]
 168         ]
 169       |apply lt_O_fact
 170       |apply lt_O_fact
 171       ]
 172     |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
 173       [rewrite > exp_plus_times.
 174        apply le_times_div_div_times.
 175        apply lt_O_fact
 176       |apply le_S_S_to_le.
 177        assumption
 178       ]
 179     ]
 180   |apply (ex_intro ? ? n).
 181    split
 182     [split
 183       [apply le_n
 184       |reflexivity
 185       ]
 186     |rewrite < minus_n_n.
 187      rewrite > bc_n_n.
 188      simplify.unfold lt.
 189      apply le_times_to_le_div
 190       [apply lt_O_fact
 191       |rewrite > sym_times.
 192        apply le_fact_exp1.
 193        assumption
 194       ]
 195     ]
 196   ]
 197 qed.
 198
 199 theorem le_exp_SSO_fact:\forall n.
 200 exp (S(S O)) (pred n) \le n!.
 201 intro.elim n
 202   [apply le_n
 203   |change with ((S(S O))\sup n1 ≤(S n1)*n1!).
 204    apply (nat_case1 n1);intros
 205     [apply le_n
 206     |change in ⊢ (? % ?) with ((S(S O))*exp (S(S O)) (pred (S m))).
 207      apply le_times
 208       [apply le_S_S.apply le_S_S.apply le_O_n
 209       |rewrite < H1.assumption
 210       ]
 211     ]
 212   ]
 213 qed.
 214
 215 theorem lt_SO_to_lt_exp_Sn_n_SSSO: \forall n. S O < n \to
 216 (exp (S n) n) < (S(S(S O)))*(exp n n).
 217 intros.
 218 apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
 219   [apply lt_exp_sigma_p_exp.assumption
 220   |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
 221     [apply le_sigma_p.intros.
 222      apply le_times_to_le_div
 223       [apply lt_O_exp.
 224        apply lt_O_S
 225       |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
 226         [apply le_times_div_div_times.
 227          apply lt_O_fact
 228         |apply le_times_to_le_div2
 229           [apply lt_O_fact
 230           |rewrite < sym_times.
 231            apply le_times_r.
 232            apply le_exp_SSO_fact
 233           ]
 234         ]
 235       ]
 236     |rewrite > eq_sigma_p_pred
 237       [rewrite > div_SO.
 238        rewrite > sym_plus.
 239        change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
 240        apply le_plus_r.
 241        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)))
 242         [apply sigma_p_div_exp
 243         |apply le_times_to_le_div2
 244           [apply lt_O_exp.
 245            apply lt_O_S.
 246           |apply le_minus_m
 247           ]
 248         ]
 249       |reflexivity
 250       ]
 251     ]
 252   ]
 253 qed.
 254
 255 theorem lt_exp_Sn_n_SSSO: \forall n.
 256 (exp (S n) n) < (S(S(S O)))*(exp n n).
 257 intro.cases n;intros
 258   [simplify.apply le_S.apply le_n
 259   |cases n1;intros
 260     [simplify.apply le_n
 261     |apply lt_SO_to_lt_exp_Sn_n_SSSO.
 262      apply le_S_S.apply le_S_S.apply le_O_n
 263     ]
 264   ]
 265 qed.
 266
 267 theorem lt_exp_Sn_m_SSSO: \forall n,m. O < m \to
 268 divides n m \to
 269 (exp (S n) m) < (exp (S(S(S O))) (m/n)) *(exp n m).
 270 intros.
 271 elim H1.rewrite > H2.
 272 rewrite < exp_exp_times.
 273 rewrite < exp_exp_times.
 274 rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?)).
 275 rewrite > lt_O_to_div_times
 276   [rewrite > times_exp.
 277    apply lt_exp1
 278     [apply (O_lt_times_to_O_lt ? n).
 279      rewrite > sym_times.
 280      rewrite < H2.
 281      assumption
 282     |apply lt_exp_Sn_n_SSSO
 283     ]
 284   |apply (O_lt_times_to_O_lt ? n2).
 285    rewrite < H2.
 286    assumption
 287   ]
 288 qed.
 289
 290 theorem le_log_exp_Sn_log_exp_n: \forall n,m,p. O < m \to S O < p \to
 291 divides n m \to
 292 log p (exp (S n) m) \le S((m/n)*S(log p (S(S(S O))))) + log p (exp n m).
 293 intros.
 294 apply (trans_le ? (log p (((S(S(S O))))\sup(m/n)*((n)\sup(m)))))
 295   [apply le_log
 296     [assumption
 297     |apply lt_to_le.
 298      apply lt_exp_Sn_m_SSSO;assumption
 299     ]
 300   |apply (trans_le ? (S(log p (exp (S(S(S O))) (m/n)) + log p (exp n m))))
 301     [apply log_times.
 302      assumption
 303     |change in ⊢ (? ? %) with (S (m/n*S (log p (S(S(S O))))+log p ((n)\sup(m)))).
 304      apply le_S_S.
 305      apply le_plus_l.
 306      apply log_exp1.
 307      assumption
 308     ]
 309   ]
 310 qed.
 311
 312 theorem le_log_exp_fact_sigma_p: \forall a,b,n,p. S O < p \to
 313 O < a \to a \le b \to b \le n \to
 314 log p (exp b n!) - log p (exp a n!) \le
 315 sigma_p b (\lambda i.leb a i) (\lambda i.S((n!/i)*S(log p (S(S(S O)))))).
 316 intros 7.
 317 elim b
 318   [simplify.
 319    apply (lt_O_n_elim ? (lt_O_fact n)).intro.
 320    apply le_n.
 321   |apply (bool_elim ? (leb a n1));intro
 322     [rewrite > true_to_sigma_p_Sn
 323       [apply (trans_le ? (S (n!/n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(n!))-log p ((a)\sup(n!)))))
 324         [rewrite > sym_plus.
 325          rewrite > plus_minus
 326           [apply le_plus_to_minus_r.
 327            rewrite < plus_minus_m_m
 328             [rewrite > sym_plus.
 329              apply le_log_exp_Sn_log_exp_n
 330               [apply lt_O_fact
 331               |assumption
 332               |apply divides_fact;
 333                  [apply (trans_le ? ? ? H1);apply leb_true_to_le;assumption
 334                  |apply lt_to_le;assumption]]
 335             |apply le_log
 336               [assumption
 337               |cut (O = exp O n!)
 338                  [rewrite > Hcut;apply monotonic_exp1;constructor 2;
 339                   apply leb_true_to_le;assumption
 340                  |elim n
 341                     [reflexivity
 342                     |simplify;rewrite > exp_plus_times;rewrite < H6;
 343                      rewrite > sym_times;rewrite < times_n_O;reflexivity]]]]
 344         |apply le_log
 345           [assumption
 346           |apply monotonic_exp1;apply leb_true_to_le;assumption]]
 347       |rewrite > sym_plus;rewrite > sym_plus in \vdash (? ? %);apply le_minus_to_plus;
 348        rewrite < minus_plus_m_m;apply H3;apply lt_to_le;assumption]
 349     |assumption]
 350   |lapply (not_le_to_lt ? ? (leb_false_to_not_le ? ? H5));
 351    rewrite > eq_minus_n_m_O
 352     [apply le_O_n
 353     |apply le_log
 354        [assumption
 355        |apply monotonic_exp1;assumption]]]]
 356 qed.
 357
 358 (* theorem le_log_exp_Sn_log_exp_n: \forall n,m,a,p. O < m \to S O < p \to
 359 divides n m \to
 360 log p (exp n m) - log p (exp a m) \le
 361 sigma_p (S n) (\lambda i.leb (S a) i) (\lambda i.S((m/i)*S(log p (S(S(S O)))))).
 362 intros.
 363 elim n
 364   [rewrite > false_to_sigma_p_Sn.
 365    simplify.
 366    apply (lt_O_n_elim ? H).intro.
 367    simplify.apply le_O_n
 368   |apply (bool_elim ? (leb a n1));intro
 369     [rewrite > true_to_sigma_p_Sn
 370       [apply (trans_le ? (S (m/S n1*S (log p (S(S(S O)))))+(log p ((n1)\sup(m))-log p ((a)\sup(m)))))
 371         [rewrite > sym_plus.
 372          rewrite > plus_minus
 373           [apply le_plus_to_minus_r.
 374            rewrite < plus_minus_m_m
 375             [rewrite > sym_plus.
 376              apply le_log_exp_Sn_log_exp_n.
 377
 378
 379 * a generalization
 380 theorem le_exp_sigma_p_exp_m: \forall m,n. (exp (S m) n) \le
 381 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
 382 intros.
 383 rewrite > exp_S_sigma_p.
 384 apply le_sigma_p.
 385 intros.unfold bc.
 386 apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
 387   [rewrite > sym_times.
 388    apply le_times_r.
 389    rewrite > sym_times.
 390    rewrite < eq_div_div_div_times
 391     [apply monotonic_div
 392       [apply lt_O_fact
 393       |apply le_times_to_le_div2
 394         [apply lt_O_fact
 395         |apply le_fact_exp.
 396          apply le_S_S_to_le.
 397          assumption
 398         ]
 399       ]
 400     |apply lt_O_fact
 401     |apply lt_O_fact
 402     ]
 403   |apply le_times_div_div_times.
 404    apply lt_O_fact
 405   ]
 406 qed.
 407
 408 theorem lt_exp_sigma_p_exp_m: \forall m,n. S O < n \to
 409 (exp (S m) n) <
 410 sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!)).
 411 intros.
 412 rewrite > exp_S_sigma_p.
 413 apply lt_sigma_p
 414   [intros.unfold bc.
 415    apply (trans_le ? ((exp m (n-i))*((n \sup i)/i!)))
 416     [rewrite > sym_times.
 417      apply le_times_r.
 418      rewrite > sym_times.
 419      rewrite < eq_div_div_div_times
 420       [apply monotonic_div
 421         [apply lt_O_fact
 422         |apply le_times_to_le_div2
 423           [apply lt_O_fact
 424           |apply le_fact_exp.
 425            apply le_S_S_to_le.
 426            assumption
 427           ]
 428         ]
 429       |apply lt_O_fact
 430       |apply lt_O_fact
 431       ]
 432     |apply le_times_div_div_times.
 433      apply lt_O_fact
 434     ]
 435   |apply (ex_intro ? ? n).
 436    split
 437     [split
 438       [apply le_n
 439       |reflexivity
 440       ]
 441     |rewrite < minus_n_n.
 442      rewrite > bc_n_n.
 443      simplify.unfold lt.
 444      apply le_times_to_le_div
 445       [apply lt_O_fact
 446       |rewrite > sym_times.
 447        rewrite < plus_n_O.
 448        apply le_fact_exp1.
 449        assumption
 450       ]
 451     ]
 452   ]
 453 qed.
 454
 455 theorem lt_SO_to_lt_exp_Sn_n_SSSO_bof: \forall m,n. S O < n \to
 456 (exp (S m) n) < (S(S(S O)))*(exp m n).
 457 intros.
 458 apply (lt_to_le_to_lt ? (sigma_p (S n) (\lambda k.true) (\lambda k.((exp m (n-k))*(exp n k))/(k!))))
 459   [apply lt_exp_sigma_p_exp_m.assumption
 460   |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) (pred i)))))
 461     [apply le_sigma_p.intros.
 462      apply le_times_to_le_div
 463       [apply lt_O_exp.
 464        apply lt_O_S
 465       |apply (trans_le ? ((S(S O))\sup (pred i)* n \sup n/i!))
 466         [apply le_times_div_div_times.
 467          apply lt_O_fact
 468         |apply le_times_to_le_div2
 469           [apply lt_O_fact
 470           |rewrite < sym_times.
 471            apply le_times_r.
 472            apply le_exp_SSO_fact
 473           ]
 474         ]
 475       ]
 476     |rewrite > eq_sigma_p_pred
 477       [rewrite > div_SO.
 478        rewrite > sym_plus.
 479        change in ⊢ (? ? %) with ((exp n n)+(S(S O)*(exp n n))).
 480        apply le_plus_r.
 481        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)))
 482         [apply sigma_p_div_exp
 483         |apply le_times_to_le_div2
 484           [apply lt_O_exp.
 485            apply lt_O_S.
 486           |apply le_minus_m
 487           ]
 488         ]
 489       |reflexivity
 490       ]
 491     ]
 492   ]
 493 qed.
 494 *)