Skip to content

Add displays for topologies #2143

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
nmolinamounier wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Add displays for topologies #2143

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 28 additions & 0 deletions CHANGELOG_top_displays.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
# Changelog (unreleased)

## [Unreleased]

### Added

- in `filter.v`:
+ new definition `with_fdisp`.
- in `function_spaces.v`:
+ new definitions `product_uniform_def`, `product_pseudometric_def`, `uniform_topology_def`, `fam_topology_def`.
+ new notations `pointwise_continuous` and `uniform_arrow`.
- in `subtype_topology.v`:
+ new definition `set_type_topology_def`.

### Changed

### Renamed

### Deprecated

- in `subspace_topology.v`:
+ `from_subspace` (superseded by topology displays)

### Removed

### Infrastructure

### Misc
8 changes: 4 additions & 4 deletions analysis_stdlib/Rstruct_topology.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ apply iff_sym.
have FF : Filter (f @ x)%classic.
by typeclasses eauto.
(*by apply fmap_filter; apply: @filter_filter' (locally_filter _).*)
case: (@fcvg_ballP _ _ (f @ x)%classic FF (f x)) => {FF}H1 H2.
case: (@fcvg_ballP _ _ _ (f @ x)%classic FF (f x)) => {FF}H1 H2.
(* TODO: in need for lemmas and/or refactoring of already existing lemmas (ball vs. Rabs) *)
split => [{H2} - /H1 {}H1 eps|{H1} H].
- have {H1} [//|_/posnumP[x0] Hx0] := H1 eps%:num.
Expand Down Expand Up @@ -100,7 +100,7 @@ Lemma RexpE (x : R) : Rtrigo_def.exp x = expR x.
Proof.
apply/esym; rewrite /exp /exist_exp; case: Alembert_C3 => y.
rewrite /Pser /infinite_sum /= => exp_ub.
rewrite /expR /exp_coeff /series/=; apply: (@cvg_lim R^o) => //.
rewrite /expR /exp_coeff /series/=; apply: (@cvg_lim _ R^o) => //.
rewrite -cvg_shiftS /=; apply/cvgrPdist_lt => /= e /RltP /exp_ub[N Nexp_ub].
near=> n.
have nN : (n >= N)%coq_nat by apply/ssrnat.leP; near: n; exact: nbhs_infty_ge.
Expand Down Expand Up @@ -133,13 +133,13 @@ case: exist_cos => y.
rewrite /cos_in /cos_n /infinite_sum/=.
set G : nat -> R^o := (G in sum_f_R0 G).
move=> cos_ub.
have /(@cvg_lim R^o) <- // : series G x @[x --> \oo] --> y.
have /(@cvg_lim _ R^o) <- // : series G x @[x --> \oo] --> y.
rewrite -cvg_shiftS/=; apply/cvgrPdist_lt => /= e /RltP /cos_ub[N Ncos_ub].
near=> n.
have nN : (n >= N)%coq_nat by apply/ssrnat.leP; near: n; exact: nbhs_infty_ge.
move: Ncos_ub => /(_ _ nN) /[!RdistE] /RltP /=.
by rewrite /G distrC sum_f_R0E.
apply: (@cvg_lim R^o) => //.
apply: (@cvg_lim _ R^o) => //.
suff -> : G = cos_coeff' x by exact: cvg_cos_coeff'.
apply/funext=> n; rewrite /G cos_coeff'E cos_coeffE.
rewrite odd_double/= mul1r plusE addn0 addnn Rsqr_def !RealsE.
Expand Down
2 changes: 1 addition & 1 deletion analysis_stdlib/showcase/uniform_bigO.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ Definition OuP (f : A -> R * R -> R) (g : R * R -> R) :=

(* first we replace sig with ex and the l^2 norm with the l^oo norm *)

Let normedR2 : normedModType _ := (R^o * R^o)%type.
Let normedR2 : normedModType _ _ := (R^o * R^o)%type.

Definition OuPex (f : A -> R * R -> R^o) (g : R * R -> R^o) :=
exists2 alp, 0 < alp & exists2 C, 0 < C &
Expand Down
230 changes: 156 additions & 74 deletions classical/filter.v
View file
Open in desktop

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion theories/borel_hierarchy.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ Import numFieldNormedType.Exports.
Local Open Scope classical_set_scope.

Section Gdelta_Fsigma.
Context {T : topologicalType}.
Context {d} {T : topologicalType d}.
Implicit Type S : set T.

Definition Gdelta S :=
Expand Down
43 changes: 22 additions & 21 deletions theories/cantor.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,15 +53,15 @@ HB.instance Definition _ := Nbhs.on cantor_space.
HB.instance Definition _ := Topological.on cantor_space.
HB.instance Definition _ := Uniform.on cantor_space.

Definition cantor_like (T : topologicalType) :=
Definition cantor_like d (T : topologicalType d) :=
[/\ perfect_set [set: T],
compact [set: T],
hausdorff_space T &
zero_dimensional T].

Lemma cantor_space_compact : compact [set: cantor_space].
Proof.
have := @tychonoff _ (fun _ : nat => _) _ (fun=> bool_compact).
have := @tychonoff _ _ (fun _ : nat => _) _ (fun=> bool_compact).
by congr (compact _); rewrite eqEsubset.
Qed.

Expand Down Expand Up @@ -103,7 +103,7 @@ Qed.
(* *)
(******************************************************************************)
Section topological_trees.
Context {K : nat -> pdiscreteTopologicalType} {X : ptopologicalType}
Context {d d'} {K : nat -> pdiscreteTopologicalType d} {X : ptopologicalType d'}
(refine_apx : forall n, set X -> K n -> set X)
(tree_invariant : set X -> Prop).

Expand All @@ -122,7 +122,7 @@ Hypothesis refine_separates: forall x y : X, x != y ->
Let refine_subset n U e : @refine_apx n U e `<=` U.
Proof. by rewrite [X in _ `<=` X](refine_cover n); exact: bigcup_sup. Qed.

Let T := prod_topology (K : nat -> ptopologicalType).
Let T := prod_topology (K : nat -> ptopologicalType d).

Local Fixpoint branch_apx (b : T) n :=
if n is m.+1 then refine_apx (branch_apx b m) (b m) else [set: X].
Expand Down Expand Up @@ -191,7 +191,7 @@ Proof.
elim: n => [|n IH]; first by near=> z => ?; rewrite ltn0.
near=> z => i; rewrite leq_eqVlt => /predU1P[|iSn]; last by rewrite (near IH z).
move=> [->]; near: z; exists (proj n @^-1` [set b n]).
split => //; suff : @open T (proj n @^-1` [set b n]) by [].
split => //; suff : @open _ T (proj n @^-1` [set b n]) by [].
apply: open_comp; [move=> + _; exact: proj_continuous| apply: discrete_open].
Unshelve. all: end_near. Qed.

Expand All @@ -204,7 +204,7 @@ Qed.

Let tree_map_apx b n : branch_apx b n (tree_map b).
Proof.
apply: (@closed_cvg _ _ _ (tree_map_filter b)); last exact: cvg_tree_map.
apply: (@closed_cvg _ _ _ _ (tree_map_filter b)); last exact: cvg_tree_map.
by apply: invar_cl; exact: tree_map_invar.
by exists n.
Qed.
Expand Down Expand Up @@ -257,13 +257,13 @@ End topological_trees.
(******************************************************************************)

Section TreeStructure.
Context {R : realType} {T : pseudoPMetricType R}.
Context {d} {R : realType} {T : pseudoPMetricType d R}.
Hypothesis cantorT : cantor_like T.

Let dsctT : zero_dimensional T. Proof. by case: cantorT. Qed.
Let pftT : perfect_set [set: T]. Proof. by case: cantorT. Qed.
Let cmptT : compact [set: T]. Proof. by case: cantorT. Qed.
Let hsdfT : @hausdorff_space T. Proof. by case: cantorT. Qed.
Let hsdfT : hausdorff_space T. Proof. by case: cantorT. Qed.

Let c_invar (U : set T) := clopen U /\ U !=set0.

Expand Down Expand Up @@ -292,7 +292,7 @@ Local Lemma cantor_map : exists f : cantor_space -> T,
set_surj [set: cantor_space] [set: T] f &
set_inj [set: cantor_space] f ].
Proof.
have [] := @tree_map_props (fun=> bool) T c_ind c_invar cmptT hsdfT.
have [] := @tree_map_props _ _ (fun=> bool) T c_ind c_invar cmptT hsdfT.
- move=> n V; rewrite eqEsubset; split => [t Vt|t [? ? []]//].
have [?|?] := pselect ((U_ n `&` V !=set0) /\ ~` U_ n `&` V !=set0).
+ have [Unt|Unt] := pselect (U_ n t).
Expand Down Expand Up @@ -340,8 +340,9 @@ Proof.
exists tree_map => /=.
have [cts surj inje] := projT2 (cid cantor_map); split; first exact: cts.
move=> A clA; apply: (compact_closed hsdfT).
apply: (@continuous_compact _ _ tree_map); first exact: continuous_subspaceT.
apply: (@subclosed_compact _ _ [set: cantor_space]) => //.
apply: (@continuous_compact _ _ _ _ tree_map).
exact: continuous_subspaceT.
apply: (@subclosed_compact _ _ _ [set: cantor_space]) => //.
exact: cantor_space_compact.
Qed.

Expand All @@ -364,21 +365,21 @@ HB.instance Definition _ (T : nat -> pointedType) : Pointed (tree_of T):=
HB.instance Definition _ (T : nat -> pointedType) := Uniform.on (tree_of T).

HB.instance Definition _ (T : nat -> pointedType) :
@PseudoMetric R _ :=
@PseudoMetric _ R _ :=
@PseudoMetric.on (tree_of T).

Lemma cantor_like_finite_prod (T : nat -> ptopologicalType) :
Lemma cantor_like_finite_prod d (T : nat -> ptopologicalType d) :
(forall n, finite_set [set: discrete_topology (T n)]) ->
(forall n, (exists xy : T n * T n, xy.1 != xy.2)) ->
cantor_like (tree_of T).
Proof.
move=> finiteT twoElems; split.
- exact/(@perfect_diagonal (discrete_topology \o T))/twoElems.
- exact/(@perfect_diagonal _ (discrete_topology \o T))/twoElems.
- have := tychonoff (fun n => finite_compact (finiteT n)).
set A := (X in compact X -> _).
suff : A = [set: tree_of (fun x : nat => T x)] by move=> ->.
by rewrite eqEsubset.
- apply: (@hausdorff_product _ (discrete_topology \o T)) => n.
- apply: (@hausdorff_product _ _ (discrete_topology \o T)) => n.
by apply: discrete_hausdorff; exact: discrete_space_discrete.
- apply: zero_dimension_prod => ?; apply: discrete_zero_dimension.
Qed.
Expand All @@ -389,7 +390,7 @@ End FinitelyBranchingTrees.
(* ## Part 4: Building a finitely branching tree to cover `T` *)
(******************************************************************************)
Section alexandroff_hausdorff.
Context {T : pseudoPMetricType R}.
Context {d} {T : pseudoPMetricType d R}.

Hypothesis cptT : compact [set: T].
Hypothesis hsdfT : hausdorff_space T.
Expand Down Expand Up @@ -440,7 +441,7 @@ Qed.
Let ent_balls E := projT1 (cid (ent_balls' E)).

Let count_unif' := cid2
((iffLR countable_uniformityP) (@countable_uniformity_metric _ T)).
((iffLR countable_uniformityP) (@countable_uniformity_metric _ _ T)).

Let count_unif := projT1 count_unif'.

Expand Down Expand Up @@ -495,7 +496,7 @@ Local Lemma cantor_surj_pt1 : exists2 f : Tree -> T,
Proof.
pose entn n := projT2 (cid (ent_balls' (count_unif n))).
have [ | |? []//| |? []// | |] := @tree_map_props
K T (embed_refine) (embed_invar) cptT hsdfT.
_ _ K T (embed_refine) (embed_invar) cptT hsdfT.
- move=> n U; rewrite eqEsubset; split=> [t Ut|t [? ? []]//].
have [//|_ _ _ + _] := entn n; rewrite -subTset.
move=> /(_ t I)[W cbW Wt]; exists (existT _ W cbW) => //.
Expand Down Expand Up @@ -526,15 +527,15 @@ have [ | |? []//| |? []// | |] := @tree_map_props
have [z [Dz DzE]] := Csub _ cbD.
have /ent_closure := DzE _ Dx => /(_ (ent_count_unif n))/xsectionP/ctE [_ /= Exz].
have /ent_closure := DzE _ Dy => /(_ (ent_count_unif n))/xsectionP/ctE [Ezy _].
exact: (@entourage_split T z).
exact: (@entourage_split _ T z).
by move=> f [ctsf surjf _]; exists f.
Qed.

Local Lemma cantor_surj_pt2 :
exists f : {surj [set: cantor_space] >-> [set: Tree]}, continuous f.
Proof.
have [|f [ctsf _]] := @homeomorphism_cantor_like R Tree; last by exists f.
apply: (@cantor_like_finite_prod (discrete_topology \o K)) => [n /=|n].
have [|f [ctsf _]] := @homeomorphism_cantor_like _ R Tree; last by exists f.
apply: (@cantor_like_finite_prod _ (discrete_topology \o K)) => [n /=|n].
have [//| fs _ _ _ _] := projT2 (cid (ent_balls' (count_unif n))).
suff -> : [set: {classic K' n}] =
(@projT1 (set T) _) @^-1` (projT1 (cid (ent_balls' (count_unif n)))).
Expand Down
Loading
Loading