fixes, changelog

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -7,8 +7,33 @@
 - in `cardinality.v`:
   + lemma `infinite_setD`
 
+- new file `metric_structure.v`:
+  + mixin `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`
+
+- 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
 
 ### Generalized

theories/lebesgue_integral_theory/lebesgue_integral_under.v

@@ -63,13 +63,13 @@ have BZ_cf x : x \in B `\` Z -> 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.
+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.
@@ -114,7 +114,7 @@ apply: (@dominated_cvg _ _ _ mu _ _
   have : x \in B `\` Z.
     move: BZUUx; rewrite inE/= => -[Bx nZUUx]; rewrite inE/=; split => //.
     by apply: contra_not nZUUx; left.
-  by move/(BZ_cf x)/(_ a)/cvg_nbhsP; apply; rewrite (cvg_shiftn N).
+  by move/(BZ_cf x)/(_ a)/(@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 => //=.
@@ -125,7 +125,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

@@ -32,9 +32,11 @@ From mathcomp Require Import tvs 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                                                            *)

theories/realfun.v

@@ -236,11 +236,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.
 
-#[deprecated(since="mathcomp-analysis 1.15.0", note="use `metricType_numDomainType.cvg_nbhsP` instead")]
-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. exact: @metricType_numDomainType.cvg_nbhsP _ R^o f p l. Qed.
-
 End cvgr_fun_cvg_seq.
 
 Section cvge_fun_cvg_seq.

theories/topology_theory/metric_structure.v

@@ -1,13 +1,24 @@
 (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
-From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
-From mathcomp Require Import archimedean finmap.
+From mathcomp Require Import interval_inference rat interval zmodp vector.
+From mathcomp Require Import fieldext falgebra archimedean finmap.
 From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.
-From mathcomp Require Import interval_inference reals topology_structure.
+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.
 
+(**md**************************************************************************)
+(* # Metric spaces                                                            *)
+(*                                                                            *)
+(* ```                                                                        *)
+(*   metricType K == metric structure with distance mdist                     *)
+(*                   The mixin is defined by extending PseudoMetric.          *)
+(*                   The HB class is Metric.                                  *)
+(*                   R^o with R : numFieldType is shown to be a metric space. *)
+(* ```                                                                        *)
+(******************************************************************************)
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -67,9 +78,9 @@ Qed.
 
 Lemma metric_hausdorff : hausdorff_space T.
 Proof.
-move=> p q pq; apply: contrapT => qp; move: pq.
+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; exact/eqP.
+  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].
@@ -93,22 +104,18 @@ Proof. by move/normr0_eq0/eqP; rewrite subr_eq0 => /eqP. Qed.
 Let ballEmdist x d : ball x d = [set y | dist x y < d].
 Proof. by apply/seteqP; split => [|]/= A; rewrite /ball/= distrC. Qed.
 
-Fail Check R^o : metricType R.
-
 HB.instance Definition _ :=
   @isMetric.Build R R^o dist dist_ge0 dist_positivity ballEmdist.
 
-Check R^o : metricType R.
-
 End numFieldType_metric.
 
 Module metricType_numDomainType.
 (* tentative generalization of the section
 pseudoMetricNormedZmod_numDomainType
-from pseudoMetricNormedZmod_numDomainType
+from pseudoMetricNormedZmod
 to
 metricType *)
-Section tmp.
+Section metricType_numDomainType.
 Context {K : numDomainType} {V : metricType K}.
 
 Local Notation ball_mdist := (fun x d => [set y : V | mdist x y < d]).
@@ -158,9 +165,9 @@ Proof.
 by move=> ? ? ?; near do rewrite ltW//; apply: cvgr_dist_lt.
 Unshelve. all: by end_near. Qed.
 
-End tmp.
+End metricType_numDomainType.
 
-Section tmp2.
+Section at_left_right_metricType.
 (* tentative generalization of the section
 at_left_right_pseudoMetricNormedZmod
 from
@@ -209,18 +216,21 @@ Lemma cvgrPdist_le {T} {F : set_system T} {FF : Filter F} (f : T -> V) (y : V) :
   f @ F --> y <-> forall eps, 0 < eps -> \forall t \near F, mdist y (f t) <= eps.
 Proof. exact: (cvgrP _ 0 1)%N. Qed.
 
-End tmp2.
+End at_left_right_metricType.
 
-Section tmp3.
+End metricType_numDomainType.
+
+Section cvg_nbhsP.
 Variables (R : realType) (V : metricType R).
 
+Import metricType_numDomainType.
+
 Lemma cvg_nbhsP (f : V -> V) (p l : V) : f x @[x --> p] --> l <->
   (forall u : nat -> V, (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.
-  rewrite -filter_from_mdist_nbhs.
-  move=> [d d0 pdf].
+  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 x : nat -> V,
@@ -232,26 +242,21 @@ have [e He] : exists e : {posnum R}, forall d : {posnum R},
   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.
+  - absurd: abs.
     near: t.
-    rewrite !near_simpl.
-    rewrite /prop_near1.
-    rewrite -nbhs_nbhs_mdist.
-    exists d%:num => //= z/=.
-    by rewrite metric_sym.
+    rewrite !near_simpl /prop_near1 -nbhs_nbhs_mdist.
+    by exists d%:num => //= z/=; rewrite metric_sym.
   - by rewrite -ltNge metric_sym => /ltW.
-have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0.
-exists (fun n => sval (cid (He (PosNum (invn n))))).
+exists (fun n => 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)// -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0//.
-  near: t; exists (trunc r^-1) => // s /= rs.
+  rewrite metric_sym (lt_le_trans xpt)//.
+  rewrite -[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 metric_sym => /negP.
 Unshelve. all: end_near. Qed.
 
-End tmp3.
-
-End metricType_numDomainType.
+End cvg_nbhsP.

theories/topology_theory/num_topology.v

@@ -210,7 +210,7 @@ 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.
+(* NB: In 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) :