Require Export Reals.

Delimit Scope Rseq_scope with Rseq.

Open Local Scope R_scope.
Open Local Scope Rseq_scope.

Definition Rseq := nat → R.

Bind Scope Rseq_scope with Rseq.

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

Definition Rseq_constant r := (fun n ⇒ r).

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 p ⇒ Vn (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.

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

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

Definition Rseq_eventually (P : Rseq → Prop) (Un : Rseq) :=
  ∃ N, P (Rseq_shifts Un N).

Definition Rseq_eventually2 (P : Rseq → Rseq → Prop) (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.

Definition Rseq_cv Un l :=
  ∀ eps,
    eps > 0 →
    ∃ N, (∀ n, (n ≥ N)%nat → R_dist (Un n) l < eps).

Definition Rseq_cv_pos_infty Un :=
  ∀ M,
    ∃ N, ∀ n, (n ≥ N)%nat → M < Un n.

Definition Rseq_cv_neg_infty Un :=
  ∀ M,
    ∃ N, ∀ n, (n ≥ N)%nat → Un n < M.

Definition Rseq_big_O Un Vn :=
  ∃ K, K ≥ 0 ∧ ∃ N, ∀ n, (n ≥ N)%nat → Rabs (Un n) ≤ K × Rabs (Vn n).

Definition Rseq_little_O Un Vn :=
  ∀ eps, eps > 0 → ∃ N, ∀ n, (n ≥ N)%nat → Rabs (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.

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.