Library Coqtail.Reals.Rseries.Rseries_def

Common definitions of real series, based on real sequences definitions.

Require Import Reals.
Require Import Rsequence_def.
Open Local Scope R_scope.
Open Local Scope Rseq_scope.

Implicit Type Un : Rseq.

Convergence of series

Definition Rser_cv Un := Rseq_cv (Rseq_sum Un).

Definition Rser_abs_cv Un := Rseq_cv (Rseq_sum (|Un |)).

Definition Rser_cv_pos_infty Un := Rseq_cv_pos_infty (Rseq_sum Un).

Definition Rser_cv_neg_infty Un := Rseq_cv_neg_infty (Rseq_sum Un).

Bounds

Definition Rser_bound_max Un := Rseq_bound_max (Rseq_sum Un).
Definition Rser_bound_min Un := Rseq_bound_min (Rseq_sum Un).
Definition Rser_bound Un := Rseq_bound (Rseq_sum Un).
Definition Rser_abs_bound Un := Rseq_bound (Rseq_sum (|Un |)).

Remainders of series

Definition Rser_rem (Un : Rseq) (l : R) (Hcv : Rser_cv Un l) (n : nat) := (l - (Rseq_sum Un n ))%R.