From aced71568c08f06f30d169415aca1a12ce084320 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 22 May 2025 21:09:27 +0900 Subject: [PATCH 1/3] alias for pseudometric and factory for normed module --- CHANGELOG_UNRELEASED.md | 4 + theories/normedtype_theory/normed_module.v | 96 ++++++++++++++++++++++ 2 files changed, 100 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 699bb89453..4ebdc95003 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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`: diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index edeccb19c2..becea15534 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -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,95 @@ Module Exports. Export numFieldTopology.Exports. HB.reexport. End Exports. End numFieldNormedType. Import numFieldNormedType.Exports. +Definition pseudoMetric_normed (K : numFieldType) (M : normedZmodType K) : 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). +(*HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) := + isPointed.Build M 0.*) + +Section pseudoMetric_from_normedZmodType. +Variables (K : numFieldType) (M : normedZmodType K). + +Notation T := (pseudoMetric_normed M). + +Local Definition ball (x : T) (r : K) : set T := ball_ Num.norm x r. + +Local Definition ent : set_system (T * T) := entourage_ ball. + +Local Definition nbhs (x : T) : set_system T := nbhs_ ent x. + +Local Lemma nbhsE : nbhs = nbhs_ ent. Proof. by []. Qed. + +HB.instance Definition _ := hasNbhs.Build T nbhs. + +Local Lemma ball_center x (e : K) : 0 < e -> ball x e x. +Proof. by rewrite /ball/= subrr normr0. Qed. + +Local Lemma ball_sym x y (e : K) : ball x e y -> ball y e x. +Proof. by rewrite /ball /= distrC. Qed. + +Local 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. + +Local Lemma entourageE : ent = entourage_ ball. +Proof. by []. Qed. + +HB.instance Definition _ := @Nbhs_isPseudoMetric.Build K T + ent nbhsE ball ball_center ball_sym ball_triangle entourageE. + +End pseudoMetric_from_normedZmodType. + +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.saturate pseudoMetric_normed.*) + +HB.instance Definition _ := PseudoMetric.copy M (pseudoMetric_normed M). +HB.instance Definition _ := isPointed.Build M 0. + +Local Lemma NormedZmod_PseudoMetric_eq_pseudometric + : NormedZmod_PseudoMetric_eq R M. +Proof. by constructor. Qed. + +HB.instance Definition _ := NormedZmod_PseudoMetric_eq_pseudometric. + +Lemma PseudoMetricNormedZmod_Lmodule_isNormedModule_pseudometric + : PseudoMetricNormedZmod_Lmodule_isNormedModule R M. +Proof. by constructor; exact: normrZ. Qed. + +HB.instance Definition _ := + PseudoMetricNormedZmod_Lmodule_isNormedModule_pseudometric. + +HB.end. + Lemma scaler1 {R : numFieldType} h : h%:A = h :> R. Proof. by rewrite /GRing.scale/= mulr1. Qed. From 0195d97d672cdc4170bb77edda70869d2f02d299 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 5 Jun 2025 13:06:33 +0900 Subject: [PATCH 2/3] fixes Co-authored-by: Quentin Vermande --- theories/normedtype_theory/normed_module.v | 46 +++++++++------------- 1 file changed, 19 insertions(+), 27 deletions(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index becea15534..7e4e29a10d 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/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. @@ -230,38 +230,36 @@ Module Exports. Export numFieldTopology.Exports. HB.reexport. End Exports. End numFieldNormedType. Import numFieldNormedType.Exports. -Definition pseudoMetric_normed (K : numFieldType) (M : normedZmodType K) : Type - := M. +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). -(*HB.instance Definition _ (K : numFieldType) (M : normedZmodType K) := - isPointed.Build M 0.*) +Module pseudoMetric_from_normedZmodType. Section pseudoMetric_from_normedZmodType. Variables (K : numFieldType) (M : normedZmodType K). Notation T := (pseudoMetric_normed M). -Local Definition ball (x : T) (r : K) : set T := ball_ Num.norm x r. +Definition ball (x : T) (r : K) : set T := ball_ Num.norm x r. -Local Definition ent : set_system (T * T) := entourage_ ball. +Definition ent : set_system (T * T) := entourage_ ball. -Local Definition nbhs (x : T) : set_system T := nbhs_ ent x. +Definition nbhs (x : T) : set_system T := nbhs_ ent x. -Local Lemma nbhsE : nbhs = nbhs_ ent. Proof. by []. Qed. +Lemma nbhsE : nbhs = nbhs_ ent. Proof. by []. Qed. -HB.instance Definition _ := hasNbhs.Build T nbhs. +#[export] HB.instance Definition _ := hasNbhs.Build T nbhs. -Local Lemma ball_center x (e : K) : 0 < e -> ball x e x. +Lemma ball_center x (e : K) : 0 < e -> ball x e x. Proof. by rewrite /ball/= subrr normr0. Qed. -Local Lemma ball_sym x y (e : K) : ball x e y -> ball y e x. +Lemma ball_sym x y (e : K) : ball x e y -> ball y e x. Proof. by rewrite /ball /= distrC. Qed. -Local Lemma ball_triangle x y z e1 e2 : ball x e1 y -> ball y e2 z -> +Lemma ball_triangle x y z e1 e2 : ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z. Proof. rewrite /ball /= => ? ?. @@ -269,13 +267,16 @@ rewrite -[x](subrK y) -(addrA (x + _)). by rewrite (le_lt_trans (ler_normD _ _))// ltrD. Qed. -Local Lemma entourageE : ent = entourage_ ball. +Lemma entourageE : ent = entourage_ ball. Proof. by []. Qed. -HB.instance Definition _ := @Nbhs_isPseudoMetric.Build K T +#[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 := { @@ -299,23 +300,14 @@ 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.saturate pseudoMetric_normed.*) - HB.instance Definition _ := PseudoMetric.copy M (pseudoMetric_normed M). -HB.instance Definition _ := isPointed.Build M 0. -Local Lemma NormedZmod_PseudoMetric_eq_pseudometric - : NormedZmod_PseudoMetric_eq R M. -Proof. by constructor. Qed. - -HB.instance Definition _ := NormedZmod_PseudoMetric_eq_pseudometric. +HB.instance Definition _ := isPointed.Build M 0. -Lemma PseudoMetricNormedZmod_Lmodule_isNormedModule_pseudometric - : PseudoMetricNormedZmod_Lmodule_isNormedModule R M. -Proof. by constructor; exact: normrZ. Qed. +HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R M erefl. HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule_pseudometric. + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R M normrZ. HB.end. From 2f6787374135191d9249e6c1ee430dd23db74f97 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 5 Jun 2025 19:10:55 +0900 Subject: [PATCH 3/3] fixes #1636 --- theories/topology_theory/bool_topology.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/theories/topology_theory/bool_topology.v b/theories/topology_theory/bool_topology.v index df8f74f0d9..bdd696a64a 100644 --- a/theories/topology_theory/bool_topology.v +++ b/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.