]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/factorial2.ma
Towards chebyshev.
[helm.git] / helm / software / matita / library / nat / factorial2.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/factorial2".
16
17 include "nat/exp.ma".
18 include "nat/factorial.ma".
19
20 theorem factS: \forall n. fact (S n) = (S n)*(fact n).
21 intro.simplify.reflexivity.
22 qed.
23
24 theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
25 intros.reflexivity.
26 qed.
27
28 lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
29 intro.simplify.rewrite < plus_n_Sm.reflexivity.
30 qed.
31
32 theorem fact1: \forall n.
33 fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
34 intro.elim n
35   [rewrite < times_n_O.apply le_n
36   |rewrite > times_SSO.
37    rewrite > factS.
38    rewrite > factS.
39    rewrite < assoc_times.
40    rewrite > factS.
41    apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
42     [apply le_times_l.
43      rewrite > times_SSO.
44      apply le_times_r.
45      apply le_n_Sn
46     |rewrite > assoc_times.
47      rewrite > assoc_times.
48      rewrite > assoc_times in ⊢ (? ? %).
49      rewrite > exp_S. 
50      rewrite > assoc_times in ⊢ (? ? %).
51      apply le_times_r.
52      rewrite < assoc_times.
53      rewrite < assoc_times.
54      rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
55      rewrite > assoc_times.
56      rewrite > assoc_times.
57      rewrite > exp_S. 
58      rewrite > assoc_times in ⊢ (? ? %).
59      apply le_times_r.
60      rewrite > sym_times in ⊢ (? ? %).
61      rewrite > assoc_times in ⊢ (? ? %).
62      rewrite > assoc_times in ⊢ (? ? %).
63      apply le_times_r.
64      rewrite < assoc_times in ⊢ (? ? %).
65      rewrite < assoc_times in ⊢ (? ? %).
66      rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
67      rewrite > assoc_times in ⊢ (? ? %).
68      rewrite > assoc_times in ⊢ (? ? %).
69      apply le_times_r.
70      rewrite > sym_times in ⊢ (? ? (? ? %)).
71      rewrite > sym_times in ⊢ (? ? %).
72      assumption
73     ]
74   ]
75 qed.
76
77 theorem lt_O_fact: \forall n. O < fact n.
78 intro.elim n
79   [simplify.apply lt_O_S
80   |rewrite > factS.
81    rewrite > (times_n_O O).
82    apply lt_times
83     [apply lt_O_S
84     |assumption
85     ]
86   ]
87 qed.
88
89 theorem fact2: \forall n.O < n \to
90 (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
91 intros.elim H
92   [simplify.apply le_S.apply le_n
93   |rewrite > times_SSO.
94    rewrite > factS.
95    rewrite > factS.
96    rewrite < assoc_times.
97    rewrite > factS.
98    rewrite < times_SSO in ⊢ (? ? %).
99    apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
100     [rewrite > assoc_times in ⊢ (? ? %).
101      rewrite > exp_S.
102      rewrite > assoc_times.
103      rewrite > assoc_times.
104      rewrite > assoc_times.
105      apply lt_times_r.
106      rewrite > exp_S.
107      rewrite > assoc_times.
108      rewrite > sym_times in ⊢ (? ? %).
109      rewrite > assoc_times in ⊢ (? ? %).
110      rewrite > assoc_times in ⊢ (? ? %).
111      apply lt_times_r.
112      rewrite > sym_times.
113      rewrite > assoc_times.
114      rewrite > assoc_times.
115      apply lt_times_r.
116      rewrite < assoc_times.
117      rewrite < assoc_times.
118      rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
119      rewrite > assoc_times.
120      rewrite > assoc_times.
121      rewrite > sym_times in ⊢ (? ? %).
122      apply lt_times_r.
123      rewrite < assoc_times.
124      rewrite < sym_times.
125      rewrite < assoc_times.
126      assumption
127     |apply lt_times_l1
128       [rewrite > (times_n_O O) in ⊢ (? % ?).
129        apply lt_times
130         [rewrite > (times_n_O O) in ⊢ (? % ?).
131          apply lt_times
132           [apply lt_O_S
133           |apply lt_O_S
134           ]
135         |apply lt_O_fact
136         ]
137       |apply le_n
138       ]
139     ]
140   ]
141 qed.
142
143 (*
144 theorem stirling: \forall n,k.k \le n \to
145 log (fact n) < n*log n - n + k*log n.
146 intro.
147 apply (nat_elim1 n).
148 intros.
149 elim (lt_O_to_or_eq_S m)
150   [elim H2.clear H2.
151    elim H4.clear H4.
152    rewrite > H2.
153    apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
154     [apply monotonic_log.
155      apply fact1
156     |rewrite > assoc_times in ⊢ (? (? %) ?).
157      rewrite > log_exp.
158      apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
159       [apply le_plus_r.
160        apply log_times
161       |rewrite < plus_n_Sm.
162        rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
163        change with
164         (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
165        apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
166         [apply le_S_S.
167          apply lt_plus_r.
168          apply lt_times_r.
169          apply H.
170          assumption
171         |
172         
173           [
174        
175        a*log a-a+k*log a
176        
177 *)