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