The Coq Proof Assistant

# Library Coq.Reals.Rfunctions

Definition of the sum functions
Require Export ArithRing.
Require Import Rdefinitions Raxioms RIneq.
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 Zpower.
Require Import Ztac.
Local Open Scope nat_scope.
Local Open Scope R_scope.

# Lemmas about factorial

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 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.
#[global]
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.
#[global]
Hint Resolve pow_lt: real.
Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.
#[global]
Hint Resolve Rlt_pow_R1: real.
Lemma Rlt_pow : forall (x:R) (n m:nat), 1 < x -> (n < m)%nat -> x ^ n < x ^ m.
#[global]
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 pow_inv x n : (/ x)^n = / x^n.
Lemma Rinv_pow_depr : forall (x:R) (n:nat), x <> 0 -> / x ^ n = (/ x) ^ n.
#[deprecated(since="8.16",note="Use pow_inv.")]
Notation Rinv_pow := Rinv_pow_depr.
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.

# PowerRZ

Section PowerRZ.
Local Coercion Z_of_nat : nat >-> Z.
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.
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.
#[local]
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.
#[local]
Hint Resolve powerRZ_lt: real.
Lemma powerRZ_le : forall (x:R) (z:Z), 0 < x -> 0 <= x ^Z z.
#[local]
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 : powerRZ (/ x) alpha = Rinv (powerRZ x alpha).
Lemma powerRZ_inv_depr x alpha : (x <> 0)%R -> powerRZ (/ x) alpha = Rinv (powerRZ x alpha).
Lemma powerRZ_neg' x : forall alpha, powerRZ x (- alpha) = Rinv (powerRZ x alpha).
Lemma powerRZ_neg_depr x : forall alpha, x <> R0 -> powerRZ x (- alpha) = powerRZ (/ x) alpha.
Lemma powerRZ_mult m x y : (powerRZ (x*y) m = powerRZ x m * powerRZ y m)%R.
Lemma powerRZ_mult_distr_depr :
forall m x y, ((0 <= m)%Z \/ (x * y <> 0)%R) ->
(powerRZ (x*y) m = powerRZ x m * powerRZ y m)%R.
End PowerRZ.
#[deprecated(since="8.16",note="Use powerRZ_inv'.")]
Notation powerRZ_inv := powerRZ_inv_depr.
#[deprecated(since="8.16",note="Use powerRZ_neg' and powerRZ_inv'.")]
Notation powerRZ_neg := powerRZ_neg_depr.
#[deprecated(since="8.16",note="Use powerRZ_mult.")]
Notation powerRZ_mult_distr := powerRZ_mult_distr_depr.
Local Infix "^Z" := powerRZ (at level 30, right associativity) : R_scope.
Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z).

# Sum of n first naturals

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 Rdist (x y:R) : R := Rabs (x - y).
Lemma Rdist_pos : forall x y:R, Rdist x y >= 0.
Lemma Rdist_sym : forall x y:R, Rdist x y = Rdist y x.
Lemma Rdist_refl : forall x y:R, Rdist x y = 0 <-> x = y.
Lemma Rdist_eq : forall x:R, Rdist x x = 0.
Lemma Rdist_tri : forall x y z:R, Rdist x y <= Rdist x z + Rdist z y.
Lemma Rdist_plus :
forall a b c d:R, Rdist (a + c) (b + d) <= Rdist a b + Rdist c d.
Lemma Rdist_mult_l : forall a b c,
Rdist (a * b) (a * c) = Rabs a * Rdist b c.
Notation R_dist := Rdist (only parsing).
Notation R_dist_pos := Rdist_pos (only parsing).
Notation R_dist_sym := Rdist_sym (only parsing).
Notation R_dist_refl := Rdist_refl (only parsing).
Notation R_dist_eq := Rdist_eq (only parsing).
Notation R_dist_tri := Rdist_tri (only parsing).
Notation R_dist_plus := Rdist_plus (only parsing).
Notation R_dist_mult_l := Rdist_mult_l (only parsing).

# 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 -> Rdist (sum_f_R0 s n) l < eps).
Compatibility with previous versions
Notation infinit_sum := infinite_sum (only parsing).