helm/software/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