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.
Lemma Rsqr_pow2 :
forall x,
Rsqr x = x ^ 2.
Section PowerRZ.
Section Z_compl.
Local Open Scope Z_scope.
Inductive Z_spec (
x :
Z) :
Z -> Type :=
|
ZintNull :
x = 0
-> Z_spec x 0
|
ZintPos (
n :
nat) :
x = n -> Z_spec x n
|
ZintNeg (
n :
nat) :
x = - n -> Z_spec x (
- n).
Lemma intP (
x :
Z) :
Z_spec x x.
End Z_compl.
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.
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.
Local Open Scope Z_scope.
Lemma pow_powerRZ (
r :
R) (
n :
nat) :
(
r ^ n)%
R = powerRZ r (
Z_of_nat n).
Lemma powerRZ_ind (
P :
Z -> R -> R -> Prop) :
(forall x,
P 0
x 1%
R) ->
(forall x n,
P (
Z.of_nat n)
x (
x ^ n)%
R) ->
(forall x n,
P ((
-(Z.of_nat n))%
Z)
x (
Rinv (
x ^ n))
) ->
forall x (
m :
Z),
P m x (
powerRZ x m)%
R.
Lemma powerRZ_inv x alpha : (
x <> 0)%
R -> powerRZ (
/ x)
alpha = Rinv (
powerRZ x alpha).
Lemma powerRZ_neg x :
forall alpha,
x <> R0 -> powerRZ x (
- alpha)
= powerRZ (
/ x)
alpha.
Lemma powerRZ_mult_distr :
forall m x y,
((0
<= m)%
Z \/ (
x * y <> 0)%
R) ->
(
powerRZ (
x*y)
m = powerRZ x m * powerRZ y m)%
R.
End PowerRZ.
Definition decimal_exp (
r:
R) (
z:
Z) :
R := (
r * 10
^Z z).
Compatibility with previous versions