Library Coq.Reals.Cauchy_prod
Require
Import
Rbase
.
Require
Import
Rfunctions
.
Require
Import
Rseries
.
Require
Import
PartSum
.
Open
Local
Scope
R_scope
.
Lemma
sum_N_predN
:
forall
(
An
:nat ->
R
) (
N
:nat),
(0 <
N
)%nat ->
sum_f_R0
An
N
=
sum_f_R0
An
(
pred
N
) +
An
N
.
Lemma
sum_plus
:
forall
(
An
Bn
:nat ->
R
) (
N
:nat),
sum_f_R0
(
fun
l
:nat =>
An
l
+
Bn
l
)
N
=
sum_f_R0
An
N
+
sum_f_R0
Bn
N
.
Theorem
cauchy_finite
:
forall
(
An
Bn
:nat ->
R
) (
N
:nat),
(0 <
N
)%nat ->
sum_f_R0
An
N
*
sum_f_R0
Bn
N
=
sum_f_R0
(
fun
k
:nat =>
sum_f_R0
(
fun
p
:nat =>
An
p
*
Bn
(
k
-
p
)%nat)
k
)
N
+
sum_f_R0
(
fun
k
:nat =>
sum_f_R0
(
fun
l
:nat =>
An
(
S
(
l
+
k
)) *
Bn
(
N
-
l
)%nat)
(
pred
(
N
-
k
))) (
pred
N
).