# Library Coqtail.Reals.Rsequence.Rsequence_def

Common definitions of real sequences.
Require Export Reals.

Delimit Scope Rseq_scope with Rseq.

Open Local Scope R_scope.
Open Local Scope Rseq_scope.

Definition Rseq := natR.

Bind Scope Rseq_scope with Rseq.

Implicit Type n : nat.
Implicit Type r : R.
Implicit Type Un Vn : Rseq.

# Morphism of functions on R to sequences.

Definition Rseq_constant r := (fun nr).

Coercion Rseq_constant : R >-> Funclass.

Definition Rseq_plus Un Vn n := Un n + Vn n.
Definition Rseq_mult Un Vn n := Un n × Vn n.
Definition Rseq_opp Un n := Ropp (Un n).
Definition Rseq_inv Un n := Rinv (Un n).
Definition Rseq_sum := sum_f_R0.
Definition Rseq_prod Un Vn n := Rseq_sum (Rseq_mult Un (fun pVn (n - p)%nat)) n.

Infix "+" := Rseq_plus : Rseq_scope.
Infix "×" := Rseq_mult : Rseq_scope.
Infix "#" := Rseq_prod (at level 65) : Rseq_scope.
Notation "- u" := (Rseq_opp u) : Rseq_scope.
Notation "/ u" := (Rseq_inv u) : Rseq_scope.

Definition Rseq_minus Un Vn n := Un n - Vn n.
Definition Rseq_div Un Vn n := Un n / Vn n.
Definition Rseq_abs Un n := Rabs (Un n).

Notation "'|' Un '|'" := (Rseq_abs Un) (at level 39, format "'|' Un '|'") : Rseq_scope.
Infix "-" := Rseq_minus : Rseq_scope.
Infix "/" := Rseq_div : Rseq_scope.

Definition Rseq_shift Un n := Un (S n).
Definition Rseq_shifts Un N n := Un (N + n)%nat.

Lemma n_modulo_2 : n:nat, {p | (n = 2 × p)%nat} + {p | n = S (2 × p)}.
Proof.
intro n ; induction n.
left ; O ; intuition.
case IHn ; intro H ; destruct H as (p,Hp) ;
[right ; p | left ; (S p)] ; intuition.
Qed.

Definition Rseq_zip Un Vn n := match n_modulo_2 n with
| inl (exist p _) ⇒ Un p
| inr (exist p _) ⇒ Vn p
end.

# Extensionnal equality.

Definition Rseq_eq (Un Vn : Rseq) := n, Un n = Vn n.

Infix "==" := Rseq_eq (at level 70, no associativity) : Rseq_scope.

# Various properties.

Definition Rseq_eventually (P : RseqProp) (Un : Rseq) :=
N, P (Rseq_shifts Un N).

Definition Rseq_eventually2 (P : RseqRseqProp) (Un Vn : Rseq) :=
N, P (Rseq_shifts Un N) (Rseq_shifts Vn N).

Definition Rseq_neq_0 Un := n, Un n 0.

Definition Rseq_growing Un := n, Un n Un (S n).

Definition Rseq_strictly_growing Un := n, Un n < Un (S n).

Definition Rseq_decreasing Un := n, Un (S n) Un n.

Definition Rseq_strictly_decreasing Un := n, Un (S n) < Un n.

Definition Rseq_bound_max Un M := n, Un n M.

Definition Rseq_bound_min Un m := n, m Un n.

Definition Rseq_bound Un M := n, Rabs (Un n) M.

Definition Rseq_le Un Vn := n, Un n Vn n.

# Convergence of sequences.

Definition Rseq_cv Un l :=
eps,
eps > 0 →
N, ( n, (n N)%natR_dist (Un n) l < eps).

Definition Rseq_cv_pos_infty Un :=
M,
N, n, (n N)%natM < Un n.

Definition Rseq_cv_neg_infty Un :=
M,
N, n, (n N)%natUn n < M.

# Landau relations on sequences.

Definition Rseq_big_O Un Vn :=
K, K 0 N, n, (n N)%natRabs (Un n) K × Rabs (Vn n).

Definition Rseq_little_O Un Vn :=
eps, eps > 0 → N, n, (n N)%natRabs (Un n) eps × Rabs (Vn n).

Definition Rseq_equiv Un Vn := Rseq_little_O (Un - Vn) Un.

Notation "Un = 'O' ( Vn )" := (Rseq_big_O Un Vn) (at level 39, format "Un = 'O' ( Vn )") : Rseq_scope.
Notation "Un = 'o' ( Vn )" := (Rseq_little_O Un Vn) (at level 40, format "Un = 'o' ( Vn )") : Rseq_scope.
Notation "Un ~ Vn" := (Rseq_equiv Un Vn) (at level 5) : Rseq_scope.

# Usual sequences.

Definition Rseq_poly d n := (INR n) ^ d.

Definition Rseq_inv_poly d n :=
match n with
| 0 ⇒ 0
| _(/ INR n) ^ d
end.

Definition Rseq_pow r n := r ^ n.

Definition Rseq_alt := Rseq_mult (Rseq_pow (- 1)).
Definition Rseq_fact n := INR (fact n).

Create HintDb Rseq.