Library Coq.Reals.ConstructiveRealsLUB
Require Import QArith_base.
Require Import Qabs.
Require Import ConstructiveReals.
Require Import ConstructiveCauchyRealsMult.
Require Import ConstructiveRealsMorphisms.
Require Import ConstructiveRcomplete.
Require Import Logic.ConstructiveEpsilon.
Local Open Scope CReal_scope.
Definition sig_forall_dec_T :
Type
:=
forall (
P :
nat -> Prop),
(forall n,
{P n} + {~P n})
-> {n | ~P n} + {forall n,
P n}.
Definition sig_not_dec_T :
Type :=
forall P :
Prop,
{ ~~P } + { ~P }.
Definition is_upper_bound (
E:
CReal -> Prop) (
m:
CReal)
:=
forall x:
CReal,
E x -> x <= m.
Definition is_lub (
E:
CReal -> Prop) (
m:
CReal) :=
is_upper_bound E m /\ (forall b:
CReal,
is_upper_bound E b -> m <= b).
Lemma is_upper_bound_dec :
forall (
E:
CReal -> Prop) (
x:
CReal),
sig_forall_dec_T
-> sig_not_dec_T
-> { is_upper_bound E x } + { ~is_upper_bound E x }.
Lemma is_upper_bound_epsilon :
forall (
E:
CReal -> Prop),
sig_forall_dec_T
-> sig_not_dec_T
-> (exists x:
CReal, is_upper_bound E x)
-> { n:nat | is_upper_bound E (
inject_Q (
Z.of_nat n # 1))
}.
Lemma is_upper_bound_not_epsilon :
forall E:
CReal -> Prop,
sig_forall_dec_T
-> sig_not_dec_T
-> (exists x :
CReal, E x)
-> { m:nat | ~is_upper_bound E (
-inject_Q (
Z.of_nat m # 1))
}.
Record DedekindDecCut :
Type :=
{
DDupcut :
Q -> Prop;
DDproper :
forall q r :
Q, (
q == r -> DDupcut q -> DDupcut r)%
Q;
DDlow :
Q;
DDhigh :
Q;
DDdec :
forall q:
Q,
{ DDupcut q } + { ~DDupcut q };
DDinterval :
forall q r :
Q,
Qle q r -> DDupcut q -> DDupcut r;
DDhighProp :
DDupcut DDhigh;
DDlowProp :
~DDupcut DDlow;
}.
Lemma DDlow_below_up :
forall (
upcut :
DedekindDecCut) (
a b :
Q),
DDupcut upcut a -> ~DDupcut upcut b -> Qlt b a.
Fixpoint DDcut_limit_fix (
upcut :
DedekindDecCut) (
r :
Q) (
n :
nat) :
Qlt 0
r
-> (DDupcut upcut (
DDlow upcut + (Z.of_nat n#1
) * r)
)
-> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (
q - r)
}.
Lemma DDcut_limit :
forall (
upcut :
DedekindDecCut) (
r :
Q),
Qlt 0
r
-> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (
q - r)
}.
Lemma glb_dec_Q :
forall upcut :
DedekindDecCut,
{ x : CReal | forall r:
Q,
(x < inject_Q r -> DDupcut upcut r)
/\ (inject_Q r < x -> ~DDupcut upcut r) }.
Lemma is_upper_bound_glb :
forall (
E:
CReal -> Prop),
sig_not_dec_T
-> sig_forall_dec_T
-> (exists x :
CReal, E x)
-> (exists x :
CReal, is_upper_bound E x)
-> { x : CReal | forall r:
Q,
(x < inject_Q r -> is_upper_bound E (
inject_Q r)
)
/\ (inject_Q r < x -> ~is_upper_bound E (
inject_Q r)
) }.
Lemma is_upper_bound_closed :
forall (
E:
CReal -> Prop) (
sig_forall_dec :
sig_forall_dec_T)
(
sig_not_dec :
sig_not_dec_T)
(
Einhab :
exists x :
CReal, E x)
(
Ebound :
exists x :
CReal, is_upper_bound E x),
is_lub
E (
proj1_sig (
is_upper_bound_glb
E sig_not_dec sig_forall_dec Einhab Ebound)).
Lemma sig_lub :
forall (
E:
CReal -> Prop),
sig_forall_dec_T
-> sig_not_dec_T
-> (exists x :
CReal, E x)
-> (exists x :
CReal, is_upper_bound E x)
-> { u : CReal | is_lub E u }.
Definition CRis_upper_bound (
R :
ConstructiveReals) (
E:
CRcarrier R -> Prop) (
m:
CRcarrier R)
:=
forall x:
CRcarrier R,
E x -> CRlt R m x -> False.
Lemma CR_sig_lub :
forall (
R :
ConstructiveReals) (
E:
CRcarrier R -> Prop),
(forall x y :
CRcarrier R,
orderEq _ (
CRlt R)
x y -> (E x <-> E y))
-> sig_forall_dec_T
-> sig_not_dec_T
-> (exists x :
CRcarrier R, E x)
-> (exists x :
CRcarrier R, CRis_upper_bound R E x)
-> { u : CRcarrier R | CRis_upper_bound R E u /\
forall y:
CRcarrier R,
CRis_upper_bound R E y -> CRlt R y u -> False }.