CoRN.metrics.CPMSTheory
Lists
Fixpoint MSmember (X : CSetoid) (x : X) (l : list X) {struct l} : CProp :=
match l with
| nil ⇒ False
| cons y m ⇒ MSmember X x m or x = y
end.
Implicit Arguments MSmember [X].
Definition to_IR (P : IR → CProp) : subcsetoid_crr IR P → IR.
Proof.
intro a.
case a.
intros b C.
exact b.
Defined.
Definition from_IR (P : IR → CProp) (x : IR) (H : P x) : subcsetoid_crr IR P.
Proof.
set (H0 := Build_subcsetoid_crr IR P) in ×.
set (H1 := H0 x H) in ×.
exact H1.
Defined.
Definition list_IR (P : IR → CProp) :
list (SubPsMetricSpace IR_as_CPsMetricSpace P) → list IR.
Proof.
intro l.
induction l as [| a l Hrecl].
apply (@nil IR).
apply (cons (to_IR P a) Hrecl).
Defined.
Lemma is_P :
∀ (P : IR → CProp)
(l : list (SubPsMetricSpace IR_as_CPsMetricSpace P))
(x : IR), pred_wd IR P → member x (list_IR P l) → P x.
Proof.
intros P l x Q.
induction l as [| a l Hrecl].
simpl in |- ×.
intuition.
case a.
simpl in |- ×.
intros b C D.
elim D.
intro E.
apply Hrecl.
exact E.
unfold pred_wd in Q.
intro H.
apply Q with b.
exact C.
apply eq_symmetric_unfolded.
exact H.
Qed.
If a real number is element of a list in the above defined sense,
it is an element of the list in the sense of member,
that uses the setoid equality.
Lemma member1 :
∀ (P : IR → CProp) (x0 : subcsetoid_crr IR P)
(l : list (SubPsMetricSpace IR_as_CPsMetricSpace P)),
MSmember (X:=SubPsMetricSpace IR_as_CPsMetricSpace P) x0 l →
member (to_IR P x0) (list_IR P l).
Proof.
intros P x0 l.
induction l as [| a l Hrecl].
simpl in |- ×.
intuition.
simpl in |- ×.
intros H.
elim H.
intro H1.
left.
apply Hrecl.
exact H1.
simpl in |- ×.
intros.
right.
rewrite b.
intuition.
Qed.
The image under a certain mapping of an element of a list l is member
of the list of images of elements of l.
Lemma map_member :
∀ (X Z : CPsMetricSpace) (f : X → Z) (l : list X) (m : X),
MSmember m l → MSmember (f m) (map f l).
Proof.
intros X Z f l m.
induction l as [| a l Hrecl].
simpl in |- ×.
auto.
simpl in |- ×.
intro H.
elim H.
intro H1.
left.
apply Hrecl.
exact H1.
intro H1.
right.
rewrite H1.
intuition.
Qed.
End lists.
Section loc_and_bound.
Definition Re_co_do (X Z : CSetoid) (f : CSetoid_fun X Z) :
X → Build_SubCSetoid Z (fun y : Z ⇒ {x : X | f x[=]y}).
Proof.
intros x.
∃ (f x).
∃ x.
apply eq_reflexive.
Defined.
Lemma Re_co_do_strext :
∀ (X Z : CSetoid) (f : CSetoid_fun X Z),
fun_strext (Re_co_do X Z f).
Proof.
intros X Z f.
unfold fun_strext in |- ×.
intros x y.
simpl in |- ×.
apply (csf_strext X Z f).
Qed.
Definition re_co_do (X Z : CSetoid) (f : CSetoid_fun X Z) :
CSetoid_fun X (Build_SubCSetoid Z (fun y : Z ⇒ {x : X | f x[=]y})) :=
Build_CSetoid_fun X (Build_SubCSetoid Z (fun y : Z ⇒ {x : X | f x[=]y}))
(Re_co_do X Z f) (Re_co_do_strext X Z f).
Lemma re_co_do_well_def :
∀ (X Z : CSetoid) (f : CSetoid_fun X Z),
pred_wd Z (fun y : Z ⇒ {x : X | f x[=]y}).
Proof.
intros X Z f.
unfold pred_wd in |- ×.
intros x y.
intros H0 H1.
elim H0.
intros x0 H3.
∃ x0.
astepr x.
exact H3.
Qed.
Implicit Arguments MSmember [X].
Again we see that the image under a certain mapping of an element of a list
l is member of the list of images of elements of l.
Lemma map_member' :
∀ (X Z : CPsMetricSpace) (f : CSetoid_fun X Z) (l : list X) (m : X),
MSmember m l →
MSmember (X:=Build_SubCSetoid Z (fun y : Z ⇒ {x0 : X | f x0[=]y}))
(re_co_do X Z f m) (map (re_co_do X Z f) l).
Proof.
intros X Z f l m.
induction l as [| a l Hrecl].
simpl in |- ×.
auto.
simpl in |- ×.
intro H.
elim H.
intro H1.
left.
apply Hrecl.
exact H1.
intro H1.
right.
rewrite H1.
intuition.
Qed.
Definition bounded (X : CPsMetricSpace) : CProp :=
{n : IR | ∀ x y : X, x[-d]y[<=]n}.
Definition MStotally_bounded (X : CPsMetricSpace) : CProp :=
∀ n : nat,
{l : list X |
∀ x : X, {y : X | MSmember y l | x[-d]y[<=]one_div_succ n}}.
Total boundedness is preserved under uniformly continuous mappings.
Implicit Arguments SubPsMetricSpace [X].
Lemma unicon_resp_totallybounded :
∀ (X Z : CPsMetricSpace) (f : CSetoid_fun X Z) (H : uni_continuous'' f),
MStotally_bounded X →
MStotally_bounded (SubPsMetricSpace (fun y : Z ⇒ {x : X | f x[=]y})).
Proof.
intros X Z f.
unfold uni_continuous'' in |- ×.
intro H.
unfold MStotally_bounded in |- ×.
intro H1.
intro n.
elim H.
intros mod_ H3.
elim (H1 (mod_ n)).
intros l H2.
simpl in |- ×.
∃ (map (re_co_do X Z f) l).
intros x.
elim x.
intros r H5.
elim H5.
intros k H6.
elim (H2 k).
intros m H7 H8.
∃ (re_co_do X Z f m).
2: simpl in |- ×.
2: astepl (f k[-d]f m).
2: apply H3.
2: exact H8.
apply map_member'.
exact H7.
Qed.
Lemma MStotallybounded_totallybounded :
∀ (P : IR → CProp) (H0 : {x : IR | P x}),
pred_wd IR P →
MStotally_bounded (SubPsMetricSpace (X:=IR_as_CPsMetricSpace) P) →
totally_bounded P.
Proof.
intros P H0 Q.
unfold MStotally_bounded in |- ×.
intro H.
unfold totally_bounded in |- ×.
constructor.
exact H0.
intros e H1.
set (H2 := OneR[/] e[//]ap_symmetric_unfolded IR [0] e (less_imp_ap IR [0] e H1)) in ×.
unfold AbsSmall in |- ×.
set (H3 := Archimedes H2) in ×.
elim H3.
intros m H4.
elim H with m.
intros l H5.
∃ (list_IR P l).
intro x.
apply is_P.
exact Q.
intros x H6.
generalize H5.
simpl in |- ×.
intro H7.
elim (H7 (from_IR P x H6)).
intros x0 H8 H9.
∃ (to_IR P x0).
apply member1.
exact H8.
split.
generalize H9.
unfold dIR_as_CSetoid_fun in |- ×.
unfold dIR in |- ×.
case x0.
intros.
simpl in |- ×.
apply leEq_transitive with ([--](one_div_succ (R:=IR) m)).
apply inv_resp_leEq.
unfold one_div_succ in |- ×.
apply shift_div_leEq.
unfold Snring in |- ×.
apply less_transitive_unfolded with (nring (R:=IR) m).
apply less_leEq_trans with H2.
unfold H2 in |- ×.
apply recip_resp_pos.
exact H1.
exact H4.
simpl in |- ×.
astepl (nring (R:=IR) m[+][0]).
apply plus_resp_less_lft.
apply pos_one.
apply shift_leEq_mult' with (ap_symmetric_unfolded IR [0] e (less_imp_ap IR [0] e H1)).
exact H1.
apply leEq_transitive with (nring (R:=IR) m).
exact H4.
unfold Snring in |- ×.
simpl in |- ×.
apply less_leEq.
astepl (nring (R:=IR) m[+][0]).
apply plus_resp_less_lft.
apply pos_one.
apply inv_cancel_leEq.
astepr (one_div_succ (R:=IR) m).
apply leEq_transitive with (AbsIR (x[-]scs_elem)).
apply inv_leEq_AbsIR.
unfold AbsIR in |- ×.
simpl in |- ×.
generalize H10.
simpl in |- ×.
intuition.
generalize H9.
case x0.
intros x1 Q0 H10.
simpl in |- ×.
apply leEq_transitive with (one_div_succ (R:=IR) m).
generalize H10.
unfold dIR_as_CSetoid_fun in |- ×.
unfold dIR in |- ×.
simpl in |- ×.
intro H11.
apply leEq_transitive with (AbsIR (x[-]x1)).
apply leEq_AbsIR.
unfold AbsIR in |- ×.
simpl in |- ×.
exact H11.
unfold one_div_succ in |- ×.
apply shift_div_leEq.
unfold Snring in |- ×.
apply less_transitive_unfolded with (nring (R:=IR) m).
apply less_leEq_trans with H2.
unfold H2 in |- ×.
apply recip_resp_pos.
exact H1.
exact H4.
simpl in |- ×.
astepl (nring (R:=IR) m[+][0]).
apply plus_resp_less_lft.
apply pos_one.
apply shift_leEq_mult' with (ap_symmetric_unfolded IR [0] e (less_imp_ap IR [0] e H1)).
exact H1.
apply leEq_transitive with (nring (R:=IR) m).
exact H4.
unfold Snring in |- ×.
simpl in |- ×.
apply less_leEq.
astepl (nring (R:=IR) m[+][0]).
apply plus_resp_less_lft.
apply pos_one.
Qed.
Every image under an uniformly continuous function of an totally bounded
pseudo metric space has an infimum and a supremum.
Lemma infimum_exists :
∀ (X : CPsMetricSpace) (f : CSetoid_fun X IR_as_CPsMetricSpace),
uni_continuous'' f →
MStotally_bounded X →
∀ x : X,
{z : IR | set_glb_IR (fun y : IR_as_CPsMetricSpace ⇒ {x : X | f x[=]y}) z}.
Proof.
intros X f H0 H1 x.
apply totally_bounded_has_glb.
apply MStotallybounded_totallybounded.
3: apply unicon_resp_totallybounded.
3: exact H0.
3: exact H1.
2: unfold IR_as_CPsMetricSpace in |- ×.
2: simpl in |- ×.
2: apply re_co_do_well_def.
∃ (f x).
∃ x.
apply eq_reflexive.
Qed.
Lemma supremum_exists :
∀ (X : CPsMetricSpace) (f : CSetoid_fun X IR_as_CPsMetricSpace),
uni_continuous'' f →
MStotally_bounded X →
∀ x : X,
{z : IR | set_lub_IR (fun y : IR_as_CPsMetricSpace ⇒ {x : X | f x[=]y}) z}.
Proof.
intros X f H0 H1 x.
apply totally_bounded_has_lub.
apply MStotallybounded_totallybounded.
3: apply unicon_resp_totallybounded.
3: exact H0.
3: exact H1.
2: unfold IR_as_CPsMetricSpace in |- ×.
2: simpl in |- ×.
2: apply re_co_do_well_def.
∃ (f x).
∃ x.
apply eq_reflexive.
Qed.
A subspace P of a pseudo metric space X is said to be located if for all
elements x of X there exists an infimum for the distance
between x and the elements of P.
Implicit Arguments dsub'_as_cs_fun [X].
Definition located (X : CPsMetricSpace) (P : X → CProp) :=
∀ (x : X) (r : SubPsMetricSpace P),
{z : IR |
set_glb_IR
(fun v : IR ⇒ {y : SubPsMetricSpace P | dsub'_as_cs_fun P x y[=]v}) z}.
Implicit Arguments located [X].
Definition located' (X : CPsMetricSpace) (P : X → CProp) :=
∀ (x : X) (y : SubPsMetricSpace P),
{z : IR |
set_glb_IR
(fun v : IR ⇒
{y : SubPsMetricSpace P | x[-d]from_SubPsMetricSpace X P y[=]v}) z}.
Implicit Arguments located' [X].
Lemma located_imp_located' :
∀ (X : CPsMetricSpace) (P : X → CProp), located P → located' P.
Proof.
intros X P.
unfold located in |- ×.
unfold located' in |- ×.
intros H x y.
set (H0 := H x y) in ×.
elim H0.
intros x0 H1.
∃ x0.
unfold dsub' in H1.
generalize H1.
unfold dsub'_as_cs_fun in |- ×.
unfold dsub' in |- ×.
simpl in |- ×.
unfold set_glb_IR in |- ×.
intros.
split.
intro x1.
elim H2.
intros a b H3.
apply a.
elim H3.
intros.
∃ x2.
astepl (x[-d]from_SubPsMetricSpace X P x2).
exact p.
apply ax_d_com.
apply CPsMetricSpace_is_CPsMetricSpace.
intros e H3.
elim H2.
intros.
set (H8 := b e H3) in ×.
elim H8.
intros.
∃ x1.
elim p.
intros.
∃ x2.
astepl (from_SubPsMetricSpace X P x2[-d]x).
exact p0.
apply ax_d_com.
apply CPsMetricSpace_is_CPsMetricSpace.
exact q.
Qed.
Every totally bounded pseudo metric space is located.
Lemma MStotally_bounded_imp_located :
∀ (X : CPsMetricSpace) (P : X → CProp),
MStotally_bounded (SubPsMetricSpace P) → located P.
Proof.
intros X P H.
unfold located in |- ×.
intros x y.
set (H0 := infimum_exists (SubPsMetricSpace P) (dsub'_as_cs_fun P x)) in ×.
set (H1 := H0 (dsub'_uni_continuous'' X P x) H y) in ×.
elim H1.
intros x0 H2.
elim H2.
intros.
simpl in |- ×.
∃ x0.
unfold set_glb_IR in |- ×.
split.
intro x1.
intro H6.
apply a.
generalize b.
intros.
elim H6.
intros.
∃ x2.
simpl in |- ×.
exact p.
intros e H3.
set (H7 := b e H3) in ×.
apply H7.
Qed.
For all x in a pseudo metric space X, for all located subspaces P of X,
Floc chooses for a given natural number n an y in P such that:
d(x,y) ≤ inf{d(x,p)| pϵP} + (n+1)-1.
Flocfun does (almost) the same, but has a different type. This enables
one to use the latter as an argument of map.
Definition Floc (X : CPsMetricSpace) (P : X → CProp)
(H0 : located' P) (H2 : SubPsMetricSpace P) (n : nat)
(x : X) :
{y : SubPsMetricSpace P |
{z : IR |
set_glb_IR
(fun v : IR ⇒
{y : SubPsMetricSpace P | x[-d]from_SubPsMetricSpace X P y[=]v}) z |
x[-d]from_SubPsMetricSpace X P y[<=]z[+]one_div_succ n}}.
Proof.
rename H2 into y.
unfold located' in H0.
set (H1 := H0 x y) in ×.
elim H1.
intros x0 H3.
unfold set_glb_IR in H3.
elim H3.
intros H4 H5.
elim (H5 (one_div_succ n)).
intros x1 H6 H7.
elim H6.
intros x2 H8.
eapply existT with (P := fun y0 : SubPsMetricSpace P ⇒ {z : IR | set_glb_IR (fun v : IR ⇒
{y1 : SubPsMetricSpace P | x[-d]from_SubPsMetricSpace X P y1[=]v}) z |
x[-d]from_SubPsMetricSpace X P y0[<=]z[+]one_div_succ n}) (x := x2).
eapply exist2T with (P := fun z : IR ⇒ set_glb_IR (fun v : IR ⇒ {y1 : SubPsMetricSpace P |
x[-d]from_SubPsMetricSpace X P y1[=]v}) z) (Q := fun z : IR ⇒
x[-d]from_SubPsMetricSpace X P x2[<=]z[+]one_div_succ n) (x := x0).
unfold set_glb_IR in |- ×.
apply H3.
apply shift_leEq_plus'.
astepl (x1[-]x0).
apply less_leEq.
apply H7.
apply one_div_succ_pos.
Defined.
Definition Flocfun (X : CPsMetricSpace) (P : X → CProp)
(H0 : located' P) (H2 : SubPsMetricSpace P) (n : nat) :
X → SubPsMetricSpace P.
Proof.
intros.
set (H1 := Floc X P H0 H2 n X0) in ×.
elim H1.
intros.
exact x.
Defined.
A located subset P of a totally bounded pseudo metric space
X is totally
bounded.
Lemma locatedsub_totallybounded_imp_totallyboundedsub :
∀ (X : CPsMetricSpace) (P : X → CProp),
SubPsMetricSpace P →
located' P → MStotally_bounded X → MStotally_bounded (SubPsMetricSpace P).
Proof.
intros X P y H0.
unfold MStotally_bounded in |- ×.
intros H1 n.
elim (H1 (3 × n + 2)).
intros l H2.
unfold located' in H0.
simpl in |- ×.
∃ (map (Flocfun X P H0 y (3 × n + 2)) l).
simpl in |- ×.
intro x.
elim (H2 (from_SubPsMetricSpace X P x)).
intros xj xjl H3.
∃ (Flocfun X P H0 y (n + (n + (n + 0)) + 2) xj).
apply map_member with (f := Flocfun X P H0 y (n + (n + (n + 0)) + 2)).
exact xjl.
unfold Flocfun in |- ×.
unfold sigT_rec in |- ×.
unfold sigT_rect in |- ×.
case Floc.
intros.
elim s.
intros x2 p0 q.
generalize H3.
case x.
intros xn Pn H4.
apply leEq_transitive with ((xn[-d]xj)[+](xj[-d]from_SubPsMetricSpace X P x0)).
case x0.
intros.
simpl in |- ×.
apply ax_d_tri_ineq.
apply CPsMetricSpace_is_CPsMetricSpace.
astepr (one_div_succ (R:=IR) (n + (n + (n + 0)) + 2)[+] (one_div_succ (n + (n + (n + 0)) + 2)[+]
one_div_succ (n + (n + (n + 0)) + 2))).
apply plus_resp_leEq_both.
apply H4.
apply leEq_transitive with (x2[+]one_div_succ (n + (n + (n + 0)) + 2)).
apply leEq_transitive with (xj[-d]from_SubPsMetricSpace X P x0).
apply eq_imp_leEq.
apply csbf_wd_unfolded.
intuition.
intuition.
exact q.
apply plus_resp_leEq.
apply leEq_transitive with (from_SubPsMetricSpace X P x[-d]xj).
unfold set_glb_IR in p0.
elim p0.
intros.
apply a.
unfold SubPsMetricSpace in |- ×.
simpl in |- ×.
∃ x.
apply ax_d_com.
apply CPsMetricSpace_is_CPsMetricSpace.
apply H3.
astepr ([1][*]one_div_succ (R:=IR) n).
astepr (((Three:IR)[/] Three:IR[//]three_ap_zero IR)[*]one_div_succ n).
astepl (one_div_succ (n + (n + (n + 0)) + 2)[+] (Two:IR)[*]one_div_succ (n + (n + (n + 0)) + 2)).
astepl (OneR[*]one_div_succ (n + (n + (n + 0)) + 2)[+]
(Two:IR)[*]one_div_succ (n + (n + (n + 0)) + 2)).
astepl ((OneR[+]Two)[*]one_div_succ (n + (n + (n + 0)) + 2)).
astepl ((Three:IR)[*]one_div_succ (n + (n + (n + 0)) + 2)).
2: apply mult_wdl.
2: rational.
astepr ((Three:IR)[*]([1][/] Three[//]three_ap_zero IR)[*]one_div_succ n).
astepr ((Three:IR)[*](([1][/] Three[//]three_ap_zero IR)[*]one_div_succ n)).
apply mult_wdr.
unfold one_div_succ in |- ×.
unfold Snring in |- ×.
simpl in |- ×.
astepr (OneR[/] (Three:IR)[*](nring n[+][1])[//]
mult_resp_ap_zero IR Three (nring n[+][1]) (three_ap_zero IR) (nringS_ap_zero IR n)).
apply eq_div.
apply mult_wdr.
astepl (Three[*]nring (R:=IR) n[+]Three[*][1]).
simpl in |- ×.
astepr (nring (R:=IR) (n + (n + (n + 0)))[+]Two[+][1]).
astepr (nring (R:=IR) n[+]nring (n + (n + 0))[+]Two[+][1]).
astepr (nring (R:=IR) n[+](nring n[+]nring (n + 0))[+]Two[+][1]).
3: apply mult_wdl.
3: rational.
2: simpl in |- ×.
2: rational.
astepr (nring (R:=IR) n[+](nring n[+]nring (n + 0))[+]Two[+][1]).
astepr (nring (R:=IR) n[+](nring n[+]nring (n + 0))[+](Two[+][1])).
astepl ((ZeroR[+][1][+][1][+][1])[*]nring n[+]([0][+][1][+][1][+][1])).
simpl in |- ×.
astepl (ZeroR[+][1][+][1][+][1][+]([0][+][1][+][1][+][1])[*]nring n).
astepr (ZeroR[+][1][+][1][+][1][+](nring n[+](nring n[+]nring (n + 0)))).
apply plus_resp_eq.
astepr (nring (R:=IR) n[+](nring n[+](nring n[+]nring 0))).
simpl in |- ×.
rational.
Qed.
Here are some definitions that could come in handy:
Definition MSCauchy_seq (X : CPsMetricSpace) (seq : nat → X) : CProp :=
∀ n : nat,
{m : nat |
∀ i j : nat, m ≤ i → m ≤ j → seq i[-d]seq j[<=]one_div_succ n}.
Implicit Arguments MSseqLimit' [X].
Definition MSComplete (X : CPsMetricSpace) : CProp :=
∀ seq : nat → X,
MSCauchy_seq X seq → {lim : X | MSseqLimit' seq lim}.
A compact pseudo metric space is a pseudo metric space which is complete and
totally bounded.
A subset P is open if for all x in P there exists an open sphere
with centre x that is contained in P.
Definition open (X : CPsMetricSpace) (P : X → CProp) :=
∀ x : X,
P x → {e : IR | [0][<]e and (∀ z : X, z[-d]x[<]e → P z)}.
Implicit Arguments open [X].
The operator infima gives the infimum for the distance between an
element x of a located pseudo metric space X and the elements of a
subspace P of X.
Definition infima (X : CPsMetricSpace) (P : X → CProp)
(H : located' P) (a : SubPsMetricSpace P) : X → IR.
Proof.
intros H0.
unfold located' in H.
elim (H H0 a).
intros.
exact x.
Defined.
Implicit Arguments infima [X].
A non-empty totally bounded sub-pseudo-metric-space P is said to be
well contained in an open sub-pseudo-metric-space Q if Q contains
all points that are in some sense close to P.
Definition well_contained (X : CPsMetricSpace) (P Q : X → CProp)
(a : SubPsMetricSpace P) :=
open Q →
∀ H : MStotally_bounded (SubPsMetricSpace P),
{r : IR | [0][<]r |
∀ q : X,
infima P (located_imp_located' X P (MStotally_bounded_imp_located X P H)) a
q[<=]r → Q q}.
End loc_and_bound.