Module mathcomp.analysis.topology_theory.pseudometric_structure

From HB Require Import structures.
From mathcomp Require Import boot order algebra archimedean all_classical.
From mathcomp Require Import interval_inference reals topology_structure.
From mathcomp Require Import uniform_structure.

# PseudoMetric Spaces This file provides pseudometric spaces, complete pseudometric spaces, and the corresponding theory. Note that a classic metric space is simply pseudometric + hausdorff. However we will make extensive use of the non-hausdorff case, such as in our proof of Urysohn's lemma. ## Mathematical structures ### PseudoMetrics ``` entourage_ ball == entourages defined using balls pseudoMetricType == interface type for pseudo metric space structure: a type equipped with balls The HB class is PseudoMetric. pseudoPMetricType == a pointed pseudoMetric space ball x e == ball of center x and radius e nbhs_ball_ ball == nbhs defined using the given balls nbhs_ball == nbhs defined using balls in a pseudometric space ``` ### Factories ``` Nbhs_isPseudoMetric == factory to build a topological space from a mixin for a pseudoMetric space ``` ### Complete Pseudometrics ``` ball_ N == balls defined by the norm/absolute value N completePseudoMetricType == interface type for a complete pseudometric space structure The HB class is CompletePseudoMetric. cauchy_ex F <-> the set of sets F is a cauchy filter (epsilon-delta definition) cauchy_ball F <-> the set of sets F is a cauchy filter (using the near notations) ``` ## Closed balls ``` closed_ball_ norm x e := [set y | norm (x - y) <= e] closed_ball == closure of a ball ```

Import Order.TTheory GRing.Theory Num.Theory.

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

