Library Coq.Reals.Cauchy.ConstructiveRcomplete
Require
Import
QArith_base
.
Require
Import
Qabs
.
Require
Import
ConstructiveReals
.
Require
Import
ConstructiveCauchyRealsMult
.
Require
Import
Logic.ConstructiveEpsilon
.
Require
Import
ConstructiveCauchyAbs
.
Require
Import
Lia
.
Require
Import
Lqa
.
Require
Import
Qpower
.
Require
Import
QExtra
.
Require
Import
PosExtra
.
Require
Import
ConstructiveExtra
.
Proof that Cauchy reals are Cauchy-complete.
WARNING: this file is experimental and likely to change in future releases.
Local Open
Scope
CReal_scope
.
Definition
seq_cv
(
un
:
nat
->
CReal
) (
l
:
CReal
) :
Set
:=
forall
p
:
positive
,
{
n
:
nat
|
forall
i
:
nat
,
le
n
i
->
CReal_abs
(
un
i
-
l
)
<=
inject_Q
(1
#
p
)
}
.
Definition
Un_cauchy_mod
(
un
:
nat
->
CReal
) :
Set
:=
forall
p
:
positive
,
{
n
:
nat
|
forall
i
j
:
nat
,
le
n
i
->
le
n
j
->
CReal_abs
(
un
i
-
un
j
)
<=
inject_Q
(1
#
p
)
}
.
Lemma
seq_cv_proper
:
forall
(
un
:
nat
->
CReal
) (
a
b
:
CReal
),
seq_cv
un
a
->
a
==
b
->
seq_cv
un
b
.
#[
global
]
Instance
seq_cv_morph
:
forall
(
un
:
nat
->
CReal
),
CMorphisms.Proper
(
CMorphisms.respectful
CRealEq
CRelationClasses.iffT
) (
seq_cv
un
).
Definition
Rfloor
(
a
:
CReal
)
:
{
p
:
Z
&
inject_Q
(
p
#
1)
<
a
<
inject_Q
(
p
#
1)
+
2
}
.
Lemma
Qabs_Rabs
:
forall
q
:
Q
,
inject_Q
(
Qabs
q
)
==
CReal_abs
(
inject_Q
q
).
Lemma
Qlt_trans_swap_hyp
:
forall
x
y
z
:
Q
,
(
y
<
z
)%
Q
->
(
x
<
y
)%
Q
->
(
x
<
z
)%
Q
.
Lemma
Qle_trans_swap_hyp
:
forall
x
y
z
:
Q
,
(
y
<=
z
)%
Q
->
(
x
<=
y
)%
Q
->
(
x
<=
z
)%
Q
.
This inequality is tight since it is equal for n=1 and n=2
Lemma
Qpower_2powneg_le_inv
:
forall
(
n
:
positive
),
(2
*
2
^
Z.neg
n
<=
1
#
n
)%
Q
.
Lemma
Pospow_lin_le_2pow
:
forall
(
n
:
positive
),
(2
*
n
<=
2
^
n
)%
positive
.
Lemma
CReal_cv_self
:
forall
(
x
:
CReal
) (
n
:
positive
),
CReal_abs
(
x
-
inject_Q
(
seq
x
(
Z.neg
n
)))
<=
inject_Q
(1
#
n
).
Lemma
CReal_cv_self'
:
forall
(
x
:
CReal
) (
n
:
Z
),
CReal_abs
(
x
-
inject_Q
(
seq
x
n
))
<=
inject_Q
(2
^
n
).
Definition
QCauchySeqLin
(
un
:
positive
->
Q
)
:
Prop
:=
forall
(
k
:
positive
) (
p
q
:
positive
),
Pos.le
k
p
->
Pos.le
k
q
->
Qlt
(
Qabs
(
un
p
-
un
q
)) (1
#
k
).
Lemma
Rcauchy_limit
:
forall
(
xn
:
nat
->
CReal
) (
xcau
:
Un_cauchy_mod
xn
),
QCauchySeqLin
(
fun
n
:
positive
=>
let
(
p
,
_
) :=
xcau
(4
*
n
)%
positive
in
seq
(
xn
p
) (4
*
Z.neg
n
)%
Z
).
Definition
CReal_from_cauchy_cm
(
n
:
Z
) :
positive
:=
match
n
with
|
Z0
|
Zpos
_
=> 1%
positive
|
Zneg
p
=>
p
end
.
Lemma
CReal_from_cauchy_cm_mono
:
forall
(
n
p
:
Z
),
(
p
<=
n
)%
Z
->
(
CReal_from_cauchy_cm
n
<=
CReal_from_cauchy_cm
p
)%
positive
.
Definition
CReal_from_cauchy_seq
(
xn
:
nat
->
CReal
) (
xcau
:
Un_cauchy_mod
xn
) (
n
:
Z
) :
Q
:=
let
p
:=
CReal_from_cauchy_cm
n
in
let
(
q
,
_
) :=
xcau
(4
*
2
^
p
)%
positive
in
seq
(
xn
q
) (
Z.neg
p
-
2)%
Z
.
Lemma
CReal_from_cauchy_cauchy
:
forall
(
xn
:
nat
->
CReal
) (
xcau
:
Un_cauchy_mod
xn
),
QCauchySeq
(
CReal_from_cauchy_seq
xn
xcau
).
Lemma
Rup_pos
(
x
:
CReal
)
:
{
n
:
positive
&
x
<
inject_Q
(
Z.pos
n
#
1)
}
.
Lemma
CReal_abs_upper_bound
(
x
:
CReal
)
:
{
n
:
positive
&
CReal_abs
x
<
inject_Q
(
Z.pos
n
#
1)
}
.
Require
Import
Qminmax
.
Lemma
CRealLt_QR_from_single_dist
:
forall
(
q
:
Q
) (
r
:
CReal
) (
n
:
Z
),
(2
^
n
<
seq
r
n
-
q
)%
Q
->
inject_Q
q
<
r
.
Lemma
CReal_abs_Qabs
:
forall
(
x
:
CReal
) (
q
:
Q
) (
n
:
Z
),
CReal_abs
x
<=
inject_Q
q
->
(
Qabs
(
seq
x
n
)
<=
q
+
2
^
n
)%
Q
.
Lemma
CReal_abs_Qabs_seq
:
forall
(
x
:
CReal
) (
n
:
Z
),
(
seq
(
CReal_abs
x
)
n
==
Qabs
(
seq
x
n
))%
Q
.
Lemma
CReal_abs_Qabs_diff
:
forall
(
x
y
:
CReal
) (
q
:
Q
) (
n
:
Z
),
CReal_abs
(
x
-
y
)
<=
inject_Q
q
->
(
Qabs
(
seq
x
n
-
seq
y
n
)
<=
q
+
2
*
2
^
n
)%
Q
.
Note: the <= in the conclusion is likely tight
Lemma
CRealLt_QR_to_single_dist
:
forall
(
q
:
Q
) (
x
:
CReal
) (
n
:
Z
),
inject_Q
q
<
x
->
(
-(
2
^
n
)
<=
seq
x
n
-
q
)%
Q
.
Lemma
CRealLt_RQ_to_single_dist
:
forall
(
x
:
CReal
) (
q
:
Q
) (
n
:
Z
),
x
<
inject_Q
q
->
(
-(
2
^
n
)
<=
q
-
seq
x
n
)%
Q
.
Lemma
Pos2Z_pos_is_pos
:
forall
(
p
:
positive
),
(1
<=
Z.pos
p
)%
Z
.
Lemma
Qabs_Qgt_condition
:
forall
x
y
:
Q
,
(
x
<
Qabs
y
)%
Q
<->
(
x
<
y
\/
x
<
-
y
)%
Q
.
Lemma
CReal_from_cauchy_seq_bound
:
forall
(
xn
:
nat
->
CReal
) (
xcau
:
Un_cauchy_mod
xn
) (
i
j
:
Z
),
(
Qabs
(
CReal_from_cauchy_seq
xn
xcau
i
-
CReal_from_cauchy_seq
xn
xcau
j
)
<=
1)%
Q
.
Definition
CReal_from_cauchy_scale
(
xn
:
nat
->
CReal
) (
xcau
:
Un_cauchy_mod
xn
) :
Z
:=
Qbound_lt_ZExp2
(
Qabs
(
CReal_from_cauchy_seq
xn
xcau
(-1))
+
2)%
Q
.
Lemma
CReal_from_cauchy_bound
:
forall
(
xn
:
nat
->
CReal
) (
xcau
:
Un_cauchy_mod
xn
),
QBound
(
CReal_from_cauchy_seq
xn
xcau
) (
CReal_from_cauchy_scale
xn
xcau
).
Definition
CReal_from_cauchy
(
xn
:
nat
->
CReal
) (
xcau
:
Un_cauchy_mod
xn
) :
CReal
:=
{|
seq
:=
CReal_from_cauchy_seq
xn
xcau
;
scale
:=
CReal_from_cauchy_scale
xn
xcau
;
cauchy
:=
CReal_from_cauchy_cauchy
xn
xcau
;
bound
:=
CReal_from_cauchy_bound
xn
xcau
|}.
Lemma
Rcauchy_complete
:
forall
(
xn
:
nat
->
CReal
),
Un_cauchy_mod
xn
->
{
l
:
CReal
&
seq_cv
xn
l
}
.
Lemma
CRealLtIsLinear
:
isLinearOrder
CRealLt
.
Lemma
CRealAbsLUB
:
forall
x
y
:
CReal
,
x
<=
y
/\
(
-
x
)
<=
y
<->
(
CReal_abs
x
)
<=
y
.
Lemma
CRealComplete
:
forall
xn
:
nat
->
CReal
,
(
forall
p
:
positive
,
{
n
:
nat
|
forall
i
j
:
nat
,
(
n
<=
i
)%
nat
->
(
n
<=
j
)%
nat
->
(
CReal_abs
(
xn
i
+
-
xn
j
)
)
<=
(
inject_Q
(1
#
p
)
)
}
)
->
{
l
:
CReal
&
forall
p
:
positive
,
{
n
:
nat
|
forall
i
:
nat
, (
n
<=
i
)%
nat
->
(
CReal_abs
(
xn
i
+
-
l
)
)
<=
(
inject_Q
(1
#
p
)
)
}
}
.
Lemma
Qnot_le_iff_lt
:
forall
x
y
:
Q
,
~
(
x
<=
y
)%
Q
<->
(
y
<
x
)%
Q
.
Lemma
Qnot_lt_iff_le
:
forall
x
y
:
Q
,
~
(
x
<
y
)%
Q
<->
(
y
<=
x
)%
Q
.
Lemma
CRealLtDisjunctEpsilon
:
forall
a
b
c
d
:
CReal
,
(
CRealLtProp
a
b
\/
CRealLtProp
c
d
)
->
CRealLt
a
b
+
CRealLt
c
d
.
Definition
CRealConstructive
:
ConstructiveReals
:=
Build_ConstructiveReals
CReal
CRealLt
CRealLtIsLinear
CRealLtProp
CRealLtEpsilon
CRealLtForget
CRealLtDisjunctEpsilon
inject_Q
inject_Q_lt
lt_inject_Q
CReal_plus
CReal_opp
CReal_mult
inject_Q_plus
inject_Q_mult
CReal_isRing
CReal_isRingExt
CRealLt_0_1
CReal_plus_lt_compat_l
CReal_plus_lt_reg_l
CReal_mult_lt_0_compat
CReal_inv
CReal_inv_l
CReal_inv_0_lt_compat
CRealQ_dense
Rup_pos
CReal_abs
CRealAbsLUB
CRealComplete
.