Library Coq.Reals.ConstructiveRcomplete
Require Import QArith_base.
Require Import Qabs.
Require Import ConstructiveReals.
Require Import ConstructiveCauchyRealsMult.
Require Import Logic.ConstructiveEpsilon.
Local Open Scope CReal_scope.
Definition absLe (
a b :
CReal) :
Prop
:=
-b <= a <= b.
Lemma CReal_absSmall :
forall (
x y :
CReal) (
n :
positive),
(Qlt (2
# n)
(
proj1_sig x (
Pos.to_nat n)
- Qabs (
proj1_sig y (
Pos.to_nat n)))
)
-> absLe y x.
Definition Un_cv_mod (
un :
nat -> CReal) (
l :
CReal) :
Set
:=
forall p :
positive,
{ n : nat | forall i:
nat,
le n i -> absLe (
un i - l) (
inject_Q (1
#p))
}.
Lemma Un_cv_mod_eq :
forall (
v u :
nat -> CReal) (
s :
CReal),
(forall n:
nat,
u n == v n)
-> Un_cv_mod u s
-> Un_cv_mod v s.
Definition Un_cauchy_mod (
un :
nat -> CReal) :
Set
:=
forall p :
positive,
{ n : nat | forall i j:
nat,
le n i -> le n j
-> absLe (
un i - un j) (
inject_Q (1
#p))
}.
Definition Rfloor (
a :
CReal)
:
{ p : Z & inject_Q (
p#1)
< a < inject_Q (
p#1)
+ 2
}.
Definition FQ_dense (
a b :
CReal)
:
a < b -> { q : Q & a < inject_Q q < b }.
Definition RQ_limit :
forall (
x :
CReal) (
n:
nat),
{ q:Q & x < inject_Q q < x + inject_Q (1
# Pos.of_nat n)
}.
Definition Un_cauchy_Q (
xn :
nat -> Q) :
Set
:=
forall n :
positive,
{ k : nat | forall p q :
nat,
le k p -> le k q
-> Qle (
-(1
#n)) (
xn p - xn q)
/\ Qle (
xn p - xn q) (1
#n)
}.
Lemma Rdiag_cauchy_sequence :
forall (
xn :
nat -> CReal),
Un_cauchy_mod xn
-> Un_cauchy_Q (
fun n:
nat =>
let (
l,
_) :=
RQ_limit (
xn n)
n in l).
Lemma doubleLeCovariant :
forall a b c d e f :
CReal,
a == b -> c == d -> e == f
-> (a <= c <= e)
-> (b <= d <= f).
Lemma CReal_cv_self :
forall (
qn :
nat -> Q) (
x :
CReal) (
cvmod :
positive -> nat),
QSeqEquiv qn (
fun n =>
proj1_sig x n)
cvmod
-> Un_cv_mod (
fun n =>
inject_Q (
qn n))
x.
Lemma Un_cv_extens :
forall (
xn yn :
nat -> CReal) (
l :
CReal),
Un_cv_mod xn l
-> (forall n :
nat,
xn n == yn n)
-> Un_cv_mod yn l.
Lemma R_has_all_rational_limits :
forall qn :
nat -> Q,
Un_cauchy_Q qn
-> { r : CReal & Un_cv_mod (
fun n:
nat =>
inject_Q (
qn n))
r }.
Lemma Rcauchy_complete :
forall (
xn :
nat -> CReal),
Un_cauchy_mod xn
-> { l : CReal & Un_cv_mod xn l }.
Definition CRealImplem :
ConstructiveReals.