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