Require Import Cbase.
Require Import Cfunctions.
Require Import Csequence.
Require Import Canalysis_def.

Delimit Scope CFseq_scope with Cseq_scope.

Open Local Scope C_scope.
Open Local Scope CFseq_scope.

Implicit Type n : nat.
Implicit Type fn gn : nat → C → C.
Implicit Type f g : C → C.

Definition CFseq_plus fn gn n := (fn n + gn n)%F.
Definition CFseq_mult fn gn n := (fn n × gn n)%F.
Definition CFseq_opp fn n := (fun x ⇒ Copp (fn n x))%F.
Definition CFseq_inv fn n := (fun x ⇒ Cinv (fn n x))%F.

Infix "+" := CFseq_plus : CFseq_scope.
Infix "×" := CFseq_mult : CFseq_scope.
Notation "- u" := (CFseq_opp u) : CFseq_scope.
Notation "/ u" := (CFseq_inv u) : CFseq_scope.

Definition CFseq_minus fn gn n := (fn n - gn n)%F.
Definition CFseq_div fn gn n := (fn n / gn n)%F.

Infix "-" := CFseq_minus : CFseq_scope.
Infix "/" := CFseq_div : CFseq_scope.

Definition CFseq_cv fn f := ∀ x, Cseq_cv (fun n ⇒ fn n x) (f x).
Definition CFseq_cv_boule fn f (c : C) (r : posreal) := ∀ x, Boule c r x → Cseq_cv (fun n ⇒ fn n x) (f x).

Definition CFseq_cvu fn f (x : C) (r : posreal) := ∀ eps : R, 0 < eps →
        ∃ N : nat, ∀ n (y : C), (N ≤ n)%nat → Boule x r y →
        C_dist (fn n y) (f y) < eps.

Definition CFpartial_sum (fn : nat → C) N := sum_f_C0 fn N.