helm/software/matita/contribs/procedural/CoRN/transc/RealPowers.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: RealPowers.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
  20
  21 (*#* printing [!] %\ensuremath{\hat{\ }}% #^# *)
  22
  23 (*#* printing {!} %\ensuremath{\hat{\ }}% #^# *)
  24
  25 include "transc/Exponential.ma".
  26
  27 (* UNEXPORTED
  28 Opaque Expon.
  29 *)
  30
  31 (*#* *Arbitrary Real Powers
  32
  33 **Powers of Real Numbers
  34
  35 We now define
  36 $x^y=e^{y\times\log(x)}$#x<sup>y</sup>=e<sup>y*log(x)</sup>#, whenever
  37 [x [>] 0], inspired by the rules for manipulating these expressions.
  38 *)
  39
  40 inline procedural "cic:/CoRN/transc/RealPowers/power.con" as definition.
  41
  42 (* NOTATION
  43 Notation "x [!] y [//] Hy" := (power x y Hy) (at level 20).
  44 *)
  45
  46 (*#*
  47 This definition yields a well defined, strongly extensional function
  48 which extends the algebraic exponentiation to an integer power and
  49 still has all the good properties of that operation; when [x [=] e] it
  50 coincides with the exponential function.
  51 *)
  52
  53 inline procedural "cic:/CoRN/transc/RealPowers/power_wd.con" as lemma.
  54
  55 inline procedural "cic:/CoRN/transc/RealPowers/power_strext.con" as lemma.
  56
  57 inline procedural "cic:/CoRN/transc/RealPowers/power_plus.con" as lemma.
  58
  59 inline procedural "cic:/CoRN/transc/RealPowers/power_inv.con" as lemma.
  60
  61 (* UNEXPORTED
  62 Hint Resolve power_wd power_plus power_inv: algebra.
  63 *)
  64
  65 inline procedural "cic:/CoRN/transc/RealPowers/power_minus.con" as lemma.
  66
  67 inline procedural "cic:/CoRN/transc/RealPowers/power_nat.con" as lemma.
  68
  69 (* UNEXPORTED
  70 Hint Resolve power_minus power_nat: algebra.
  71 *)
  72
  73 inline procedural "cic:/CoRN/transc/RealPowers/power_zero.con" as lemma.
  74
  75 inline procedural "cic:/CoRN/transc/RealPowers/power_one.con" as lemma.
  76
  77 (* UNEXPORTED
  78 Hint Resolve power_zero power_one: algebra.
  79 *)
  80
  81 (* UNEXPORTED
  82 Opaque nexp_op.
  83 *)
  84
  85 inline procedural "cic:/CoRN/transc/RealPowers/power_int.con" as lemma.
  86
  87 (* UNEXPORTED
  88 Hint Resolve power_int: algebra.
  89 *)
  90
  91 inline procedural "cic:/CoRN/transc/RealPowers/Exp_power.con" as lemma.
  92
  93 inline procedural "cic:/CoRN/transc/RealPowers/mult_power.con" as lemma.
  94
  95 inline procedural "cic:/CoRN/transc/RealPowers/recip_power.con" as lemma.
  96
  97 (* UNEXPORTED
  98 Hint Resolve Exp_power mult_power recip_power: algebra.
  99 *)
 100
 101 inline procedural "cic:/CoRN/transc/RealPowers/div_power.con" as lemma.
 102
 103 (* UNEXPORTED
 104 Hint Resolve div_power: algebra.
 105 *)
 106
 107 inline procedural "cic:/CoRN/transc/RealPowers/power_ap_zero.con" as lemma.
 108
 109 inline procedural "cic:/CoRN/transc/RealPowers/power_mult.con" as lemma.
 110
 111 inline procedural "cic:/CoRN/transc/RealPowers/power_pos.con" as lemma.
 112
 113 (* UNEXPORTED
 114 Hint Resolve power_mult: algebra.
 115 *)
 116
 117 inline procedural "cic:/CoRN/transc/RealPowers/power_recip.con" as lemma.
 118
 119 (* UNEXPORTED
 120 Hint Resolve power_recip: algebra.
 121 *)
 122
 123 inline procedural "cic:/CoRN/transc/RealPowers/power_div.con" as lemma.
 124
 125 (* UNEXPORTED
 126 Hint Resolve power_div: algebra.
 127 *)
 128
 129 (* UNEXPORTED
 130 Section Power_Function
 131 *)
 132
 133 (*#* **Power Function
 134
 135 This operation on real numbers gives birth to an analogous operation
 136 on partial functions which preserves continuity.
 137
 138 %\begin{convention}% Let [F, G : PartIR].
 139 %\end{convention}%
 140 *)
 141
 142 (* UNEXPORTED
 143 cic:/CoRN/transc/RealPowers/Power_Function/J.var
 144 *)
 145
 146 (* UNEXPORTED
 147 cic:/CoRN/transc/RealPowers/Power_Function/F.var
 148 *)
 149
 150 (* UNEXPORTED
 151 cic:/CoRN/transc/RealPowers/Power_Function/G.var
 152 *)
 153
 154 inline procedural "cic:/CoRN/transc/RealPowers/FPower.con" as definition.
 155
 156 inline procedural "cic:/CoRN/transc/RealPowers/FPower_domain.con" as lemma.
 157
 158 inline procedural "cic:/CoRN/transc/RealPowers/Continuous_power.con" as lemma.
 159
 160 (* UNEXPORTED
 161 End Power_Function
 162 *)
 163
 164 (* NOTATION
 165 Notation "F {!} G" := (FPower F G) (at level 20).
 166 *)
 167
 168 (* UNEXPORTED
 169 Section More_on_Power_Function
 170 *)
 171
 172 (* UNEXPORTED
 173 Opaque Expon Logarithm.
 174 *)
 175
 176 (*#* From global continuity we can obviously get local continuity: *)
 177
 178 inline procedural "cic:/CoRN/transc/RealPowers/continuous_I_power.con" as lemma.
 179
 180 (*#* The rule for differentiation is a must. *)
 181
 182 (* UNEXPORTED
 183 Transparent Logarithm.
 184 *)
 185
 186 (* UNEXPORTED
 187 Opaque Logarithm.
 188 *)
 189
 190 inline procedural "cic:/CoRN/transc/RealPowers/Derivative_power.con" as lemma.
 191
 192 inline procedural "cic:/CoRN/transc/RealPowers/Diffble_power.con" as lemma.
 193
 194 (* UNEXPORTED
 195 End More_on_Power_Function
 196 *)
 197
 198 (* UNEXPORTED
 199 Hint Resolve Derivative_power: derivate.
 200 *)
 201