Library Coq.Reals.SeqSeries

Require Import Rbase.
Require Import Rfunctions.
Require Export Rseries.
Require Export SeqProp.
Require Export Rcomplete.
Require Export PartSum.
Require Export AltSeries.
Require Export Binomial.
Require Export Rsigma.
Require Export Rprod.
Require Export Cauchy_prod.
Require Export Alembert.
Require Import Lra.
Local Open Scope R_scope.

Lemma sum_maj1 :
  forall (fn:nat -> R -> R) (An:nat -> R) (x l1 l2:R)
    (N:nat),
    Un_cv (fun n:nat => SP fn n x) l1 ->
    Un_cv (fun n:nat => sum_f_R0 An n) l2 ->
    (forall n:nat, Rabs (fn n x) <= An n) ->
    Rabs (l1 - SP fn N x) <= l2 - sum_f_R0 An N.

Lemma Rseries_CV_comp :
  forall An Bn:nat -> R,
    (forall n:nat, 0 <= An n <= Bn n) ->
    { l:R | Un_cv (fun N:nat => sum_f_R0 Bn N) l } ->
    { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }.

Lemma Cesaro :
  forall (An Bn:nat -> R) (l:R),
    Un_cv Bn l ->
    (forall n:nat, 0 < An n) ->
    cv_infty (fun n:nat => sum_f_R0 An n) ->
    Un_cv (fun n:nat => sum_f_R0 (fun k:nat => An k * Bn k) n / sum_f_R0 An n)
    l.

Lemma Cesaro_1 :
  forall (An:nat -> R) (l:R),
    Un_cv An l -> Un_cv (fun n:nat => sum_f_R0 An (pred n) / INR n) l.