Module mathcomp.analysis.topology_theory.uniform_structure

From HB Require Import structures.
From mathcomp Require Import boot order algebra all_classical.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import topology_structure.

# Uniform Spaces This file provides uniform spaces, and their theory. It also includes complete spaces, which extends uniform in the hierarchy. ## Mathematical structures ### Uniform ``` nbhs_ ent == neighborhoods defined using entourages uniformType == interface type for uniform spaces: a type equipped with entourages The HB class is Uniform. puniformType == a pointed and uniform space entourage == set of entourages in a uniform space split_ent E == when E is an entourage, split_ent E is an entourage E' such that E' \o E' is included in E when seen as a relation countable_uniformity T == T's entourage has a countable base This is equivalent to `T` being metrizable. unif_continuous f == f is uniformly continuous entourage_ ball == entourages defined using balls ``` ## Factories ``` Nbhs_isUniform == factory to build a topological space from a mixin for a uniform space ``` ### Complete uniform spaces ``` cauchy F <-> the set of sets F is a cauchy filter (entourage definition) completeType == interface type for a complete uniform space structure The HB class is Complete. ```

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Definition { } ( : set_system (T * T')) ( : T) :=
filter_from ent (fun => xsection A x).

Lemma { } ( : set_system (T * T')) :
nbhs_ ent x = filter_from ent (fun => xsection A x).

Proof.

by []. Qed.

Local Open Scope relation_scope.

. M := {
  entourage : set_system (M * M);
  entourage_filter : Filter entourage;
  entourage_diagonal_subproof :
    forall , entourage A -> diagonal `<=` A;
  entourage_inv_subproof : forall , entourage A -> entourage A^-1;
  entourage_split_ex_subproof :
    forall , entourage A -> exists2 , entourage B & B \; B `<=` A;
  nbhsE_subproof : nbhs = nbhs_ entourage;
}.

()
.
  { of Topological T & Nbhs_isUniform_mixin T}.

()
.
  { of PointedTopological T & Nbhs_isUniform_mixin T}.

. M := {
  entourage : set_system (M * M);
  entourage_filter : Filter entourage;
  entourage_diagonal : forall , entourage A -> diagonal `<=` A;
  entourage_inv : forall , entourage A -> entourage A^-1;
  entourage_split_ex :
    forall , entourage A -> exists2 , entourage B & B \; B `<=` A;
  nbhsE : nbhs = nbhs_ entourage;
}.

Local Close Scope relation_scope.

. M.

Let ( : M) : ProperFilter (nbhs p).

Proof.

rewrite nbhsE nbhs_E; apply: filter_from_proper; last first.
by move=> A entA; exists p; apply/mem_set; apply: entourage_diagonal entA _ _.
apply: filter_from_filter.
by exists setT; exact: @filterT entourage_filter.
move=> A B entA entB; exists (A `&` B); last by rewrite xsectionI.
exact: (@filterI _ _ entourage_filter).
Qed.

Let ( : M) : nbhs p A -> A p.

Proof.

rewrite nbhsE nbhs_E => - [B entB sBpA].
by apply/sBpA/mem_set; exact: entourage_diagonal entB _ _.
Qed.

Let ( : M) : nbhs p A -> nbhs p (nbhs^~ A).

Proof.

rewrite nbhsE nbhs_E => - [B entB sBpA].
have /entourage_split_ex[C entC sC2B] := entB.
exists C => // q Cpq; rewrite nbhs_E; exists C => // r Cqr.
by apply/sBpA/mem_set/sC2B; exists q; exact/set_mem.
Qed.

..Build M
  nbhs_filter nbhs_singleton nbhs_nbhs.

..Build M
  entourage_filter entourage_diagonal entourage_inv entourage_split_ex nbhsE.

..

Local Open Scope relation_scope.

. M := {
  entourage : set_system (M * M);
  entourage_filter : Filter entourage;
  entourage_diagonal : forall , entourage A -> diagonal `<=` A;
  entourage_inv : forall , entourage A -> entourage A^-1;
  entourage_split_ex :
    forall , entourage A -> exists2 , entourage B & B \; B `<=` A;
}.

Local Close Scope relation_scope.

. M.

..Build M (nbhs_ entourage).

..Build M entourage
  entourage_filter entourage_diagonal entourage_inv entourage_split_ex erefl.

..

Lemma { : uniformType} : nbhs_ (@entourage M) = nbhs.

Proof.

by rewrite -Nbhs_isUniform_mixin.nbhsE_subproof. Qed.

Lemma { : Type} ( : X) ( : Y) :
E (x, y) <-> (E ^-1)%relation (y, x).

Proof.

by []. Qed.

Lemma { : uniformType} :
filter_from (@entourage M) (fun => xsection A x) = nbhs x.

Proof.

by rewrite -nbhs_entourageE. Qed.

Module Export .
Definition :=
(nbhs_simpl,@filter_from_entourageE,@nbhs_entourageE).
End NbhsEntourage.

Lemma { : uniformType} ( : M) : nbhs x P <-> nbhs_ entourage x P.

Proof.

by rewrite nbhs_simpl. Qed.

Lemma { : Type} ( : set_system (T * T)) :
Filter F -> Filter [set V^-1 | in F]%relation.

Proof.

move=> FF; split => /=.
- by exists [set: T * T] => //; exact: filterT.
- by move=> P Q [R FR <-] [S FS <-]; exists (R `&` S) => //; exact: filterI.
- move=> P Q PQ [R FR RP]; exists Q^-1%relation => //; first last.
by rewrite eqEsubset; split; case.
by apply: filterS FR; case=> ? ? /= ?; apply: PQ; rewrite -RP.
Qed.

Section uniformType1.
Local Open Scope relation_scope.
Context { : uniformType}.

Lemma ( : set (M * M)) : entourage A -> A (x, x).

Proof.

by move=> entA; exact: entourage_diagonal_subproof entA _ _. Qed.

Global Instance : Filter (@entourage M).

Proof.

exact: entourage_filter.
Qed.

Lemma : entourage [set: M * M].

Proof.

exact: filterT. Qed.

Lemma ( : set (M * M)) : entourage A -> entourage A^-1.

Proof.

exact: entourage_inv_subproof. Qed.

Lemma ( : set (M * M)) :
entourage A -> exists2 , entourage B & B \; B `<=` A.

Proof.

exact: entourage_split_ex_subproof. Qed.

Definition ( : set (M * M)) :=
get (entourage `&` [set | B \; B `<=` A]).

Lemma ( : set (M * M)) : entourage A ->
entourage (split_ent A) /\ split_ent A \; split_ent A `<=` A.

Proof.

by move/entourage_split_ex/exists2P/getPex. Qed.

Lemma ( : set (M * M)) : entourage A ->
entourage (split_ent A).

Proof.

by move=> /split_entP []. Qed.

Lemma ( : set (M * M)) : entourage A ->
split_ent A \; split_ent A `<=` A.

Proof.

by move=> /split_entP []. Qed.

Lemma ( : M) : entourage A ->
split_ent A (x, z) -> split_ent A (z, y) -> A (x, y).

Proof.

by move=> /subset_split_ent sA ? ?; apply: sA; exists z. Qed.

Lemma ( : M) : entourage A -> nbhs x (xsection A x).

Proof.

by move=> ?; apply/nbhsP; exists A. Qed.

Lemma ( : Filter F) ( : M) :
F --> p <-> forall , entourage A -> \forall \near F, A (p, q).

Proof.

rewrite -filter_fromP [X in filter_from _ X](_ : _ = @xsection M M ^~ p)//.
by apply/funext => E; apply/seteqP; split => [|] ? /xsectionP.
by rewrite filter_from_entourageE.
Qed.

Lemma {} { : Filter F} ( : M) :
F --> x -> forall , entourage A -> \forall \near F, A (x, y).

Proof.

by move/cvg_entourageP. Qed.

Lemma ( : T -> M) ( : Filter F) :
f @ F --> p <-> forall , entourage A -> \forall \near F, A (p, f t).

Proof.

exact: cvg_entourageP. Qed.

Lemma ( : set (M * M)) : entourage E -> entourage (E `&` E^-1).

Proof.

by move=> ?; apply: filterI; last exact: entourage_inv. Qed.

Lemma ( : set (M * M)) : entourage E -> split_ent E `<=` E.

Proof.

move=> entE; case=> x y splitxy; apply: subset_split_ent => //; exists y => //.
by apply: entourage_refl; exact: entourage_split_ent.
Qed.

End uniformType1.

Global Instance { : puniformType} :
ProperFilter (@entourage M).

Proof.

apply Build_ProperFilter_ex; last exact: entourage_filter.
by move=> A entA; exists (point, point); apply: entourage_refl.
Qed.

#[global]
Hint Extern 0 (entourage (split_ent _)) => exact: entourage_split_ent : core.
#[global]
Hint Extern 0 (entourage (get _)) => exact: entourage_split_ent : core.
#[global]
Hint Extern 0 (entourage (_^-1)%relation) => exact: entourage_inv : core.
Arguments entourage_split {M} z {x y A}.
#[global]
Hint Extern 0 (nbhs _ (xsection _ _)) => exact: nbhs_entourage : core.

Lemma { : uniformType} ( : M) : entourage E ->
closure (xsection (split_ent E) x) `<=` xsection E x.

Proof.

pose E' := (split_ent E) `&` (split_ent E)^-1%relation.
move=> entE z /(_ (xsection E' z))[].
by rewrite -nbhs_entourageE; exists E' => //; exact: filterI.
move=> y; rewrite xsectionI => -[/xsectionP xy [_ /xsectionP yz]].
by apply/xsectionP; move: xy yz; exact: entourage_split.
Qed.

Lemma { : uniformType} ( : U -> V) :
{for x, continuous f} <-> f @ x^' --> f x.

Proof.

split=> - cfx P /= fxP.
by rewrite !near_simpl; apply: cvg_within; apply: cfx.
rewrite !nbhs_nearE !near_map in fxP *; have /= := cfx P fxP.
rewrite !near_simpl near_withinE near_simpl => Pf; near=> y.
by have [->|] := eqVneq y x; [by apply: nbhs_singleton|near: y].
Unshelve. all: by end_near. Qed.

Lemma
  ( : topologicalType) ( : T -> U) ( : T) :
  {for x, continuous f} ->
  (forall , f y = f x -> y = x) -> f @ x^' --> (f x)^'.

Proof.

move=> cf fI A; rewrite /nbhs /= /dnbhs !withinE/= => -[V Vfx AV].
exists (f @^-1` V); first exact: cf Vfx.
by apply/seteqP; split=> y/=;
move/predeqP : AV => /(_ (f y))/= AV [AVfy yx];
have /contra_neq /(_ yx) := fI y; tauto.
Qed.

Definition ( : uniformType) :=
  exists : set_system (T * T), [/\
    countable R,
    R `<=` entourage &
    forall , entourage P -> exists2 , R Q & Q `<=` P].

Lemma { : uniformType} :
  countable_uniformity T <-> exists2 : nat -> set (T * T),
    (forall , entourage A -> exists , f N `<=` A) &
    (forall , entourage (f n)).

Proof.

split=> [[M []]|[f fsubE entf]].
  move=> /pfcard_geP[-> _ /(_ _ (@entourageT _))[]//|/unsquash f eM Msub].
  exists f; last by move=> n; apply: eM; exact: funS.
  by move=> ? /Msub [Q + ?] => /(@surj _ _ _ _ f)[n _ fQ]; exists n; rewrite fQ.
exists (range f); split; first exact: card_image_le.
  by move=> E [n _] <-; exact: entf.
by move=> E /fsubE [n fnA]; exists (f n) => //; exists n.
Qed.

Lemma ( : uniformType) ( : U) ( : set (U * U)) :
entourage A -> open_nbhs x (xsection A x)°.

Proof.

move=> entA; split; first exact: open_interior.
by apply: nbhs_singleton; apply: nbhs_interior; exact: nbhs_entourage.
Qed.

Definition ( : uniformType) ( : U -> V) :=
(map_pair f) @ entourage --> entourage.

Lemma ( : uniformType) ( : U -> V) :
unif_continuous f -> continuous f.

Proof.

rewrite /unif_continuous /cvg_to !nbhs_simpl => ucf.
rewrite /cvg_to /= => u X; rewrite !nbhs_simpl /= -!nbhs_entourageE.
case => Y /ucf /=; set Y' := (Y' in entourage Y') => eY' YX.
exists Y' => //.
rewrite /Y' /=.
rewrite -image_sub => v [] u' /= Yfuu' <-.
exact: YX.
Qed.

Lemma { : uniformType} ( : U -> V) ( : V -> W) :
unif_continuous f -> unif_continuous g -> unif_continuous (g \o f).

Proof.

by move=> cf cg A /cg /cf; exact. Qed.

Definition ( : uniformType) ( : set ((set U) * (set U))) :=
exists2 , entourage B & forall , A PQ -> forall ,
PQ.1 p -> PQ.2 q -> B (p,q).

Complete uniform spaces

Definition { : uniformType} ( : set_system T) := (F, F) --> entourage.

Lemma { : puniformType} ( : set_system T) : Filter F ->
[cvg F in T] -> cauchy F.

Proof.

move=> FF cvF A entA; have /entourage_split_ex [B entB sB2A] := entA.
exists (xsection (B^-1%relation) (lim F), xsection B (lim F)).
split=> /=; apply: cvF; rewrite /= -nbhs_entourageE; last by exists B.
by exists B^-1%relation => //; exact: entourage_inv.
move=> ab [/= /xsectionP Balima /xsectionP Blimb]; apply: sB2A.
by exists (lim F).
Qed.

. T := {
  cauchy_cvg :
    forall ( : set_system T), ProperFilter F -> cauchy F -> cvg F
}.

()
.
  { of Uniform T & Uniform_isComplete T & isPointed T}.

Section completeType1.

Context { : completeType}.

Lemma ( : set_system T) ( : ProperFilter F) : cauchy F <-> cvg F.

Proof.

by split=> [/cauchy_cvg|/cvg_cauchy]. Qed.

End completeType1.
Arguments cauchy_cvg {T} F {FF} _ : rename.
Arguments cauchy_cvgP {T} F {FF}.

Files

Module mathcomp.analysis.topology_theory.uniform_structure