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 *********************)
19 (* $Id: RealPowers.v,v 1.5 2004/04/23 10:01:08 lcf Exp $ *)
21 (*#* printing [!] %\ensuremath{\hat{\ }}% #^# *)
23 (*#* printing {!} %\ensuremath{\hat{\ }}% #^# *)
25 include "transc/Exponential.ma".
31 (*#* *Arbitrary Real Powers
33 **Powers of Real Numbers
36 $x^y=e^{y\times\log(x)}$#x<sup>y</sup>=e<sup>y*log(x)</sup>#, whenever
37 [x [>] 0], inspired by the rules for manipulating these expressions.
40 inline procedural "cic:/CoRN/transc/RealPowers/power.con" as definition.
43 Notation "x [!] y [//] Hy" := (power x y Hy) (at level 20).
47 This definition yields a well defined, strongly extensional function
48 which extends the algebraic exponentiation to an integer power and
49 still has all the good properties of that operation; when [x [=] e] it
50 coincides with the exponential function.
53 inline procedural "cic:/CoRN/transc/RealPowers/power_wd.con" as lemma.
55 inline procedural "cic:/CoRN/transc/RealPowers/power_strext.con" as lemma.
57 inline procedural "cic:/CoRN/transc/RealPowers/power_plus.con" as lemma.
59 inline procedural "cic:/CoRN/transc/RealPowers/power_inv.con" as lemma.
62 Hint Resolve power_wd power_plus power_inv: algebra.
65 inline procedural "cic:/CoRN/transc/RealPowers/power_minus.con" as lemma.
67 inline procedural "cic:/CoRN/transc/RealPowers/power_nat.con" as lemma.
70 Hint Resolve power_minus power_nat: algebra.
73 inline procedural "cic:/CoRN/transc/RealPowers/power_zero.con" as lemma.
75 inline procedural "cic:/CoRN/transc/RealPowers/power_one.con" as lemma.
78 Hint Resolve power_zero power_one: algebra.
85 inline procedural "cic:/CoRN/transc/RealPowers/power_int.con" as lemma.
88 Hint Resolve power_int: algebra.
91 inline procedural "cic:/CoRN/transc/RealPowers/Exp_power.con" as lemma.
93 inline procedural "cic:/CoRN/transc/RealPowers/mult_power.con" as lemma.
95 inline procedural "cic:/CoRN/transc/RealPowers/recip_power.con" as lemma.
98 Hint Resolve Exp_power mult_power recip_power: algebra.
101 inline procedural "cic:/CoRN/transc/RealPowers/div_power.con" as lemma.
104 Hint Resolve div_power: algebra.
107 inline procedural "cic:/CoRN/transc/RealPowers/power_ap_zero.con" as lemma.
109 inline procedural "cic:/CoRN/transc/RealPowers/power_mult.con" as lemma.
111 inline procedural "cic:/CoRN/transc/RealPowers/power_pos.con" as lemma.
114 Hint Resolve power_mult: algebra.
117 inline procedural "cic:/CoRN/transc/RealPowers/power_recip.con" as lemma.
120 Hint Resolve power_recip: algebra.
123 inline procedural "cic:/CoRN/transc/RealPowers/power_div.con" as lemma.
126 Hint Resolve power_div: algebra.
130 Section Power_Function
133 (*#* **Power Function
135 This operation on real numbers gives birth to an analogous operation
136 on partial functions which preserves continuity.
138 %\begin{convention}% Let [F, G : PartIR].
143 cic:/CoRN/transc/RealPowers/Power_Function/J.var
147 cic:/CoRN/transc/RealPowers/Power_Function/F.var
151 cic:/CoRN/transc/RealPowers/Power_Function/G.var
154 inline procedural "cic:/CoRN/transc/RealPowers/FPower.con" as definition.
156 inline procedural "cic:/CoRN/transc/RealPowers/FPower_domain.con" as lemma.
158 inline procedural "cic:/CoRN/transc/RealPowers/Continuous_power.con" as lemma.
165 Notation "F {!} G" := (FPower F G) (at level 20).
169 Section More_on_Power_Function
173 Opaque Expon Logarithm.
176 (*#* From global continuity we can obviously get local continuity: *)
178 inline procedural "cic:/CoRN/transc/RealPowers/continuous_I_power.con" as lemma.
180 (*#* The rule for differentiation is a must. *)
183 Transparent Logarithm.
190 inline procedural "cic:/CoRN/transc/RealPowers/Derivative_power.con" as lemma.
192 inline procedural "cic:/CoRN/transc/RealPowers/Diffble_power.con" as lemma.
195 End More_on_Power_Function
199 Hint Resolve Derivative_power: derivate.