1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/transc/RealPowers".
19 include "CoRN_notation.ma".
21 (* $Id: RealPowers.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
23 (*#* printing [!] %\ensuremath{\hat{\ }}% #^# *)
25 (*#* printing {!} %\ensuremath{\hat{\ }}% #^# *)
27 include "transc/Exponential.ma".
33 (*#* *Arbitrary Real Powers
35 **Powers of Real Numbers
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.
42 inline "cic:/CoRN/transc/RealPowers/power.con".
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.
51 inline "cic:/CoRN/transc/RealPowers/power_wd.con".
53 inline "cic:/CoRN/transc/RealPowers/power_strext.con".
55 inline "cic:/CoRN/transc/RealPowers/power_plus.con".
57 inline "cic:/CoRN/transc/RealPowers/power_inv.con".
60 Hint Resolve power_wd power_plus power_inv: algebra.
63 inline "cic:/CoRN/transc/RealPowers/power_minus.con".
65 inline "cic:/CoRN/transc/RealPowers/power_nat.con".
68 Hint Resolve power_minus power_nat: algebra.
71 inline "cic:/CoRN/transc/RealPowers/power_zero.con".
73 inline "cic:/CoRN/transc/RealPowers/power_one.con".
76 Hint Resolve power_zero power_one: algebra.
83 inline "cic:/CoRN/transc/RealPowers/power_int.con".
86 Hint Resolve power_int: algebra.
89 inline "cic:/CoRN/transc/RealPowers/Exp_power.con".
91 inline "cic:/CoRN/transc/RealPowers/mult_power.con".
93 inline "cic:/CoRN/transc/RealPowers/recip_power.con".
96 Hint Resolve Exp_power mult_power recip_power: algebra.
99 inline "cic:/CoRN/transc/RealPowers/div_power.con".
102 Hint Resolve div_power: algebra.
105 inline "cic:/CoRN/transc/RealPowers/power_ap_zero.con".
107 inline "cic:/CoRN/transc/RealPowers/power_mult.con".
109 inline "cic:/CoRN/transc/RealPowers/power_pos.con".
112 Hint Resolve power_mult: algebra.
115 inline "cic:/CoRN/transc/RealPowers/power_recip.con".
118 Hint Resolve power_recip: algebra.
121 inline "cic:/CoRN/transc/RealPowers/power_div.con".
124 Hint Resolve power_div: algebra.
128 Section Power_Function.
131 (*#* **Power Function
133 This operation on real numbers gives birth to an analogous operation
134 on partial functions which preserves continuity.
136 %\begin{convention}% Let [F, G : PartIR].
140 inline "cic:/CoRN/transc/RealPowers/J.var".
142 inline "cic:/CoRN/transc/RealPowers/F.var".
144 inline "cic:/CoRN/transc/RealPowers/G.var".
146 inline "cic:/CoRN/transc/RealPowers/FPower.con".
148 inline "cic:/CoRN/transc/RealPowers/FPower_domain.con".
150 inline "cic:/CoRN/transc/RealPowers/Continuous_power.con".
157 Section More_on_Power_Function.
161 Opaque Expon Logarithm.
164 (*#* From global continuity we can obviously get local continuity: *)
166 inline "cic:/CoRN/transc/RealPowers/continuous_I_power.con".
168 (*#* The rule for differentiation is a must. *)
171 Transparent Logarithm.
178 inline "cic:/CoRN/transc/RealPowers/Derivative_power.con".
180 inline "cic:/CoRN/transc/RealPowers/Diffble_power.con".
183 End More_on_Power_Function.
187 Hint Resolve Derivative_power: derivate.