#[local]
Obligation Tactic := idtac.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Definition { : numDomainType} { } ( : T -> R -> set T') :=
  @filter_from R _ [set | 0 < x] (fun => [set | ball xy.1 e xy.2]).

Lemma { : numDomainType} { } ( : T -> R -> set T') :
  entourage_ ball =
  @filter_from R _ [set | 0 < x] (fun => [set | ball xy.1 e xy.2]).

Proof.

by []. Qed.

. () M & Uniform M := {
  ball : M -> R -> M -> Prop ;
  ball_center_subproof : forall ( : R), 0 < e -> ball x e x ;
  ball_sym_subproof : forall ( : R), ball x e y -> ball y e x ;
  ball_triangle_subproof :
    forall , ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z;
  entourageE_subproof : entourage = entourage_ ball
}.

()
. () :=
  { of Uniform T & Uniform_isPseudoMetric R T}.

()
. () :=
  { of Pointed T & Uniform T & Uniform_isPseudoMetric R T}.

. () M & Nbhs M := {
  ent : set_system (M * M);
  nbhsE : nbhs = nbhs_ ent;
  ball : M -> R -> M -> Prop ;
  ball_center : forall ( : R), 0 < e -> ball x e x ;
  ball_sym : forall ( : R), ball x e y -> ball y e x ;
  ball_triangle :
    forall , ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z;
  entourageE : ent = entourage_ ball
}.

. R M.
Local Open Scope relation_scope.

Let : {homo ball x : / e1 <= e2 >-> e1 `<=` e2}.

Proof.

move=> e1 e2 le12 y xe1_y.
move: le12; rewrite le_eqVlt => /orP [/eqP <- //|].
rewrite -subr_gt0 => lt12.
rewrite -[e2](subrK e1); apply: ball_triangle xe1_y.
suff : ball x (PosNum lt12)%:num x by [].
exact: ball_center.
Qed.

Let : Filter ent.

Proof.

rewrite entourageE; apply: filter_from_filter; first by exists 1 => /=.
move=> _ _ /posnumP[e1] /posnumP[e2]; exists (Num.min e1 e2)%:num => //=.
by rewrite subsetI; split=> ?; apply: ball_le;
rewrite num_le// ge_min lexx ?orbT.
Qed.

Let : ent A -> diagonal `<=` A.

Proof.

rewrite entourageE; move=> [e egt0 sbeA] xy xey.
by apply: sbeA; rewrite /= xey; exact: ball_center.
Qed.

Let : ent A -> ent A^-1.

Proof.

rewrite entourageE => - [e egt0 sbeA].
by exists e => // xy xye; apply: sbeA; exact: ball_sym.
Qed.

Let : ent A -> exists2 , ent B & B \; B `<=` A.

Proof.

rewrite entourageE; move=> [_/posnumP[e] sbeA].
exists [set | ball xy.1 (e%:num / 2) xy.2].
by exists (e%:num / 2) => /=.
move=> xy [z xzhe zyhe]; apply: sbeA.
by rewrite [e%:num]splitr; exact: ball_triangle zyhe.
Qed.

..Build M
  entourage_filter_subproof ball_sym_subproof ball_triangle_subproof
  entourageE_subproof nbhsE.

..Build R M
  ball_center ball_sym ball_triangle entourageE.

..

Lemma { : numDomainType} { : pseudoMetricType R} :
  entourage_ (@ball R M) = entourage.

Proof.

by rewrite entourageE_subproof. Qed.

Lemma { : numDomainType} { : pseudoMetricType R} :
@filter_from R _ [set : R | 0 < x]
(fun => [set | @ball R M xy.1 e xy.2]) = entourage.

Proof.

by rewrite -entourage_ballE. Qed.

Lemma { : numDomainType} ( : pseudoMetricType R)
( : {posnum R}) : entourage [set : M * M | ball xy.1 e%:num xy.2].

Proof.

by rewrite -entourage_ballE; exists e%:num => /=. Qed.

#[global] Hint Resolve entourage_ball : core.

Definition { : numDomainType} { } ( : T -> R -> set T')
  ( : T) := @filter_from R _ [set | e > 0] (ball x).

Definition { : numDomainType} { : pseudoMetricType R} :=
  nbhs_ball_ (@ball R M).

Lemma { : numDomainType} { : pseudoMetricType R} :
  @nbhs_ball R M = nbhs.

Proof.

rewrite predeq2E => x P; rewrite -nbhs_entourageE; split.
move=> [_/posnumP[e] sbxeP]; exists [set | ball xy.1 e%:num xy.2] => //.
by move=> y /xsectionP/sbxeP.
rewrite -entourage_ballE; move=> [A [e egt0 sbeA] sAP].
by exists e => // ? ?; exact/sAP/xsectionP/sbeA.
Qed.

Lemma { : numDomainType} { : pseudoMetricType R} :
@filter_from R _ [set : R | 0 < x] (@ball R M x) = nbhs x.

Proof.

by rewrite -nbhs_ballE. Qed.

Module Export .
Definition := (nbhs_simpl,@filter_from_ballE,@nbhs_ballE).
End NbhsBall.

Lemma { : numDomainType} { : pseudoMetricType R} ( : M) :
nbhs x P <-> nbhs_ball x P.

Proof.

by rewrite nbhs_simpl. Qed.

Lemma { : numDomainType} ( : pseudoMetricType R) ( : M)
( : {posnum R}) : ball x e%:num x.

Proof.

exact: ball_center_subproof. Qed.

#[global] Hint Extern 0 (ball _ _ _) => solve[apply: ball_center] : core.

Section pseudoMetricType_numDomainType.
Context { : numDomainType} { : pseudoMetricType R}.
Implicit Types x y z : M.

Lemma ( : R) : 0 < e -> ball x e x.

Proof.

by move=> e_gt0; apply: ball_center (PosNum e_gt0). Qed.

Lemma ( : R) : ball x e y -> ball y e x.

Proof.

exact: ball_sym_subproof. Qed.

Lemma ( : R) : ball x e y = ball y e x.

Proof.

by rewrite propeqE; split; exact/ball_sym. Qed.

Lemma ( : R) :
ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z.

Proof.

exact: ball_triangle_subproof. Qed.

Lemma ( : R) : 0 < eps -> nbhs x (ball x eps).

Proof.

by move=> e0; apply/nbhs_ballP; exists eps. Qed.

Lemma ( : {posnum R}) : open_nbhs x (ball x eps%:num)°.

Proof.

split; first exact: open_interior.
by apply: nbhs_singleton; apply: nbhs_interior; exact: nbhsx_ballx.
Qed.

Lemma ( : R) : e1 <= e2 -> ball x e1 `<=` ball x e2.

Proof.

move=> le12 y. case: comparableP le12 => [lte12 _|//|//|->//].
by rewrite -[e2](subrK e1); apply/ball_triangle/ballxx; rewrite subr_gt0.
Qed.

Lemma ( : R) : 0 < eps -> \forall \near y, ball y eps y'.

Proof.

exact: nbhsx_ballx. Qed.

Lemma ( : R) : (0 < e)%R -> x^' (ball x e `\ x).

Proof.

move: e => _/posnumP[e]; rewrite /dnbhs /within /=; near=> r => ra.
split => //=; last exact/eqP.
by near: r; rewrite near_simpl; exact: near_ball.
Unshelve. all: by end_near. Qed.

Lemma {} { : Filter F} ( : M) :
F --> y <-> forall : R, 0 < eps -> \forall \near F, ball y eps y'.

Proof.

by rewrite -filter_fromP !nbhs_simpl /=. Qed.

Lemma {} { : Filter F} ( : M) :
F --> y -> forall : R, 0 < eps -> \forall \near F, ball y eps y'.

Proof.

by move/fcvg_ballP. Qed.

Lemma {} {} { : Filter F} ( : T -> M) :
f @ F --> y <-> forall : R, 0 < eps -> \forall \near F, ball y eps (f x).

Proof.

exact: fcvg_ballP. Qed.

Lemma {} {} { : Filter F} ( : T -> M) :
f @ F --> y -> forall : R, 0 < eps -> \forall \near F, ball y eps (f x).

Proof.

exact: fcvg_ball. Qed.

Lemma {} { : Filter F} ( : T -> M -> Prop) :
f `@ F --> y <->
forall : R, 0 < eps -> \forall \near F, exists , f x z /\ ball y eps z.

Proof.

split=> [Fy _/posnumP[eps] |Fy P] /=; first exact/Fy/nbhsx_ballx.
move=> /nbhs_ballP[_ /posnumP[eps] subP].
rewrite near_simpl near_mapi; near=> x.
have [//|z [fxz yz]] := near (Fy _ (gt0 eps)) x.
by exists z => //; split => //; apply: subP.
Unshelve. all: end_near. Qed.

Lemma {} { : Filter F} ( : T -> M -> Prop) :
f `@ F --> y ->
forall : R, 0 < eps -> F [set | exists , f x z /\ ball y eps z].

Proof.

by move/cvgi_ballP. Qed.

End pseudoMetricType_numDomainType.

#[global] Hint Resolve nbhsx_ballx : core.

Global Instance { : numDomainType}
{ : pseudoPMetricType R} : ProperFilter (@entourage M).

Proof.

apply: Build_ProperFilter_ex; rewrite -entourage_ballE => A [_/posnumP[e] sbeA].
by exists (point, point); apply: sbeA; apply: ballxx.
Qed.

Arguments nbhsx_ballx {R M} x eps.
Arguments near_ball {R M} y eps.

Section pseudoMetricType_numFieldType.
Context { : numFieldType} { : pseudoMetricType R}.
Implicit Types x y z p : M.

Lemma ( : R) :
ball x (e / 2) z -> ball z (e / 2) y -> ball x e y.

Proof.

by move=> /ball_triangle h /h; rewrite -splitr. Qed.

Lemma ( : R) :
ball z (e / 2) x -> ball z (e / 2) y -> ball x e y.

Proof.

by move=> /ball_sym /ball_split; apply. Qed.

Lemma ( : R) :
ball x (e / 2) z -> ball y (e / 2) z -> ball x e y.

Proof.

by move=> bxz /ball_sym /(ball_split bxz). Qed.

End pseudoMetricType_numFieldType.

Lemma { : topologicalType} { : archiRealFieldType}
  { : pseudoMetricType R} ( : M -> T) ( : M) ( : T) ( : set M) :
  f @ within A (nbhs p) --> l <->
  (forall : M^nat, (forall , A (u n)) /\ u @ \oo --> p ->
    f (u n) @[ --> \oo] --> l).

Proof.

split=> [fpl u [Au up]|ful].
  move=> V Vnb.
  have := fpl _ Vnb; rewrite {1 2 4}/nbhs/= /within/= near_nbhs => Unb.
  have [N _ {}up] := up _ Unb.
  by exists N => // n /= Nn; exact: up.
apply: contrapT => fpl; move: ful; apply/existsNP.
suff: exists2 : M^nat,
    (forall , A (u k)) /\ u @ \oo --> p & ~ f (u n) @[ --> \oo] --> l.
  by move=> [x_] h; exists x_; exact/not_implyP.
have [V Vnb hV] : exists2 : set T, nbhs l V & forall : {posnum R},
    exists : M, [/\ A xn, ball xn d%:num p & ~ V (f xn)].
  apply: contrapT; apply: contra_not fpl => /forallPNP h.
  move=> V Vnb; have /existsNP[d] := h V Vnb; move/forallNP => {}h.
  rewrite nbhs_nearE near_map near_withinE; near=> t => At.
  have /not_and3P[//|bp|/contrapT //] := h t.
  exfalso; apply: bp.
  by rewrite ball_symE; near: t; rewrite !near_nbhs; apply: near_ball.
have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0.
exists (fun => sval (cid (hV (PosNum (invn n))))).
- split => [k|]; first by rewrite /sval/=; case: cid => x [].
  apply/cvg_ballP => r r0; near=> n.
  rewrite /sval/=; case: cid => x [Ax xpn _].
  rewrite ball_symE; apply: le_ball xpn.
  rewrite -(@invrK _ r) lef_pV2 ?posrE ?invr_gt0//.
  near: n; exists (Num.truncn r^-1) => // s /= rs.
  by apply/ltW; rewrite -truncn_le_nat.
- move=> /(_ V Vnb)[N _] /(_ _ (leqnn _)).
  by rewrite /sval/=; case: cid => // x [Ax xpN].
Unshelve. all: by end_near. Qed.

Lemma { : topologicalType} { : archiRealFieldType}
  { : pseudoMetricType R} ( : M -> T) ( : M) ( : T) :
  f @ p --> l <->
  (forall : M^nat, u @ \oo --> p -> f (u n) @[ --> \oo] --> l).

Proof.

rewrite -(withinET (F := nbhs p)) cvg_withinP withinET.
apply/propeqP; apply: eq_forall => u; congr (_ -> _).
by apply/propeqP; split=> [[]|].
Qed.

Section entourages.
Context { : numDomainType}.

Lemma ( : pseudoMetricType R) ( : U -> V) :
  unif_continuous f <->
  forall , e > 0 -> exists2 , d > 0 &
    forall , ball x.1 d x.2 -> ball (f x.1) e (f x.2).

Proof.

have fappF : Filter ((fun => (f xy.1, f xy.2)) @ entourage_ ball).
by rewrite entourage_ballE; apply: fmap_filter.
by rewrite /unif_continuous -!entourage_ballE filter_fromP.
Qed.

End entourages.

Lemma { : realType} { : pseudoMetricType R} :
countable_uniformity T.

Proof.

apply/countable_uniformityP.
exists (fun => [set : T * T | ball xy.1 n.+1%:R^-1 xy.2]); last first.
by move=> n; exact: (entourage_ball _ n.+1%:R^-1%:pos).
move=> E; rewrite -entourage_ballE => -[e e0 subE].
exists (Num.truncn e^-1); apply: subset_trans subE => xy; apply: le_ball.
by rewrite /= -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0// ltW// truncnS_gt.
Qed.

Specific pseudoMetric spaces

. () := isPointed.Build R 0.

Definition
  ( : numDomainType) ( : zmodType) ( : V -> R) ( : V) ( : R) :=
  [set | norm (x - y) < e].
Arguments ball_ {R} {V} norm x e%_R y /.

Lemma ( : realDomainType) ( : R) :
  ball_ Num.Def.normr x e `<=` P <->
  {in `](x - e), (x + e)[, forall , P y}.

Proof.

by split=> exP y /=; rewrite ?in_itv (ltr_distlC, =^~ltr_distlC); apply: exP.
Qed.

Lemma ( : realDomainType) ( : R) : 0 < e ->
ball_ Num.Def.normr x (2 * e) `<=` P ->
{in `[(x - e), (x + e)], forall , P y}.

Proof.

move=> e_gt0 PP y; rewrite in_itv/= -ler_distlC => ye; apply: PP => /=.
by rewrite (le_lt_trans ye)// ltr_pMl// ltr1n.
Qed.

Global Instance ( : realDomainType) ( : R) : Filter
[set | exists2 : R, 0 < i & ball_ Num.norm t i `<=` P].

Proof.

apply: Build_Filter; [by exists 1 | move=> P Q | move=> P Q PQ]; rewrite /mkset.
- move=> -[x x0 xP] [y ? yQ]; exists (Num.min x y); first by rewrite lt_min x0.
  move=> z tz; split.
    by apply: xP; rewrite /= (lt_le_trans tz) // ge_min lexx.
  by apply: yQ; rewrite /= (lt_le_trans tz) // ge_min lexx orbT.
- by move=> -[x ? xP]; exists x => //; apply: (subset_trans xP).
Qed.

#[global] Hint Extern 0 (Filter [set | exists2 , _ & ball_ _ _ i `<=` P]) =>
(apply: ball_filter) : typeclass_instances.

Section pseudoMetric_of_normedDomain.
Context { : numDomainType} { : normedZmodType K}.

Lemma ( : R) ( : K) : 0 < e -> ball_ Num.norm x e x.

Proof.

by move=> ? /=; rewrite subrr normr0. Qed.

Lemma ( : R) ( : K) :
ball_ Num.norm x e y -> ball_ Num.norm y e x.

Proof.

by rewrite /= distrC. Qed.

Lemma ( : R) ( : K) :
ball_ Num.norm x e1 y -> ball_ Num.norm y e2 z -> ball_ Num.norm x (e1 + e2) z.

Proof.

by move=> /= ? ?; rewrite -(subrKA y) (le_lt_trans (ler_normD _ _)) // ltrD.
Qed.

Lemma :
@nbhs_ball_ K R R (ball_ Num.norm) = nbhs_ (entourage_ (ball_ Num.norm)).

Proof.

rewrite /nbhs_ entourage_E predeq2E => x A; split.
  move=> [e egt0 sbeA].
  exists [set | ball_ Num.norm xy.1 e xy.2]; first by exists e.
  by move=> r /xsectionP; exact: sbeA.
by move=> [E [e egt0 sbeE] sEA]; exists e => // ? ?; exact/sEA/xsectionP/sbeE.
Qed.

End pseudoMetric_of_normedDomain.

. () := Pointed.on R^o.

()
.
  { of Complete T & PseudoPointedMetric R T}.

Definition { : numDomainType} { : pseudoMetricType R}
    ( : set_system T) :=
  forall : R, 0 < eps -> exists , F (ball x eps).

Definition { : numDomainType} { : pseudoMetricType R}
    ( : set_system T) :=
  forall , e > 0 -> \forall & \near F, ball x e y.

Lemma ( : numDomainType) (  : pseudoMetricType R)
    ( : set_system T) ( : Filter F) :
  cauchy_ball F <-> cauchy F.

Proof.

split=> cauchyF; last first.
by move=> _/posnumP[eps]; apply/cauchyF/entourage_ball.
move=> U; rewrite -entourage_ballE => - [_/posnumP[eps] xyepsU].
by near do apply: xyepsU; apply: cauchyF.
Unshelve. all: by end_near. Qed.

Arguments cauchy_ballP {R T} F {FF}.

Lemma ( : numFieldType) ( : pseudoMetricType R)
( : set_system T) ( : Filter F) :
cauchy_ex F -> cauchy F.

Proof.

move=> Fc A; rewrite !nbhs_simpl /= -entourage_ballE => -[_/posnumP[e] sdeA].
have /Fc [z /= Fze] := [gt0 of e%:num / 2]; near=> x y; apply: sdeA => /=.
by apply: (@ball_splitr _ _ z); [near: x|near: y].
Unshelve. all: by end_near. Qed.

Arguments cauchy_exP {R T} F {FF}.

Lemma ( : numFieldType) ( : pseudoMetricType R)
( : set_system T) ( : ProperFilter F) :
cauchy F <-> cauchy_ex F.

Proof.

split=> [Fcauchy _/posnumP[e] |/cauchy_exP//].
near F => x; exists x; near: x; apply: (@nearP_dep _ _ F F).
exact/Fcauchy/entourage_ball.
Unshelve. all: by end_near. Qed.

Arguments cauchyP {R T} F {PF}.

Definition { : numDomainType} { : zmodType} ( : V -> R)
( : V) ( : R) := [set | norm (x - y) <= e].

Definition { : numDomainType} { : pseudoMetricType R}
( : V) ( : R) := closure (ball x e).

Section closed_ball_lemmas.
Context { : numDomainType} { : pseudoMetricType R}.
Implicit Types (x : V) (r : R).

Lemma : closure (ball x r) = closed_ball x r.

Proof.

by []. Qed.

Lemma : 0 < r -> closed_ball x r x.

Proof.

by move=> ?; exact/subset_closure/ballxx. Qed.

Lemma : closed (closed_ball x r).

Proof.

exact: closed_closure. Qed.

Lemma : ball x r `<=` closed_ball x r.

Proof.

exact: subset_closure. Qed.

Lemma : (r1 <= r2)%O ->
closed_ball x r1 `<=` closed_ball x r2.

Proof.

by rewrite /closed_ball => le; apply/closureS/le_ball. Qed.

End closed_ball_lemmas.
#[deprecated(since="mathcomp-analysis 1.14.0", note="renamed to `closure_ballE`")]
Notation := closure_ballE (only parsing).

Lemma { : numFieldType} { : pseudoMetricType R} ( : V)
( : R) : 0 < r -> closed_ball x (r / 2) `<=` ball x r.

Proof.

move:r => _/posnumP[r] z /(_ (ball z ((r%:num/2)%:pos)%:num)) [].
exact: nbhsx_ballx.
by move=> y [+/ball_sym]; rewrite [t in ball x t z]splitr; apply: ball_triangle.
Qed.

Files

Module mathcomp.analysis.topology_theory.pseudometric_structure