Metric 20260629

CHANGELOG_UNRELEASED.md

@@ -186,12 +186,6 @@
   + lemma `ge0_integration_by_substitution_shift_itvy`,
     `ge0_integration_by_substitution_shift_itvNy`
 
-### Changed
-
-- moved from `measurable_structure.v` to `classical_sets.v`:
-  + definition `preimage_set_system`
-  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
-    `preimage_set_system_id`
 - in `functions.v`:
   + lemmas `linfunP`, `linfun_eqP`
   + instances of `SubLmodule` and `pointedType` on `{linear _->_ | _ }`
@@ -224,6 +218,10 @@
 - in `realsum.v`:
   + lemma `__admitted__psumB` proved and renamed to `psumB`
 
+- in `pseudometric_normed_Zmodule.v`:
+  + factory `isPseudoMetricNormedZmodule`
+  + structure `PseudoMetricNormedZmod0`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:
@@ -335,6 +333,12 @@
   + definition `seqD`
   + lemmas `eq_bigcup_seqD`, `trivIset_seqD`, `seqDU_seqD`, `bigcup_bigsetU_bigcup`
 
+- in `pseudometric_normed_Zmodule.v`:
+  + structure `PseudoMetricNormedZmod` not inherits from `Metric`
+
+- moved form `normed_module.v` to `pseudometric_normed_Zmodule.v` and generalized:
+  + lemmas `fcvgr2dist_ltP`, `cvgr2dist_ltP`, `cvgr2dist_lt`
+
 ### Renamed
 
 - in `tvs.v`:

theories/measure_theory/measurable_function.v

