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 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 (
refl_equal name);
pattern name at -1
in |- *;
case name.
Definition powerRZ (
x:R) (
n:Z) :=
match n with
|
Z0 => 1
|
Zpos p =>
x ^
nat_of_P p
|
Zneg p => /
x ^
nat_of_P p
end.
Infix Local "^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
Zsucc 0 =
x.
Lemma powerRZ_NOR :
forall (
x:R) (
z:Z),
x <> 0 ->
x ^Z
z <> 0.
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 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 (
Zabs_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).
Definition infinite_sum (
s:nat ->
R) (
l:R) :
Prop :=
forall eps:R,
eps > 0 ->
exists N :
nat,
(
forall n:nat, (
n >=
N)%nat ->
R_dist (
sum_f_R0 s n)
l <
eps).
Compatibility with previous versions