Require Export Complex.
Require Export Csequence.
Require Import Rsequence_def.
Open Local Scope C_scope.
Open Local Scope Cseq_scope.

Definition Cser_cv Un l := Cseq_cv (sum_f_C0 Un) l.

Definition Cser_abs_cv Un l := Rseq_cv (sum_f_R0 (fun n ⇒ Cnorm (Un n))) l.

Definition Cser_cv_infty Un := Rseq_cv_pos_infty (sum_f_R0 (fun n ⇒ Cnorm (Un n))).

Definition Cser_bound Un M := ∀ n, Cnorm (sum_f_C0 Un n) ≤ M.

Definition Cser_abs_bound Un M := ∀ n, sum_f_R0 (fun k ⇒ Cnorm (Un k)) n ≤ M.

Definition Cser_rem (Un : nat → R) (l : R) (Hcv : Cser_cv Un l) (n : nat) :=
 (l - (sum_f_C0 Un n))%C.