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 (* $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
  26 Exponential
  27 *)
  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