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
.
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
.
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
.