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 boolp classical_sets contra reals.
From mathcomp Require Import topology_structure uniform_structure
pseudometric_structure 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. ```

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_numDomainType.
Context { : numDomainType} ( : metricType R).

Let := @mdist R T.

Lemma : dist x y = dist y x.

Proof.

have cxy : dist x y >=< dist y x.
  by apply: real_comparable; apply: ger0_real; exact: mdist_ge0.
apply/eqP; rewrite eq_le; apply/andP; split.
- rewrite comparable_leNgt//; apply/negP => xy.
  have := @ball_sym _ _ y x (dist x y); rewrite !ballEmdist/= => /(_ xy).
  by rewrite ltxx.
- rewrite comparable_leNgt//; first by rewrite comparable_sym.
  apply/negP => xy.
  have := @ball_sym _ _ x y (dist y x); rewrite !ballEmdist/= => /(_ xy).
  by rewrite ltxx.
Qed.

Lemma : dist x x = 0.

Proof.

have := mdist_ge0 x x.
rewrite /dist le_eqVlt => /predU1P[<-//|].
by move/(ballxx x); rewrite ballEmdist /= ltxx.
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 [eqbRHS]mdistxx.
Qed.

End metric_numDomainType.

Section metric_numFieldType.
Context { : numFieldType} ( : metricType R).

Let := @mdist R T.

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

Proof.

have c : dist x z >=< dist x y + dist y z.
by rewrite real_comparable// ger0_real ?addr_ge0// mdist_ge0.
rewrite (comparable_leNgt c); apply/negP => xy.
set e := dist x z - (dist x y + dist y z).
have e0 : 0 < e by rewrite subr_gt0.
have e20 : 0 < e / 2 by rewrite divr_gt0.
have xe2y : ball x (dist x y + e / 2) y by rewrite ballEmdist/= ltrDl.
have ye2z : ball y (dist y z + e / 2) z by rewrite ballEmdist/= ltrDl.
have := ball_triangle xe2y ye2z.
by rewrite ballEmdist/= addrACA -splitr subrKC ltxx.
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_numFieldType.

Section prod_metric.
Context { : numDomainType} ( : metricType K).

Let := (T * U)%type.

Let ( : M) : mdist x.1 y.1 >=< mdist x.2 y.2.

Proof.

by apply: real_comparable; apply: ger0_real; exact: mdist_ge0. Qed.

Definition ( : M) := maxr (mdist x.1 y.1) (mdist x.2 y.2).

Let : 0 <= prod_mdist x y.

Proof.

by rewrite /prod_mdist comparable_le_max// mdist_ge0. Qed.

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

Proof.

rewrite /prod_mdist /= => m0.
have le01 : mdist x.1 y.1 <= 0 by rewrite -m0 comparable_le_max// lexx.
have le02 : mdist x.2 y.2 <= 0 by rewrite -m0 comparable_le_max// lexx orbT.
have eq01 : mdist x.1 y.1 = 0 by apply/le_anti; rewrite le01 mdist_ge0.
have eq02 : mdist x.2 y.2 = 0 by apply/le_anti; rewrite le02 mdist_ge0.
rewrite (surjective_pairing x) (surjective_pairing y).
by congr pair; exact: mdist_positivity.
Qed.

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

Proof.

apply/seteqP; split => [y []|y /= xyd].
rewrite !ballEmdist/= /prod_mdist => b1 b2.
by rewrite comparable_gt_max// b1 b2.
rewrite /ball/= /prod_ball/= !ballEmdist/=.
by apply/andP; rewrite -comparable_gt_max.
Qed.

..Build K (T * U)%type
  prod_mdist_ge0 prod_mdist_positivity ballEprod_mdist.

End prod_metric.

. () (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) :
(\forall \near x, P x0) <-> 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 near_withinE.
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 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 : (\forall \near F, f x <= g x <= h x) ->
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}.
Arguments squeeze_cvgr {T F FF R} f g h.

Files

Module mathcomp.analysis.topology_theory.metric_structure