pseudometric alias (#1628)

* alias for pseudometric and factory for normed module

---------

Co-authored-by: Quentin Vermande <quentin.vermande@ens.fr>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -52,6 +52,10 @@
 - in `lebesgue_integral_differentiation.v`:
   + lemma `nicely_shrinking_fin_num`
 
+- in `normed_module.v`:
+  + definition `pseudoMetric_normed`
+  + factory `Lmodule_isNormed`
+
 ### Changed
 
 - in `convex.v`:

theories/normedtype_theory/normed_module.v

@@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.
 From mathcomp Require Import rat interval zmodp vector fieldext falgebra.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.
-From mathcomp Require Import functions cardinality set_interval.
+From mathcomp Require Import filter functions cardinality set_interval.
 From mathcomp Require Import interval_inference ereal reals topology.
 From mathcomp Require Import function_spaces real_interval.
 From mathcomp Require Import prodnormedzmodule tvs num_normedtype.
@@ -26,6 +26,13 @@ From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule.
 (* We endow `numFieldType` with the types of norm-related notions (accessible *)
 (* with `Import numFieldNormedType.Exports`).                                 *)
 (*                                                                            *)
+(* ```                                                                        *)
+(*   pseudoMetric_normed M == an alias for the pseudometric structure defined *)
+(*                            from a normed module                            *)
+(*                            M : normedZmodType K with K : numFieldType.     *)
+(*      Lmodule_isNormed M == factory for a normed module defined using       *)
+(*                            an L-module M over R : numFieldType             *)
+(* ```                                                                        *)
 (* ## Hulls                                                                   *)
 (* ```                                                                        *)
 (*                        Rhull A == the real interval hull of a set A        *)
@@ -223,6 +230,87 @@ Module Exports. Export numFieldTopology.Exports. HB.reexport. End Exports.
 End numFieldNormedType.
 Import numFieldNormedType.Exports.
 
+Definition pseudoMetric_normed (M : Type) : Type := M.
+
+HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) :=
+  Choice.on (pseudoMetric_normed M).
+HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) :=
+  Num.NormedZmodule.on (pseudoMetric_normed M).
+
+Module pseudoMetric_from_normedZmodType.
+Section pseudoMetric_from_normedZmodType.
+Variables (K : numFieldType) (M : normedZmodType K).
+
+Notation T := (pseudoMetric_normed M).
+
+Definition ball (x : T) (r : K) : set T := ball_ Num.norm x r.
+
+Definition ent : set_system (T * T) := entourage_ ball.
+
+Definition nbhs (x : T) : set_system T := nbhs_ ent x.
+
+Lemma nbhsE : nbhs = nbhs_ ent. Proof. by []. Qed.
+
+#[export] HB.instance Definition _ := hasNbhs.Build T nbhs.
+
+Lemma ball_center x (e : K) : 0 < e -> ball x e x.
+Proof. by rewrite /ball/= subrr normr0. Qed.
+
+Lemma ball_sym x y (e : K) : ball x e y -> ball y e x.
+Proof. by rewrite /ball /= distrC. Qed.
+
+Lemma ball_triangle x y z e1 e2 : ball x e1 y -> ball y e2 z ->
+  ball x (e1 + e2) z.
+Proof.
+rewrite /ball /= => ? ?.
+rewrite -[x](subrK y) -(addrA (x + _)).
+by rewrite (le_lt_trans (ler_normD _ _))// ltrD.
+Qed.
+
+Lemma entourageE : ent = entourage_ ball.
+Proof. by []. Qed.
+
+#[export] HB.instance Definition _ := @Nbhs_isPseudoMetric.Build K T
+  ent nbhsE ball ball_center ball_sym ball_triangle entourageE.
+
+End pseudoMetric_from_normedZmodType.
+Module Exports. HB.reexport. End Exports.
+End pseudoMetric_from_normedZmodType.
+Export pseudoMetric_from_normedZmodType.Exports.
+
+HB.factory Record Lmodule_isNormed (R : numFieldType) M
+    of GRing.Lmodule R M := {
+ norm : M -> R;
+ ler_normD : forall x y, norm (x + y) <= norm x + norm y ;
+ normrZ : forall (l : R) (x : M), norm (l *: x) = `|l| * norm x ;
+ normr0_eq0 : forall x : M, norm x = 0 -> x = 0
+}.
+
+HB.builders Context R M of Lmodule_isNormed R M.
+
+Lemma normrMn x n : norm (x *+ n) = norm x *+ n.
+Proof.
+have := normrZ n%:R x; rewrite ger0_norm// mulr_natl => <-.
+by rewrite scaler_nat.
+Qed.
+
+Lemma normrN x : norm (- x) = norm x.
+Proof. by have := normrZ (- 1)%R x; rewrite scaleN1r normrN normr1 mul1r. Qed.
+
+HB.instance Definition _ := Num.Zmodule_isNormed.Build
+  R M ler_normD normr0_eq0 normrMn normrN.
+
+HB.instance Definition _ := PseudoMetric.copy M (pseudoMetric_normed M).
+
+HB.instance Definition _ := isPointed.Build M 0.
+
+HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R M erefl.
+
+HB.instance Definition _ :=
+  PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R M normrZ.
+
+HB.end.
+
 Lemma scaler1 {R : numFieldType} h : h%:A = h :> R.
 Proof. by rewrite /GRing.scale/= mulr1. Qed.
 

theories/topology_theory/bool_topology.v

@@ -7,8 +7,7 @@ From mathcomp Require Import discrete_topology.
 
 (**md**************************************************************************)
 (* # Topology for boolean numbers                                             *)
-(*          pseudoMetric_bool == an alias for bool equipped with the          *)
-(*                               discrete pseudometric                        *)
+(* This file equips bool with the discrete pseudometric.                      *)
 (******************************************************************************)
 
 Import Order.TTheory GRing.Theory Num.Theory.