Module mathcomp.analysis.topology_theory.metric_structure

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrint ssrnum matrix.
From mathcomp Require Import interval_inference rat interval zmodp vector.
From mathcomp Require Import fieldext falgebra archimedean finmap.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import mathcomp_extra boolp classical_sets.
From mathcomp Require Import contra reals topology_structure.
From mathcomp Require Import uniform_structure pseudometric_structure.
From mathcomp Require Import num_topology product_topology separation_axioms.

# Metric spaces ``` metricType K == metric structure with distance mdist The HB class is Metric. R^o with R : numFieldType is shown to be a metric space. The mixin PseudoMetric_isMetric extends PseudoMetric. The factor isMetric just requires a distance. ```

Unset SsrOldRewriteGoalsOrder.
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.
Local Open Scope ring_scope.

. () M & PseudoMetric K M := {
  mdist : M -> M -> K ;
  mdist_ge0 : forall , 0 <= mdist x y ;
  mdist_positivity : forall , mdist x y = 0 -> x = y;
  ballEmdist : forall , ball x d = [set | mdist x y < d]
}.

()
. () :=
  { of PseudoMetric K M & PseudoMetric_isMetric K M }.

Section metric_lemmas.
Context { : realFieldType} ( : metricType R).

Let := @mdist R T.

Lemma : dist x y = dist y x.

Proof.

apply/eqP; rewrite eq_le; apply/andP; split; rewrite leNgt; apply/negP => xy.
- have := @ball_sym _ _ y x (dist x y); rewrite !ballEmdist/= => /(_ xy).
by rewrite ltxx.
- have := @ball_sym _ _ x y (dist y x); rewrite !ballEmdist/= => /(_ xy).
by rewrite ltxx.
Qed.

Lemma : dist x x = 0.

Proof.

apply/eqP; rewrite eq_le mdist_ge0 andbT; apply/ler_addgt0Pl => /= e e0.
rewrite addr0 leNgt; apply/negP => exx.
by have := @ball_center _ _ x (PosNum e0); rewrite ballEmdist/= ltNge (ltW exx).
Qed.

Lemma : (0 < dist x y) = (x != y).

Proof.

