Library Coq.Reals.SeqSeries
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
Max
.
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
.
Open
Local
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
.
Comparaison of convergence for series
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
}.
Cesaro's theorem
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
.