Library Coq.Reals.Rfunctions
Definition of the sum functions
Infix "^" :=
pow :
R_scope.
Lemma pow_O :
forall x:
R,
x ^ 0
= 1.
Lemma pow_1 :
forall x:
R,
x ^ 1
= x.
Lemma pow_add :
forall (
x:
R) (
n m:
nat),
x ^ (n + m) = x ^ n * x ^ m.
Lemma Rpow_mult_distr :
forall (
x y:
R) (
n:
nat),
(x * y) ^ n = x^n * y^n.
Lemma pow_nonzero :
forall (
x:
R) (
n:
nat),
x <> 0 ->
x ^ n <> 0.
Hint Resolve pow_O pow_1 pow_add pow_nonzero:
real.
Lemma pow_RN_plus :
forall (
x:
R) (
n m:
nat),
x <> 0 ->
x ^ n = x ^ (n + m) * / x ^ m.
Lemma pow_lt :
forall (
x:
R) (
n:
nat), 0
< x -> 0
< x ^ n.
Hint Resolve pow_lt:
real.
Lemma Rlt_pow_R1 :
forall (
x:
R) (
n:
nat), 1
< x -> (0
< n)%
nat -> 1
< x ^ n.
Hint Resolve Rlt_pow_R1:
real.
Lemma Rlt_pow :
forall (
x:
R) (
n m:
nat), 1
< x -> (
n < m)%
nat ->
x ^ n < x ^ m.
Hint Resolve Rlt_pow:
real.
Lemma tech_pow_Rmult :
forall (
x:
R) (
n:
nat),
x * x ^ n = x ^ S n.
Lemma tech_pow_Rplus :
forall (
x:
R) (
a n:
nat),
x ^ a + INR n * x ^ a = INR (
S n)
* x ^ a.
Lemma poly :
forall (
n:
nat) (
x:
R), 0
< x -> 1
+ INR n * x <= (1
+ x) ^ n.
Lemma Power_monotonic :
forall (
x:
R) (
m n:
nat),
Rabs x > 1 -> (
m <= n)%
nat ->
Rabs (
x ^ m)
<= Rabs (
x ^ n).
Lemma RPow_abs :
forall (
x:
R) (
n:
nat),
Rabs x ^ n = Rabs (
x ^ n).
Lemma Pow_x_infinity :
forall x:
R,
Rabs x > 1 ->
forall b:
R,
exists N :
nat, (forall n:
nat, (
n >= N)%
nat ->
Rabs (
x ^ n)
>= b).
Lemma pow_ne_zero :
forall n:
nat,
n <> 0%
nat -> 0
^ n = 0.
Lemma Rinv_pow :
forall (
x:
R) (
n:
nat),
x <> 0 ->
/ x ^ n = (/ x) ^ n.
Lemma pow_lt_1_zero :
forall x:
R,
Rabs x < 1 ->
forall y:
R,
0
< y ->
exists N :
nat, (forall n:
nat, (
n >= N)%
nat ->
Rabs (
x ^ n)
< y).
Lemma pow_R1 :
forall (
r:
R) (
n:
nat),
r ^ n = 1 ->
Rabs r = 1
\/ n = 0%
nat.
Lemma pow_Rsqr :
forall (
x:
R) (
n:
nat),
x ^ (2
* n) = Rsqr x ^ n.
Lemma pow_le :
forall (
a:
R) (
n:
nat), 0
<= a -> 0
<= a ^ n.
Lemma pow_1_even :
forall n:
nat,
(-1
) ^ (2
* n) = 1.
Lemma pow_1_odd :
forall n:
nat,
(-1
) ^ S (2
* n)
= -1.
Lemma pow_1_abs :
forall n:
nat,
Rabs (
(-1
) ^ n)
= 1.
Lemma pow_mult :
forall (
x:
R) (
n1 n2:
nat),
x ^ (n1 * n2) = (x ^ n1) ^ n2.
Lemma pow_incr :
forall (
x y:
R) (
n:
nat), 0
<= x <= y ->
x ^ n <= y ^ n.
Lemma pow_R1_Rle :
forall (
x:
R) (
k:
nat), 1
<= x -> 1
<= x ^ k.
Lemma Rle_pow :
forall (
x:
R) (
m n:
nat), 1
<= x -> (
m <= n)%
nat ->
x ^ m <= x ^ n.
Lemma pow1 :
forall n:
nat, 1
^ n = 1.
Lemma pow_Rabs :
forall (
x:
R) (
n:
nat),
x ^ n <= Rabs x ^ n.
Lemma pow_maj_Rabs :
forall (
x y:
R) (
n:
nat),
Rabs y <= x ->
y ^ n <= x ^ n.
Ltac case_eq name :=
generalize (
eq_refl name);
pattern name at -1;
case name.
Definition powerRZ (
x:
R) (
n:
Z) :=
match n with
|
Z0 => 1
|
Zpos p =>
x ^ Pos.to_nat p
|
Zneg p =>
/ x ^ Pos.to_nat p
end.
Local Infix "^Z" :=
powerRZ (
at level 30,
right associativity) :
R_scope.
Lemma Zpower_NR0 :
forall (
x:
Z) (
n:
nat), (0
<= x)%
Z -> (0
<= Zpower_nat x n)%
Z.
Lemma powerRZ_O :
forall x:
R,
x ^Z 0
= 1.
Lemma powerRZ_1 :
forall x:
R,
x ^Z Z.succ 0
= x.
Lemma powerRZ_NOR :
forall (
x:
R) (
z:
Z),
x <> 0 ->
x ^Z z <> 0.
Lemma powerRZ_pos_sub (
x:
R) (
n m:
positive) :
x <> 0 ->
x ^Z (Z.pos_sub n m) = x ^ Pos.to_nat n * / x ^ Pos.to_nat m.
Lemma powerRZ_add :
forall (
x:
R) (
n m:
Z),
x <> 0 ->
x ^Z (n + m) = x ^Z n * x ^Z m.
Hint Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add:
real.
Lemma Zpower_nat_powerRZ :
forall n m:
nat,
IZR (
Zpower_nat (
Z.of_nat n)
m)
= INR n ^Z Z.of_nat m.
Lemma Zpower_pos_powerRZ :
forall n m,
IZR (
Z.pow_pos n m)
= IZR n ^Z Zpos m.
Lemma powerRZ_lt :
forall (
x:
R) (
z:
Z), 0
< x -> 0
< x ^Z z.
Hint Resolve powerRZ_lt:
real.
Lemma powerRZ_le :
forall (
x:
R) (
z:
Z), 0
< x -> 0
<= x ^Z z.
Hint Resolve powerRZ_le:
real.
Lemma Zpower_nat_powerRZ_absolu :
forall n m:
Z, (0
<= m)%
Z ->
IZR (
Zpower_nat n (
Z.abs_nat m))
= IZR n ^Z m.
Lemma powerRZ_R1 :
forall n:
Z, 1
^Z n = 1.
Definition decimal_exp (
r:
R) (
z:
Z) :
R := (
r * 10
^Z z).
Compatibility with previous versions