Merge pull request #1589 from affeldt-aist/metric_space

metric structure

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -190,6 +190,33 @@
       `variations_opp`, `nondecreasing_bounded_variation`
 - in `Rstruct.v`:
   + lemmas `RleP`, `RltP` (change implicits)
+- new file `metric_structure.v`:
+  + mixin `PseudoMetric_isMetric`, structure `Metric`, type `metricType`
+    * with fields `mdist`, `mdist_ge0`, `mdist_positivity`, `ballEmdist`
+  + lemmas `metric_sym`, `mdistxx`, `mdist_gt0`, `metric_triangle`,
+    `metric_hausdorff`
+  + `R^o` declared to be an instance of `metricType`
+  + module `metricType_numDomainType`
+    * lemmas `ball_mdistE`, `nbhs_nbhs_mdist`, `nbhs_mdistP`,
+      `filter_from_mdist_nbhs`, `fcvgrPdist_lt`, `cvgrPdist_lt`,
+      `cvgr_dist_lt`, `cvgr_dist_le`, `nbhsr0P`, `cvgrPdist_le`
+  + factory `isMetric`
+
+- in `pseudometric_normed_Zmodule.v`:
+  + factory `NormedZmoduleMetric` with field `mdist_norm`
+
+### Changed
+
+- moved from `pseudometric_normed_Zmodule.v` to `num_topology.v`:
+  + notations `^'+`, `^'-`
+  + definitions `at_left`, `at_right`
+  + instances `at_right_proper_filter`, `at_left_proper_filter`
+  + lemmas `nbhs_right_gt`, `nbhs_left_lt`, `nbhs_right_neq`, `nbhs_left_neq`,
+    `nbhs_left_neq`, `nbhs_left_le`, `nbhs_right_lt`, `nbhs_right_ltW`,
+    `nbhs_right_ltDr`, `nbhs_right_le`, `not_near_at_rightP`
+
+- moved from `realfun.v` to `metric_structure.v` and generalized:
+  + lemma `cvg_nbhsP`
 
 ### Renamed
 

_CoqProject

@@ -64,6 +64,7 @@ theories/topology_theory/one_point_compactification.v
 theories/topology_theory/sigT_topology.v
 theories/topology_theory/discrete_topology.v
 theories/topology_theory/separation_axioms.v
+theories/topology_theory/metric_structure.v
 
 theories/homotopy_theory/homotopy.v
 theories/homotopy_theory/wedge_sigT.v

theories/Make

@@ -31,6 +31,7 @@ topology_theory/one_point_compactification.v
 topology_theory/sigT_topology.v
 topology_theory/discrete_topology.v
 topology_theory/separation_axioms.v
+topology_theory/metric_structure.v
 
 homotopy_theory/homotopy.v
 homotopy_theory/wedge_sigT.v

theories/lebesgue_integral_theory/lebesgue_integral_under.v

