Library Coq.Reals.Rpower
Definition Rpower (
x y:R) :=
exp (
y *
ln x).
Infix Local "^R" :=
Rpower (
at level 30,
right associativity) :
R_scope.
Note: Rpower is prolongated to 1 on negative real numbers and
it thus does not extend integer power. The next two lemmas, which
hold for integer power, accidentally hold on negative real numbers
as a side effect of the default value taken on negative real
numbers. Contrastingly, the lemmas that do not hold for the
integer power of a negative number are stated for Rpower on the
positive numbers only (even if they accidentally hold due to the
default value of Rpower on the negative side, as it is the case
for Rpower_O).
Theorem Rpower_plus :
forall x y z:R,
z ^R (
x +
y) =
z ^R
x *
z ^R
y.
Theorem Rpower_mult :
forall x y z:R, (
x ^R
y) ^R
z =
x ^R (
y *
z).
Theorem Rpower_O :
forall x:R, 0 <
x ->
x ^R 0 = 1.
Theorem Rpower_1 :
forall x:R, 0 <
x ->
x ^R 1 =
x.
Theorem Rpower_pow :
forall (
n:nat) (
x:R), 0 <
x ->
x ^R
INR n =
x ^
n.
Theorem Rpower_lt :
forall x y z:R, 1 <
x -> 0 <=
y ->
y <
z ->
x ^R
y <
x ^R
z.
Theorem Rpower_sqrt :
forall x:R, 0 <
x ->
x ^R (/ 2) =
sqrt x.
Theorem Rpower_Ropp :
forall x y:R,
x ^R (-
y) = /
x ^R
y.
Theorem Rle_Rpower :
forall e n m:R, 1 <
e -> 0 <=
n ->
n <=
m ->
e ^R
n <=
e ^R
m.
Theorem ln_lt_2 : / 2 <
ln 2.
Differentiability of Ln and Rpower
Theorem limit1_ext :
forall (
f g:R ->
R) (
D:R ->
Prop) (
l x:R),
(
forall x:R,
D x ->
f x =
g x) ->
limit1_in f D l x ->
limit1_in g D l x.
Theorem limit1_imp :
forall (
f:R ->
R) (
D D1:R ->
Prop) (
l x:R),
(
forall x:R,
D1 x ->
D x) ->
limit1_in f D l x ->
limit1_in f D1 l x.
Theorem Rinv_Rdiv :
forall x y:R,
x <> 0 ->
y <> 0 -> / (
x /
y) =
y /
x.
Theorem Dln :
forall y:R, 0 <
y ->
D_in ln Rinv (
fun x:R => 0 <
x)
y.
Lemma derivable_pt_lim_ln :
forall x:R, 0 <
x ->
derivable_pt_lim ln x (/
x).
Theorem D_in_imp :
forall (
f g:R ->
R) (
D D1:R ->
Prop) (
x:R),
(
forall x:R,
D1 x ->
D x) ->
D_in f g D x ->
D_in f g D1 x.
Theorem D_in_ext :
forall (
f g h:R ->
R) (
D:R ->
Prop) (
x:R),
f x =
g x ->
D_in h f D x ->
D_in h g D x.
Theorem Dpower :
forall y z:R,
0 <
y ->
D_in (
fun x:R =>
x ^R
z) (
fun x:R =>
z *
x ^R (
z - 1)) (
fun x:R => 0 <
x)
y.
Theorem derivable_pt_lim_power :
forall x y:R,
0 <
x ->
derivable_pt_lim (
fun x =>
x ^R
y)
x (
y *
x ^R (
y - 1)).