Require Export Cbase Cfunctions.

Delimit Scope Cseq_scope with Cseq.

Open Local Scope C_scope.
Open Local Scope Cseq_scope.

Definition Cseq := nat → C.

Implicit Type n : nat.
Implicit Type z : C.
Implicit Type An Bn : Cseq.

Definition Cseq_constant z := (fun n ⇒ z).

Coercion Cseq_constant : C >-> Funclass.

Definition Cseq_add An Bn n := An n + Bn n.
Definition Cseq_mult An Bn n := An n × Bn n.
Definition Cseq_opp An n := Copp (An n).
Definition Cseq_inv An n := Cinv (An n).
Definition Cseq_sum := sum_f_C0.

Infix "+" := Cseq_add : Cseq_scope.
Infix "×" := Cseq_mult : Cseq_scope.
Notation "- u" := (Cseq_opp u) : Cseq_scope.
Notation "/ u" := (Cseq_inv u) : Cseq_scope.

Definition Cseq_minus An Bn n := An n - Bn n.
Definition Cseq_div An Bn n := An n / Bn n.
Definition Cseq_norm An n := Cnorm (An n).

Notation "'|' An '|'" := (Cseq_norm An) (at level 39, format "'|' An '|'") : Cseq_scope.
Infix "-" := Cseq_minus : Cseq_scope.
Infix "/" := Cseq_div : Cseq_scope.

Definition Cseq_shift An n := An (S n).
Definition Cseq_shifts An N n := An (N + n)%nat.

Definition Cseq_eventually (P : Cseq → Prop) (Un : Cseq) :=
  ∃ N, P (fun n ⇒ Un (N + n)%nat).

Definition Cseq_eventually2 (P : Cseq → Cseq → Prop) (Un Vn : Cseq) :=
  ∃ N, P (fun n ⇒ Un (N + n)%nat) (fun n ⇒ Vn (N + n)%nat).

Definition Cseq_neq_0 Un := ∀ n, Un n ≠ 0.

Definition Cseq_bound (Un:Cseq) (M:R) := ∀ n, Cnorm (Un n) ≤ M.

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

Definition Cauchy_crit (Un : nat → C) := ∀ eps : R,
 eps > 0 → ∃ N : nat, ∀ n (m : nat),
 (n ≥ N)%nat → (m ≥ N)%nat → Cnorm (Un n - Un m) < eps.