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
  21 theorem sigma_p_div_exp: \forall n,m.
  22 sigma_p n (\lambda i.true) (\lambda i.m/(exp (S(S O)) i)) \le
  23 ((S(S O))*m*(exp (S(S O)) n) - (S(S O))*m)/(exp (S(S O)) n).
  24 intros.
  25 elim n
  26   [apply le_O_n.
  27   |rewrite > true_to_sigma_p_Sn
  28     [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)))
  29       [apply le_plus_r.assumption
  30       |rewrite > assoc_times in ⊢ (? ? (? (? % ?) ?)).
  31        rewrite < distr_times_minus.
  32        change in ⊢ (? ? (? ? %)) with ((S(S O))*(exp (S(S O)) n1)).
  33        rewrite > sym_times in ⊢ (? ? (? % ?)).
  34        rewrite > sym_times in ⊢ (? ? (? ? %)).
  35        rewrite < lt_to_lt_to_eq_div_div_times_times
  36         [apply (trans_le ? ((m+((S(S O))*m*((S(S O)))\sup(n1)-(S(S O))*m))/((S(S O)))\sup(n1)))
  37           [apply le_plus_div.
  38            apply lt_O_exp.
  39            apply lt_O_S
  40           |change in ⊢ (? (? (? ? (? ? %)) ?) ?) with (m + (m +O)).
  41            rewrite < plus_n_O.
  42            rewrite < eq_minus_minus_minus_plus.
  43            rewrite > sym_plus.
  44            rewrite > sym_times in ⊢ (? (? (? (? (? (? % ?) ?) ?) ?) ?) ?).
  45            rewrite > assoc_times.
  46            rewrite < plus_minus_m_m
  47             [apply le_n
  48             |apply le_plus_to_minus_r.
  49              rewrite > plus_n_O in ⊢ (? (? ? %) ?).
  50              change in ⊢ (? % ?) with ((S(S O))*m).
  51              rewrite > sym_times.
  52              apply le_times_r.
  53              rewrite > times_n_SO in ⊢ (? % ?).
  54              apply le_times_r.
  55              apply lt_O_exp.
  56              apply lt_O_S
  57             ]
  58           ]
  59         |apply lt_O_S
  60         |apply lt_O_exp.
  61          apply lt_O_S
  62         ]
  63       ]
  64     |reflexivity
  65     ]
  66   ]
  67 qed.
  68
  69 theorem le_fact_exp: \forall i,m. i \le m \to m!≤ m \sup i*(m-i)!.
  70 intro.elim i
  71   [rewrite < minus_n_O.
  72    simplify.rewrite < plus_n_O.
  73    apply le_n
  74   |simplify.
  75    apply (trans_le ? ((m)\sup(n)*(m-n)!))
  76     [apply H.
  77      apply lt_to_le.assumption
  78     |rewrite > sym_times in ⊢ (? ? (? % ?)).
  79      rewrite > assoc_times.
  80      apply le_times_r.
  81      generalize in match H1.
  82      cases m;intro
  83       [apply False_ind.
  84        apply (lt_to_not_le ? ? H2).
  85        apply le_O_n
  86       |rewrite > minus_Sn_m.
  87        simplify.
  88        apply le_plus_r.
  89        apply le_times_l.
  90        apply le_minus_m.
  91        apply le_S_S_to_le.
  92        assumption
  93       ]
  94     ]
  95   ]
  96 qed.
  97
  98 theorem le_fact_exp1: \forall n. S O < n \to (S(S O))*n!≤ n \sup n.
  99 intros.elim H
 100   [apply le_n
 101   |change with ((S(S O))*((S n1)*(fact n1)) \le (S n1)*(exp (S n1) n1)).
 102    rewrite < assoc_times.
 103    rewrite < sym_times in ⊢ (? (? % ?) ?).
 104    rewrite > assoc_times.
 105    apply le_times_r.
 106    apply (trans_le ? (exp n1 n1))
 107     [assumption
 108     |apply monotonic_exp1.
 109      apply le_n_Sn
 110     ]
 111   ]
 112 qed.
 113
 114 theorem le_exp_sigma_p_exp: \forall n. (exp (S n) n) \le
 115 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
 116 intro.
 117 rewrite > exp_S_sigma_p.
 118 apply le_sigma_p.
 119 intros.unfold bc.
 120 apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
 121   [rewrite > sym_times.
 122    apply le_times_r.
 123    rewrite > sym_times.
 124    rewrite < eq_div_div_div_times
 125     [apply monotonic_div
 126       [apply lt_O_fact
 127       |apply le_times_to_le_div2
 128         [apply lt_O_fact
 129         |apply le_fact_exp.
 130          apply le_S_S_to_le.
 131          assumption
 132         ]
 133       ]
 134     |apply lt_O_fact
 135     |apply lt_O_fact
 136     ]
 137   |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
 138     [rewrite > exp_plus_times.
 139      apply le_times_div_div_times.
 140      apply lt_O_fact
 141     |apply le_S_S_to_le.
 142      assumption
 143     ]
 144   ]
 145 qed.
 146
 147 theorem lt_exp_sigma_p_exp: \forall n. S O < n \to
 148 (exp (S n) n) <
 149 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
 150 intros.
 151 rewrite > exp_S_sigma_p.
 152 apply lt_sigma_p
 153   [intros.unfold bc.
 154    apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
 155     [rewrite > sym_times.
 156      apply le_times_r.
 157      rewrite > sym_times.
 158      rewrite < eq_div_div_div_times
 159       [apply monotonic_div
 160         [apply lt_O_fact
 161         |apply le_times_to_le_div2
 162           [apply lt_O_fact
 163           |apply le_fact_exp.
 164            apply le_S_S_to_le.
 165            assumption
 166           ]
 167         ]
 168       |apply lt_O_fact
 169       |apply lt_O_fact
 170       ]
 171     |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
 172       [rewrite > exp_plus_times.
 173        apply le_times_div_div_times.
 174        apply lt_O_fact
 175       |apply le_S_S_to_le.
 176        assumption
 177       ]
 178     ]
 179   |apply (ex_intro ? ? n).
 180    split
 181     [split
 182       [apply le_n
 183       |reflexivity
 184       ]
 185     |rewrite < minus_n_n.
 186      rewrite > bc_n_n.
 187      simplify.unfold lt.
 188      apply le_times_to_le_div
 189       [apply lt_O_fact
 190       |rewrite > sym_times.
 191        apply le_fact_exp1.
 192        assumption
 193       ]
 194     ]
 195   ]
 196 qed.
 197
 198
 199
 200
 201