From bcc5d6a39881e447ff7fca1c9283d982620c07cf Mon Sep 17 00:00:00 2001
From: zstone1 <zstonex@gmail.com>
Date: Tue, 12 Apr 2022 09:37:54 -0400
Subject: [PATCH 1/7] Arzela Ascoli main results (#545)

Adding main lemmas for arzela ascoli, some lemmas for dealing with compactness, and a technique for getting "sufficiently small" sets from a filter.
---
 CHANGELOG_UNRELEASED.md |  28 +++-
 theories/topology.v     | 274 +++++++++++++++++++++++++++++++++++-----
 2 files changed, 270 insertions(+), 32 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index a90e1b20c1..38448627c8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -34,6 +34,32 @@
   + lemma `fset_set_image`, `card_fset_set`, `geq_card_fset_set`,
     `leq_card_fset_set`, `infinite_set_fset`, `infinite_set_fsetP` and
     `fcard_eq`.
+  + notations `{posnum \bar R}` and `{nonneg \bar R}`
+  + notations `%:pos` and `%:nng` in `ereal_dual_scope` and `ereal_scope`
+  + variants `posnume_spec` and `nonnege_spec`
+  + definitions `posnume`, `nonnege`, `abse_reality_subdef`,
+    `ereal_sup_reality_subdef`, `ereal_inf_reality_subdef`
+  + lemmas `ereal_comparable`, `pinfty_snum_subproof`, `ninfty_snum_subproof`,
+    `EFin_snum_subproof`, `fine_snum_subproof`, `oppe_snum_subproof`,
+    `adde_snum_subproof`, `dadde_snum_subproof`, `mule_snum_subproof`,
+    `abse_reality_subdef`, `abse_snum_subproof`, `ereal_sup_snum_subproof`,
+    `ereal_inf_snum_subproof`, `num_abse_eq0`, `num_lee_maxr`, `num_lee_maxl`,
+    `num_lee_minr`, `num_lee_minl`, `num_lte_maxr`, `num_lte_maxl`,
+    `num_lte_minr`, `num_lte_minl`, `num_abs_le`, `num_abs_lt`,
+    `posnumeP`, `nonnegeP`
+  + signed instances `pinfty_snum`, `ninfty_snum`, `EFin_snum`, `fine_snum`,
+    `oppe_snum`, `adde_snum`, `dadde_snum`, `mule_snum`, `abse_snum`,
+    `ereal_sup_snum`, `ereal_inf_snum`
+- in `topology.v`:
+  + Definition `powerset_filter_from`
+  + globals `powerset_filter_from_filter`, 
+  + lemmas `near_small_set`, `small_set_sub`
+  + lemmas `withinET`, `closureEcvg`, `entourage_sym`, `fam_nbhs`
+  + generalize `cluster_cvgE`, `ptws_cvg_compact_family`
+  + lemma `near_compact_covering`
+  + rewrite `equicontinuous` and `pointwise_precompact` to use index 
+  + lemmas `ptws_cvg_entourage`, `equicontinuous_closure`, `ptws_compact_cvg`
+    `ptws_compact_closed`, `ascoli_forward`, `compact_equicontinuous`
 
 ### Changed
 
@@ -109,4 +135,4 @@
 
 ### Infrastructure
 
-### Misc
+### Misc
\ No newline at end of file
diff --git a/theories/topology.v b/theories/topology.v
index 09ff3d509d..478bed15e3 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -103,6 +103,9 @@ Require Import mathcomp_extra boolp reals classical_sets signed functions.
 (*                                     domain D.                              *)
 (*                subset_filter F D == similar to within D F, but with        *)
 (*                                     dependent types.                       *)
+(*           powerset_filter_from F == The filter of downward closed subsets  *)
+(*                                     of F. Enables use of near notation to  *)
+(*                                     pick suitably small members of F       *)
 (*                      in_filter F == interface type for the sets that       *)
 (*                                     belong to the set of sets F.           *)
 (*                      InFilter FP == packs a set P with a proof of F P to   *)
@@ -1538,6 +1541,12 @@ Proof. exact: withinT. Qed.
 Lemma cvg_within {F} {FF : Filter F} D : within D F --> F.
 Proof. by move=> P; apply: filterS. Qed.
 
+Lemma withinET {F} {FF : Filter F} : within setT F = F.
+Proof.
+rewrite eqEsubset /within; split => ?; apply: filter_app; apply: nearW => //.
+by move=> ?; exact.
+Qed.
+
 End within.
 
 Global Instance within_filter T D F : Filter F -> Filter (@within T D F).
@@ -1547,6 +1556,7 @@ move=> FF; rewrite /within; constructor.
 - by move=> P Q; apply: filterS2 => x DP DQ Dx; split; [apply: DP|apply: DQ].
 - by move=> P Q subPQ; apply: filterS => x DP /DP /subPQ.
 Qed.
+
 #[global] Typeclasses Opaque within.
 
 Canonical within_filter_on T D (F : filter_on T) :=
@@ -1574,6 +1584,50 @@ move=> DAP; apply: Build_ProperFilter'; rewrite /subset_filter => subFD.
 by have /(_ subFD) := DAP (~` D); apply => -[x [dx /(_ dx)]].
 Qed.
 
+(* For using near on sets in a filter *)
+Section NearSet.
+
+Context {T : choiceType} {Y : filteredType T}.
+Context (F : set (set Y)) (PF : ProperFilter F).
+
+Definition powerset_filter_from : set (set (set Y)) := filter_from
+  [set M | [/\ M `<=` F,
+    (forall E1 E2, M E1 -> F E2 -> E2 `<=` E1 -> M E2) & M !=set0 ] ]
+  id.
+
+Global Instance powerset_filter_from_filter : ProperFilter powerset_filter_from.
+Proof.
+split.
+  rewrite (_ : xpredp0 = set0); last by rewrite eqEsubset; split.
+  by move=> [W [_ _ [N +]]]; rewrite subset0 => /[swap] ->; apply.
+apply: filter_from_filter.
+  by exists F; split => //; exists setT; exact: filterT.
+move=> M N /= [entM subM [M0 MM0]] [entN subN [N0 NN0]].
+exists [set E | exists P Q, [/\ M P, N Q & E = P `&` Q] ]; first split.
+- by move=> ? [? [? [? ? ->]]]; apply filterI; [exact: entM | exact: entN].
+- move=> ? E2 [P [Q [MP MQ ->]]] entE2 E2subPQ; exists E2, E2.
+  split; last by rewrite setIid.
+  + by apply: (subM _ _ MP) => // ? /E2subPQ [].
+  + by apply: (subN _ _ MQ) => // ? /E2subPQ [].
+- by exists (M0 `&` N0), M0, N0.
+- move=> E /= [P [Q [MP MQ ->]]]; have entPQ : F (P `&` Q).
+    by apply filterI; [exact: entM | exact: entN].
+  by split; [apply: (subM _ _ MP) | apply: (subN _ _ MQ)] => // ? [].
+Qed.
+
+Lemma near_small_set : \forall E \near powerset_filter_from, F E.
+Proof. by exists F => //; split => //; exists setT; exact: filterT. Qed.
+
+Lemma small_set_sub (E : set Y) : F E -> 
+  \forall E' \near powerset_filter_from, E' `<=` E.
+Proof.
+move=> entE; exists [set E' | F E' /\ E' `<=` E]; last by move=> ? [].
+split; [by move=> E' [] | | by exists E; split].
+by move=> E1 E2 [] ? sub ? ?; split => //; exact: subset_trans sub.
+Qed.
+
+End NearSet.
+
 (** * Topological spaces *)
 
 Module Topological.
@@ -2586,10 +2640,14 @@ Lemma cvg_cluster F G : F --> G -> cluster F `<=` cluster G.
 Proof. by move=> sGF p Fp P Q GP Qp; apply: Fp Qp; apply: sGF. Qed.
 
 Lemma cluster_cvgE F :
-  ProperFilter F ->
+  Filter F ->
   cluster F = [set p | exists2 G, ProperFilter G & G --> p /\ F `<=` G].
 Proof.
-move=> FF; rewrite predeqE => p.
+move=> FF; have [F0|nF0] := pselect (F set0).
+  have -> : cluster F = set0.
+    by rewrite -subset0 clusterE => x /(_ set0 F0); rewrite closure0.
+  by apply/esym; rewrite -subset0 => p [? PG [_ /(_ set0 F0)]]; apply PG.
+rewrite predeqE => p; have PF : ProperFilter F by [].
 split=> [clFp|[G Gproper [cvGp sFG]] A B]; last first.
   by move=> /sFG GA /cvGp GB; apply: (@filter_ex _ G); apply: filterI.
 exists (filter_from (\bigcup_(A in F) [set A `&` B | B in nbhs p]) id).
@@ -2609,6 +2667,11 @@ move=> A FA; exists A => //; exists A => //; exists setT; first exact: filterT.
 by rewrite setIT.
 Qed.
 
+Lemma closureEcvg (E : set T):
+  closure E =
+  [set p | exists2 G, ProperFilter G & G --> p /\ globally E `<=` G].
+Proof. by rewrite closureEcluster cluster_cvgE. Qed.
+
 Definition compact A := forall (F : set (set T)),
   ProperFilter F -> F A -> A `&` cluster F !=set0.
 
@@ -2651,6 +2714,34 @@ Qed.
 End Compact.
 Arguments hausdorff_space : clear implicits.
 
+Lemma near_compact_covering {X : Type} {Y : topologicalType}
+    (F : set (set X)) (Q P : X -> Y -> Prop) (K : set Y) :
+  Filter F -> compact K ->
+  (forall y, K y -> \forall x \near F, Q x y) ->
+  (forall y, \forall y' \near y & x \near F, Q x y -> P x y') ->
+  \forall x \near F, K `<=` P x.
+Proof.
+move=> FF cptK cover nearby.
+pose badPoints := fun U => K `\` [set y | K y /\ forall x, U x -> P x y].
+pose G := filter_from F badPoints.
+have FG : Filter G.
+  apply: filter_from_filter; first by exists setT; exact: filterT.
+  move=> L R ? ?; exists (L `&` R); first exact: filterI.
+  rewrite /badPoints /= !setDIr !setDv !set0U -setDUr; apply: setDS.
+  by move=> x [|] => + ? [? ?]; exact.
+have [|?] := pselect (G set0).
+  move=> [V fV]; rewrite subset0 setD_eq0 => subK.
+  by apply: (@filterS _ _ _ V) => // ? ? ? /subK [?]; apply.
+have PG : ProperFilter G by [].
+have GK : G K by exists setT; [exact: filterT | by move=> ? []].
+case: (cptK _ PG GK) => y [Ky]; have [[U1 U2] [U1y ? subP]] := nearby y.
+have GP : G (badPoints ([set x | Q x y] `&` U2)).
+  apply: filterI => //; exists ([set x | Q x y] `&` U2); last by move=> ? [].
+  by apply: filterI => //; exact: (cover y Ky).
+move=> /(_ _ _ GP U1y) => [[y'[]]][] ? /[swap] ?.
+by case; split => // x [? ?]; exact: (subP (y', x)).
+Qed.
+
 Section Tychonoff.
 
 Class UltraFilter T (F : set (set T)) := {
@@ -3471,6 +3562,10 @@ Definition entourage {M : uniformType} := Uniform.entourage (Uniform.class M).
 Lemma nbhs_entourageE {M : uniformType} : nbhs_ (@entourage M) = nbhs.
 Proof. by case: M=> [?[?[]]]. Qed.
 
+Lemma entourage_sym {X Y : Type} E (x : X) (y : Y) :
+  E (x, y) <-> (E ^-1)%classic (y, x).
+Proof. by []. Qed.
+
 Lemma filter_from_entourageE {M : uniformType} x :
   filter_from (@entourage M) (fun A => to_set A x) = nbhs x.
 Proof. by rewrite -nbhs_entourageE. Qed.
@@ -3547,6 +3642,7 @@ End uniformType1.
 Hint Extern 0 (entourage (split_ent _)) => exact: entourage_split_ent : core.
 #[global]
 Hint Extern 0 (entourage (get _)) => exact: entourage_split_ent : core.
+Hint Extern 0 (entourage (_^-1)%classic) => exact: entourage_inv : core.
 Arguments entourage_split {M} z {x y A}.
 #[global]
 Hint Extern 0 (nbhs _ (to_set _ _)) => exact: nbhs_entourage : core.
@@ -4431,7 +4527,6 @@ apply/cvg_fct_entourageP => A entA; near=> f => t; near F => g.
 apply: (entourage_split (g t)) => //; first by near: g; apply: cvF.
 move: (t); near: g; near: f; apply: nearP_dep; apply: Fc.
 exists ((split_ent A)^-1)%classic=> //=.
-by apply: entourage_inv; apply: entourage_split_ent.
 Unshelve. all: by end_near. Qed.
 
 Canonical fun_completeType := CompleteType (T -> U) fun_complete.
@@ -5342,11 +5437,19 @@ Notation "{ 'family' fam , U -> V }" :=  (@fct_UniformFamily U V fam).
 Notation "{ 'family' fam , F --> f }" :=
   (F --> restrict_fam fam f) : classical_set_scope.
 
-Lemma fam_cvgE {U : topologicalType} {V : uniformType} (F : set (set (U -> V)))
+Lemma fam_cvgE {U : choiceType} {V : uniformType} (F : set (set (U -> V)))
     (f : U -> V) fam :
   {family fam, F --> f} = (F --> (f : {family fam, U -> V})).
 Proof. by []. Qed.
 
+Lemma fam_nbhs {U : choiceType} {V : uniformType} (fam : set U -> Prop)
+    (A : set U) (E : set (V * V)) (f : {family fam, U -> V}) :
+  entourage E -> fam A -> nbhs f [set g | forall y, A y -> E (f y, g y)].
+Proof.
+move=> entE famA; have /fam_cvgP /(_ A) : (nbhs f --> f) by []; apply => //.
+by apply uniform_nbhs; exists E; split.
+Qed.
+
 Definition compactly_in {U : topologicalType} (A : set U) :=
   [set B | B `<=` A /\ compact B].
 
@@ -5901,7 +6004,7 @@ by rewrite eqEsubset; split => [j [? + <-//]|j Wj]; exists (fun _ => j).
 Qed.
 
 Lemma ptws_cvg_compact_family F (f : U -> V) :
-  ProperFilter F -> {family compact, F --> f} -> {ptws, F --> f}.
+  Filter F -> {family compact, F --> f} -> {ptws, F --> f}.
 Proof.
 move=> PF; rewrite ptws_cvg_family_singleton; apply: family_cvg_subset.
 by move=> A [x _ <-]; exact: compact_set1.
@@ -5912,51 +6015,63 @@ Section ArzelaAscoli.
 Context {X : topologicalType}.
 Context {Y : uniformType}.
 Context {hsdf : hausdorff_space Y}.
+Implicit Types (I : Type).
+
 
 (* The key condition in Arzela-Ascoli that, like uniform continuity,
    moves a quantifier around so all functions have the same 'deltas'. *)
 
-Definition equicontinuous (W : set (X -> Y)) :=
+Definition equicontinuous {I} (W : set I) (d : I -> (X -> Y)) :=
   forall x (E : set (Y * Y)), entourage E ->
-    \forall y \near x, forall f, W f -> E(f x, f y).
+    \forall y \near x, forall i, W i -> E(d i x, d i y).
 
-Lemma equicontinuous_subset (W V : set (X -> Y)) :
-  W `<=` V -> equicontinuous V -> equicontinuous W.
+Lemma equicontinuous_subset {I J} (W : set I) (V : set J) {fW : I -> X -> Y} {fV : J -> X -> Y} :
+  fW @`W `<=` fV @` V -> equicontinuous V fV -> equicontinuous W fW.
 Proof.
-move=> WsubV + x E entE => /(_ x E entE); apply: filter_app; apply: nearW.
-by move=> ? Vf ? /WsubV; exact: Vf.
+move=> WsubV + x E entE => /(_ x E entE); apply: filterS => y VE i Wi.
+by case: (WsubV (fW i)); [exists i | move=> j Vj <-; exact: VE].
 Qed.
 
-Lemma equicontinuous_cts (W : set (X -> Y)) f :
-  equicontinuous W -> W f -> continuous f.
+Lemma equicontinuous_continuous_for {I} (W : set I) (fW : I -> X -> Y) i x :
+  {for x, equicontinuous W fW} -> W i -> {for x, continuous (fW i)}.
 Proof.
-move=> ectsW Wf x; apply/cvg_entourageP => E entE; near_simpl;
-by move: (ectsW x _ entE); apply: filter_app; apply: nearW => ?; exact.
+move=> ectsW Wf; apply/cvg_entourageP => E entE; near_simpl.
+by near=> y; apply: (near (ectsW _ entE) y).
+Unshelve. end_near. Qed.
+
+Lemma equicontinuous_continuous {I} (W : set I) (fW : I -> (X -> Y)) (i : I) :
+  equicontinuous W fW -> W i -> continuous (fW i).
+Proof.
+move=> ectsW Wf x; apply: equicontinuous_continuous_for; last exact: Wf.
+by move=> ?; exact: ectsW.
 Qed.
 
 (* A convenient notion that is in between compactness in
-   {family compact, X -> y} and compactness in {ptws X -> y}. *)
-Definition pointwise_precompact (W : set (X -> Y)):=
-  forall x, precompact [set (f x) | f in W].
+   {family compact, X -> y} and compactness in {ptws X -> y}.*)
+Definition pointwise_precompact {I} (W : set I) (d : I -> X -> Y) :=
+  forall x, precompact [set (d i x) | i in W].
 
-Lemma pointwise_precomact_subset (W V : set (X -> Y)) :
-  W `<=` V -> pointwise_precompact V -> pointwise_precompact W.
+Lemma pointwise_precompact_subset {I J} (W : set I) (V : set J) {fW : I -> X -> Y} {fV : J -> X -> Y}:
+  fW @` W `<=` fV @` V -> pointwise_precompact V fV -> 
+  pointwise_precompact W fW.
 Proof.
-move=> WsubV + x => /(_ x) pcptV.
-by apply: precompact_subset pcptV; exact: image_subset.
+move=> WsubV + x => /(_ x) pcptV; apply: precompact_subset pcptV => y [i Wi <-].
+by case: (WsubV (fW i)); [exists i | move=> j Vj <-; exists j].
 Qed.
 
-Lemma pointwise_precompact_precompact (W : set {ptws X -> Y}):
-  pointwise_precompact W -> precompact W.
+Lemma pointwise_precompact_precompact {I} (W : set I) (fW : I -> (X -> Y)) :
+  pointwise_precompact W fW -> precompact ((fW @` W) : set {ptws X -> Y}).
 Proof.
