# 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 }.