Library Coq.Reals.Abstract.ConstructiveLimits
Require
Import
QArith
Qabs
.
Require
Import
ConstructiveReals
.
Require
Import
ConstructiveAbs
.
Local Open
Scope
ConstructiveReals
.
Definitions and basic properties of limits of real sequences and series.
WARNING: this file is experimental and likely to change in future releases.
Lemma
CR_cv_extens
:
forall
{
R
:
ConstructiveReals
} (
xn
yn
:
nat
->
CRcarrier
R
) (
l
:
CRcarrier
R
),
(
forall
n
:
nat
,
xn
n
==
yn
n
)
->
CR_cv
R
xn
l
->
CR_cv
R
yn
l
.
Lemma
CR_cv_opp
:
forall
{
R
:
ConstructiveReals
} (
xn
:
nat
->
CRcarrier
R
) (
l
:
CRcarrier
R
),
CR_cv
R
xn
l
->
CR_cv
R
(
fun
n
=>
-
xn
n
) (
-
l
).
Lemma
CR_cv_plus
:
forall
{
R
:
ConstructiveReals
} (
xn
yn
:
nat
->
CRcarrier
R
) (
a
b
:
CRcarrier
R
),
CR_cv
R
xn
a
->
CR_cv
R
yn
b
->
CR_cv
R
(
fun
n
=>
xn
n
+
yn
n
) (
a
+
b
).
Lemma
CR_cv_unique
:
forall
{
R
:
ConstructiveReals
} (
xn
:
nat
->
CRcarrier
R
)
(
a
b
:
CRcarrier
R
),
CR_cv
R
xn
a
->
CR_cv
R
xn
b
->
a
==
b
.
Lemma
CR_cv_eq
:
forall
{
R
:
ConstructiveReals
}
(
v
u
:
nat
->
CRcarrier
R
) (
s
:
CRcarrier
R
),
(
forall
n
:
nat
,
u
n
==
v
n
)
->
CR_cv
R
u
s
->
CR_cv
R
v
s
.
Lemma
CR_cauchy_eq
:
forall
{
R
:
ConstructiveReals
}
(
un
vn
:
nat
->
CRcarrier
R
),
(
forall
n
:
nat
,
un
n
==
vn
n
)
->
CR_cauchy
R
un
->
CR_cauchy
R
vn
.
Lemma
CR_cv_proper
:
forall
{
R
:
ConstructiveReals
}
(
un
:
nat
->
CRcarrier
R
) (
a
b
:
CRcarrier
R
),
CR_cv
R
un
a
->
a
==
b
->
CR_cv
R
un
b
.
Instance
CR_cv_morph
:
forall
{
R
:
ConstructiveReals
} (
un
:
nat
->
CRcarrier
R
),
CMorphisms.Proper
(
CMorphisms.respectful
(
CReq
R
)
CRelationClasses.iffT
) (
CR_cv
R
un
).
Lemma
Un_cv_nat_real
:
forall
{
R
:
ConstructiveReals
}
(
un
:
nat
->
CRcarrier
R
) (
l
:
CRcarrier
R
),
CR_cv
R
un
l
->
forall
eps
:
CRcarrier
R
,
0
<
eps
->
{
p
:
nat
&
forall
i
:
nat
,
le
p
i
->
CRabs
R
(
un
i
-
l
)
<
eps
}
.
Lemma
Un_cv_real_nat
:
forall
{
R
:
ConstructiveReals
}
(
un
:
nat
->
CRcarrier
R
) (
l
:
CRcarrier
R
),
(
forall
eps
:
CRcarrier
R
,
0
<
eps
->
{
p
:
nat
&
forall
i
:
nat
,
le
p
i
->
CRabs
R
(
un
i
-
l
)
<
eps
}
)
->
CR_cv
R
un
l
.
Lemma
CR_cv_minus
:
forall
{
R
:
ConstructiveReals
}
(
An
Bn
:
nat
->
CRcarrier
R
) (
l1
l2
:
CRcarrier
R
),
CR_cv
R
An
l1
->
CR_cv
R
Bn
l2
->
CR_cv
R
(
fun
i
:
nat
=>
An
i
-
Bn
i
) (
l1
-
l2
).
Lemma
CR_cv_nonneg
:
forall
{
R
:
ConstructiveReals
} (
An
:
nat
->
CRcarrier
R
) (
l
:
CRcarrier
R
),
CR_cv
R
An
l
->
(
forall
n
:
nat
, 0
<=
An
n
)
->
0
<=
l
.
Lemma
CR_cv_scale
:
forall
{
R
:
ConstructiveReals
} (
u
:
nat
->
CRcarrier
R
)
(
a
:
CRcarrier
R
) (
s
:
CRcarrier
R
),
CR_cv
R
u
s
->
CR_cv
R
(
fun
n
=>
u
n
*
a
) (
s
*
a
).
Lemma
CR_cv_const
:
forall
{
R
:
ConstructiveReals
} (
a
:
CRcarrier
R
),
CR_cv
R
(
fun
n
=>
a
)
a
.
Lemma
Rcv_cauchy_mod
:
forall
{
R
:
ConstructiveReals
}
(
un
:
nat
->
CRcarrier
R
) (
l
:
CRcarrier
R
),
CR_cv
R
un
l
->
CR_cauchy
R
un
.
Lemma
CR_growing_transit
:
forall
{
R
:
ConstructiveReals
} (
un
:
nat
->
CRcarrier
R
),
(
forall
n
:
nat
,
un
n
<=
un
(
S
n
)
)
->
forall
n
p
:
nat
,
le
n
p
->
un
n
<=
un
p
.
Lemma
growing_ineq
:
forall
{
R
:
ConstructiveReals
} (
Un
:
nat
->
CRcarrier
R
) (
l
:
CRcarrier
R
),
(
forall
n
:
nat
,
Un
n
<=
Un
(
S
n
)
)
->
CR_cv
R
Un
l
->
forall
n
:
nat
,
Un
n
<=
l
.
Lemma
CR_cv_open_below
:
forall
{
R
:
ConstructiveReals
}
(
un
:
nat
->
CRcarrier
R
) (
m
l
:
CRcarrier
R
),
CR_cv
R
un
l
->
m
<
l
->
{
n
:
nat
&
forall
i
:
nat
,
le
n
i
->
m
<
un
i
}
.
Lemma
CR_cv_open_above
:
forall
{
R
:
ConstructiveReals
}
(
un
:
nat
->
CRcarrier
R
) (
m
l
:
CRcarrier
R
),
CR_cv
R
un
l
->
l
<
m
->
{
n
:
nat
&
forall
i
:
nat
,
le
n
i
->
un
i
<
m
}
.
Lemma
CR_cv_bound_down
:
forall
{
R
:
ConstructiveReals
}
(
u
:
nat
->
CRcarrier
R
) (
A
l
:
CRcarrier
R
) (
N
:
nat
),
(
forall
n
:
nat
,
le
N
n
->
A
<=
u
n
)
->
CR_cv
R
u
l
->
A
<=
l
.
Lemma
CR_cv_bound_up
:
forall
{
R
:
ConstructiveReals
}
(
u
:
nat
->
CRcarrier
R
) (
A
l
:
CRcarrier
R
) (
N
:
nat
),
(
forall
n
:
nat
,
le
N
n
->
u
n
<=
A
)
->
CR_cv
R
u
l
->
l
<=
A
.
Lemma
CR_cv_le
:
forall
{
R
:
ConstructiveReals
}
(
u
v
:
nat
->
CRcarrier
R
) (
a
b
:
CRcarrier
R
),
(
forall
n
:
nat
,
u
n
<=
v
n
)
->
CR_cv
R
u
a
->
CR_cv
R
v
b
->
a
<=
b
.
Lemma
CR_cv_abs_cont
:
forall
{
R
:
ConstructiveReals
}
(
u
:
nat
->
CRcarrier
R
) (
s
:
CRcarrier
R
),
CR_cv
R
u
s
->
CR_cv
R
(
fun
n
=>
CRabs
R
(
u
n
)) (
CRabs
R
s
).
Lemma
CR_cv_dist_cont
:
forall
{
R
:
ConstructiveReals
}
(
u
:
nat
->
CRcarrier
R
) (
a
s
:
CRcarrier
R
),
CR_cv
R
u
s
->
CR_cv
R
(
fun
n
=>
CRabs
R
(
a
-
u
n
)) (
CRabs
R
(
a
-
s
)).
Lemma
CR_cv_shift
:
forall
{
R
:
ConstructiveReals
}
f
k
l
,
CR_cv
R
(
fun
n
=>
f
(
n
+
k
)%
nat
)
l
->
CR_cv
R
f
l
.
Lemma
CR_cv_shift'
:
forall
{
R
:
ConstructiveReals
}
f
k
l
,
CR_cv
R
f
l
->
CR_cv
R
(
fun
n
=>
f
(
n
+
k
)%
nat
)
l
.