Arbitrary Real Powers
Powers of Real Numbers
We now define xy=ey*log(x), whenever x > 0, inspired by the rules for manipulating these expressions.
Definition power x y (Hx : 0 [<] x) := Exp (y[*]Log x Hx).
Notation "x ^ y ‡ Hy" := (power x y Hy) (at level 20).
This definition yields a well defined, strongly extensional function
which extends the algebraic exponentiation to an integer power and
still has all the good properties of that operation; when x = e it
coincides with the exponential function.
Lemma power_wd : forall x x' y y' Hx Hx', x [=] x' -> y [=] y' -> x[!]y[//]Hx [=] x'[!]y'[//]Hx'.
Lemma power_strext : forall x x' y y' Hx Hx', x[!]y[//]Hx [#] x'[!]y'[//]Hx' -> x [#] x' or y [#] y'.
Lemma power_plus : forall x y z Hx, x[!]y[+]z[//]Hx [=] x[!]y[//]Hx[*]x[!]z[//]Hx.
Lemma power_inv : forall x y Hx Hxy, x[!] [--]y[//]Hx [=] (1[/] x[!]y[//]Hx[//]Hxy).
Lemma power_minus : forall x y z Hx Hxz, x[!]y[-]z[//]Hx [=] (x[!]y[//]Hx[/] x[!]z[//]Hx[//]Hxz).
Lemma power_nat : forall x n Hx, x[!]nring n[//]Hx [=] x[^]n.
Lemma power_zero : forall (x : IR) Hx, x[!]0[//]Hx [=] 1.
Lemma power_one : forall (x : IR) Hx, x[!]1[//]Hx [=] x.
Lemma one_power : forall (x : IR) H, 1[!]x[//]H [=] 1.
Lemma power_int : forall x z Hx Hx', x[!]zring z[//]Hx [=] (x[//]Hx') [^^] (z).
Lemma Exp_power : forall (x : IR) He, E[!]x[//]He [=] Exp x.
Lemma mult_power : forall x y z Hx Hy Hxy, (x[*]y) [!]z[//]Hxy [=] x[!]z[//]Hx[*]y[!]z[//]Hy.
Lemma recip_power : forall x y Hx Hx' Hx'' Hxy, (1[/] x[//]Hx') [!]y[//]Hx'' [=] (1[/] x[!]y[//]Hx[//]Hxy).
Lemma div_power : forall x y z Hx Hy Hy' Hxy Hyz,
(x[/] y[//]Hy') [!]z[//]Hxy [=] (x[!]z[//]Hx[/] y[!]z[//]Hy[//]Hyz).
Lemma power_ap_zero : forall (x y : IR) Hx, x[!]y[//]Hx [#] 0.
Lemma power_mult : forall x y z Hx Hxy, x[!]y[*]z[//]Hx [=] (x[!]y[//]Hx) [!]z[//]Hxy.
Lemma power_pos : forall (x y : IR) Hx, 0 [<] x[!]y[//]Hx.
Lemma power_recip : forall x q Hx (Hx' : 0 [<=] x) Hq (Hq' : 0 < q),
x[!]1[/] nring q[//]Hq[//]Hx [=] NRoot Hx' Hq'.
Lemma power_div : forall x p q Hx (Hx' : 0 [<=] x) Hq (Hq' : 0 < q),
x[!]nring p[/] nring q[//]Hq[//]Hx [=] (NRoot Hx' Hq') [^]p.
Lemma real_power_resp_leEq_rht : forall x y p Hx Hy,
0[<=] p -> x[<=]y -> x[!]p[//]Hx [<=] y[!]p[//]Hy.
Lemma real_power_resp_less_rht : forall x y p Hx Hy,
0[<] p -> x[<]y -> x[!]p[//]Hx [<] y[!]p[//]Hy.
Lemma real_power_resp_leEq_lft : forall x p q Hx Hx',
1[<=]x -> p[<=]q -> x[!]p[//]Hx [<=] x[!]q[//]Hx'.
Lemma real_power_resp_less_lft : forall x p q Hx Hx',
1[<]x -> p[<]q -> x[!]p[//]Hx [<] x[!]q[//]Hx'.
Lemma real_power_resp_leEq_both : forall x y p q Hx Hy',
1[<=]x -> 0 [<=] p -> x[<=]y -> p[<=]q ->
x[!]p[//]Hx [<=] y[!]q[//]Hy'.
Lemma real_power_resp_less_both : forall x y p q Hx Hy',
1[<]x -> 0 [<] p -> x[<]y -> p[<]q ->
x[!]p[//]Hx [<] y[!]q[//]Hy'.
Section Power_Function.
Power Function
This operation on real numbers gives birth to an analogous operation on partial functions which preserves continuity.
Let F, G : PartIR.
Variable J : interval.
Variables F G : PartIR.
Definition FPower := Expon[o]G{*} (Logarithm[o]F).
Lemma FPower_domain : forall x, Dom F x -> Dom G x ->
(forall Hx, 0 [<] F x Hx) -> Dom FPower x.
Lemma Continuous_power : positive_fun J F ->
Continuous J F -> Continuous J G -> Continuous J FPower.
End Power_Function.
Notation "F {!} G" := (FPower F G) (at level 20).
Section More_on_Power_Function.
From global continuity we can obviously get local continuity:
Lemma continuous_I_power : forall F G a b Hab, Continuous_I Hab F ->
Continuous_I Hab G -> positive_fun (compact a b Hab) F -> Continuous_I Hab (F{!}G).
The rule for differentiation is a must.
Lemma Derivative_power : forall (J : interval) pJ F F' G G', positive_fun J F ->
Derivative J pJ F F' -> Derivative J pJ G G' ->
Derivative J pJ (F{!}G) (G{*} (F{!} (G{-} [-C-]1) {*}F') {+}F{!}G{*} (G'{*} (Logarithm[o]F))).
Included.
Included.
Included.
Included.
Included.
Included.
Included.
Included.
Qed.
Lemma Diffble_power : forall (J : interval) pJ F G, positive_fun J F ->
Diffble J pJ F -> Diffble J pJ G -> Diffble J pJ (F{!}G).
End More_on_Power_Function.