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 (* $Id: RealPowers.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
21 (*#* printing [!] %\ensuremath{\hat{\ }}% #^# *)
23 (*#* printing {!} %\ensuremath{\hat{\ }}% #^# *)
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.