Library Coq.Reals.Abstract.ConstructiveSum
Require
Import
QArith
Qabs
.
Require
Import
ConstructiveReals
.
Require
Import
ConstructiveRealsMorphisms
.
Require
Import
ConstructiveAbs
.
Require
Import
ConstructiveLimits
.
Local Open
Scope
ConstructiveReals
.
Definition and properties of finite sums and powers.
WARNING: this file is experimental and likely to change in future releases.
Fixpoint
CRsum
{
R
:
ConstructiveReals
}
(
f
:
nat
->
CRcarrier
R
) (
N
:
nat
) :
CRcarrier
R
:=
match
N
with
|
O
=>
f
0%
nat
|
S
i
=>
CRsum
f
i
+
f
(
S
i
)
end
.
Lemma
CRsum_eq
:
forall
{
R
:
ConstructiveReals
} (
An
Bn
:
nat
->
CRcarrier
R
) (
N
:
nat
),
(
forall
i
:
nat
, (
i
<=
N
)%
nat
->
An
i
==
Bn
i
)
->
CRsum
An
N
==
CRsum
Bn
N
.
Lemma
sum_eq_R0
:
forall
{
R
:
ConstructiveReals
} (
un
:
nat
->
CRcarrier
R
) (
n
:
nat
),
(
forall
k
:
nat
,
un
k
==
0
)
->
CRsum
un
n
==
0.
Definition
INR
{
R
:
ConstructiveReals
} (
n
:
nat
) :
CRcarrier
R
:=
CR_of_Q
R
(
Z.of_nat
n
#
1).
Lemma
sum_const
:
forall
{
R
:
ConstructiveReals
} (
a
:
CRcarrier
R
) (
n
:
nat
),
CRsum
(
fun
_
=>
a
)
n
==
a
*
INR
(
S
n
).
Lemma
multiTriangleIneg
:
forall
{
R
:
ConstructiveReals
} (
u
:
nat
->
CRcarrier
R
) (
n
:
nat
),
CRabs
R
(
CRsum
u
n
)
<=
CRsum
(
fun
k
=>
CRabs
R
(
u
k
))
n
.
Lemma
sum_assoc
:
forall
{
R
:
ConstructiveReals
} (
u
:
nat
->
CRcarrier
R
) (
n
p
:
nat
),
CRsum
u
(
S
n
+
p
)
==
CRsum
u
n
+
CRsum
(
fun
k
=>
u
(
S
n
+
k
)%
nat
)
p
.
Lemma
sum_Rle
:
forall
{
R
:
ConstructiveReals
} (
un
vn
:
nat
->
CRcarrier
R
) (
n
:
nat
),
(
forall
k
,
le
k
n
->
un
k
<=
vn
k
)
->
CRsum
un
n
<=
CRsum
vn
n
.
Lemma
Abs_sum_maj
:
forall
{
R
:
ConstructiveReals
} (
un
vn
:
nat
->
CRcarrier
R
),
(
forall
n
:
nat
,
CRabs
R
(
un
n
)
<=
(
vn
n
)
)
->
forall
n
p
:
nat
, (
CRabs
R
(
CRsum
un
n
-
CRsum
un
p
)
<=
CRsum
vn
(
Init.Nat.max
n
p
)
-
CRsum
vn
(
Init.Nat.min
n
p
)).
Lemma
cond_pos_sum
:
forall
{
R
:
ConstructiveReals
} (
un
:
nat
->
CRcarrier
R
) (
n
:
nat
),
(
forall
k
, 0
<=
un
k
)
->
0
<=
CRsum
un
n
.
Lemma
pos_sum_more
:
forall
{
R
:
ConstructiveReals
} (
u
:
nat
->
CRcarrier
R
)
(
n
p
:
nat
),
(
forall
k
:
nat
, 0
<=
u
k
)
->
le
n
p
->
CRsum
u
n
<=
CRsum
u
p
.
Lemma
sum_opp
:
forall
{
R
:
ConstructiveReals
} (
un
:
nat
->
CRcarrier
R
) (
n
:
nat
),
CRsum
(
fun
k
=>
-
un
k
)
n
==
-
CRsum
un
n
.
Lemma
sum_scale
:
forall
{
R
:
ConstructiveReals
} (
u
:
nat
->
CRcarrier
R
) (
a
:
CRcarrier
R
) (
n
:
nat
),
CRsum
(
fun
k
:
nat
=>
u
k
*
a
)
n
==
CRsum
u
n
*
a
.
Lemma
sum_plus
:
forall
{
R
:
ConstructiveReals
} (
u
v
:
nat
->
CRcarrier
R
) (
n
:
nat
),
CRsum
(
fun
n0
:
nat
=>
u
n0
+
v
n0
)
n
==
CRsum
u
n
+
CRsum
v
n
.
Lemma
decomp_sum
:
forall
{
R
:
ConstructiveReals
} (
An
:
nat
->
CRcarrier
R
) (
N
:
nat
),
(0
<
N
)%
nat
->
CRsum
An
N
==
An
0%
nat
+
CRsum
(
fun
i
:
nat
=>
An
(
S
i
)) (
pred
N
).
Lemma
reverse_sum
:
forall
{
R
:
ConstructiveReals
} (
u
:
nat
->
CRcarrier
R
) (
n
:
nat
),
CRsum
u
n
==
CRsum
(
fun
k
=>
u
(
n
-
k
)%
nat
)
n
.
Lemma
Rplus_le_pos
:
forall
{
R
:
ConstructiveReals
} (
a
b
:
CRcarrier
R
),
0
<=
b
->
a
<=
a
+
b
.
Lemma
selectOneInSum
:
forall
{
R
:
ConstructiveReals
} (
u
:
nat
->
CRcarrier
R
) (
n
i
:
nat
),
le
i
n
->
(
forall
k
:
nat
, 0
<=
u
k
)
->
u
i
<=
CRsum
u
n
.
Lemma
splitSum
:
forall
{
R
:
ConstructiveReals
} (
un
:
nat
->
CRcarrier
R
)
(
filter
:
nat
->
bool
) (
n
:
nat
),
CRsum
un
n
==
CRsum
(
fun
i
=>
if
filter
i
then
un
i
else
0)
n
+
CRsum
(
fun
i
=>
if
filter
i
then
0
else
un
i
)
n
.
Definition
series_cv
{
R
:
ConstructiveReals
}
(
un
:
nat
->
CRcarrier
R
) (
s
:
CRcarrier
R
) :
Set
:=
CR_cv
R
(
CRsum
un
)
s
.
Definition
series_cv_lim_lt
{
R
:
ConstructiveReals
}
(
un
:
nat
->
CRcarrier
R
) (
x
:
CRcarrier
R
) :
Set
:=
{
l
:
CRcarrier
R
&
prod
(
series_cv
un
l
) (
l
<
x
)
}
.
Definition
series_cv_le_lim
{
R
:
ConstructiveReals
}
(
x
:
CRcarrier
R
) (
un
:
nat
->
CRcarrier
R
) :
Set
:=
{
l
:
CRcarrier
R
&
prod
(
series_cv
un
l
) (
x
<=
l
)
}
.
Lemma
series_cv_maj
:
forall
{
R
:
ConstructiveReals
}
(
un
vn
:
nat
->
CRcarrier
R
) (
s
:
CRcarrier
R
),
(
forall
n
:
nat
,
CRabs
R
(
un
n
)
<=
vn
n
)
->
series_cv
vn
s
->
{
l
:
CRcarrier
R
&
prod
(
series_cv
un
l
) (
l
<=
s
)
}
.
Lemma
series_cv_abs_lt
:
forall
{
R
:
ConstructiveReals
} (
un
vn
:
nat
->
CRcarrier
R
) (
l
:
CRcarrier
R
),
(
forall
n
:
nat
,
CRabs
R
(
un
n
)
<=
vn
n
)
->
series_cv_lim_lt
vn
l
->
series_cv_lim_lt
un
l
.
Definition
series_cv_abs
{
R
:
ConstructiveReals
} (
u
:
nat
->
CRcarrier
R
)
:
CR_cauchy
R
(
CRsum
(
fun
n
=>
CRabs
R
(
u
n
)))
->
{
l
:
CRcarrier
R
&
series_cv
u
l
}
.
Lemma
series_cv_unique
:
forall
{
R
:
ConstructiveReals
} (
Un
:
nat
->
CRcarrier
R
) (
l1
l2
:
CRcarrier
R
),
series_cv
Un
l1
->
series_cv
Un
l2
->
l1
==
l2
.
Lemma
series_cv_abs_eq
:
forall
{
R
:
ConstructiveReals
} (
u
:
nat
->
CRcarrier
R
) (
a
:
CRcarrier
R
)
(
cau
:
CR_cauchy
R
(
CRsum
(
fun
n
=>
CRabs
R
(
u
n
)))),
series_cv
u
a
->
(
a
==
(
let
(
l
,
_
):=
series_cv_abs
u
cau
in
l
)
)%
ConstructiveReals
.
Lemma
series_cv_abs_cv
:
forall
{
R
:
ConstructiveReals
} (
u
:
nat
->
CRcarrier
R
)
(
cau
:
CR_cauchy
R
(
CRsum
(
fun
n
=>
CRabs
R
(
u
n
)))),
series_cv
u
(
let
(
l
,
_
):=
series_cv_abs
u
cau
in
l
).
Lemma
series_cv_opp
:
forall
{
R
:
ConstructiveReals
}
(
s
:
CRcarrier
R
) (
u
:
nat
->
CRcarrier
R
),
series_cv
u
s
->
series_cv
(
fun
n
=>
-
u
n
) (
-
s
).
Lemma
series_cv_scale
:
forall
{
R
:
ConstructiveReals
}
(
a
:
CRcarrier
R
) (
s
:
CRcarrier
R
) (
u
:
nat
->
CRcarrier
R
),
series_cv
u
s
->
series_cv
(
fun
n
=>
(
u
n
)
*
a
) (
s
*
a
).
Lemma
series_cv_plus
:
forall
{
R
:
ConstructiveReals
}
(
u
v
:
nat
->
CRcarrier
R
) (
s
t
:
CRcarrier
R
),
series_cv
u
s
->
series_cv
v
t
->
series_cv
(
fun
n
=>
u
n
+
v
n
) (
s
+
t
).
Lemma
series_cv_minus
:
forall
{
R
:
ConstructiveReals
}
(
u
v
:
nat
->
CRcarrier
R
) (
s
t
:
CRcarrier
R
),
series_cv
u
s
->
series_cv
v
t
->
series_cv
(
fun
n
=>
u
n
-
v
n
) (
s
-
t
).
Lemma
series_cv_nonneg
:
forall
{
R
:
ConstructiveReals
}
(
u
:
nat
->
CRcarrier
R
) (
s
:
CRcarrier
R
),
(
forall
n
:
nat
, 0
<=
u
n
)
->
series_cv
u
s
->
0
<=
s
.
Lemma
series_cv_eq
:
forall
{
R
:
ConstructiveReals
}
(
u
v
:
nat
->
CRcarrier
R
) (
s
:
CRcarrier
R
),
(
forall
n
:
nat
,
u
n
==
v
n
)
->
series_cv
u
s
->
series_cv
v
s
.
Lemma
series_cv_remainder_maj
:
forall
{
R
:
ConstructiveReals
} (
u
:
nat
->
CRcarrier
R
)
(
s
eps
:
CRcarrier
R
)
(
N
:
nat
),
series_cv
u
s
->
0
<
eps
->
(
forall
n
:
nat
, 0
<=
u
n
)
->
CRabs
R
(
CRsum
u
N
-
s
)
<=
eps
->
forall
n
:
nat
,
CRsum
(
fun
k
=>
u
(
N
+
S
k
)%
nat
)
n
<=
eps
.
Lemma
series_cv_abs_remainder
:
forall
{
R
:
ConstructiveReals
} (
u
:
nat
->
CRcarrier
R
)
(
s
sAbs
:
CRcarrier
R
)
(
n
:
nat
),
series_cv
u
s
->
series_cv
(
fun
n
=>
CRabs
R
(
u
n
))
sAbs
->
CRabs
R
(
CRsum
u
n
-
s
)
<=
sAbs
-
CRsum
(
fun
n
=>
CRabs
R
(
u
n
))
n
.
Lemma
series_cv_triangle
:
forall
{
R
:
ConstructiveReals
}
(
u
:
nat
->
CRcarrier
R
) (
s
sAbs
:
CRcarrier
R
),
series_cv
u
s
->
series_cv
(
fun
n
=>
CRabs
R
(
u
n
))
sAbs
->
CRabs
R
s
<=
sAbs
.
Lemma
series_cv_shift
:
forall
{
R
:
ConstructiveReals
} (
f
:
nat
->
CRcarrier
R
)
k
l
,
series_cv
(
fun
n
=>
f
(
S
k
+
n
)%
nat
)
l
->
series_cv
f
(
l
+
CRsum
f
k
).
Lemma
series_cv_shift'
:
forall
{
R
:
ConstructiveReals
}
(
un
:
nat
->
CRcarrier
R
) (
s
:
CRcarrier
R
) (
shift
:
nat
),
series_cv
un
s
->
series_cv
(
fun
n
=>
un
(
n
+
shift
)%
nat
)
(
s
-
match
shift
with
|
O
=> 0
|
S
p
=>
CRsum
un
p
end
).
Lemma
CRmorph_sum
:
forall
{
R1
R2
:
ConstructiveReals
}
(
f
: @
ConstructiveRealsMorphism
R1
R2
)
(
un
:
nat
->
CRcarrier
R1
) (
n
:
nat
),
CRmorph
f
(
CRsum
un
n
)
==
CRsum
(
fun
n0
:
nat
=>
CRmorph
f
(
un
n0
))
n
.
Lemma
CRmorph_INR
:
forall
{
R1
R2
:
ConstructiveReals
}
(
f
: @
ConstructiveRealsMorphism
R1
R2
)
(
n
:
nat
),
CRmorph
f
(
INR
n
)
==
INR
n
.
Lemma
CRmorph_series_cv
:
forall
{
R1
R2
:
ConstructiveReals
}
(
f
: @
ConstructiveRealsMorphism
R1
R2
)
(
un
:
nat
->
CRcarrier
R1
)
(
l
:
CRcarrier
R1
),
series_cv
un
l
->
series_cv
(
fun
n
=>
CRmorph
f
(
un
n
)) (
CRmorph
f
l
).