# Library Coq.Reals.Rfunctions

Definition of the sum functions
Require Export ArithRing.

Require Import Rbase.
Require Export Rpow_def.
Require Export R_Ifp.
Require Export Rbasic_fun.
Require Export R_sqr.
Require Export SplitAbsolu.
Require Export SplitRmult.
Require Export ArithProp.
Require Import Omega.
Require Import Zpower.
Open Local Scope nat_scope.
Open Local Scope R_scope.

Lemma INR_fact_neq_0 : forall n:nat, INR (fact n) <> 0.

Lemma fact_simpl : forall n:nat, fact (S n) = (S n * fact n)%nat.

Lemma simpl_fact :
forall n:nat, / INR (fact (S n)) * / / INR (fact n) = / INR (S n).

# Power

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.

# PowerRZ

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.

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 (Zpower_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 (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).

# Sum of n first naturals

Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) : nat :=
match n with
| O => f 0%nat
| S n' => (sum_nat_f_O f n' + f (S n'))%nat
end.

Definition sum_nat_f (s n:nat) (f:nat -> nat) : nat :=
sum_nat_f_O (fun x:nat => f (x + s)%nat) (n - s).

Definition sum_nat_O (n:nat) : nat := sum_nat_f_O (fun x:nat => x) n.

Definition sum_nat (s n:nat) : nat := sum_nat_f s n (fun x:nat => x).

# Sum

Fixpoint sum_f_R0 (f:nat -> R) (N:nat) : R :=
match N with
| O => f 0%nat
| S i => sum_f_R0 f i + f (S i)
end.

Definition sum_f (s n:nat) (f:nat -> R) : R :=
sum_f_R0 (fun x:nat => f (x + s)%nat) (n - s).

Lemma GP_finite :
forall (x:R) (n:nat),
sum_f_R0 (fun n:nat => x ^ n) n * (x - 1) = x ^ (n + 1) - 1.

Lemma sum_f_R0_triangle :
forall (x:nat -> R) (n:nat),
Rabs (sum_f_R0 x n) <= sum_f_R0 (fun i:nat => Rabs (x i)) n.

# Distance in R

Definition R_dist (x y:R) : R := Rabs (x - y).

Lemma R_dist_pos : forall x y:R, R_dist x y >= 0.

Lemma R_dist_sym : forall x y:R, R_dist x y = R_dist y x.

Lemma R_dist_refl : forall x y:R, R_dist x y = 0 <-> x = y.

Lemma R_dist_eq : forall x:R, R_dist x x = 0.

Lemma R_dist_tri : forall x y z:R, R_dist x y <= R_dist x z + R_dist z y.

Lemma R_dist_plus :
forall a b c d:R, R_dist (a + c) (b + d) <= R_dist a b + R_dist c d.

# Infinite Sum

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
Notation infinit_sum := infinite_sum (only parsing).