Library Stdlib.Reals.SeqSeries

From Stdlib Require Import Rbase.
From Stdlib Require Import Rfunctions.
From Stdlib Require Export Rseries.
From Stdlib Require Export SeqProp.
From Stdlib Require Export Rcomplete.
From Stdlib Require Export PartSum.
From Stdlib Require Export AltSeries.
From Stdlib Require Export Binomial.
From Stdlib Require Export Rsigma.
From Stdlib Require Export Rprod.
From Stdlib Require Export Cauchy_prod.
From Stdlib Require Export Alembert.
From Stdlib Require Import Lra.
From Stdlib Require Import Compare_dec.
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.