rewrite lt_neqAle mdist_ge0 andbT.
apply/negPn/negPn => [/eqP/esym/mdist_positivity/eqP//|/eqP ->].
by rewrite mdistxx.
Qed.

Lemma : dist x z <= dist x y + dist y z.

Proof.

apply/ler_addgt0Pl => /= e e0; rewrite leNgt; apply/negP => xyz.
have := @ball_triangle _ _ y x z (dist x y + e / 2) (dist y z + e / 2).
rewrite !ballEmdist/= addrACA -splitr !ltrDl !divr_gt0// => /(_ isT isT).
by rewrite ltNge => /negP; apply; rewrite addrC ltW.
Qed.

Lemma : hausdorff_space T.

Proof.

move=> p q pq; absurd_not => qp; move: pq.
pose D := dist p q / 2; have D0 : 0 < D.
by rewrite divr_gt0// mdist_gt0.
have p2Dq : ~ ball p (dist p q) q by rewrite ballEmdist/= ltxx.
move=> /(_ (ball p _) (ball q _) (nbhsx_ballx _ _ D0) (nbhsx_ballx _ _ D0)).
move/set0P/eqP; apply; rewrite -subset0 => x [pDx /ball_sym qDx].
by have := ball_triangle pDx qDx; rewrite -splitr.
Qed.

End metric_lemmas.

. () (M : Type) & Choice M := {
  mdist : M -> M -> K ;
  mdistxx : forall , mdist x x = 0 ;
  mdist_positivity : forall , mdist x y = 0 -> x = y ;
  mdist_sym : forall , mdist x y = mdist y x ;
  mdist_triangle : forall , mdist x z <= mdist x y + mdist y z
}.

. K M.

Let ( : M) : set M := [set | mdist x y < e].

Let : set_system (M * M) := entourage_ ball.

Let ( : M) : set_system M := nbhs_ ent x.

Let : nbhs = nbhs_ ent

Proof.

by []. Qed.

..Build M nbhs.

Let ( : K) : 0 < e -> ball x e x.

Proof.

by move=> e0; rewrite /ball/= mdistxx. Qed.

Let ( : K) : ball x e y -> ball y e x.

Proof.

by rewrite /ball/= mdist_sym. Qed.

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

Proof.

by rewrite /ball/= => ? ?; rewrite (le_lt_trans (mdist_triangle y _ _))// ltrD.
Qed.

Let : ent = entourage_ ball

Proof.

by []. Qed.

..Build K M
ent nbhsE ball ball_center ball_sym ball_triangle entourageE.

Let : 0 <= mdist x y.

Proof.

rewrite -(@pmulrn_lge0 _ _ 2)// -(mdistxx x).
by rewrite (le_trans (mdist_triangle y _ _))// mdist_sym -mulr2n.
Qed.

Let : ball x d = [set | mdist x y < d]

Proof.

by []. Qed.

..Build K M
mdist_ge0 mdist_positivity ballEmdist.

..

Section numFieldType_metric.
Context { : numFieldType}.
Implicit Type x y : R.

Let := `|y - x|.

Let : 0 <= dist x y.

Proof.

exact: normr_ge0. Qed.

Let : dist x y = 0 -> x = y.

Proof.

by move/normr0_eq0/eqP; rewrite subr_eq0 => /eqP. Qed.

Let : ball x d = [set | dist x y < d].

Proof.

by apply/seteqP; split => [|]/= A; rewrite /ball/= distrC. Qed.

.
.Build R R^o dist dist_ge0 dist_positivity ballEmdist.

End numFieldType_metric.

Module .
Section metricType_numDomainType.
Context { : numDomainType} { : metricType K}.

Local Notation := (fun => [set : V | mdist x y < d]).

Lemma : ball_mdist = ball.

Proof.

by apply/funext => x; apply/funext=> d; rewrite - ballEmdist. Qed.

Local Notation := (nbhs_ball_ ball_mdist).

Lemma : nbhs_mdist = nbhs.

Proof.

apply/funext => x.
rewrite /nbhs_ball_.
rewrite -filter_from_ballE.
by rewrite -ball_mdistE.
Qed.

Lemma ( : V -> Prop) : (\near , P x) <-> nbhs_mdist x P.

Proof.

by rewrite nbhs_nbhs_mdist. Qed.

Lemma ( : V) :
filter_from (fun : K => 0 < i) (fun ( : K) ( : V) => mdist y y' < i)
= nbhs y.

Proof.

rewrite -filter_from_ballE; apply/seteqP; split => [A|A]/=.
by move=> [x x0 yxA]; exists x => //; rewrite ballEmdist.
by move=> [x x0 yxA]; exists x => //; rewrite ballEmdist in yxA.
Qed.

Let := (nbhs_simpl,@nbhs_nbhs_mdist,@filter_from_mdist_nbhs).

Lemma { : set_system V} { : Filter F} ( : V) :
F --> y <-> forall , 0 < eps -> \forall \near F, mdist y y' < eps.

Proof.

by rewrite -filter_fromP/= !nbhs_simpl. Qed.

Lemma {} { : set_system T} { : Filter F} ( : T -> V) ( : V) :
f @ F --> y <-> forall , 0 < eps -> \forall \near F, mdist y (f t) < eps.

Proof.

exact: fcvgrPdist_lt. Qed.

Lemma {} { : set_system T} { : Filter F} ( : T -> V) ( : V) :
f @ F --> y -> forall , eps > 0 -> \forall \near F, mdist y (f t) < eps.

Proof.

by move=> /cvgrPdist_lt. Qed.

Lemma {} { : set_system T} { : Filter F} ( : T -> V) ( : V) :
f @ F --> y -> forall , eps > 0 -> \forall \near F, mdist y (f t) <= eps.

Proof.

by move=> ? ? ?; near do rewrite ltW//; apply: cvgr_dist_lt.
Unshelve. all: by end_near. Qed.

End metricType_numDomainType.

Section at_left_right_metricType.
Variables ( : numFieldType) ( : metricType R).

Lemma ( : set V) :
(\forall \near x, P y) <->
(\forall \near 0^'+, forall , mdist x y <= e -> P y).

Proof.

rewrite (*nbhs0P*)/= near_withinE !near_simpl.
split.
  move => /nbhs_mdistP[/= _/posnumP[e] /(_ _) Px].
  apply/(@nbhs_mdistP R R^o).
  exists e%:num => //= r /= re yr y xyr.
  apply: Px => /=.
  rewrite (le_lt_trans _ re)//.
  rewrite (le_trans xyr)//.
  by rewrite /mdist/= subr0 real_ler_norm// gtr0_real.
move => /(@nbhs_mdistP R R^o)[/= _/posnumP[e] /(_ _) Px].
apply/(@nbhs_mdistP R V).
exists (e%:num / 2) => //= r /= re; apply: (Px (e%:num / 2)) => //=.
  by rewrite /mdist/= subr0 gtr0_norm// ltr_pdivrMr// ltr_pMr// ltr1n.
by rewrite ltW.
Qed.

Let { : set_system V} { : Filter F} ( : V) : [<->
  F --> y;
  forall , 0 < eps -> \forall \near F, mdist y t <= eps;
  \forall \near 0^'+, \forall \near F, mdist y t <= eps;
  \forall \near 0^'+, \forall \near F, mdist y t < eps].

Proof.

tfae; first by move=> *; apply: cvgr_dist_le.
- by move=> Fy; near do apply: Fy; apply: nbhs_right_gt.
- move=> Fy; near=> e; near (0:R)^'+ => d; near=> x.
  rewrite (@le_lt_trans _ _ d)//; first by near: x; near: d.
  by near: d; apply: nbhs_right_lt; near: e; apply: nbhs_right_gt.
- move=> Fy; apply/cvgrPdist_lt => e e_gt0; near (0:R)^'+ => d.
  near=> x; rewrite (@lt_le_trans _ _ d)//; first by near: x; near: d.
  by near: d; apply: nbhs_right_le.
Unshelve. all: by end_near. Qed.

Lemma {} { : set_system T} { : Filter F} ( : T -> V) ( : V) :
f @ F --> y <-> forall , 0 < eps -> \forall \near F, mdist y (f t) <= eps.

Proof.

exact: (cvgrP _ 0 1)%N. Qed.

End at_left_right_metricType.

End metricType_numDomainType.

Section cvg_nbhsP.
Variables ( : realType) ( : metricType R).

Import metricType_numDomainType.

Lemma ( : V -> V) ( : V) : f x @[ --> p] --> l <->
(forall : nat -> V, (u n @[ --> \oo] --> p) -> f (u n) @[ --> \oo] --> l).

Proof.

split=> [/cvgrPdist_le /= fpl u /cvgrPdist_lt /= uyp|pfl].
  apply/cvgrPdist_le => e /fpl.
  rewrite -filter_from_mdist_nbhs => -[d d0 pdf].
  by apply: filterS (uyp d d0) => t /pdf.
apply: contrapT => fpl; move: pfl; apply/existsNP.
suff: exists2 : nat -> V,
    x n @[ --> \oo] --> p & ~ f (x n) @[ --> \oo] --> l.
  by move=> [x_] hp; exists x_; exact/not_implyP.
have [e He] : exists : {posnum R}, forall : {posnum R},
    exists , mdist xn p < d%:num /\ mdist (f xn) l >= e%:num.
  apply: contrapT; apply: contra_not fpl => /forallNP h.
  apply/cvgrPdist_le => e e0; have /existsNP[d] := h (PosNum e0).
  move/forallNP => {}h; near=> t.
  have /not_andP[abs|/negP] := h t.
  - absurd: abs.
    near: t.
    rewrite !near_simpl /prop_near1 -nbhs_nbhs_mdist.
    by exists d%:num => //= z/=; rewrite metric_sym.
  - by rewrite -ltNge metric_sym => /ltW.
exists (fun => sval (cid (He n.+1%:R^-1%:pos))).
  apply/cvgrPdist_lt => r r0; near=> t.
  rewrite /sval/=; case: cid => x [xpt _].
  rewrite metric_sym (lt_le_trans xpt)//.
  rewrite -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0//.
  near: t; exists (truncn r^-1) => // s /= rs.
  by apply/ltW; rewrite -truncn_le_nat.
move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)).
rewrite /sval/=; case: cid => // x [px xpn].
by rewrite ltNge metric_sym => /negP.
Unshelve. all: end_near. Qed.

End cvg_nbhsP.

Section cvg_at_right_left_dnbhs.
Variables ( : realFieldType) ( : metricType R).

Import metricType_numDomainType.

Lemma ( : R -> T) ( : R) ( : T) :
f x @[ --> p^'+] --> l -> f x @[ --> p^'-] --> l ->
f x @[ --> p^'] --> l.

Proof.

move=> /cvgrPdist_le fppl /cvgrPdist_le fpnl; apply/cvgrPdist_le => e e0.
have {fppl}[a /= a0 fppl] := fppl (at_right_proper_filter p) _ e0.
have {fpnl}[b /= b0 fpnl] := fpnl (at_left_proper_filter p) _ e0.
near=> t.
have : t != p by near: t; exact: nbhs_dnbhs_neq.
rewrite neq_lt => /orP[tp|pt].
- apply: fpnl => //=; near: t.
  exists (b / 2) => //=; first by rewrite divr_gt0.
  move=> z/= + _ => /lt_le_trans; apply.
  by rewrite ler_pdivrMr// ler_pMr// ler1n.
- apply: fppl =>//=; near: t.
  exists (a / 2) => //=; first by rewrite divr_gt0.
  move=> z/= + _ => /lt_le_trans; apply.
  by rewrite ler_pdivrMr// ler_pMr// ler1n.
Unshelve. all: by end_near. Qed.

End cvg_at_right_left_dnbhs.

Section at_left_rightR.
Variable ( : numFieldType).

`cvgrPdistC_lt` is also defined in `pseudometric_normed_Zmodule.v` where it only needs `numDomainType`

Let {} { : set_system T} { : Filter F} ( : T -> R^o) ( : R) :
f @ F --> y <-> forall , 0 < eps -> \forall \near F, mdist (f t) y < eps.

Proof.

rewrite metricType_numDomainType.cvgrPdist_lt.
by under eq_forall do under eq_near do rewrite /mdist/= (@distrC _ R^o).
Qed.

`cvgr_distC_lt` is also defined in `pseudometric_normed_Zmodule.v` where it only needs `numDomainType`

Let {} { : set_system T} { : Filter F} ( : T -> R^o) ( : R) :
f @ F --> y -> forall , eps > 0 -> \forall \near F, mdist (f t) y < eps.

Proof.

by move=> /cvgrPdistC_lt. Qed.

Lemma {} { : set_system T} { : Filter F} ( : T -> R) ( : R) :
y \is Num.real -> f @ F --> y ->
forall , z > y -> \forall \near F, f t \is Num.real -> f t < z.

Proof.

move=> yr Fy z zy; near=> x => fxr.
rewrite -(ltrD2r (- y)) real_ltr_normlW// ?rpredB// distrC.
by near: x; apply: cvgr_distC_lt => //; rewrite subr_gt0.
Unshelve. all: by end_near. Qed.

Lemma {} { : set_system T} { : Filter F} ( : T -> R) ( : R) :
y \is Num.real -> f @ F --> y ->
forall , z > y -> \forall \near F, f t \is Num.real -> f t <= z.

Proof.

move=> /real_cvgr_lt/[apply] + ? z0 => /(_ _ z0).
by apply: filterS => ? /[apply]/ltW.
Qed.

Lemma {} { : set_system T} { : Filter F} ( : T -> R) ( : R) :
y \is Num.real -> f @ F --> y ->
forall , y > z -> \forall \near F, f t \is Num.real -> f t > z.

Proof.

move=> yr Fy z zy; near=> x => fxr.
rewrite -ltrN2 -(ltrD2l y) real_ltr_normlW// ?rpredB// distrC.
by near: x; apply: (@metricType_numDomainType.cvgr_dist_lt _ R^o) => //; rewrite subr_gt0.
Unshelve. all: by end_near. Qed.

Lemma {} { : set_system T} { : Filter F} ( : T -> R) ( : R) :
y \is Num.real -> f @ F --> y ->
forall , z < y -> \forall \near F, f t \is Num.real -> f t >= z.

Proof.

move=> /real_cvgr_gt/[apply] + ? z0 => /(_ _ z0).
by apply: filterS => ? /[apply]/ltW.
Qed.

End at_left_rightR.
Arguments real_cvgr_le {R T F FF f}.
Arguments real_cvgr_lt {R T F FF f}.
Arguments real_cvgr_ge {R T F FF f}.
Arguments real_cvgr_gt {R T F FF f}.

Section squeeze_cvgr.
Context { : Type} { : set_system T} { : Filter F} { : realFieldType}.
Implicit Types f g h : T -> R.

Lemma ( : R) :
f @ F --> y -> forall , z > y -> \forall \near F, f t < z.

Proof.

move=> Fy z zy; near=> x; rewrite -(ltrD2r (- y)) ltr_normlW//.
by near: x; apply: (@metricType_numDomainType.cvgr_dist_lt _ R^o) => //; rewrite subr_gt0.
Unshelve. all: by end_near. Qed.

Lemma ( : R) :
f @ F --> y -> forall , y > z -> \forall \near F, f t > z.

Proof.

move=> Fy z zy; near=> x; rewrite -ltrN2 -(ltrD2l y) ltr_normlW// distrC.
by near: x; apply: (@metricType_numDomainType.cvgr_dist_lt _ R^o) => //; rewrite subr_gt0.
Unshelve. all: by end_near. Qed.

Lemma ( : R) :
f @ F --> y -> forall , z > y -> \forall \near F, f t <= z.

Proof.

by move=> /cvgr_lt + ? z0 => /(_ _ z0); apply: filterS => ?; apply/ltW.
Qed.

Lemma ( : R) :
f @ F --> y -> forall , z < y -> \forall \near F, f t >= z.

Proof.

by move=> /cvgr_gt + ? z0 => /(_ _ z0); apply: filterS => ?; apply/ltW.
Qed.

Lemma : (\near , f F <= g F <= h F) ->
forall ( : R), f @ F --> l -> h @ F --> l -> g @ F --> l.

Proof.

move=> fgh l lfa lga.
apply/(@metricType_numDomainType.cvgrPdist_lt R R^o) => e e_gt0.
near=> x; have /(_ _)/andP[//|fg gh] := near fgh x.
rewrite ltr_distl (lt_le_trans _ fg) ?(le_lt_trans gh)//=.
by near: x; apply: (cvgr_gt lfa); rewrite // gtrDl oppr_lt0.
by near: x; apply: (cvgr_lt lga); rewrite // ltrDl.
Unshelve. all: end_near. Qed.

End squeeze_cvgr.
Arguments cvgr_lt {T F FF R f}.
Arguments cvgr_gt {T F FF R f}.
Arguments cvgr_le {T F FF R f}.
Arguments cvgr_ge {T F FF R f}.

Files

Module mathcomp.analysis.topology_theory.metric_structure