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