@@ -62,14 +62,14 @@ have [Z [mZ Z0 /subsetCPl ncfZ]] := cf.
 have BZ_cf x : x \in B `\` Z -> {in I, continuous (f ^~ x)}.
   by rewrite inE/= => -[Bx nZx]; exact: ncfZ.
 have [vu|uv] := lerP v u.
-  by move: (Ia); rewrite /I set_itv_ge// -leNgt bnd_simp.
-apply/cvg_nbhsP => w wa.
+  by move: Ia; rewrite /I set_itv_ge// -leNgt bnd_simp.
+apply/(@cvg_nbhsP _ R^o) => w wa.
 have /near_in_itvoo[e /= e0 aeuv] : a \in `]u, v[ by rewrite inE.
 move/cvgrPdist_lt : (wa) => /(_ _ e0)[N _ aue].
 have IwnN n : I (w (n + N)) by apply: aeuv; apply: aue; exact: leq_addl.
 have : forall n, {ae mu, forall y, B y -> `|f (w (n + N)) y| <= g y}.
   by move=> n; exact: g_ub.
-move/choice  => [/= U /all_and3[mU U0 Ug_ub]].
+move/choice => [/= U /all_and3[mU U0 Ug_ub]].
 have mUU n : measurable (\big[setU/set0]_(k < n) U k).
   exact: bigsetU_measurable.
 set UU := \bigcup_n U n.
@@ -115,7 +115,7 @@ apply: (@dominated_cvg _ _ _ mu _ _
     move: BZUUx; rewrite inE/= => -[Bx nZUUx]; rewrite inE/=; split => //.
     by apply: contra_not nZUUx; left.
   move/(BZ_cf x)/(_ a); move/mem_set : Ia => /[swap] /[apply].
-  by move/cvg_nbhsP; apply; rewrite (cvg_shiftn N).
+  by move/(@cvg_nbhsP _ R^o); apply; rewrite (cvg_shiftn N).
 - by apply: (integrableS mB) => //; exact: measurableD.
 - move=> n x [Bx ZUUx]; rewrite lee_fin.
   move/subsetCPl : (Ug_ub n); apply => //=.
@@ -126,7 +126,8 @@ End continuity_under_integral.
 
 Section differentiation_under_integral.
 
-Definition partial1of2 {R : realType} {T : Type} (f : R -> T -> R) : R -> T -> R := fun x y => (f ^~ y)^`() x.
+Definition partial1of2 {R : realType} {T : Type} (f : R -> T -> R) : R -> T -> R
+  := fun x y => (f ^~ y)^`() x.
 
 Local Notation "'d1 f" := (partial1of2 f).
 

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -30,9 +30,11 @@ From mathcomp Require Import num_normedtype.
 (*                                                                            *)
 (* ## Normed topological abelian groups                                       *)
 (* ```                                                                        *)
-(*  pseudoMetricNormedZmodType R  == interface type for a normed topological  *)
-(*                                   abelian group equipped with a norm       *)
-(*                                   The HB class is PseudoMetricNormedZmod.  *)
+(*  pseudoMetricNormedZmodType R == interface type for a normed topological   *)
+(*                                  abelian group equipped with a norm        *)
+(*                                  The HB class is PseudoMetricNormedZmod.   *)
+(*           NormedZmoduleMetric == factory for pseudoMetricNormedZmodType    *)
+(*                                  based on metric structures                *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* ## Closed balls                                                            *)
@@ -59,8 +61,6 @@ From mathcomp Require Import num_normedtype.
 (*                                                                            *)
 (******************************************************************************)
 
-Reserved Notation "x ^'+" (at level 3, left associativity, format "x ^'+").
-Reserved Notation "x ^'-" (at level 3, left associativity, format "x ^'-").
 Reserved Notation "[ 'bounded' E | x 'in' A ]"
   (at level 0, x name, format "[ 'bounded'  E  |  x  'in'  A ]").
 
@@ -97,97 +97,6 @@ End Shift.
 Arguments shift {R} x / y.
 Notation center c := (shift (- c)).
 
-Section at_left_right.
-Variable R : numFieldType.
-
-Definition at_left (x : R) := within (fun u => u < x) (nbhs x).
-Definition at_right (x : R) := within (fun u => x < u) (nbhs x).
-Local Notation "x ^'-" := (at_left x) : classical_set_scope.
-Local Notation "x ^'+" := (at_right x) : classical_set_scope.
-
-Global Instance at_right_proper_filter (x : R) : ProperFilter x^'+.
-Proof.
-apply: Build_ProperFilter => -[_/posnumP[d] /(_ (x + d%:num / 2))].
-apply; last by rewrite ltrDl.
-by rewrite /= opprD addNKr normrN ger0_norm// gtr_pMr// invf_lt1// ltr1n.
-Qed.
-
-Global Instance at_left_proper_filter (x : R) : ProperFilter x^'-.
-Proof.
-apply: Build_ProperFilter => -[_ /posnumP[d] /(_ (x - d%:num / 2))].
-apply; last by rewrite gtrBl.
-by rewrite /= opprB addrC subrK ger0_norm// gtr_pMr// invf_lt1// ltr1n.
-Qed.
-
-Lemma nbhs_right_gt x : \forall y \near x^'+, x < y.
-Proof. by rewrite near_withinE; apply: nearW. Qed.
-
-Lemma nbhs_left_lt x : \forall y \near x^'-, y < x.
-Proof. by rewrite near_withinE; apply: nearW. Qed.
-
-Lemma nbhs_right_neq x : \forall y \near x^'+, y != x.
-Proof. by rewrite near_withinE; apply: nearW => ? /gt_eqF->. Qed.
-
-Lemma nbhs_left_neq x : \forall y \near x^'-, y != x.
-Proof. by rewrite near_withinE; apply: nearW => ? /lt_eqF->. Qed.
-
-Lemma nbhs_right_ge x : \forall y \near x^'+, x <= y.
-Proof. by rewrite near_withinE; apply: nearW; apply/ltW. Qed.
-
-Lemma nbhs_left_le x : \forall y \near x^'-, y <= x.
-Proof. by rewrite near_withinE; apply: nearW => ?; apply/ltW. Qed.
-
-Lemma nbhs_right_lt x z : x < z -> \forall y \near x^'+, y < z.
-Proof.
-move=> xz; exists (z - x) => //=; first by rewrite subr_gt0.
-by move=> y /= + xy; rewrite distrC ?ger0_norm ?subr_ge0 1?ltW// ltrD2r.
-Qed.
-
-Lemma nbhs_right_ltW x z : x < z -> \forall y \near nbhs x^'+, y <= z.
-Proof.
-by move=> xz; near=> y; apply/ltW; near: y; exact: nbhs_right_lt.
-Unshelve. all: by end_near. Qed.
-
-Lemma nbhs_right_ltDr x e : 0 < e -> \forall y \near x ^'+, y - x < e.
-Proof.
-move=> e0; near=> y; rewrite ltrBlDr; near: y.
-by apply: nbhs_right_lt; rewrite ltrDr.
-Unshelve. all: by end_near. Qed.
-
-Lemma nbhs_right_le x z : x < z -> \forall y \near x^'+, y <= z.
-Proof. by move=> xz; near do apply/ltW; apply: nbhs_right_lt.
-Unshelve. all: by end_near. Qed.
-
-(* NB: In not_near_at_rightP (and not_near_at_rightP), R has type numFieldType.
-  It is possible realDomainType could make the proof simpler and at least as
-  useful. *)
-Lemma not_near_at_rightP (p : R) (P : pred R) :
-  ~ (\forall x \near p^'+, P x) <->
-  forall e : {posnum R}, exists2 x, p < x < p + e%:num & ~ P x.
-Proof.
-split=> [pPf e|ex_notPx].
-- apply: contrapT => /forallPNP peP; apply: pPf; near=> t.
-  apply: contrapT; apply: peP; apply/andP; split.
-  + by near: t; exact: nbhs_right_gt.
-  + by near: t; apply: nbhs_right_lt; rewrite ltrDl.
-- rewrite /at_right near_withinE nearE.
-  rewrite -filter_from_ballE /filter_from/= -forallPNP => _ /posnumP[d].
-  have [x /andP[px xpd] notPx] := ex_notPx d; rewrite -existsNP; exists x => /=.
-  apply: contra_not notPx; apply => //.
-  by rewrite /ball/= ltr0_norm ?subr_lt0// opprB ltrBlDl.
-Unshelve. all: by end_near. Qed.
-
-End at_left_right.
-#[global] Typeclasses Opaque at_left at_right.
-Notation "x ^'-" := (at_left x) : classical_set_scope.
-Notation "x ^'+" := (at_right x) : classical_set_scope.
-
-#[global] Hint Extern 0 (Filter (nbhs _^'+)) =>
-  (apply: at_right_proper_filter) : typeclass_instances.
-
-#[global] Hint Extern 0 (Filter (nbhs _^'-)) =>
-  (apply: at_left_proper_filter) : typeclass_instances.
-
 Section at_left_right_topologicalType.
 Variables (R : numFieldType) (V : topologicalType) (f : R -> V) (x : R).
 
@@ -225,6 +134,25 @@ HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) :=
   {T of Num.NormedZmodule R T & PseudoMetric R T
    & NormedZmod_PseudoMetric_eq R T & isPointed T}.
 
+(* alternative definition of a PseudoMetricNormedZmod *)
+HB.factory Record NormedZmoduleMetric (R : numDomainType) T
+    of Num.NormedZmodule R T & Metric R T & isPointed T := {
+  mdist_norm : forall x y : T, mdist x y = `|y - x|
+}.
+
+HB.builders Context (R : numDomainType) T of NormedZmoduleMetric R T.
+
+Let pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |).
+Proof.
+apply/funext => /= t; apply/funext => d; rewrite ballEmdist.
+by apply/seteqP; split => [y|y]/=; rewrite mdist_norm distrC.
+Qed.
+
+HB.instance Definition _ :=
+  NormedZmod_PseudoMetric_eq.Build R T pseudo_metric_ball_norm.
+
+HB.end.
+
 Section pseudoMetricNormedZmod_numDomainType.
 Context {K : numDomainType} {V : pseudoMetricNormedZmodType K}.
 

theories/realfun.v

@@ -199,37 +199,6 @@ apply: cvg_at_right_left_dnbhs.
 - by apply/cvg_at_leftP => u [pu ?]; apply: pfl; split => // n; rewrite lt_eqF.
 Unshelve. all: end_near. Qed.
 
-Lemma cvg_nbhsP f p l : f x @[x --> p] --> l <->
-  (forall u : R^nat, (u n @[n --> \oo] --> p) -> f (u n) @[n --> \oo] --> l).
-Proof.
-split=> [/cvgrPdist_le /= fpl u /cvgrPdist_lt /= uyp|pfl].
-  apply/cvgrPdist_le => e /fpl[d d0 pdf].
-  by apply: filterS (uyp d d0) => t /pdf.
-apply: contrapT => fpl; move: pfl; apply/existsNP.
-suff: exists2 x : R ^nat,
-    x n @[n --> \oo] --> p & ~ f (x n) @[n --> \oo] --> l.
-  by move=> [x_] hp; exists x_; exact/not_implyP.
-have [e He] : exists e : {posnum R}, forall d : {posnum R},
-    exists xn, `|xn - p| < d%:num /\ `|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.
-  - exfalso; apply: abs.
-    by near: t; exists d%:num => //= z/=; rewrite distrC.
-  - by rewrite -ltNge distrC => /ltW.
-have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0.
-exists (fun n => sval (cid (He (PosNum (invn n))))).
-  apply/cvgrPdist_lt => r r0; near=> t.
-  rewrite /sval/=; case: cid => x [xpt _].
-  rewrite distrC (lt_le_trans xpt)// -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0//.
-  near: t; exists (truncn r^-1) => // s /= rs.
-  by rewrite (le_trans (ltW (truncnS_gt _)))// ler_nat.
-move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)).
-rewrite /sval/=; case: cid => // x [px xpn].
-by rewrite ltNge distrC => /negP.
-Unshelve. all: end_near. Qed.
-
 End cvgr_fun_cvg_seq.
 
 Section cvge_fun_cvg_seq.