Library Coqtail.Reals.Rpser.Rpser_def


Require Export MyReals.
Require Import Rsequence_def.

Local Open Scope Rseq_scope.

Definitions

General term of a Power Serie and its absolute value

Definition gt_pser An x := An × (pow x).
Definition gt_abs_pser An x := | gt_pser An x |.

Formal derivative.

Definition An_deriv An := Rseq_shift (INR × An).
Definition An_nth_deriv An k := Rseq_shifts (Rseq_fact × An) k / Rseq_fact.
Definition An_expand An l := (Rseq_pow l × An).

Definition gt_deriv_Pser An x := gt_pser (An_deriv An) x.
Definition gt_nth_deriv_Pser An k x := gt_pser (An_nth_deriv An k) x.

Partial sums and convergence predicates.

Definition Rseq_pps An x := Rseq_sum (gt_pser An x).
Definition Rseq_pps_abs An x := Rseq_sum (gt_abs_pser An x).
Definition Rpser An x l := Rseq_cv (Rseq_pps An x) l.
Definition Rpser_abs An x l := Rseq_cv (Rseq_pps_abs An x) l.

Lower bound on the cv radius

Definition Cv_radius_weak An r := has_ub (gt_abs_pser An 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.