]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/transc/Exponential.mma
Stuff moved from old Matita.
[helm.git] / matita / matita / contribs / procedural / CoRN / transc / Exponential.mma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "CoRN.ma".
18
19 (* $Id: Exponential.v,v 1.7 2004/04/23 10:01:07 lcf Exp $ *)
20
21 include "transc/TaylorSeries.ma".
22
23 (* UNEXPORTED
24 Opaque Min Max.
25 *)
26
27 (*#* *Exponential and Logarithmic Functions
28
29 The main properties of the exponential and logarithmic functions.
30
31 **Properties of Exponential
32
33 Exponential is strongly extensional and well defined.
34 *)
35
36 inline procedural "cic:/CoRN/transc/Exponential/Exp_strext.con" as lemma.
37
38 inline procedural "cic:/CoRN/transc/Exponential/Exp_wd.con" as lemma.
39
40 (* UNEXPORTED
41 Hint Resolve Exp_wd: algebra.
42 *)
43
44 inline procedural "cic:/CoRN/transc/Exponential/Exp_zero.con" as lemma.
45
46 (*#* $e^1=e$#e<sup>1</sup>=e#, where [e] was defined a long time ago.
47 *)
48
49 inline procedural "cic:/CoRN/transc/Exponential/Exp_one.con" as lemma.
50
51 (* UNEXPORTED
52 Hint Resolve Exp_zero Exp_one: algebra.
53 *)
54
55 (*#*
56 The exponential function is its own derivative, and continuous.
57 *)
58
59 inline procedural "cic:/CoRN/transc/Exponential/Derivative_Exp.con" as lemma.
60
61 (* UNEXPORTED
62 Hint Resolve Derivative_Exp: derivate.
63 *)
64
65 inline procedural "cic:/CoRN/transc/Exponential/Continuous_Exp.con" as lemma.
66
67 (* UNEXPORTED
68 Hint Resolve Continuous_Exp: continuous.
69 *)
70
71 (*#*
72 Negative numbers are projected into the interval [[0,1]].
73 *)
74
75 inline procedural "cic:/CoRN/transc/Exponential/One_less_Exp.con" as lemma.
76
77 inline procedural "cic:/CoRN/transc/Exponential/One_leEq_Exp.con" as lemma.
78
79 inline procedural "cic:/CoRN/transc/Exponential/Exp_pos'.con" as lemma.
80
81 (*#*
82 Exponential is the unique function which evaluates to 1 at 0 and is
83 its own derivative.
84 *)
85
86 inline procedural "cic:/CoRN/transc/Exponential/Exp_unique_lemma.con" as lemma.
87
88 inline procedural "cic:/CoRN/transc/Exponential/Exp_bnd.con" as lemma.
89
90 (* UNEXPORTED
91 Opaque Expon.
92 *)
93
94 (* UNEXPORTED
95 Transparent Expon.
96 *)
97
98 inline procedural "cic:/CoRN/transc/Exponential/Exp_unique.con" as lemma.
99
100 (* UNEXPORTED
101 Opaque Expon.
102 *)
103
104 inline procedural "cic:/CoRN/transc/Exponential/Exp_plus_pos.con" as lemma.
105
106 (*#* The usual rules for computing the exponential of a sum. *)
107
108 inline procedural "cic:/CoRN/transc/Exponential/Exp_plus.con" as lemma.
109
110 (* UNEXPORTED
111 Hint Resolve Exp_plus: algebra.
112 *)
113
114 inline procedural "cic:/CoRN/transc/Exponential/Exp_plus'.con" as lemma.
115
116 inline procedural "cic:/CoRN/transc/Exponential/Exp_inv_char.con" as lemma.
117
118 (* UNEXPORTED
119 Hint Resolve Exp_inv_char: algebra.
120 *)
121
122 (*#* The exponential of any number is always positive---and thus apart
123 from zero.
124 *)
125
126 inline procedural "cic:/CoRN/transc/Exponential/Exp_pos.con" as lemma.
127
128 inline procedural "cic:/CoRN/transc/Exponential/Exp_ap_zero.con" as lemma.
129
130 (*#*
131 And the rules for the exponential of differences.
132 *)
133
134 inline procedural "cic:/CoRN/transc/Exponential/Exp_inv.con" as lemma.
135
136 (* UNEXPORTED
137 Hint Resolve Exp_inv: algebra.
138 *)
139
140 inline procedural "cic:/CoRN/transc/Exponential/Exp_minus.con" as lemma.
141
142 (* UNEXPORTED
143 Hint Resolve Exp_minus: algebra.
144 *)
145
146 inline procedural "cic:/CoRN/transc/Exponential/Exp_inv'.con" as lemma.
147
148 inline procedural "cic:/CoRN/transc/Exponential/Exp_minus'.con" as lemma.
149
150 (*#* Exponential is a monotonous function. *)
151
152 inline procedural "cic:/CoRN/transc/Exponential/Exp_less_One.con" as lemma.
153
154 inline procedural "cic:/CoRN/transc/Exponential/Exp_leEq_One.con" as lemma.
155
156 inline procedural "cic:/CoRN/transc/Exponential/Exp_resp_less.con" as lemma.
157
158 inline procedural "cic:/CoRN/transc/Exponential/Exp_resp_leEq.con" as lemma.
159
160 (*#* **Properties of Logarithm
161
162 The logarithm is a continuous function with derivative [One[/]x].
163 *)
164
165 inline procedural "cic:/CoRN/transc/Exponential/Derivative_Log.con" as lemma.
166
167 (* UNEXPORTED
168 Hint Resolve Derivative_Log: derivate.
169 *)
170
171 inline procedural "cic:/CoRN/transc/Exponential/Continuous_Log.con" as lemma.
172
173 (* UNEXPORTED
174 Hint Resolve Continuous_Log: continuous.
175 *)
176
177 (*#* Logarithm of [One]. *)
178
179 inline procedural "cic:/CoRN/transc/Exponential/Log_one.con" as lemma.
180
181 (* UNEXPORTED
182 Hint Resolve Log_one: algebra.
183 *)
184
185 (*#* The logarithm is (strongly) extensional. *)
186
187 inline procedural "cic:/CoRN/transc/Exponential/Log_strext.con" as lemma.
188
189 inline procedural "cic:/CoRN/transc/Exponential/Log_wd.con" as lemma.
190
191 (* UNEXPORTED
192 Hint Resolve Log_wd: algebra.
193 *)
194
195 (*#* The rule for the logarithm of the product. *)
196
197 (* UNEXPORTED
198 Opaque Logarithm.
199 *)
200
201 (* UNEXPORTED
202 Transparent Logarithm.
203 *)
204
205 inline procedural "cic:/CoRN/transc/Exponential/Log_mult.con" as lemma.
206
207 (* UNEXPORTED
208 Hint Resolve Log_mult: algebra.
209 *)
210
211 inline procedural "cic:/CoRN/transc/Exponential/Log_mult'.con" as lemma.
212
213 (*#* A characterization of the domain of the logarithm. *)
214
215 inline procedural "cic:/CoRN/transc/Exponential/Log_domain.con" as lemma.
216
217 (* UNEXPORTED
218 Opaque Expon Logarithm.
219 *)
220
221 (*#* $\log(e^x)=x$#log(e<sup>x</sup>)=x# for all [x], both as a
222 numerical and as a functional equation.
223 *)
224
225 inline procedural "cic:/CoRN/transc/Exponential/Log_Exp_inv.con" as lemma.
226
227 inline procedural "cic:/CoRN/transc/Exponential/Log_Exp.con" as lemma.
228
229 (* UNEXPORTED
230 Transparent Logarithm.
231 *)
232
233 (* UNEXPORTED
234 Hint Resolve Log_Exp: algebra.
235 *)
236
237 inline procedural "cic:/CoRN/transc/Exponential/Exp_Log_lemma.con" as lemma.
238
239 (*#* The converse expression. *)
240
241 inline procedural "cic:/CoRN/transc/Exponential/Exp_Log.con" as lemma.
242
243 (* UNEXPORTED
244 Hint Resolve Exp_Log: algebra.
245 *)
246
247 (*#* Exponential and logarithm are injective. *)
248
249 inline procedural "cic:/CoRN/transc/Exponential/Exp_cancel.con" as lemma.
250
251 inline procedural "cic:/CoRN/transc/Exponential/Log_cancel.con" as lemma.
252
253 (* UNEXPORTED
254 Opaque Logarithm.
255 *)
256
257 (*#* And the final characterization as inverse functions. *)
258
259 inline procedural "cic:/CoRN/transc/Exponential/Exp_Log_inv.con" as lemma.
260
261 inline procedural "cic:/CoRN/transc/Exponential/Log_E.con" as lemma.
262
263 (* UNEXPORTED
264 Hint Resolve Log_E: algebra.
265 *)
266
267 (*#* Several rules regarding inequalities. *)
268
269 inline procedural "cic:/CoRN/transc/Exponential/Log_cancel_less.con" as lemma.
270
271 inline procedural "cic:/CoRN/transc/Exponential/Log_cancel_leEq.con" as lemma.
272
273 inline procedural "cic:/CoRN/transc/Exponential/Log_resp_less.con" as lemma.
274
275 inline procedural "cic:/CoRN/transc/Exponential/Log_resp_leEq.con" as lemma.
276
277 inline procedural "cic:/CoRN/transc/Exponential/Exp_cancel_less.con" as lemma.
278
279 inline procedural "cic:/CoRN/transc/Exponential/Exp_cancel_leEq.con" as lemma.
280
281 inline procedural "cic:/CoRN/transc/Exponential/Log_less_Zero.con" as lemma.
282
283 inline procedural "cic:/CoRN/transc/Exponential/Log_leEq_Zero.con" as lemma.
284
285 inline procedural "cic:/CoRN/transc/Exponential/Zero_less_Log.con" as lemma.
286
287 inline procedural "cic:/CoRN/transc/Exponential/Zero_leEq_Log.con" as lemma.
288
289 (*#* Finally, rules for logarithm of quotients. *)
290
291 inline procedural "cic:/CoRN/transc/Exponential/Log_recip_char.con" as lemma.
292
293 inline procedural "cic:/CoRN/transc/Exponential/Log_recip.con" as lemma.
294
295 (* UNEXPORTED
296 Hint Resolve Log_recip: algebra.
297 *)
298
299 inline procedural "cic:/CoRN/transc/Exponential/Log_recip'.con" as lemma.
300
301 inline procedural "cic:/CoRN/transc/Exponential/Log_div.con" as lemma.
302
303 (* UNEXPORTED
304 Hint Resolve Log_div: algebra.
305 *)
306
307 inline procedural "cic:/CoRN/transc/Exponential/Log_div'.con" as lemma.
308