@@ -1,11 +1,10 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat algebra.
+From mathcomp Require Import all_ssreflect_compat.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
-From mathcomp Require Import boolp classical_sets functions cardinality reals.
-From mathcomp Require Import ereal topology normedtype.
-From mathcomp Require Import sequences measurable_structure.
+From mathcomp Require Import boolp classical_sets functions.
+From mathcomp Require Import measurable_structure.
 
 (**md**************************************************************************)
 (* # Measurable Functions                                                     *)
@@ -29,7 +28,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Import ProperNotations.
-Import Order.TTheory GRing.Theory Num.Theory.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -358,7 +356,7 @@ Context {d} {T : measurableType d} {d1} {T1 : measurableType d1}
 
 Lemma g_sigma_algebra_preimage_comp (X : {mfun T >-> T1}) (f : T1 -> T2) :
   measurable_fun [set: T1] f ->
-  g_sigma_algebra_preimage (f \o X)%R `<=` g_sigma_algebra_preimage X.
+  g_sigma_algebra_preimage (f \o X) `<=` g_sigma_algebra_preimage X.
 Proof. exact: preimage_set_system_compS. Qed.
 
 End g_sigma_algebra_preimage_comp.

theories/normedtype_theory/matrix_normedtype.v

@@ -217,6 +217,8 @@ Qed.
 HB.instance Definition _ :=
   NormedZmod_PseudoMetric_eq.Build K 'M[K]_(m, n) mx_norm_ball.
 
+HB.instance Definition _ := isPseudoMetricNormedZmodule.Build _ 'M[K]_(m, n).
+
 End matrix_pseudoMetricNormedZmod.
 
 Lemma bounded_closed_compact (R : realType) n (A : set 'rV[R]_n) :

theories/normedtype_theory/normed_module.v

@@ -369,13 +369,15 @@ HB.instance Definition _ := isPointed.Build M 0.
 
 HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R M erefl.
 
+HB.instance Definition _ := isPseudoMetricNormedZmodule.Build R M.
+
 HB.instance Definition _ :=
   PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R M normrZ.
 
 HB.end.
 
 Definition subLmodule_isSubNormedmodule (R : realFieldType)
-    (V : normedModType R) (S : pred V) (U : Type) : Type := U.
+  (V : normedModType R) (S : pred V) (U : Type) : Type := U.
 
 Section SubLmodule_isSubNormedmodule.
 Context (R : realFieldType) (V : normedModType R) (S : pred V)
@@ -1721,7 +1723,7 @@ Qed.
 Section prod_NormedModule.
 Context {K : numFieldType} {U V : normedModType K}.
 
-Lemma prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |.
+Let prod_norm_scale (l : K) (x : U * V) : `| l *: x | = `|l| * `| x |.
 Proof. by rewrite prod_normE /= !normrZ maxr_pMr. Qed.
 
 HB.instance Definition _ :=
@@ -1730,37 +1732,6 @@ HB.instance Definition _ :=
 
 End prod_NormedModule.
 
-Section prod_NormedModule_lemmas.
-Context {T : Type} {K : numDomainType} {U V : normedModType K}.
-
-Lemma fcvgr2dist_ltP {F : set_system U} {G : set_system V}
-  {FF : Filter F} {FG : Filter G} (y : U) (z : V) :
-  (F, G) --> (y, z) <->
-  forall eps, 0 < eps ->
-   \forall y' \near F & z' \near G, `| (y, z) - (y', z') | < eps.
-Proof. exact: fcvgrPdist_lt. Qed.
-
-Lemma cvgr2dist_ltP {I J} {F : set_system I} {G : set_system J}
-  {FF : Filter F} {FG : Filter G} (f : I -> U) (g : J -> V) (y : U) (z : V) :
-  (f @ F, g @ G) --> (y, z) <->
-  forall eps, 0 < eps ->
-   \forall i \near F & j \near G, `| (y, z) - (f i, g j) | < eps.
-Proof.
-rewrite fcvgr2dist_ltP; split=> + e e0 => /(_ e e0);
-  by rewrite !near_simpl// => ?; rewrite !near_simpl.
-Qed.
-
-Lemma cvgr2dist_lt {I J} {F : set_system I} {G : set_system J}
-  {FF : Filter F} {FG : Filter G} (f : I -> U) (g : J -> V) (y : U) (z : V) :
-  (f @ F, g @ G) --> (y, z) ->
-  forall eps, 0 < eps ->
-   \forall i \near F & j \near G, `| (y, z) - (f i, g j) | < eps.
-Proof. by rewrite cvgr2dist_ltP. Qed.
-
-End prod_NormedModule_lemmas.
-Arguments cvgr2dist_ltP {_ _ _ _ _ F G FF FG}.
-Arguments cvgr2dist_lt {_ _ _ _ _ F G FF FG}.
-
 (* Local properties in R *)
 
 (* Topology on [R]² *)
@@ -2653,6 +2624,9 @@ HB.instance Definition _ (V : vectType R) :=
 HB.instance Definition _ (V : vectType R) :=
   NormedZmod_PseudoMetric_eq.Build R (max_space V) erefl.
 
+HB.instance Definition _ (V : vectType R) :=
+  isPseudoMetricNormedZmodule.Build _ (max_space V).
+
 HB.instance Definition _ (V : vectType R) :=
   PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V)
     (@Norm.normZ _ _ (@max_norm V)).

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -29,8 +29,9 @@ From mathcomp Require Import prodnormedzmodule num_normedtype.
 (*                                                                            *)
 (* ## Normed topological abelian groups                                       *)
 (* ```                                                                        *)
-(*  pseudoMetricNormedZmodType R == interface type for a normed topological   *)
+(*     PseudoMetricNormedZmod0 R == interface type for a normed topological   *)
 (*                                  abelian group equipped with a norm        *)
+(*  pseudoMetricNormedZmodType R == PseudoMetricNormedZmod0 R + Metric R      *)
 (*                                  The HB class is PseudoMetricNormedZmod.   *)
 (*           NormedZmoduleMetric == factory for pseudoMetricNormedZmodType    *)
 (*                                  based on metric structures                *)
@@ -148,10 +149,44 @@ HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T
   pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |)
 }.
 
+HB.structure Definition PseudoMetricNormedZmod0 (R : numDomainType) :=
+  {T of Num.NormedZmodule R T & PseudoPointedMetric R T
+   & NormedZmod_PseudoMetric_eq R T }.
+
+Section PseudoMetricNormedZmod0_numDomainType.
+Context {K : numDomainType} {V : PseudoMetricNormedZmod0.type K}.
+
+(**md Balls defined by the norm: *)
+Local Notation ball_norm := (ball_ (@Num.norm K V)).
+
+Lemma ball_normE : ball_norm = ball.
+Proof. by rewrite pseudo_metric_ball_norm. Qed.
+
+End PseudoMetricNormedZmod0_numDomainType.
+
 #[short(type="pseudoMetricNormedZmodType")]
 HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) :=
-  {T of Num.NormedZmodule R T & PseudoMetric R T
-   & NormedZmod_PseudoMetric_eq R T & isPointed T}.
+  {T of PseudoMetricNormedZmod0 R T & Metric R T}.
+
+HB.factory Record isPseudoMetricNormedZmodule
+  (K : numDomainType) T & PseudoMetricNormedZmod0 K T := { }.
+
+HB.builders Context K T & isPseudoMetricNormedZmodule K T.
+
+Let mdist (x y : T) : K := `|x - y|.
+
+Let mdist_ge0 x y : 0 <= mdist x y. Proof. by rewrite /mdist. Qed.
+
+Let mdist_positivity x y : mdist x y = 0 -> x = y.
+Proof. by move=> /normr0_eq0/subr0_eq. Qed.
+
+Let ballEmdist x d : ball x d = [set y | mdist x y < d].
+Proof. by rewrite -ball_normE. Qed.
+
+HB.instance Definition _ :=
+  @PseudoMetric_isMetric.Build K T mdist mdist_ge0 mdist_positivity ballEmdist.
+
+HB.end.
 
 (* alternative definition of a PseudoMetricNormedZmod *)
 HB.factory Record NormedZmoduleMetric (R : numDomainType) T
@@ -175,12 +210,6 @@ HB.end.
 Section pseudoMetricNormedZmod_numDomainType.
 Context {K : numDomainType} {V : pseudoMetricNormedZmodType K}.
 
-(**md Balls defined by the norm: *)
-Local Notation ball_norm := (ball_ (@Num.norm K V)).
-
-Lemma ball_normE : ball_norm = ball.
-Proof. by rewrite pseudo_metric_ball_norm. Qed.
-
 Lemma ball_open (x : V) (r : K) : open (ball x r).
 Proof.
 rewrite openE/= -ball_normE/= /interior => y /= bxy; rewrite -nbhs_ballE.
@@ -193,6 +222,7 @@ Lemma ball_open_nbhs (x : V) (r : K) : 0 < r -> open_nbhs x (ball x r).
 Proof. by move=> e0; split; [exact: ball_open|exact: ballxx]. Qed.
 
 (**md Neighborhoods defined by the norm: *)
+Local Notation ball_norm := (ball_ (@Num.norm K V)).
 Local Notation nbhs_norm := (nbhs_ball_ ball_norm).
 
 (* if we do not give the V argument to nbhs, the universally quantified set that
@@ -469,14 +499,47 @@ rewrite /ball /= /prod_ball -!ball_normE /ball_ /=.
 by rewrite comparable_gt_max// ?real_comparable//; split=> /andP.
 Qed.
 
-Lemma prod_norm_ball : @ball _ (U * V)%type = ball_ (fun x => `|x|).
+Let prod_norm_ball : @ball _ (U * V)%type = ball_ (fun x => `|x|).
 Proof. by rewrite /= - ball_prod_normE. Qed.
 
 HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build K (U * V)%type
   prod_norm_ball.
 
+HB.instance Definition _ := isPseudoMetricNormedZmodule.Build _ (U * V)%type.
+
 End prod_pseudoMetricNormedZmod.
 
+Section prod_NormedModule_lemmas.
+Context {T : Type} {K : numDomainType} {U V : pseudoMetricNormedZmodType K}.
+
+Lemma fcvgr2dist_ltP {F : set_system U} {G : set_system V}
+  {FF : Filter F} {FG : Filter G} (y : U) (z : V) :
+  (F, G) --> (y, z) <->
+  forall eps, 0 < eps ->
+   \forall y' \near F & z' \near G, `| (y, z) - (y', z') | < eps.
+Proof. exact: fcvgrPdist_lt. Qed.
+
+Lemma cvgr2dist_ltP {I J} {F : set_system I} {G : set_system J}
+  {FF : Filter F} {FG : Filter G} (f : I -> U) (g : J -> V) (y : U) (z : V) :
+  (f @ F, g @ G) --> (y, z) <->
+  forall eps, 0 < eps ->
+   \forall i \near F & j \near G, `| (y, z) - (f i, g j) | < eps.
+Proof.
+rewrite fcvgr2dist_ltP; split=> + e e0 => /(_ e e0);
+  by rewrite !near_simpl// => ?; rewrite !near_simpl.
+Qed.
+
+Lemma cvgr2dist_lt {I J} {F : set_system I} {G : set_system J}
+  {FF : Filter F} {FG : Filter G} (f : I -> U) (g : J -> V) (y : U) (z : V) :
+  (f @ F, g @ G) --> (y, z) ->
+  forall eps, 0 < eps ->
+   \forall i \near F & j \near G, `| (y, z) - (f i, g j) | < eps.
+Proof. by rewrite cvgr2dist_ltP. Qed.
+
+End prod_NormedModule_lemmas.
+Arguments cvgr2dist_ltP {_ _ _ _ _ F G FF FG}.
+Arguments cvgr2dist_lt {_ _ _ _ _ F G FF FG}.
+
 Section standard_topology_pseudoMetricNormedZmod.
 Variable R : numFieldType.