1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/neper".
17 include "nat/iteration2.ma".
18 include "nat/div_and_mod_diseq.ma".
19 include "nat/binomial.ma".
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).
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)))
40 |change in ⊢ (? (? (? ? (? ? %)) ?) ?) with (m + (m +O)).
42 rewrite < eq_minus_minus_minus_plus.
44 rewrite > sym_times in ⊢ (? (? (? (? (? (? % ?) ?) ?) ?) ?) ?).
45 rewrite > assoc_times.
46 rewrite < plus_minus_m_m
48 |apply le_plus_to_minus_r.
49 rewrite > plus_n_O in ⊢ (? (? ? %) ?).
50 change in ⊢ (? % ?) with ((S(S O))*m).
53 rewrite > times_n_SO in ⊢ (? % ?).
69 theorem le_fact_exp: \forall i,m. i \le m \to m!≤ m \sup i*(m-i)!.
72 simplify.rewrite < plus_n_O.
75 apply (trans_le ? ((m)\sup(n)*(m-n)!))
77 apply lt_to_le.assumption
78 |rewrite > sym_times in ⊢ (? ? (? % ?)).
79 rewrite > assoc_times.
81 generalize in match H1.
84 apply (lt_to_not_le ? ? H2).
86 |rewrite > minus_Sn_m.
98 theorem le_fact_exp1: \forall n. S O < n \to (S(S O))*n!≤ n \sup 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.
106 apply (trans_le ? (exp n1 n1))
108 |apply monotonic_exp1.
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!).
117 rewrite > exp_S_sigma_p.
120 apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
121 [rewrite > sym_times.
124 rewrite < eq_div_div_div_times
127 |apply le_times_to_le_div2
137 |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
138 [rewrite > exp_plus_times.
139 apply le_times_div_div_times.
147 theorem lt_exp_sigma_p_exp: \forall n. S O < n \to
149 sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!).
151 rewrite > exp_S_sigma_p.
154 apply (trans_le ? ((exp n (n-i))*((n \sup i)/i!)))
155 [rewrite > sym_times.
158 rewrite < eq_div_div_div_times
161 |apply le_times_to_le_div2
171 |rewrite > (plus_minus_m_m ? i) in ⊢ (? ? (? (? ? %) ?))
172 [rewrite > exp_plus_times.
173 apply le_times_div_div_times.
179 |apply (ex_intro ? ? n).
185 |rewrite < minus_n_n.
188 apply le_times_to_le_div
190 |rewrite > sym_times.
198 theorem le_exp_Sn_n_SSSO: \forall n. (exp (S n) n) \le (S(S(S O))).
200 apply (trans_le ? (sigma_p (S n) (\lambda k.true) (\lambda k.(exp n n)/k!)))
201 [apply le_exp_sigma_p_exp
202 |apply (trans_le ? (sigma_p (S n) (\lambda i.true) (\lambda i.(exp n n)/(exp (S(S O)) i))))
203 [apply le_sigma_p.intros.
204 apply le_times_to_le_div
207 |apply (trans_le ? ((S(S O))\sup i* n \sup n/i!))
208 [apply le_times_div_div_times.
210 |apply le_times_to_le_div2
212 |rewrite < sym_times.