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