Library Coqtail.Complex.Cpser_def


Require Import Csequence_def.
Require Import Cpow.

Local Open Scope C_scope.
Local Open Scope Cseq_scope.

Definitions

General term of a Power Serie and its absolute value
Definition gt_pser An z := Cseq_mult An (Cpow z).
Definition gt_norm_pser An z := | gt_pser An z |.

Formal derivative
Definition An_deriv An := Cseq_shift (INC × An).
Definition gt_deriv_pser An z := gt_pser (An_deriv An) z.

Definition Cpser An z l := Cseq_cv (Cseq_sum (gt_pser An z)) l.
Definition Cpser_norm An z l := Cseq_cv (Cseq_sum (gt_norm_pser An z)) l.

Lower bound on the cv radius

Definition Cv_radius_weak An r := has_ub (gt_norm_pser An (IRC r)).

Cv radius definition

Definition finite_cv_radius An r :=
    (∀ r', 0 ≤ r' < r → Cv_radius_weak An r') ∧
    (∀ r', r < r' → ¬ (Cv_radius_weak An r')).

Definition infinite_cv_radius An := ∀ r, Cv_radius_weak An r.

Ltac unfold_gt := unfold gt_norm_pser, gt_pser, Cseq_norm, Cseq_mult.