-rewrite precompactE => ptwsPreW; pose K := fun x => closure [set f x | f in W].
+rewrite precompactE => ptwsPreW. 
+pose K := fun x => closure [set fW i x | i in W].
 set R := [set f : {ptws X -> Y} | forall x : X, K x (f x)].
 have C : compact R.
-  by apply: tychonoff => x; rewrite -precompactE; exact: ptwsPreW.
+  by apply: tychonoff => x; rewrite -precompactE; move: ptwsPreW; exact.
 apply: (subclosed_compact _ C); first exact: closed_closure.
-have WsubR : W `<=` R.
-  by move=> f Wf x; rewrite /R /K closure_limit_point; left; exists f.
-rewrite closureE; apply: smallest_sub (compact_closed _ C) WsubR.
+have WsubR : (fW @` W) `<=` R.
+  move=> f Wf x; rewrite /R /K closure_limit_point; left. 
+  by case: Wf => i ? <-; exists i.
+rewrite closureE;  apply: smallest_sub (compact_closed _ C) WsubR. 
 exact: hausdorff_product.
 Qed.
 
@@ -5970,14 +6085,111 @@ by move=> Q Fq; apply: (ptws_cvg_compact_family _ Fh).
 Qed.
 
 Lemma compact_pointwise_precompact (W : set (X -> Y)) :
-  compact (W : set {family compact, X -> Y}) -> pointwise_precompact W.
+  compact (W : set {family compact, X -> Y}) -> pointwise_precompact W id.
 Proof.
 move=> cptFamW x; pose V : set Y := prod_topo_apply x @` W.
-rewrite precompactE (_ : [set f x | f in W] = V ) //.
+rewrite precompactE (_ : [set f x | f in W] = V ) ?image_id //.
 suff: (compact V) by move=> /[dup]/(compact_closed hsdf)/closure_id <-.
 apply: (@continuous_compact _ _  (prod_topo_apply x)).
   by apply: continuous_subspaceT => f ?; exact: prod_topo_apply_continuous.
 exact: uniform_pointwise_compact.
 Qed.
 
+Lemma ptws_cvg_entourage (x : X) (f : {ptws X -> Y}) E :
+  entourage E -> \forall g \near f, E (f x, g x).
+Proof.
+move=> entE; have : ({ptws, nbhs f --> f}) by [].
+rewrite ptws_cvg_family_singleton => /fam_cvgP /(_ [set x]).
+rewrite uniform_set1 => /(_ _ (to_set E (f x))); apply; first by exists x.
+by move: E entE; exact/cvg_entourageP.
+Qed.
+
+Lemma equicontinuous_closure (W : set {ptws X -> Y}) :
+  equicontinuous W id -> equicontinuous (closure W) id.
+Proof.
+move=> ectsW => x E entE; near=> y => f clWf.
+near (within W (nbhs (f : {ptws X -> Y}))) => g.
+near: g; rewrite near_withinE; near_simpl; near=> g => Wg.
+apply: (@entourage_split _ (g x)) => //.
+  exact: (near (ptws_cvg_entourage _ _ _)).
+apply: (@entourage_split _ (g y)) => //; first exact: (near (@ectsW x _ _)).
+by apply/entourage_sym; exact: (near (ptws_cvg_entourage _ _ _)).
+Unshelve. all: by end_near. Qed.
+
+Definition small_ent_sub := @small_set_sub _ _ (@entourage Y).
+
+Lemma ptws_compact_cvg (W : set {ptws X -> Y}) F (f : {ptws X -> Y}) :
+  equicontinuous W id -> ProperFilter F -> F W ->
+  {ptws, F --> f} <-> {family compact, F --> f}.
+Proof.
+move=> + PF; wlog Wf : f W / W f.
+  move=> + /equicontinuous_closure ? FW => /(_ f (closure W)) Q.
+  split => Ff; last exact: ptws_cvg_compact_family.
+  apply Q => //; last by apply: (filterS _ FW); exact: subset_closure.
+  by rewrite closureEcvg; exists F; [|split] => // ? /filterS; apply.
+move=> ectsW FW; split=> [ptwsF|]; last exact: ptws_cvg_compact_family.
+apply/fam_cvgP => K ? U /=; rewrite uniform_nbhs => [[E [? EsubU]]].
+suff : \forall g \near within W (nbhs f), forall y, K y -> E (f y, g y).
+  rewrite near_withinE; near_simpl => N; apply: (filter_app _ _ FW).
+  by apply ptwsF; near=> g => ?; apply EsubU; apply: (near N g).
+near (powerset_filter_from (@entourage Y)) => E'.
+have entE' : entourage E' by exact: (near (near_small_set _)).
+pose Q := fun (h : X -> Y) x => E' (f x, h x).
+apply: (@near_compact_covering _ _ _ Q) => //.
+  by move=> y Ky; apply: (@cvg_within _ (nbhs f)); exact: ptws_cvg_entourage.
+move=> x; near_simpl; near=> y g => /= E'fxgx.
+apply: (@entourage_split _ (f x)) => //.
+  apply entourage_sym; apply: (near (small_ent_sub _) E') => //.
+  exact: (near (ectsW x E' entE') y).
+apply: (@entourage_split _ (g x)) => //.
+  exact: (near (small_ent_sub _) E').
+apply: (near (small_ent_sub _) E') => //.
+  apply: (near (ectsW x E' entE')) => //.
+  exact: (near (withinT _ (nbhs_filter f))).
+Unshelve. all: end_near. Qed.
+
+Lemma ptws_compact_closed (W : set (X -> Y)) :
+  equicontinuous W id ->
+  closure (W : set {family compact, X -> Y}) =
+  closure (W : set {ptws X -> Y}).
+Proof.
+rewrite ?closureEcvg // predeqE => ? ?.
+split; move=> [F PF [Fx WF]]; (exists F; last split) => //.
+  by apply/(@ptws_compact_cvg W )=>//; exact: WF.
+by apply/(@ptws_compact_cvg W)=>//; exact: WF.
+Qed.
+
+Lemma ascoli_forward (W : set (X -> Y)) :
+  pointwise_precompact W id ->
+  equicontinuous W id ->
+  precompact (W : set {family compact, X -> Y }).
+Proof.
+move=> /pointwise_precompact_precompact + ectsW.
+rewrite ?precompactE compact_ultra compact_ultra ptws_compact_closed => //.
+move=> /= + F UF FcW => /(_ F UF); rewrite image_id; case => // p [cWp Fp].
+exists p; split => //; apply/(ptws_compact_cvg _ _ _ FcW) => //.
+exact: equicontinuous_closure.
+Qed.
+
+Lemma compact_equicontinuous (W : set {family compact, X -> Y}) :
+  locally_compact (@setT X) ->
+  (forall f, W f -> continuous f) ->
+  compact (W : set {family compact, X -> Y}) ->
+  equicontinuous W id.
+Proof.
+move=> lcptX ctsW cptW x E entE.
+have [//|U UWx [cptU clU]] := lcptX x; rewrite withinET in UWx.
+near (powerset_filter_from (@entourage Y)) => E'.
+have entE' : entourage E' by exact: (near (near_small_set _)).
+pose Q := fun (y : X) (f : {family compact, X -> Y}) => E' (f x, f y).
+apply: (@near_compact_covering _ _ _ Q) => // f; rewrite /Q; near_simpl.
+  by move=> Wf; apply: ((ctsW f Wf x) (to_set _ _)); exact: nbhs_entourage.
+near=> g y => /= fxfy; apply: (@entourage_split _ (f x)) => //.
+  apply/entourage_sym; apply: (near (small_ent_sub _) E') => //.
+  exact: (near (fam_nbhs _ entE' (@compact_set1 _ x)) g) => //.
+apply: (@entourage_split _ _) => //; apply: (near (small_ent_sub _) E') => //.
+  exact: fxfy.
+by apply (near (fam_nbhs _ entE' cptU) g) => //; exact: (near UWx y).
+Unshelve. all: end_near. Qed.
+
 End ArzelaAscoli.

From 638320e3759a65354f29ed3d7fae00d5a1354203 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Sun, 3 Apr 2022 22:23:01 -0400
Subject: [PATCH 2/7] basic cantor set stuff

cantor hausdorff

trying to prove false
---
 _CoqProject       |   1 +
 theories/cantor.v | 211 ++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 212 insertions(+)
 create mode 100644 theories/cantor.v

diff --git a/_CoqProject b/_CoqProject
index b18763da0e..8d3f0fd526 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -35,6 +35,7 @@ theories/lebesgue_integral.v
 theories/summability.v
 theories/functions.v
 theories/signed.v
+theories/cantor.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v
diff --git a/theories/cantor.v b/theories/cantor.v
new file mode 100644
index 0000000000..b45c950861
--- /dev/null
+++ b/theories/cantor.v
@@ -0,0 +1,211 @@
+(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
+From mathcomp Require Import interval rat.
+Require Import mathcomp_extra boolp classical_sets signed functions cardinality.
+Require Import reals ereal topology normedtype landau sequences.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+Import numFieldTopology.Exports.
+Local Open Scope classical_set_scope.
+Definition principle_filter {X} (x : X) : set (set X) := globally [set x].
+
+Lemma principle_filterP {X} (x : X) (W : set X) : 
+  principle_filter x W <-> W x.
+Proof.
+rewrite /principle_filter/globally /=; split => //=; first exact.
+by move=>? ? ->.
+Qed.
+
+Lemma principle_filter_proper {X} (x : X) : ProperFilter (principle_filter x).
+Proof. exact: globally_properfilter. Qed.
+
+Canonical bool_discrete_filter := FilteredType bool bool (principle_filter).
+ 
+Program Definition discrete_topological_mixin {X : pointedType} :
+  Topological.mixin_of (principle_filter) := @topologyOfFilterMixin
+    X principle_filter principle_filter_proper _ _.
+Next Obligation. by move=> ???/principle_filterP. Qed.
+Next Obligation. 
+  move=> ???/principle_filterP?. 
+  exact/principle_filterP/principle_filterP.
+Qed.
+
+Canonical bool_discrete_topology := 
+    TopologicalType bool (@discrete_topological_mixin _).
+
+
+Lemma compactU {X : topologicalType} (A B : set X) : 
+  compact A -> compact B -> compact (A `|` B).
+Proof.
+rewrite ?compact_ultra=> cptA cptB F UF FAB; rewrite setIUl.
+case: (in_ultra_setVsetC A); first by move=>/cptA [x ?]; exists x; left.
+move=> /(filterI FAB); rewrite setIUl setIv set0U => FBA.
+have : F B by apply: (filterS _ FBA); exact: subIsetr.
+by move=> /cptB [x ?]; exists x; right.
+Qed.
+
+Lemma bool2E : [set: bool] = [set true; false].
+Proof.  by rewrite eqEsubset; split => //= [[]] //= _;[left|right]. Qed.
+
+Lemma bool_compact : compact [set: bool].
+Proof. by rewrite bool2E; apply compactU; exact: compact_set1. Qed.
+
+Lemma open_bool (b : bool): open [set b].
+Proof. by rewrite /open /= /open_of_nbhs => ? /= -> //=. Qed.
+
+Lemma bool_discrete_hausdorff : hausdorff_space bool_discrete_topology.
+Proof.
+move=> p q => //= /(_ [set p] [set q]) //=; case.
+- exact: open_bool.
+- exact: open_bool.
+- by move=> r //= [] ->.
+Qed.
+
+Definition cantor_space := 
+  product_topologicalType (fun (_ : nat) => bool_discrete_topology).
+
+Lemma cantor_space_compact: compact [set: cantor_space].
+Proof.
+have := (@tychonoff _ (fun (_: nat) => bool_discrete_topology) _ 
+  (fun=> bool_compact)).
+by congr (compact _) => //=; rewrite eqEsubset; split => b //=.
+Qed.
+
+Lemma cantor_space_hausdorff : hausdorff_space cantor_space.
+Proof. apply: hausdorff_product => ?; exact: bool_discrete_hausdorff. Qed.
+
+Definition min_diff (x y : cantor_space) n :=
+  x n != y n /\ (forall m, m < n -> x m == y m).
+
+Lemma cantor_space_neqP (x y : cantor_space) :
+  x != y <-> exists n, min_diff x y n.
+Proof.
+split. 
+  apply: contra_neqP=> /forallNP N; rewrite funeqE.
+  apply: (@well_founded_ind nat lt (Wf_nat.lt_wf) (fun q => x q = y q)) => n E.
+  move: (N n); apply contra_notP => xnNyn; split; first exact/eqP.
+  by move=> M Mn; apply/eqP; apply E; apply/ ssrnat.leP.
+case=> n [+ _]; apply: contraNN=> /eqP; rewrite funeqE => ?; exact/eqP.
+Qed.
+
+Definition pull (x : cantor_space) : cantor_space := fun n => x (S n).
+
+Inductive prefix (x : cantor_space) : seq bool -> Prop := 
+  | NilPrefix : prefix x nil 
+  | ConsPrefix : forall b s, b = x 0 -> prefix (pull x) s -> prefix x (b :: s)
+.
+
+Lemma prefixP (x : cantor_space) (b : bool) (s : seq bool) : 
+  prefix x (b :: s) <-> (b = x 0 /\ prefix (pull x) s).
+Proof.
+(* TODO: Why does `case` discard the nil case?*)
+split; first by move=> pxb; inversion pxb; subst; tauto.
+by move=>[??]; constructor.
+Qed.
+
+  
+
+
+
+Definition fixed_prefix (s : seq bool) (x : cantor_space) : Prop := 
+  prefix x s.
+
+Lemma empty_prefix : fixed_prefix nil = [set: cantor_space] .
+Proof. by rewrite eqEsubset; split => //= x _; constructor. Qed.
+
+Fixpoint false_extend (s : seq bool) : cantor_space :=
+  match s with 
+  | nil => (fun=> false)
+  | b :: s => (fun n => 
+    match n with 
+    | 0 => b
+    | S m => (false_extend s m)
+    end)
+  end.
+
+Lemma false_extend_prefix (s : seq bool) : fixed_prefix s (false_extend s).
+Proof.  by elim:s=> //=; [constructor | move=> ???; constructor]. Qed.
+
+Fixpoint prefix_of (x : cantor_space) (n : nat) : seq bool :=
+  match n with 
+  | 0 => nil
+  | S m => x 0 :: prefix_of (pull x) m
+  end.
+
+Lemma prefix_of_prefix (x : cantor_space) (i : nat) : fixed_prefix (prefix_of x i) x.
+Proof.
+move:x; elim i=> //=; first (by move=> ?; rewrite empty_prefix).
+by move=> n ind x /=; constructor => //=; exact: ind.
+Qed.
+
+Local Fixpoint prefix_helper (i : nat) (s : seq bool) :=
+match s with 
+| nil => [set: cantor_space]
+| b :: l => prod_topo_apply i @^-1` [set b] `&` 
+    prefix_helper (S i) l
+end.
+
+Local Lemma prefix_helper_S (s : seq bool) j x :
+    prefix_helper j s (pull x) <-> 
+    prefix_helper (j + 1) s x.
+Proof.
+move: j; elim: s => //= b l; rewrite /prod_topo_apply/pull => E; split.
+by case=> <- Q; split; rewrite -add1n ?addn0 addn1 // addnC; apply/ E.
+rewrite -add1n ?addn0 addn1 => [[]] <- Q; split => //=.
+by apply/E; rewrite addn1.
+Qed.
+
+
+Local Lemma fixed_helperE (s : seq bool) : 
+  fixed_prefix s = prefix_helper 0 s.
+Proof.
+elim:s; first by rewrite empty_prefix.
+move=> b l => //=; rewrite ?eqEsubset => E; split => x //=.
+  move=> /prefixP [-> ?]; split; first by done.
+  by rewrite -[1]add0n; apply/prefix_helper_S;  apply E.
+rewrite -[1]add0n/prod_topo_apply => [[<-]] W. 
+by constructor => //=;  apply: (proj2 E); exact/prefix_helper_S.
+Qed.
+
+Local Lemma open_fixed_prefix i (s : seq bool) : open (prefix_helper i s).
+Proof.
+move: i; elim: s; first (move=> ? //=; exact: openT).
+move=> ???? //=; apply: openI => //; apply: open_comp; last exact: open_bool.
+by move=> + _; exact: prod_topo_apply_continuous.
+Qed.
+
+Lemma open_fixed (s : seq bool) : open (fixed_prefix s).
+Proof. rewrite fixed_helperE; exact: open_fixed_prefix. Qed.
+
+Lemma negb_neqP (a b : bool) : ~~ a = b <-> a <> b.
+Proof. by case: a; case: b => //=. Qed.
+
+Lemma closed_fixed (s : seq bool) (b : bool) :  
+  ~`(fixed_prefix (b :: s)) = fixed_prefix(map negb (b :: s)).
+Proof.
+move: b; elim s => //.
+  move=> b; rewrite eqEsubset; split => x => //.
+    move=> W; constructor; last constructor.
+    by apply/negb_neqP => Q; apply W; constructor => //; constructor.
+  by move=> /prefixP [] /negb_neqP W _ /prefixP [??]; apply W.
+move=> a l IH b; rewrite eqEsubset; split => x => //.
+  move=> //= /prefixP/not_andP [/negb_neqP nbx|].
+  apply/prefixP; split=> //=. move: (IH a) => //=; rewrite eqEsubset.
+  case => + _. apply.
+
+
+Section cantor_sets.
+
+Context {R: realFieldType} {base : nat}.
+Local Open Scope ereal_scope.
+Local Open Scope ring_scope.
+Definition cantor_map (x : cantor_space) : R := 
+  lim (series (fun n => 
+    (if x n then ((base%:~R - 1) * (1/(base%:~R))^+n ) else 0) : R)).
+
+End cantor_sets.
+
+Definition cantor_ternary {R : realFieldType} := @cantor_map R 3 @` [set: cantor_space].

From 733f4a9029af683dd22f2ef9b88616f1468d1f04 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Wed, 11 May 2022 23:34:15 -0400
Subject: [PATCH 3/7] fixed prefixes are closed

---
 theories/cantor.v | 42 ++++++++++++++++++++++++------------------
 1 file changed, 24 insertions(+), 18 deletions(-)

diff --git a/theories/cantor.v b/theories/cantor.v
index b45c950861..228261500c 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -106,10 +106,6 @@ split; first by move=> pxb; inversion pxb; subst; tauto.
 by move=>[??]; constructor.
 Qed.
 
-  
-
-
-
 Definition fixed_prefix (s : seq bool) (x : cantor_space) : Prop := 
   prefix x s.
 
@@ -135,6 +131,10 @@ Fixpoint prefix_of (x : cantor_space) (n : nat) : seq bool :=
   | S m => x 0 :: prefix_of (pull x) m
   end.
 
+Lemma length_prefix_of (x : cantor_space) (n : nat) : 
+  length (prefix_of x n) = n.
+Proof.  by elim: n x => //= n IH x; congr( _ .+1); exact: IH. Qed.
+
 Lemma prefix_of_prefix (x : cantor_space) (i : nat) : fixed_prefix (prefix_of x i) x.
 Proof.
 move:x; elim i=> //=; first (by move=> ?; rewrite empty_prefix).
@@ -180,22 +180,28 @@ Qed.
 Lemma open_fixed (s : seq bool) : open (fixed_prefix s).
 Proof. rewrite fixed_helperE; exact: open_fixed_prefix. Qed.
 
-Lemma negb_neqP (a b : bool) : ~~ a = b <-> a <> b.
-Proof. by case: a; case: b => //=. Qed.
-
-Lemma closed_fixed (s : seq bool) (b : bool) :  
-  ~`(fixed_prefix (b :: s)) = fixed_prefix(map negb (b :: s)).
+Lemma fixed_prefix_unique (s1 s2 : seq bool) (x : cantor_space): 
+  length s1 = length s2 -> fixed_prefix s1 x -> fixed_prefix s2 x -> s1 = s2.
 Proof.
-move: b; elim s => //.
-  move=> b; rewrite eqEsubset; split => x => //.
-    move=> W; constructor; last constructor.
-    by apply/negb_neqP => Q; apply W; constructor => //; constructor.
-  by move=> /prefixP [] /negb_neqP W _ /prefixP [??]; apply W.
-move=> a l IH b; rewrite eqEsubset; split => x => //.
-  move=> //= /prefixP/not_andP [/negb_neqP nbx|].
-  apply/prefixP; split=> //=. move: (IH a) => //=; rewrite eqEsubset.
-  case => + _. apply.
+move: s2 x; elim s1. 
+  by move=> ? ? ? ? ?; apply sym_equal; apply List.length_zero_iff_nil.
+move=> a l1 IH [] //= b l2 x /eq_add_S lng /prefixP [] -> ? /prefixP [] -> ?. 
+by congr (_ :: _); apply: (IH _ (pull x)) => //=.
+Qed.
 
+Lemma closed_fixed (s : seq bool) : closed (fixed_prefix s).
+Proof.
+elim s; first by rewrite empty_prefix //.
+move=> b l clsFl x.
+pose B := fixed_prefix (prefix_of x ((length l) + 1)).
+move=> /(_ B) /=; case. 
+  suff: (open_nbhs x B) by rewrite open_nbhsE=> [[]].
+  by split; [exact: open_fixed | exact: prefix_of_prefix].
+move=> y [] pfy By /=; suff -> : (b :: l = (prefix_of x (length l + 1))).
+  exact: prefix_of_prefix.
+apply: (@fixed_prefix_unique _ _ y) => //=. 
+by rewrite length_prefix_of addn1.
+Qed.
 
 Section cantor_sets.
 

From 57287536be83452ac3dba2f8161a62a98dc8d83a Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Sun, 29 May 2022 12:21:44 -0400
Subject: [PATCH 4/7] working on metric

---
 theories/cantor.v | 157 +++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 142 insertions(+), 15 deletions(-)

diff --git a/theories/cantor.v b/theories/cantor.v
index 228261500c..03d343470c 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -77,20 +77,6 @@ Qed.
 Lemma cantor_space_hausdorff : hausdorff_space cantor_space.
 Proof. apply: hausdorff_product => ?; exact: bool_discrete_hausdorff. Qed.
 
-Definition min_diff (x y : cantor_space) n :=
-  x n != y n /\ (forall m, m < n -> x m == y m).
-
-Lemma cantor_space_neqP (x y : cantor_space) :
-  x != y <-> exists n, min_diff x y n.
-Proof.
-split. 
-  apply: contra_neqP=> /forallNP N; rewrite funeqE.
-  apply: (@well_founded_ind nat lt (Wf_nat.lt_wf) (fun q => x q = y q)) => n E.
-  move: (N n); apply contra_notP => xnNyn; split; first exact/eqP.
-  by move=> M Mn; apply/eqP; apply E; apply/ ssrnat.leP.
-case=> n [+ _]; apply: contraNN=> /eqP; rewrite funeqE => ?; exact/eqP.
-Qed.
-
 Definition pull (x : cantor_space) : cantor_space := fun n => x (S n).
 
 Inductive prefix (x : cantor_space) : seq bool -> Prop := 
@@ -158,7 +144,6 @@ rewrite -add1n ?addn0 addn1 => [[]] <- Q; split => //=.
 by apply/E; rewrite addn1.
 Qed.
 
-
 Local Lemma fixed_helperE (s : seq bool) : 
   fixed_prefix s = prefix_helper 0 s.
 Proof.
@@ -203,6 +188,148 @@ apply: (@fixed_prefix_unique _ _ y) => //=.
 by rewrite length_prefix_of addn1.
 Qed.
 
+Section cantor_space_metric.
+
+Definition is_min_diff (x y : cantor_space) (n : nat) : Prop :=
+  x n != y n /\ (forall m, m < n -> x m == y m).
+
+Lemma is_min_diff_sym (x y : cantor_space) (n : nat) : 
+  is_min_diff x y n <-> is_min_diff y x n.
+Proof.
+by split; move=> [? W]; (split; first by rewrite eq_sym) => m; rewrite eq_sym; exact: W.
+Qed.
+
+Lemma is_min_diff_unique (x y : cantor_space) (m n : nat) : 
+  is_min_diff x y n -> is_min_diff x y m  -> n = m.
+Proof.
+wlog : n m / (n <= m).
+  case (leqP n m); first by (move=> ? + ? ?; exact).
+  by move=> ? W ? ?; apply sym_equal; apply W => //; exact: ltnW.
+move=> W [neqN minN] [neqM minM]; apply/eqTleqif; first exact/leqif_geq.
+by case (leqP m n)=> // => /minM; move/negP: neqN.
+Qed.
+
+Lemma cantor_space_neqP (x y : cantor_space) :
+  x != y -> exists n, is_min_diff x y n.
+Proof.
+apply: contra_neqP=> /forallNP N; rewrite funeqE.
+apply: (@well_founded_ind nat lt (Wf_nat.lt_wf) (fun q => x q = y q)) => n E.
+move: (N n); apply contra_notP => /eqP; split => // M Mn; apply/eqP; apply E. 
+exact/ ssrnat.leP.
+Qed.
+
+Definition min_diff (x y : cantor_space) : nat :=
+  if pselect (x != y) is left neq
+  then (projT1 (cid ((@cantor_space_neqP x y) neq)))
+  else 0
+.
+
+Lemma min_diff_sym (x y : cantor_space) : 
+  min_diff x y = min_diff y x.
+Proof.
+rewrite /min_diff; case (eqVneq x y); first by move=> ->.
+move=> /[dup]; rewrite {2} eq_sym; (do 2 (case: pselect => //)).
+move=> ? ? ? ?; apply: (@is_min_diff_unique x y); first exact: projT2.
+by apply is_min_diff_sym; exact: projT2.
+Qed.
+
+Lemma min_diff_is_min_diff (x y : cantor_space) : 
+  x != y -> is_min_diff x y (min_diff x y).
+Proof. rewrite/ min_diff; case pselect => // ? ?; exact: projT2. Qed.
+
+
+Lemma min_diff_le (x y : cantor_space) (n : nat) : 
+  x != y ->
+  (forall m, m < n -> x m == y m) ->  n <= min_diff x y.
+Proof.
+move=> neq W. 
+have [_] := (@min_diff_is_min_diff x y neq).
+apply: projT2.
+rewrite /cantor_dist; case: (eqVneq x y) => //=; first by move=> ->.
+by rewrite min_diff_sym.
+Qed.
+
+Context {R : realType}.
+
+Definition cantor_dist (x y : cantor_space) : R := 
+  (if pselect (x != y) is left neq
+  then (((min_diff x y).+1)%:~R)^-1 else 0)%R.
+Proof.
+
+Lemma cantor_dist_sym (x y : cantor_space) : 
+  cantor_dist x y = cantor_dist y x.
+Proof.
+rewrite /cantor_dist; case: (eqVneq x y) => //=; first by move=> ->.
+by rewrite min_diff_sym.
+Qed.
+
+Lemma cantor_dist_refl (x : cantor_space) : 
+  cantor_dist x x = (0)%R.
+Proof.
+by rewrite /cantor_dist; case pselect => //= ?; exact: (@contra_neqP _ x x).
+Qed.
+
+Lemma cantor_dist_pos (x y : cantor_space) : 
+  (x != y -> 0 < (cantor_dist x y))%R.
+Proof.
+rewrite /cantor_dist; case pselect => //= ? _.
+by rewrite invr_gt0 => //; rewrite ltr0z.
+Qed.
+ 
+Lemma cantor_dist_nneg (x y : cantor_space) : (0 <= cantor_dist x y)%R.
+Proof.
+case E : (x != y); first by apply ltW; exact: cantor_dist_pos.
+by move/negbT/negPn/eqP: E => ->; rewrite cantor_dist_refl.
+Qed.
+
+Lemma foo (x y z : cantor_space) : 
+  Order.min (min_diff x y) (min_diff y z) <= min_diff x z .
+Proof.
+wlog yzLe : x y z / (min_diff x y <= min_diff y z).
+    case/orP: (@leq_total (min_diff y z) (min_diff x y)).
+    move=> ? E2; rewrite minC.
+    rewrite (min_diff_sym x z) (min_diff_sym y z) (min_diff_sym x y).
+    by apply: E2 => //=; rewrite (min_diff_sym y x) (min_diff_sym z y).
+  by move=> /[swap]; apply.
+rewrite min_l //.
+Search (Order.min) (Order.le).
+
+Lemma cantor_dist_triangle (x y z : cantor_space) : 
+  (cantor_dist x z <= cantor_dist x y + cantor_dist y z)%R.
+Proof.
+wlog yzLe : x y z / (min_diff x y <= min_diff y z).
+    case/orP: (@leq_total (min_diff y z) (min_diff x y)).
+    move=> ? E2; rewrite addrC.
+    rewrite (cantor_dist_sym x z) (cantor_dist_sym y z) (cantor_dist_sym x y).
+    by apply: E2 => //=; rewrite (min_diff_sym y x) (min_diff_sym z y).
+  by move=> /[swap]; apply.
+rewrite {1}/cantor_dist; case pselect; last first.
+  move=>/negP/negPn/eqP ->; apply addr_ge0; exact: cantor_dist_nneg.
+move=> xz; rewrite {1}/cantor_dist; case pselect; last first.
+  move=>/negP/negPn/eqP <-; rewrite add0r; rewrite /cantor_dist. 
+  by case pselect.
+move=> xy; rewrite /cantor_dist; case pselect; last first.
+  by move=>/negP/negPn/eqP ->; rewrite addr0.
+move=> yz. 
+
+  case: (min_diff y z < min_diff x y)
+
+Search ( negbK).
+by rewrite /cantor_dist; case pselect => //= ?; exact: (@contra_neqP _ x x).
+Qed.
+
+
+Definition cantor_ball (r : realType) (x : cantor_space) : set (cantor_space) := 
+  projT1 ((archimed r)).
+  
+Print Num.archimedean_axiom.
+Search "archim".
+
+Definition cantor_space_pseudo_metric : 
+  PseudoMetric.mixin_of R (@entourage_ R cantor_space cantor_space (ball_ (fun x => cantor_norm x))).
+
+End cantor_space_metric.
+
 Section cantor_sets.
 
 Context {R: realFieldType} {base : nat}.

From c14ac71ee07565a8dc1436476baf56cc1ba62cfe Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 30 May 2022 00:50:23 -0400
Subject: [PATCH 5/7] ugly proofs, but helpful facts

---
 theories/cantor.v | 232 +++++++++++++++++++++++++++++++++++-----------
 1 file changed, 180 insertions(+), 52 deletions(-)

diff --git a/theories/cantor.v b/theories/cantor.v
index 03d343470c..e0a522e7ca 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -79,11 +79,61 @@ Proof. apply: hausdorff_product => ?; exact: bool_discrete_hausdorff. Qed.
 
 Definition pull (x : cantor_space) : cantor_space := fun n => x (S n).
 
+Lemma pull_projection_preimage (n : nat) (b : bool) : 
+  pull @^-1` (prod_topo_apply n @^-1` [set b]) = prod_topo_apply (n.+1) @^-1` [set b].
+Proof.  by rewrite eqEsubset; split=> x /=; rewrite /prod_topo_apply /pull /=. Qed.
+
+Lemma continuous_pull : continuous pull.
+move=> x; apply/ cvg_sup; first by apply: fmap_filter; case: (nbhs_filter x).
+move=> n; apply/cvg_image; first by apply: fmap_filter; case: (nbhs_filter x).
+  by rewrite eqEsubset; split=> u //= _; exists (fun=> u).
+move=> W.
+have Q: nbhs [set[set f n | f in A] | A in pull x @[x --> x]] [set pull x n].
+  exists (prod_topo_apply n @^-1` [set (pull x n)]); first last.
+    rewrite eqEsubset; split => u //=; first by  by case=> ? <- <-.
+    move->; exists (pull x) => //=.
+  apply: open_nbhs_nbhs; split.
+    rewrite pull_projection_preimage; apply: open_comp; last exact: open_bool.
+    by move=> + _; apply: prod_topo_apply_continuous.
+  done.
+have [] := (@subset_set2 _ W true false). 
+- by rewrite -bool2E; exact: subsetT.
+- by move=> ->; rewrite /nbhs /= => /principle_filterP.
+- by move -> => /= /nbhs_singleton <-; exact Q.
+- by move -> => /= /nbhs_singleton <-; exact Q.
+- rewrite -bool2E => -> _; exists setT; last by rewrite eqEsubset; split.
+  by rewrite /= preimage_setT; exact: filterT.
+Qed.
+
 Inductive prefix (x : cantor_space) : seq bool -> Prop := 
   | NilPrefix : prefix x nil 
   | ConsPrefix : forall b s, b = x 0 -> prefix (pull x) s -> prefix x (b :: s)
 .
 
+Fixpoint prefix_of (x : cantor_space) (n : nat) : seq bool :=
+  match n with 
+  | 0 => nil
+  | S m => x 0 :: prefix_of (pull x) m
+  end.
+
+Definition fixed_prefix (s : seq bool) (x : cantor_space) : Prop := 
+  prefix x s.
+
+(*
+Lemma prefix_near (x : cantor_space) (n: nat): 
+  \forall y \near x, prefix_of y n = prefix_of x n.
+Proof.
+move: x; elim: n; first by move=>?; near=> y.
+move=> n IH x; near=> y => //=; congr(_ :: _).
+  near: y; pose U := (prod_topo_apply 0 @^-1` [set (x 0)]).
+  have : open_nbhs x U.
+    (split; last by []); apply: open_comp => //=; last exact: open_bool.
+    by move=> + _; exact: prod_topo_apply_continuous.
+  by rewrite open_nbhsE => [[_]].
+by near: y; near_simpl; have /continuous_pull := (IH (pull x)); exact.
+Unshelve. all: end_near. Qed.
+*)
+
 Lemma prefixP (x : cantor_space) (b : bool) (s : seq bool) : 
   prefix x (b :: s) <-> (b = x 0 /\ prefix (pull x) s).
 Proof.
@@ -92,41 +142,74 @@ split; first by move=> pxb; inversion pxb; subst; tauto.
 by move=>[??]; constructor.
 Qed.
 
-Definition fixed_prefix (s : seq bool) (x : cantor_space) : Prop := 
-  prefix x s.
-
 Lemma empty_prefix : fixed_prefix nil = [set: cantor_space] .
 Proof. by rewrite eqEsubset; split => //= x _; constructor. Qed.
 
-Fixpoint false_extend (s : seq bool) : cantor_space :=
-  match s with 
-  | nil => (fun=> false)
-  | b :: s => (fun n => 
-    match n with 
-    | 0 => b
-    | S m => (false_extend s m)
-    end)
-  end.
 
-Lemma false_extend_prefix (s : seq bool) : fixed_prefix s (false_extend s).
-Proof.  by elim:s=> //=; [constructor | move=> ???; constructor]. Qed.
+Lemma prefix_of_prefix (x : cantor_space) (i : nat) : 
+  fixed_prefix (prefix_of x i) x.
+Proof.
+move:x; elim i=> //=; first (by move=> ?; rewrite empty_prefix).
+by move=> n ind x /=; constructor => //=; exact: ind.
+Qed.
 
-Fixpoint prefix_of (x : cantor_space) (n : nat) : seq bool :=
-  match n with 
-  | 0 => nil
-  | S m => x 0 :: prefix_of (pull x) m
-  end.
+Lemma fixed_prefixP (x y : cantor_space) (j : nat) : 
+  fixed_prefix (prefix_of x j) y <->
+  (forall i, i < j -> x i = y i).
+Proof.
+split.
+  move=> + i; move: x y i; elim: j => //= j IH x y; case; first by move=> /prefixP [].
+  by move=> i /prefixP [_ ?] ?; rewrite -/(pull x i) -/(pull y i); exact: IH.
+move: x y; elim: j; first by move=> ? ? ?; rewrite empty_prefix.
+move=> n IH x y xy; apply/prefixP; split; first by apply: xy.
+by apply: IH => ? ?; apply: xy.
+Qed.
 
-Lemma length_prefix_of (x : cantor_space) (n : nat) : 
-  length (prefix_of x n) = n.
-Proof.  by elim: n x => //= n IH x; congr( _ .+1); exact: IH. Qed.
+Lemma fixed_prefixW (x y : cantor_space) (i j : nat) : 
+  i < j ->
+  fixed_prefix (prefix_of x j) y ->
+  fixed_prefix (prefix_of x i) y.
+Proof.
+move=> ij /fixed_prefixP P; apply/fixed_prefixP=> k ?; apply: P.
+exact: (ltn_trans _ ij).
+Qed.
 
-Lemma prefix_of_prefix (x : cantor_space) (i : nat) : fixed_prefix (prefix_of x i) x.
+Lemma prefix_cvg (x : cantor_space) : 
+  filter_from [set: nat] (fun n => fixed_prefix (prefix_of x n)) --> x.
 Proof.
-move:x; elim i=> //=; first (by move=> ?; rewrite empty_prefix).
-by move=> n ind x /=; constructor => //=; exact: ind.
+have ? : Filter (filter_from [set: nat] (fun n => fixed_prefix(prefix_of x n))).
+  apply: filter_from_filter; first by exists 0.
+  move=> i j _ _; exists (i + j) => //.
+  move: x j; elim: i => //= i; first by move=> ?; rewrite empty_prefix setTI add0n.
+  move=> IH x j /=; rewrite -addnE => z /prefixP [] x0z0 /IH [??].
+  split; first by apply/prefixP; split => //.
+  by apply: (@fixed_prefixW _ _ _ (j.+1)) => //=; apply/prefixP; split.
+apply/cvg_sup => n; apply/cvg_image; first by (rewrite eqEsubset; split).
+move=> W /=; rewrite /nbhs /= => /principle_filterP Wxn.
+have [] := (@subset_set2 _ W true false). 
+- by rewrite -bool2E; exact: subsetT.
+- by move: Wxn => /[swap] ->.
+- move: Wxn => /[swap] -> <-; exists (fixed_prefix (prefix_of x (n.+1))); first by exists (n.+1).
+  rewrite eqEsubset; split => y; last (move=> -> /=; exists x => //=; exact: (prefix_of_prefix x (n.+1))).
+  by case=> z /fixed_prefixP/(_ n) P <-; simpl; apply/sym_equal/P.
+- move: Wxn => /[swap] -> <-; exists (fixed_prefix (prefix_of x (n.+1))); first by exists (n.+1).
+  rewrite eqEsubset; split => y; last (move=> -> /=; exists x => //=; exact: (prefix_of_prefix x (n.+1))).
+  by case=> z /fixed_prefixP/(_ n) P <-; simpl; apply/sym_equal/P.
+- rewrite -bool2E => ->; exists setT; last by rewrite eqEsubset; split.
+  exact: filterT.
 Qed.
 
+Lemma cantor_nbhs_prefix (x : cantor_space) (W : set cantor_space) : 
+  nbhs x W -> exists n, fixed_prefix (prefix_of x n) `<=` W.
+Proof.
+move=> nbhsW; move: (@prefix_cvg x _ nbhsW) => /=; rewrite nbhs_simpl.
+by case=> n _ ?; exists n.
+Qed.
+
+Lemma length_prefix_of (x : cantor_space) (n : nat) : 
+  length (prefix_of x n) = n.
+Proof.  by elim: n x => //= n IH x; congr( _ .+1); exact: IH. Qed.
+
 Local Fixpoint prefix_helper (i : nat) (s : seq bool) :=
 match s with 
 | nil => [set: cantor_space]
@@ -188,6 +271,7 @@ apply: (@fixed_prefix_unique _ _ y) => //=.
 by rewrite length_prefix_of addn1.
 Qed.
 
+
 Section cantor_space_metric.
 
 Definition is_min_diff (x y : cantor_space) (n : nat) : Prop :=
@@ -200,7 +284,7 @@ by split; move=> [? W]; (split; first by rewrite eq_sym) => m; rewrite eq_sym; e
 Qed.
 
 Lemma is_min_diff_unique (x y : cantor_space) (m n : nat) : 
-  is_min_diff x y n -> is_min_diff x y m  -> n = m.
+  is_min_diff x y n -> is_min_diff x y m -> n = m.
 Proof.
 wlog : n m / (n <= m).
   case (leqP n m); first by (move=> ? + ? ?; exact).
@@ -237,23 +321,22 @@ Lemma min_diff_is_min_diff (x y : cantor_space) :
   x != y -> is_min_diff x y (min_diff x y).
 Proof. rewrite/ min_diff; case pselect => // ? ?; exact: projT2. Qed.
 
-
 Lemma min_diff_le (x y : cantor_space) (n : nat) : 
   x != y ->
-  (forall m, m < n -> x m == y m) ->  n <= min_diff x y.
+  (forall m, m < n -> x m == y m) -> n <= min_diff x y.
 Proof.
-move=> neq W. 
-have [_] := (@min_diff_is_min_diff x y neq).
-apply: projT2.
-rewrite /cantor_dist; case: (eqVneq x y) => //=; first by move=> ->.
-by rewrite min_diff_sym.
+move=> xneqy; elim: n => // n IH Q.
+have: n <= min_diff x y by apply: IH=> ??; apply: Q; rewrite ltnS; apply ltnW.
+rewrite leq_eqVlt=> /orP; case => //.
+move: Q => /[swap] /eqP -> /(_ (min_diff x y) (ltnSn _)) /eqP. 
+by have [+ _ ?] := min_diff_is_min_diff xneqy => /eqP ?.
 Qed.
 
 Context {R : realType}.
 
 Definition cantor_dist (x y : cantor_space) : R := 
   (if pselect (x != y) is left neq
-  then (((min_diff x y).+1)%:~R)^-1 else 0)%R.
+  then (GRing.natmul (GRing.one R) ((min_diff x y).+1))^-1 else 0)%R.
 Proof.
 
 Lemma cantor_dist_sym (x y : cantor_space) : 
@@ -273,7 +356,6 @@ Lemma cantor_dist_pos (x y : cantor_space) :
   (x != y -> 0 < (cantor_dist x y))%R.
 Proof.
 rewrite /cantor_dist; case pselect => //= ? _.
-by rewrite invr_gt0 => //; rewrite ltr0z.
 Qed.
  
 Lemma cantor_dist_nneg (x y : cantor_space) : (0 <= cantor_dist x y)%R.
@@ -282,17 +364,25 @@ case E : (x != y); first by apply ltW; exact: cantor_dist_pos.
 by move/negbT/negPn/eqP: E => ->; rewrite cantor_dist_refl.
 Qed.
 
-Lemma foo (x y z : cantor_space) : 
+Lemma min_diff_trans (x y z : cantor_space) : 
+  (x != y) -> 
+  (y != z) -> 
+  (x != z) -> 
   Order.min (min_diff x y) (min_diff y z) <= min_diff x z .
 Proof.
 wlog yzLe : x y z / (min_diff x y <= min_diff y z).
-    case/orP: (@leq_total (min_diff y z) (min_diff x y)).
-    move=> ? E2; rewrite minC.
+  case/orP: (@leq_total (min_diff y z) (min_diff x y)).
+    move=> ? E2; rewrite minC => ? ? ?.
     rewrite (min_diff_sym x z) (min_diff_sym y z) (min_diff_sym x y).
-    by apply: E2 => //=; rewrite (min_diff_sym y x) (min_diff_sym z y).
+    apply: E2; try (rewrite eq_sym //). 
+    by rewrite (min_diff_sym y x) (min_diff_sym z y).
   by move=> /[swap]; apply.
-rewrite min_l //.
-Search (Order.min) (Order.le).
+rewrite min_l // => ???; apply: min_diff_le => // m mLe. 
+have [ // | _ /(_ _ mLe) /eqP -> ] := @min_diff_is_min_diff x y _.
+have [ // | _ ] := @min_diff_is_min_diff y z; apply.
+rewrite leq_eqVlt in yzLe; case/orP: yzLe; first by move=>/eqP <-.
+by apply ltn_trans.
+Qed.
 
 Lemma cantor_dist_triangle (x y z : cantor_space) : 
   (cantor_dist x z <= cantor_dist x y + cantor_dist y z)%R.
@@ -310,23 +400,61 @@ move=> xz; rewrite {1}/cantor_dist; case pselect; last first.
   by case pselect.
 move=> xy; rewrite /cantor_dist; case pselect; last first.
   by move=>/negP/negPn/eqP ->; rewrite addr0.
-move=> yz. 
+move=> yz.
+have := (@min_diff_trans x y z xy yz xz); rewrite min_l // => lexz.
+Search (GRing.natmul) (GRing.inv).
+rewrite -ler_pinv ?invrK; first last.
+  + rewrite inE; apply/andP; split;[rewrite unitfE; apply: lt0r_neq0|]; exact: gt0.
+  + rewrite inE; apply/andP; split;[rewrite unitfE; apply: lt0r_neq0|]; exact: gt0.
+rewrite -[w in (w + _)%R]div1r -[w in (_ + w)%R]div1r. 
+rewrite GRing.addf_div ?mul1r; first last. 
+  + apply: lt0r_neq0; exact: gt0.
+  + apply: lt0r_neq0; exact: gt0.
+rewrite invf_div ler_pdivr_mulr; first last.
+  + exact: gt0.
+rewrite -natrD -?natrM ler_nat mulnDr.
+apply: (@leq_trans  (S(min_diff x z) * S(min_diff y z))).
+  rewrite leq_pmul2r //=.
+apply leq_addr.
+Qed.
 
-  case: (min_diff y z < min_diff x y)
+Check entourage_.
+Definition cantor_ball (x : cantor_space) (eps : R) (y : cantor_space) : Prop := 
+  (cantor_dist x y < eps)%R.
 
-Search ( negbK).
-by rewrite /cantor_dist; case pselect => //= ?; exact: (@contra_neqP _ x x).
+Definition cantor_ball_center (x : cantor_space) (e : R) : 
+  (0 < e)%R -> cantor_ball x e x.
+Proof. by move=> ?; rewrite /cantor_ball cantor_dist_refl. Qed.
+
+Definition cantor_ball_sym (x y : cantor_space) (e : R) : 
+  cantor_ball x e y -> cantor_ball y e x.
+Proof. by rewrite /cantor_ball cantor_dist_sym. Qed.
+
+Definition cantor_ball_triangle (x y z : cantor_space) (e1 e2 : R) : 
+  cantor_ball x e1 y -> cantor_ball y e2 z -> cantor_ball x (e1 + e2) z.
+Proof. 
+rewrite /cantor_ball => L1 L2. 
+by apply: (le_lt_trans (@cantor_dist_triangle x y z)); exact: ltr_add.
 Qed.
 
+Definition cantor_space_pseudo_metric_mixin : 
+  (@PseudoMetric.mixin_of R cantor_space (entourage_ cantor_ball)) :=
+  PseudoMetricMixin cantor_ball_center cantor_ball_sym cantor_ball_triangle erefl.
+
+Lemma cantor_space_uniformity : nbhs = nbhs_ (entourage_ cantor_ball).
+Proof.
+rewrite funeqE=> x; rewrite eqEsubset; split=> W /=.
+Qed.
+
+Program Definition cantor_space_uniformity_mixin := 
+  uniformityOfBallMixin cantor_space_uniformity cantor_space_pseudo_metric_mixin.
+
+Canonical cantor_space_uniform := 
+  UniformType cantor_space cantor_space_uniformity_mixin.
 
-Definition cantor_ball (r : realType) (x : cantor_space) : set (cantor_space) := 
-  projT1 ((archimed r)).
-  
-Print Num.archimedean_axiom.
-Search "archim".
+Canonical cantor_space_pseudo_metric := 
+  PseudoMetricType cantor_space cantor_space_pseudo_metric_mixin.
 
-Definition cantor_space_pseudo_metric : 
-  PseudoMetric.mixin_of R (@entourage_ R cantor_space cantor_space (ball_ (fun x => cantor_norm x))).
 
 End cantor_space_metric.
 

From 34b31b34de9385df9a24a22c782de7d4f0c007ab Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 30 May 2022 01:13:19 -0400
Subject: [PATCH 6/7] done with most of the convergence stuff

---
 theories/cantor.v | 85 ++++++++++++++---------------------------------
 1 file changed, 25 insertions(+), 60 deletions(-)

diff --git a/theories/cantor.v b/theories/cantor.v
index e0a522e7ca..7d90990922 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -119,21 +119,6 @@ Fixpoint prefix_of (x : cantor_space) (n : nat) : seq bool :=
 Definition fixed_prefix (s : seq bool) (x : cantor_space) : Prop := 
   prefix x s.
 
-(*
-Lemma prefix_near (x : cantor_space) (n: nat): 
-  \forall y \near x, prefix_of y n = prefix_of x n.
-Proof.
-move: x; elim: n; first by move=>?; near=> y.
-move=> n IH x; near=> y => //=; congr(_ :: _).
-  near: y; pose U := (prod_topo_apply 0 @^-1` [set (x 0)]).
-  have : open_nbhs x U.
-    (split; last by []); apply: open_comp => //=; last exact: open_bool.
-    by move=> + _; exact: prod_topo_apply_continuous.
-  by rewrite open_nbhsE => [[_]].
-by near: y; near_simpl; have /continuous_pull := (IH (pull x)); exact.
-Unshelve. all: end_near. Qed.
-*)
-
 Lemma prefixP (x : cantor_space) (b : bool) (s : seq bool) : 
   prefix x (b :: s) <-> (b = x 0 /\ prefix (pull x) s).
 Proof.
@@ -199,54 +184,31 @@ have [] := (@subset_set2 _ W true false).
   exact: filterT.
 Qed.
 
-Lemma cantor_nbhs_prefix (x : cantor_space) (W : set cantor_space) : 
+Lemma nbhs_prefix (x : cantor_space) (W : set cantor_space) : 
   nbhs x W -> exists n, fixed_prefix (prefix_of x n) `<=` W.
-Proof.
-move=> nbhsW; move: (@prefix_cvg x _ nbhsW) => /=; rewrite nbhs_simpl.
-by case=> n _ ?; exists n.
-Qed.
+Proof. by move=> /prefix_cvg => /=; case=> n _ ?; exists n. Qed.
 
-Lemma length_prefix_of (x : cantor_space) (n : nat) : 
-  length (prefix_of x n) = n.
-Proof.  by elim: n x => //= n IH x; congr( _ .+1); exact: IH. Qed.
-
-Local Fixpoint prefix_helper (i : nat) (s : seq bool) :=
-match s with 
-| nil => [set: cantor_space]
-| b :: l => prod_topo_apply i @^-1` [set b] `&` 
-    prefix_helper (S i) l
-end.
-
-Local Lemma prefix_helper_S (s : seq bool) j x :
-    prefix_helper j s (pull x) <-> 
-    prefix_helper (j + 1) s x.
+Lemma prefix_nbhs (x : cantor_space) (n : nat) : 
+  nbhs x (fixed_prefix (prefix_of x n)).
 Proof.
-move: j; elim: s => //= b l; rewrite /prod_topo_apply/pull => E; split.
-by case=> <- Q; split; rewrite -add1n ?addn0 addn1 // addnC; apply/ E.
-rewrite -add1n ?addn0 addn1 => [[]] <- Q; split => //=.
-by apply/E; rewrite addn1.
-Qed.
-
-Local Lemma fixed_helperE (s : seq bool) : 
-  fixed_prefix s = prefix_helper 0 s.
-Proof.
-elim:s; first by rewrite empty_prefix.
-move=> b l => //=; rewrite ?eqEsubset => E; split => x //=.
-  move=> /prefixP [-> ?]; split; first by done.
-  by rewrite -[1]add0n; apply/prefix_helper_S;  apply E.
-rewrite -[1]add0n/prod_topo_apply => [[<-]] W. 
-by constructor => //=;  apply: (proj2 E); exact/prefix_helper_S.
-Qed.
+move: x; elim: n => //=; first by move=>?; rewrite empty_prefix; exact: filterT.
+move=> n IH x; near=> y; apply/prefixP; split.
+  apply/sym_equal.
+  near: y; near_simpl.
+  have : open_nbhs (x : cantor_space) (prod_topo_apply 0 @^-1` [set (x 0)]).
+    (split; last by []); apply: open_comp => //=; last exact: open_bool.
+    by move=> + _; exact: prod_topo_apply_continuous.
+  by rewrite open_nbhsE => [[_]]. 
+by near: y; near_simpl; have /continuous_pull := (IH (pull x)); exact.
+Unshelve. all: end_near. Qed.
 
-Local Lemma open_fixed_prefix i (s : seq bool) : open (prefix_helper i s).
+Lemma open_fixed (x : cantor_space) (n : nat) : 
+  open (fixed_prefix (prefix_of x n)).
 Proof.
-move: i; elim: s; first (move=> ? //=; exact: openT).
-move=> ???? //=; apply: openI => //; apply: open_comp; last exact: open_bool.
-by move=> + _; exact: prod_topo_apply_continuous.
-Qed.
-
-Lemma open_fixed (s : seq bool) : open (fixed_prefix s).
-Proof. rewrite fixed_helperE; exact: open_fixed_prefix. Qed.
+rewrite openE => z /fixed_prefixP xz; near=> y.
+apply/fixed_prefixP => i W; rewrite xz //; move: i W; apply/fixed_prefixP.
+by near: y; apply: prefix_nbhs.
+Unshelve. all: end_near. Qed.
 
 Lemma fixed_prefix_unique (s1 s2 : seq bool) (x : cantor_space): 
   length s1 = length s2 -> fixed_prefix s1 x -> fixed_prefix s2 x -> s1 = s2.
@@ -257,6 +219,10 @@ move=> a l1 IH [] //= b l2 x /eq_add_S lng /prefixP [] -> ? /prefixP [] -> ?.
 by congr (_ :: _); apply: (IH _ (pull x)) => //=.
 Qed.
 
+Lemma length_prefix_of (x : cantor_space) (n : nat) : 
+  length (prefix_of x n) = n.
+Proof.  by elim: n x => //= n IH x; congr( _ .+1); exact: IH. Qed.
+
 Lemma closed_fixed (s : seq bool) : closed (fixed_prefix s).
 Proof.
 elim s; first by rewrite empty_prefix //.
@@ -271,7 +237,6 @@ apply: (@fixed_prefix_unique _ _ y) => //=.
 by rewrite length_prefix_of addn1.
 Qed.
 
-
 Section cantor_space_metric.
 
 Definition is_min_diff (x y : cantor_space) (n : nat) : Prop :=
@@ -443,7 +408,7 @@ Definition cantor_space_pseudo_metric_mixin :
 
 Lemma cantor_space_uniformity : nbhs = nbhs_ (entourage_ cantor_ball).
 Proof.
-rewrite funeqE=> x; rewrite eqEsubset; split=> W /=.
+  (*this is the only part left*)
 Qed.
 
 Program Definition cantor_space_uniformity_mixin := 

From 99323b2168778e0c5c4920476bd540b1f7c53ae9 Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Mon, 30 May 2022 13:04:16 -0400
Subject: [PATCH 7/7] cantor space metric proof

---
 theories/cantor.v | 236 +++++++++++++++++++++-------------------------
 1 file changed, 105 insertions(+), 131 deletions(-)

diff --git a/theories/cantor.v b/theories/cantor.v
index 7d90990922..980b2e5c3c 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -64,21 +64,70 @@ move=> p q => //= /(_ [set p] [set q]) //=; case.
 - by move=> r //= [] ->.
 Qed.
 
+#[global] Hint Resolve bool_discrete_hausdorff : core.
+
 Definition cantor_space := 
   product_topologicalType (fun (_ : nat) => bool_discrete_topology).
 
 Lemma cantor_space_compact: compact [set: cantor_space].
 Proof.
-have := (@tychonoff _ (fun (_: nat) => bool_discrete_topology) _ 
-  (fun=> bool_compact)).
+have := (@tychonoff _ (fun (_: nat) => _) _ (fun=> bool_compact)).
 by congr (compact _) => //=; rewrite eqEsubset; split => b //=.
 Qed.
 
 Lemma cantor_space_hausdorff : hausdorff_space cantor_space.
 Proof. apply: hausdorff_product => ?; exact: bool_discrete_hausdorff. Qed.
 
+Definition common_prefix (n : nat) (x y : cantor_space) :=
+  (forall i, i < n -> x i == y i).
+
 Definition pull (x : cantor_space) : cantor_space := fun n => x (S n).
 
+Lemma common_prefixS (n : nat) (x y : cantor_space) :
+  common_prefix n.+1 x y <-> x 0 == y 0 /\ common_prefix n (pull x) (pull y).
+Proof.
+split; last by case=> ?? []. 
+by (move=> cmn; split; first exact: cmn) => i ?; apply: cmn.
+Qed.
+
+Lemma empty_prefix (x : cantor_space) : common_prefix 0 x = setT .
+Proof. by rewrite eqEsubset; split. Qed.
+
+Lemma prefix_of_prefix (x : cantor_space) (n : nat) : 
+  common_prefix n x x.
+Proof. by move=> ?. Qed.
+
+Lemma fixed_prefixW (x : cantor_space) (i j : nat) : 
+  i < j ->
+  common_prefix j x `<=` common_prefix i x.
+Proof. by move=> ij y + q ?; apply; apply: (ltn_trans _ ij). Qed.
+
+Lemma prefix_cvg (x : cantor_space) : 
+  filter_from [set: nat] (common_prefix^~ x) --> x.
+Proof.
+have ? : Filter (filter_from [set: nat] (common_prefix^~ x)).
+  apply: filter_from_filter; first by exists 0.
+  move=> i j _ _; exists (i.+1 + j.+1) => //; rewrite -[x in x `<=` _]setIid. 
+  by apply: setISS; apply: fixed_prefixW; [exact: ltn_addr| exact: ltn_addl].
+apply/cvg_sup => n; apply/cvg_image; first by (rewrite eqEsubset; split).
+move=> W /=; rewrite /nbhs /= => /principle_filterP.
+have [] := (@subset_set2 _ W true false). 
+- by rewrite -bool2E; exact: subsetT.
+- by move ->.
+- move => -> <-; exists (common_prefix (n.+1) x); first by exists (n.+1).
+  rewrite eqEsubset; split => y; first by case=> z P <-; apply/sym_equal/eqP/P.
+  by move=> ->; exists x => //=; exact: (prefix_of_prefix x (n.+1)).
+- move => -> <-; exists (common_prefix (n.+1) x); first by exists (n.+1).
+  rewrite eqEsubset; split => y; first by case=> z P <-; apply/sym_equal/eqP/P.
+  by move=> ->; exists x => //=; exact: (prefix_of_prefix x (n.+1)).
+- rewrite -bool2E => ->; exists setT; last by rewrite eqEsubset; split.
+  exact: filterT.
+Qed.
+
+Lemma nbhs_prefix (x : cantor_space) (W : set cantor_space) : 
+  nbhs x W -> exists n, common_prefix n x `<=` W.
+Proof. by move=> /prefix_cvg => /=; case=> n _ ?; exists n. Qed.
+
 Lemma pull_projection_preimage (n : nat) (b : bool) : 
   pull @^-1` (prod_topo_apply n @^-1` [set b]) = prod_topo_apply (n.+1) @^-1` [set b].
 Proof.  by rewrite eqEsubset; split=> x /=; rewrite /prod_topo_apply /pull /=. Qed.
@@ -105,142 +154,41 @@ have [] := (@subset_set2 _ W true false).
   by rewrite /= preimage_setT; exact: filterT.
 Qed.
 
-Inductive prefix (x : cantor_space) : seq bool -> Prop := 
-  | NilPrefix : prefix x nil 
-  | ConsPrefix : forall b s, b = x 0 -> prefix (pull x) s -> prefix x (b :: s)
-.
-
-Fixpoint prefix_of (x : cantor_space) (n : nat) : seq bool :=
-  match n with 
-  | 0 => nil
-  | S m => x 0 :: prefix_of (pull x) m
-  end.
-
-Definition fixed_prefix (s : seq bool) (x : cantor_space) : Prop := 
-  prefix x s.
-
-Lemma prefixP (x : cantor_space) (b : bool) (s : seq bool) : 
-  prefix x (b :: s) <-> (b = x 0 /\ prefix (pull x) s).
+Lemma open_prefix (x : cantor_space) (n : nat) : 
+  open (common_prefix n x).
 Proof.
-(* TODO: Why does `case` discard the nil case?*)
-split; first by move=> pxb; inversion pxb; subst; tauto.
-by move=>[??]; constructor.
-Qed.
-
-Lemma empty_prefix : fixed_prefix nil = [set: cantor_space] .
-Proof. by rewrite eqEsubset; split => //= x _; constructor. Qed.
-
-
-Lemma prefix_of_prefix (x : cantor_space) (i : nat) : 
-  fixed_prefix (prefix_of x i) x.
-Proof.
-move:x; elim i=> //=; first (by move=> ?; rewrite empty_prefix).
-by move=> n ind x /=; constructor => //=; exact: ind.
-Qed.
-
-Lemma fixed_prefixP (x y : cantor_space) (j : nat) : 
-  fixed_prefix (prefix_of x j) y <->
-  (forall i, i < j -> x i = y i).
-Proof.
-split.
-  move=> + i; move: x y i; elim: j => //= j IH x y; case; first by move=> /prefixP [].
-  by move=> i /prefixP [_ ?] ?; rewrite -/(pull x i) -/(pull y i); exact: IH.
-move: x y; elim: j; first by move=> ? ? ?; rewrite empty_prefix.
-move=> n IH x y xy; apply/prefixP; split; first by apply: xy.
-by apply: IH => ? ?; apply: xy.
-Qed.
-
-Lemma fixed_prefixW (x y : cantor_space) (i j : nat) : 
-  i < j ->
-  fixed_prefix (prefix_of x j) y ->
-  fixed_prefix (prefix_of x i) y.
-Proof.
-move=> ij /fixed_prefixP P; apply/fixed_prefixP=> k ?; apply: P.
-exact: (ltn_trans _ ij).
-Qed.
-
-Lemma prefix_cvg (x : cantor_space) : 
-  filter_from [set: nat] (fun n => fixed_prefix (prefix_of x n)) --> x.
-Proof.
-have ? : Filter (filter_from [set: nat] (fun n => fixed_prefix(prefix_of x n))).
-  apply: filter_from_filter; first by exists 0.
-  move=> i j _ _; exists (i + j) => //.
-  move: x j; elim: i => //= i; first by move=> ?; rewrite empty_prefix setTI add0n.
-  move=> IH x j /=; rewrite -addnE => z /prefixP [] x0z0 /IH [??].
-  split; first by apply/prefixP; split => //.
-  by apply: (@fixed_prefixW _ _ _ (j.+1)) => //=; apply/prefixP; split.
-apply/cvg_sup => n; apply/cvg_image; first by (rewrite eqEsubset; split).
-move=> W /=; rewrite /nbhs /= => /principle_filterP Wxn.
-have [] := (@subset_set2 _ W true false). 
-- by rewrite -bool2E; exact: subsetT.
-- by move: Wxn => /[swap] ->.
-- move: Wxn => /[swap] -> <-; exists (fixed_prefix (prefix_of x (n.+1))); first by exists (n.+1).
-  rewrite eqEsubset; split => y; last (move=> -> /=; exists x => //=; exact: (prefix_of_prefix x (n.+1))).
-  by case=> z /fixed_prefixP/(_ n) P <-; simpl; apply/sym_equal/P.
-- move: Wxn => /[swap] -> <-; exists (fixed_prefix (prefix_of x (n.+1))); first by exists (n.+1).
-  rewrite eqEsubset; split => y; last (move=> -> /=; exists x => //=; exact: (prefix_of_prefix x (n.+1))).
-  by case=> z /fixed_prefixP/(_ n) P <-; simpl; apply/sym_equal/P.
-- rewrite -bool2E => ->; exists setT; last by rewrite eqEsubset; split.
-  exact: filterT.
-Qed.
-
-Lemma nbhs_prefix (x : cantor_space) (W : set cantor_space) : 
-  nbhs x W -> exists n, fixed_prefix (prefix_of x n) `<=` W.
-Proof. by move=> /prefix_cvg => /=; case=> n _ ?; exists n. Qed.
-
-Lemma prefix_nbhs (x : cantor_space) (n : nat) : 
-  nbhs x (fixed_prefix (prefix_of x n)).
-Proof.
-move: x; elim: n => //=; first by move=>?; rewrite empty_prefix; exact: filterT.
-move=> n IH x; near=> y; apply/prefixP; split.
-  apply/sym_equal.
-  near: y; near_simpl.
-  have : open_nbhs (x : cantor_space) (prod_topo_apply 0 @^-1` [set (x 0)]).
+move: x; elim: n; first by move=>?; rewrite empty_prefix; exact: openT.
+move=> n IH x; rewrite openE=> z /common_prefixS [/eqP x0z0] cmn; near=> y. 
+apply/common_prefixS; split. 
+  apply/eqP; rewrite x0z0; apply: sym_equal; near: y; near_simpl.
+  have : open_nbhs (z : cantor_space) (prod_topo_apply 0 @^-1` [set (z 0)]).
     (split; last by []); apply: open_comp => //=; last exact: open_bool.
     by move=> + _; exact: prod_topo_apply_continuous.
-  by rewrite open_nbhsE => [[_]]. 
-by near: y; near_simpl; have /continuous_pull := (IH (pull x)); exact.
-Unshelve. all: end_near. Qed.
-
-Lemma open_fixed (x : cantor_space) (n : nat) : 
-  open (fixed_prefix (prefix_of x n)).
-Proof.
-rewrite openE => z /fixed_prefixP xz; near=> y.
-apply/fixed_prefixP => i W; rewrite xz //; move: i W; apply/fixed_prefixP.
-by near: y; apply: prefix_nbhs.
+  by rewrite open_nbhsE => [[_]].
+by near: y; by move: (IH (pull x)); rewrite openE => /(_ _ cmn)/continuous_pull.
 Unshelve. all: end_near. Qed.
 
-Lemma fixed_prefix_unique (s1 s2 : seq bool) (x : cantor_space): 
-  length s1 = length s2 -> fixed_prefix s1 x -> fixed_prefix s2 x -> s1 = s2.
-Proof.
-move: s2 x; elim s1. 
-  by move=> ? ? ? ? ?; apply sym_equal; apply List.length_zero_iff_nil.
-move=> a l1 IH [] //= b l2 x /eq_add_S lng /prefixP [] -> ? /prefixP [] -> ?. 
-by congr (_ :: _); apply: (IH _ (pull x)) => //=.
-Qed.
-
-Lemma length_prefix_of (x : cantor_space) (n : nat) : 
-  length (prefix_of x n) = n.
-Proof.  by elim: n x => //= n IH x; congr( _ .+1); exact: IH. Qed.
-
-Lemma closed_fixed (s : seq bool) : closed (fixed_prefix s).
+Lemma closed_fixed  (x : cantor_space) (n : nat) : closed (common_prefix n x).
 Proof.
-elim s; first by rewrite empty_prefix //.
-move=> b l clsFl x.
-pose B := fixed_prefix (prefix_of x ((length l) + 1)).
-move=> /(_ B) /=; case. 
-  suff: (open_nbhs x B) by rewrite open_nbhsE=> [[]].
-  by split; [exact: open_fixed | exact: prefix_of_prefix].
-move=> y [] pfy By /=; suff -> : (b :: l = (prefix_of x (length l + 1))).
-  exact: prefix_of_prefix.
-apply: (@fixed_prefix_unique _ _ y) => //=. 
-by rewrite length_prefix_of addn1.
+move: x; elim: n; first by move=> ?; rewrite empty_prefix; exact: closedT.
+move=> n IH x.
+pose B1 := pull @^-1` common_prefix n (pull x).
+pose B2 := prod_topo_apply 0 @^-1` [set x 0].
+suff <- : B1 `&` B2 = common_prefix n.+1 x.
+  apply: closedI; apply: closed_comp.
+  - move=> + _; exact: continuous_pull.
+  - exact: IH.
+  - move=> + _; exact: prod_topo_apply_continuous.
+  - by apply: compact_closed => //; exact: compact_set1.
+rewrite eqEsubset; split => y /=; rewrite common_prefixS; case=> P Q. 
+(split => //; first (by apply/eqP)). 
+by move/eqP: P.
 Qed.
 
 Section cantor_space_metric.
 
 Definition is_min_diff (x y : cantor_space) (n : nat) : Prop :=
-  x n != y n /\ (forall m, m < n -> x m == y m).
+  x n != y n /\ common_prefix n x y.
 
 Lemma is_min_diff_sym (x y : cantor_space) (n : nat) : 
   is_min_diff x y n <-> is_min_diff y x n.
@@ -287,8 +235,7 @@ Lemma min_diff_is_min_diff (x y : cantor_space) :
 Proof. rewrite/ min_diff; case pselect => // ? ?; exact: projT2. Qed.
 
 Lemma min_diff_le (x y : cantor_space) (n : nat) : 
-  x != y ->
-  (forall m, m < n -> x m == y m) -> n <= min_diff x y.
+  x != y -> common_prefix n x y -> n <= min_diff x y.
 Proof.
 move=> xneqy; elim: n => // n IH Q.
 have: n <= min_diff x y by apply: IH=> ??; apply: Q; rewrite ltnS; apply ltnW.
@@ -402,13 +349,41 @@ rewrite /cantor_ball => L1 L2.
 by apply: (le_lt_trans (@cantor_dist_triangle x y z)); exact: ltr_add.
 Qed.
 
+Definition cantor_ball_prefix (x : cantor_space) (n : nat) (eps: R) : 
+  ((GRing.natmul (GRing.one R) (n.+1))^-1 <= eps)%R ->
+  common_prefix n.+1 x `<=` cantor_ball x eps.
+Proof.
+move=> bign y cmn; apply: (lt_le_trans _ bign).
+rewrite /cantor_dist; case pselect => //= xy.
+rewrite -ltr_pinv ?invrK; first last.
+  + rewrite inE; apply/andP; split;[rewrite unitfE; apply: lt0r_neq0|]; exact: gt0.
+  + rewrite inE; apply/andP; split;[rewrite unitfE; apply: lt0r_neq0|]; exact: gt0.
+rewrite ltr_nat; suff : (n < min_diff x y) by [].
+by apply: min_diff_le.
+Qed.
+
 Definition cantor_space_pseudo_metric_mixin : 
   (@PseudoMetric.mixin_of R cantor_space (entourage_ cantor_ball)) :=
   PseudoMetricMixin cantor_ball_center cantor_ball_sym cantor_ball_triangle erefl.
 
 Lemma cantor_space_uniformity : nbhs = nbhs_ (entourage_ cantor_ball).
 Proof.
-  (*this is the only part left*)
+rewrite funeqE => x; rewrite eqEsubset; split => W.
+  move=> /nbhs_prefix [n cmnN]; exists [set h | common_prefix n h.1 h.2] => //=.
+  exists ((GRing.natmul (GRing.one R) (n.+1))^-1)%R => //= [[p q]] /=.
+  rewrite /cantor_ball/cantor_dist. 
+  case: pselect; last by move=>/negP/negPn/eqP -> ?; exact: prefix_of_prefix.
+  move=> pq /=; rewrite ltr_pinv; first last.
+  + rewrite inE; apply/andP; split;[rewrite unitfE; apply: lt0r_neq0|]; exact: gt0.
+  + rewrite inE; apply/andP; split;[rewrite unitfE; apply: lt0r_neq0|]; exact: gt0.
+  rewrite ltr_nat => ?; apply: (@fixed_prefixW _ _ (min_diff p q)) => //.
+  by case: (min_diff_is_min_diff pq).
+case=> ent [eps] /= epsPos subent subW. 
+apply: (filterS subW); apply: (@filterS _ _ _ (cantor_ball x eps)).
+  by move=> y //= ?; apply: subent.
+case: (near_infty_natSinv_lt (PosNum epsPos))%R => n _ /(_ n) //=.
+move=> /(_ (ltac:(done)))/ltW/cantor_ball_prefix/filterS; apply.
+move: (open_prefix x (n.+1)); rewrite openE; apply; exact: prefix_of_prefix.
 Qed.
 
 Program Definition cantor_space_uniformity_mixin := 
@@ -420,7 +395,6 @@ Canonical cantor_space_uniform :=
 Canonical cantor_space_pseudo_metric := 
   PseudoMetricType cantor_space cantor_space_pseudo_metric_mixin.
 
-
 End cantor_space_metric.
 
 Section cantor_sets.