Bishop Compactness
This section formalizes Bishops definition of compactness to serve as a reference specification for our definition of compactness.Variable X : MetricSpace.
Variable P : X -> Prop.
Definition CompleteSubset :=
forall (f:Complete X), (forall e, P (approximate f e)) ->
{y:X | P y & st_eq (Cunit y) f}.
Definition ExtSubset :=
forall x y, (st_eq x y) -> (P x <-> P y).
Definition TotallyBoundedSubset :=
forall e, {l : list X | forall y, In y l -> P y & forall x, P x -> exists y, In y l /\ ball e x y }.
A Bishop compact set is an (extensional) predicate that is complete
and totally bounded.
Record CompactSubset :=
{completeSubset : CompleteSubset
;totallyBoundedSubset : TotallyBoundedSubset
;extSubset : ExtSubset
}.
End BishopCompact.
Section AlmostIn.
Variable X : MetricSpace.
Hypothesis stableX : stableMetric X.
{completeSubset : CompleteSubset
;totallyBoundedSubset : TotallyBoundedSubset
;extSubset : ExtSubset
}.
End BishopCompact.
Section AlmostIn.
Variable X : MetricSpace.
Hypothesis stableX : stableMetric X.
almostIn is a useful predicate that says when a point is within e
of (classically) some member of a finite enumeration. We won't know which
point it is close to.
Fixpoint almostIn (e:Qpos) (x:X) (l:FinEnum stableX) : Prop :=
match l with
| nil => ⊥
| y::ys => orC (ball e x y) (almostIn e x ys)
end.
Lemma almostIn_stable : forall e x l, ~~almostIn e x l -> almostIn e x l.
Lemma almostIn_weak_le : forall (e1 e2:Qpos) x l, (e1 <= e2) -> almostIn e1 x l -> almostIn e2 x l.
match l with
| nil => ⊥
| y::ys => orC (ball e x y) (almostIn e x ys)
end.
Lemma almostIn_stable : forall e x l, ~~almostIn e x l -> almostIn e x l.
Lemma almostIn_weak_le : forall (e1 e2:Qpos) x l, (e1 <= e2) -> almostIn e1 x l -> almostIn e2 x l.
If you are almost in for every e, then you are infact in the finite
enumeration
Lemma InAlmostIn : forall x l, (forall e, almostIn e x l)<->(InFinEnumC x l).
Lemma almostIn_closed : forall e x l, (forall d, almostIn (e+d) x l) -> almostIn e x l.
Lemma almostIn_closed : forall e x l, (forall d, almostIn (e+d) x l) -> almostIn e x l.
Left and right triangle laws for balls and almostIn.
Lemma almostIn_triangle_l : forall e1 e2 x1 x2 l, (ball e1 x1 x2) -> almostIn e2 x2 l -> almostIn (e1 + e2) x1 l.
Lemma almostIn_triangle_r : forall e1 e2 x l1 l2, almostIn e1 x l1 -> (ball e2 l1 l2) -> almostIn (e1 + e2) x l2.
Lemma almostIn_triangle_r : forall e1 e2 x l1 l2, almostIn e1 x l1 -> (ball e2 l1 l2) -> almostIn (e1 + e2) x l2.
If you are almost in a finite enumeration then you are close to
(classically) some point that is in the enumeration.
Lemma almostInExistsC : forall e x s, almostIn e x s <-> existsC X (fun y => ball e x y /\ InFinEnumC y s).
End AlmostIn.
End AlmostIn.
Definition of Compact
A compact set is defined as the completion of finite enumerations as a metric space
A point is in a compact set if all the approximations are almost in
the approximations of the compact set.
Definition inCompact X stableX (x:Complete X) (s:Compact stableX) :=
forall e1 e2, almostIn (e1 + e2) (approximate x e1) (approximate s e2).
Section Compact.
Variable X : MetricSpace.
Hypothesis stableX : stableMetric X.
Let Compact := Compact stableX.
Let inCompact := @inCompact X stableX.
Lemma inCompact_stable : forall x s, ~~inCompact x s -> inCompact x s.
forall e1 e2, almostIn (e1 + e2) (approximate x e1) (approximate s e2).
Section Compact.
Variable X : MetricSpace.
Hypothesis stableX : stableMetric X.
Let Compact := Compact stableX.
Let inCompact := @inCompact X stableX.
Lemma inCompact_stable : forall x s, ~~inCompact x s -> inCompact x s.
Compact is Bishop Compact.
Here we show that our definiton of compactness satifies Bishop's compactness.First we show that our compact sets are complete.
Lemma CompactCompleteSubset : forall x, CompleteSubset _ (fun z => inCompact z x).
Section CompactTotallyBounded.
In order to show that compact sets are totally bounded we need to assume
that the underlying metric space is located. According to Bishop's
definition, every metric space is located. Therefore this is a fair
assumption to make.
If a point is almost in an enumeration, then there it is close to
a point in the enumeration in a constructive sense.
Lemma AlmostInExists: forall (e d:Qpos) x (s:FinEnum stableX), e < d -> almostIn e x s -> {y | In y s /\ ball d x y}.
The limit of this stream is going to be used to construct a point
inside the compact set close to a suitable starting point.
CoFixpoint CompactTotallyBoundedStream (s:Compact) (k d1 d2:Qpos) (pt:X) Hpt : Stream X :=
Cons pt
(let (f,_) := HausdorffBallHausdorffBallStrong locatedX
(regFun_prf s d1 (k*d1)%Qpos) in
let (pt',HptX) := f pt Hpt d2 in
let (Hpt',_) := HptX in
(CompactTotallyBoundedStream s k (k*d1) (k*d2) pt' Hpt')).
Cons pt
(let (f,_) := HausdorffBallHausdorffBallStrong locatedX
(regFun_prf s d1 (k*d1)%Qpos) in
let (pt',HptX) := f pt Hpt d2 in
let (Hpt',_) := HptX in
(CompactTotallyBoundedStream s k (k*d1) (k*d2) pt' Hpt')).
This stream is Cauchy
Lemma CompactTotallyBoundedStreamCauchyLemma : forall n (k d:Qpos),
k < 1 ->
0 < (d*(1-k^(S n))/(1-k)).
Lemma CompactTotallyBoundedStreamCauchy1 : forall n s (k d1 d2:Qpos) pt Hpt
(Hd:0 < ((((1#1)+k)*d1+d2)%Qpos*(1-k^(S n))/(1-k))), k < 1 ->
ball (mkQpos Hd) pt (Str_nth n (CompactTotallyBoundedStream s k d1 d2 pt Hpt)).
Lemma CompactTotallyBoundedStreamCauchy2 : forall (m n:nat) s (k d1 d2:Qpos) pt Hpt
(Hd:0 < ((((1#1)+k)*d1+d2)%Qpos*(1-k^(S n))/(1-k))), k < 1 ->
ball (k^m*(mkQpos Hd))
(Str_nth m (CompactTotallyBoundedStream s k d1 d2 pt Hpt))
(Str_nth (m + n) (CompactTotallyBoundedStream s k d1 d2 pt Hpt)).
Lemma StreamInCompactApprox : forall n s k d1 d2 pt Hpt,
{q:Qpos | InFinEnumC (Str_nth n (CompactTotallyBoundedStream s k d1 d2 pt Hpt)) (approximate s q) & q==k^n*d1}.
Definition CompactTotallyBoundedIndex (e d1 d2:Qpos) : N :=
let (n,d):=((1+(1#4))*d1 + d2)/e/(1-(1#4)) in
match Zsucc (Zdiv n d) with
| Zpos p => div2 (S (Z_to_nat (log_sup_correct1 p)))
| _ => O
end.
Lemma CompactTotallyBoundedIndexLemma : forall (e d1 d2:Qpos),
((1+(1#4))*d1 + d2)*(1#4)^(CompactTotallyBoundedIndex e d1 d2)/(1-(1#4)) <= e.
Definition CompactTotallyBounded_raw (s:Compact) (d1 d2:Qpos) (pt:X) Hpt (e:QposInf) : X :=
match e with
|QposInfinity => pt
|Qpos2Q+∞ e' => (Str_nth (CompactTotallyBoundedIndex e' d1 d2)
(CompactTotallyBoundedStream s (1#4) d1 d2 pt Hpt))
end.
k < 1 ->
0 < (d*(1-k^(S n))/(1-k)).
Lemma CompactTotallyBoundedStreamCauchy1 : forall n s (k d1 d2:Qpos) pt Hpt
(Hd:0 < ((((1#1)+k)*d1+d2)%Qpos*(1-k^(S n))/(1-k))), k < 1 ->
ball (mkQpos Hd) pt (Str_nth n (CompactTotallyBoundedStream s k d1 d2 pt Hpt)).
Lemma CompactTotallyBoundedStreamCauchy2 : forall (m n:nat) s (k d1 d2:Qpos) pt Hpt
(Hd:0 < ((((1#1)+k)*d1+d2)%Qpos*(1-k^(S n))/(1-k))), k < 1 ->
ball (k^m*(mkQpos Hd))
(Str_nth m (CompactTotallyBoundedStream s k d1 d2 pt Hpt))
(Str_nth (m + n) (CompactTotallyBoundedStream s k d1 d2 pt Hpt)).
Lemma StreamInCompactApprox : forall n s k d1 d2 pt Hpt,
{q:Qpos | InFinEnumC (Str_nth n (CompactTotallyBoundedStream s k d1 d2 pt Hpt)) (approximate s q) & q==k^n*d1}.
Definition CompactTotallyBoundedIndex (e d1 d2:Qpos) : N :=
let (n,d):=((1+(1#4))*d1 + d2)/e/(1-(1#4)) in
match Zsucc (Zdiv n d) with
| Zpos p => div2 (S (Z_to_nat (log_sup_correct1 p)))
| _ => O
end.
Lemma CompactTotallyBoundedIndexLemma : forall (e d1 d2:Qpos),
((1+(1#4))*d1 + d2)*(1#4)^(CompactTotallyBoundedIndex e d1 d2)/(1-(1#4)) <= e.
Definition CompactTotallyBounded_raw (s:Compact) (d1 d2:Qpos) (pt:X) Hpt (e:QposInf) : X :=
match e with
|QposInfinity => pt
|Qpos2Q+∞ e' => (Str_nth (CompactTotallyBoundedIndex e' d1 d2)
(CompactTotallyBoundedStream s (1#4) d1 d2 pt Hpt))
end.
This stream forms a regular function
Lemma CompactTotallyBounded_prf : forall (s:Compact) (d1 d2:Qpos) (pt:X) Hpt,
is_RegularFunction (CompactTotallyBounded_raw s d1 d2 pt Hpt).
Definition CompactTotallyBounded_fun (s:Compact) (d1 d2:Qpos) (pt:X) Hpt : Complete X :=
Build_RegularFunction (CompactTotallyBounded_prf s d1 d2 pt Hpt).
is_RegularFunction (CompactTotallyBounded_raw s d1 d2 pt Hpt).
Definition CompactTotallyBounded_fun (s:Compact) (d1 d2:Qpos) (pt:X) Hpt : Complete X :=
Build_RegularFunction (CompactTotallyBounded_prf s d1 d2 pt Hpt).
The limit is inside the compact set
Lemma CompactTotallyBoundedInCompact : forall (s:Compact) (d1 d2:Qpos) (pt:X) Hpt,
inCompact (CompactTotallyBounded_fun s d1 d2 pt Hpt) s.
inCompact (CompactTotallyBounded_fun s d1 d2 pt Hpt) s.
The limit is close to the initial starting point
Lemma CompactTotallyBoundedNotFar : forall (s:Compact) (d1 d2:Qpos) (pt:X) Hpt,
ball ((5#3)*d1 + (4#3)*d2) (Cunit pt) (CompactTotallyBounded_fun s d1 d2 pt Hpt).
ball ((5#3)*d1 + (4#3)*d2) (Cunit pt) (CompactTotallyBounded_fun s d1 d2 pt Hpt).
Using CompactTotallyBounded_fun we can map the approximation of
a compact set to a new enumeration that contains only points inside
the compact sets, without moving the points too much
Definition CompactTotalBound (s:Compact) (e:Qpos) : list (Complete X).
Defined.
Lemma CompactTotalBoundNotFar : forall SCX (s:Compact) (e:Qpos),
ball ((3#5)*e) (map Cunit (approximate s ((1#5)*e)%Qpos):FinEnum SCX) (CompactTotalBound s e).
Defined.
Lemma CompactTotalBoundNotFar : forall SCX (s:Compact) (e:Qpos),
ball ((3#5)*e) (map Cunit (approximate s ((1#5)*e)%Qpos):FinEnum SCX) (CompactTotalBound s e).
This means that our compact sets are totally bounded.
Lemma CompactTotallyBoundedA : forall s e y, In y (CompactTotalBound s e) -> inCompact y s.
Lemma CompactTotallyBoundedB : forall s e x, (inCompact x s) -> exists y, In y (CompactTotalBound s e) /\ ball e x y.
Lemma CompactTotallyBounded : forall s, TotallyBoundedSubset _ (fun z => inCompact z s).
Lemma CompactTotallyBoundedB : forall s e x, (inCompact x s) -> exists y, In y (CompactTotalBound s e) /\ ball e x y.
Lemma CompactTotallyBounded : forall s, TotallyBoundedSubset _ (fun z => inCompact z s).
And hence our compact sets are Bishop compact.
Lemma CompactAsBishopCompact : forall s, CompactSubset _ (fun z => inCompact z s).
End CompactTotallyBounded.
End CompactTotallyBounded.
Bishop Compact is Compact.
Next we must show that Bishop compact sets are compact according to our definition.Given a Bishop compact set we construct finite enumerations that approximate that set.
Definition BishopCompactAsCompact_raw
(P:Complete X->Prop) (HP:CompactSubset _ P) (e:QposInf) : (FinEnum stableX) :=
match e with
|QposInfinity => nil
|Qpos2Q+∞ e' =>
(let (l,_,_) := (totallyBoundedSubset HP ((1#2)*e')) in
map (fun x => approximate x ((1#2)*e')) l)%Qpos
end.
(P:Complete X->Prop) (HP:CompactSubset _ P) (e:QposInf) : (FinEnum stableX) :=
match e with
|QposInfinity => nil
|Qpos2Q+∞ e' =>
(let (l,_,_) := (totallyBoundedSubset HP ((1#2)*e')) in
map (fun x => approximate x ((1#2)*e')) l)%Qpos
end.
These approximations are coherent
Lemma BishopCompactAsCompact_prf :
forall P (HP:CompactSubset _ P), is_RegularFunction (BishopCompactAsCompact_raw HP).
forall P (HP:CompactSubset _ P), is_RegularFunction (BishopCompactAsCompact_raw HP).
Hence Bishop compact sets are compact in our sense.
Definition BishopCompactAsCompact
(P:Complete X->Prop) (HP:CompactSubset _ P) : Compact :=
Build_RegularFunction (BishopCompactAsCompact_prf HP).
Section Isomorphism.
(P:Complete X->Prop) (HP:CompactSubset _ P) : Compact :=
Build_RegularFunction (BishopCompactAsCompact_prf HP).
Section Isomorphism.
Isomorphism
We claim that Bishop compact sets correspond to our compact sets, but to be sure we need to show that the definitions are isomoprhic. We need to show that the conversions back and forth are equivalent to the identity.
Hypothesis locatedX : locatedMetric X.
Lemma BishopCompact_Compact_BishopCompact1 :
forall (P:Complete X->Prop) (HP:CompactSubset _ P) x,
P x -> inCompact x (BishopCompactAsCompact HP).
Lemma BishopCompact_Compact_BishopCompact2 :
forall (P:Complete X->Prop) (HP:CompactSubset _ P) x,
inCompact x (BishopCompactAsCompact HP) -> P x.
Lemma BishopCompact_Compact_BishopCompact :
forall (P:Complete X->Prop) (HP:CompactSubset _ P) x,
P x <-> inCompact x (BishopCompactAsCompact HP).
Lemma Compact_BishopCompact_Compact : forall s,
st_eq s (BishopCompactAsCompact (CompactAsBishopCompact locatedX s)).
End Isomorphism.
End Compact.
Section CompactDistr.
Variable X : MetricSpace.
Hypothesis stableX : stableMetric X.
Hypothesis stableCX : stableMetric (Complete X).
Lemma BishopCompact_Compact_BishopCompact1 :
forall (P:Complete X->Prop) (HP:CompactSubset _ P) x,
P x -> inCompact x (BishopCompactAsCompact HP).
Lemma BishopCompact_Compact_BishopCompact2 :
forall (P:Complete X->Prop) (HP:CompactSubset _ P) x,
inCompact x (BishopCompactAsCompact HP) -> P x.
Lemma BishopCompact_Compact_BishopCompact :
forall (P:Complete X->Prop) (HP:CompactSubset _ P) x,
P x <-> inCompact x (BishopCompactAsCompact HP).
Lemma Compact_BishopCompact_Compact : forall s,
st_eq s (BishopCompactAsCompact (CompactAsBishopCompact locatedX s)).
End Isomorphism.
End Compact.
Section CompactDistr.
Variable X : MetricSpace.
Hypothesis stableX : stableMetric X.
Hypothesis stableCX : stableMetric (Complete X).
FinEnum distributes over Complete
The FiniteEnumeration monad distributes over the Completion monad. This corresponds to a function from FinEnum (Complete X) to Complete (FinEnum X).
Definition FinCompact_raw (x: FinEnum stableCX) (e:QposInf) : FinEnum stableX :=
map (fun x => approximate x e) x.
Lemma FinCompact_prf : forall x, is_RegularFunction (FinCompact_raw x).
Definition FinCompact_fun (x: FinEnum stableCX) : Compact stableX :=
Build_RegularFunction (FinCompact_prf x).
Lemma FinCompact_uc : is_UniformlyContinuousFunction FinCompact_fun Qpos2QposInf.
Definition FinCompact : FinEnum stableCX --> Compact stableX :=
Build_UniformlyContinuousFunction FinCompact_uc.
Lemma FinCompact_correct : forall x (s:FinEnum stableCX),
InFinEnumC x s <-> inCompact x (FinCompact s).
Lemma CompactCompleteCompact_prf : forall x,
is_RegularFunction (Cmap_raw FinCompact x).
Definition CompactCompleteCompact_fun x : Complete (Compact stableX) :=
Build_RegularFunction (CompactCompleteCompact_prf x).
Lemma CompactCompleteCompact_uc :
is_UniformlyContinuousFunction CompactCompleteCompact_fun Qpos2QposInf.
Definition CompactCompleteCompact : Compact stableCX --> Compact stableX :=
uc_compose Cjoin (Build_UniformlyContinuousFunction CompactCompleteCompact_uc).
Lemma CompactCompleteCompact_correct : forall x s,
inCompact x s <-> inCompact (Cjoin x) (CompactCompleteCompact s).
End CompactDistr.
Section CompactImage.
map (fun x => approximate x e) x.
Lemma FinCompact_prf : forall x, is_RegularFunction (FinCompact_raw x).
Definition FinCompact_fun (x: FinEnum stableCX) : Compact stableX :=
Build_RegularFunction (FinCompact_prf x).
Lemma FinCompact_uc : is_UniformlyContinuousFunction FinCompact_fun Qpos2QposInf.
Definition FinCompact : FinEnum stableCX --> Compact stableX :=
Build_UniformlyContinuousFunction FinCompact_uc.
Lemma FinCompact_correct : forall x (s:FinEnum stableCX),
InFinEnumC x s <-> inCompact x (FinCompact s).
Lemma CompactCompleteCompact_prf : forall x,
is_RegularFunction (Cmap_raw FinCompact x).
Definition CompactCompleteCompact_fun x : Complete (Compact stableX) :=
Build_RegularFunction (CompactCompleteCompact_prf x).
Lemma CompactCompleteCompact_uc :
is_UniformlyContinuousFunction CompactCompleteCompact_fun Qpos2QposInf.
Definition CompactCompleteCompact : Compact stableCX --> Compact stableX :=
uc_compose Cjoin (Build_UniformlyContinuousFunction CompactCompleteCompact_uc).
Lemma CompactCompleteCompact_correct : forall x s,
inCompact x s <-> inCompact (Cjoin x) (CompactCompleteCompact s).
End CompactDistr.
Section CompactImage.
Compact Image
If x is in a compact set S, then f x is in the compact image of S under f. (My definiton of compact image is really the closure of the image under f.)
Variable z : Q+.
Variable X Y : MetricSpace.
Hypothesis stableX : stableMetric X.
Hypothesis stableY : stableMetric Y.
Hypothesis plX : PrelengthSpace X.
Hypothesis plFEX : PrelengthSpace (FinEnum stableX).
Variable f : X --> Y.
Lemma almostIn_map : forall (e d:Qpos) a (b:FinEnum stableX), (QposInf_le d (mu f e)) -> almostIn d a b ->
almostIn e (f a) (FinEnum_map z stableX stableY f b).
Lemma almostIn_map2 : forall (e1 e2 d:Qpos) a (b:FinEnum stableX), (QposInf_le d ((mu f e1) + (mu f e2))) -> almostIn d a b ->
almostIn (e1 + e2) (f a) (FinEnum_map z stableX stableY f b).
Definition CompactImage : Compact stableX --> Compact stableY :=
Cmap plFEX (FinEnum_map z stableX stableY f).
Lemma CompactImage_correct1 : forall x s,
(inCompact x s) -> (inCompact (Cmap plX f x) (CompactImage s)).
End CompactImage.
Section CompactImageBind.
Variable z : Q+.
Variable X Y : MetricSpace.
Hypothesis stableX : stableMetric X.
Hypothesis stableY : stableMetric Y.
Hypothesis plX : PrelengthSpace X.
Hypothesis plFEX : PrelengthSpace (FinEnum stableX).
Variable f : X --> Complete Y.
Definition CompactImage_b : Compact stableX --> Compact stableY :=
uc_compose (CompactCompleteCompact _ _) (CompactImage z (Complete_stable stableY) plFEX f).
Lemma CompactImage_b_correct1 : forall x s,
(inCompact x s) -> (inCompact (Cbind plX f x) (CompactImage_b s)).
End CompactImageBind.
Variable X Y : MetricSpace.
Hypothesis stableX : stableMetric X.
Hypothesis stableY : stableMetric Y.
Hypothesis plX : PrelengthSpace X.
Hypothesis plFEX : PrelengthSpace (FinEnum stableX).
Variable f : X --> Y.
Lemma almostIn_map : forall (e d:Qpos) a (b:FinEnum stableX), (QposInf_le d (mu f e)) -> almostIn d a b ->
almostIn e (f a) (FinEnum_map z stableX stableY f b).
Lemma almostIn_map2 : forall (e1 e2 d:Qpos) a (b:FinEnum stableX), (QposInf_le d ((mu f e1) + (mu f e2))) -> almostIn d a b ->
almostIn (e1 + e2) (f a) (FinEnum_map z stableX stableY f b).
Definition CompactImage : Compact stableX --> Compact stableY :=
Cmap plFEX (FinEnum_map z stableX stableY f).
Lemma CompactImage_correct1 : forall x s,
(inCompact x s) -> (inCompact (Cmap plX f x) (CompactImage s)).
End CompactImage.
Section CompactImageBind.
Variable z : Q+.
Variable X Y : MetricSpace.
Hypothesis stableX : stableMetric X.
Hypothesis stableY : stableMetric Y.
Hypothesis plX : PrelengthSpace X.
Hypothesis plFEX : PrelengthSpace (FinEnum stableX).
Variable f : X --> Complete Y.
Definition CompactImage_b : Compact stableX --> Compact stableY :=
uc_compose (CompactCompleteCompact _ _) (CompactImage z (Complete_stable stableY) plFEX f).
Lemma CompactImage_b_correct1 : forall x s,
(inCompact x s) -> (inCompact (Cbind plX f x) (CompactImage_b s)).
End CompactImageBind.