Normedtype 20260924

CHANGELOG_UNRELEASED.md

@@ -13,6 +13,31 @@
   + lemma `limn_einf_cst`
 - in `uniform_structure.v`:
   + lemma `unif_continuous_continuous`
+- in `uniform_structure.v`:
+  + lemma `unif_continuous_comp`
+
+- in `initial_topology.v`:
+  + lemma `initial_unif_continuous`
+  + lemma `initial_unif_continuous_comp`
+  + lemma `initial_unif_continuous_comp_fst`
+  + lemma `initial_unif_continuous_comp_snd`
+
+- in `product_topology.v`:
+  + lemma `entourage_prod_exS`
+  + definition `interchange_prod`
+  + lemma `entourage_interchange_prod`
+  + lemma `pair_unif_continuous`
+  + lemma `fst_unif_continuous`
+  + lemma `snd_unif_continuous`
+
+- in `metric_space.v`:
+  + definition `prod_mdist`
+
+- in `pseudometric_normed_Zmodule.v`:
+  + lemma `PseudoMetricNormedZmodule_add_unif_continuous`
+  + lemma `PseudoMetricNormedZmodule_opp_unif_continuous`
+  + lemma `standard_scale_continuous`
+  + notation `topologicalNmodType`
 
 ### Changed
 
@@ -30,18 +55,77 @@
 
 ### Changed
 
+- moved from `tvs.v` to `pseudometric_normed_Zmodule.v`
+  + mixin `PreTopologicalNmodule_isTopologicalNmodule`
+  + structure `TopologicalNmodule`
+  + lemmas `fun_cvgD`, `cvg_sum`, `sum_continuous`
+  + mixin `TopologicalNmodule_isTopologicalZmodule`
+  + structure `TopologicalZmodule`, type `topologicalZmodType`
+  + lemmas `sub_continuous`, `fun_cvgN`
+  + factory `PreTopologicalNmodule_isTopologicalZmodule`
+  + mixin `PreUniformNmodule_isUniformNmodule`
+  + structure `UniformNmodule`
+  + mixin `UniformNmodule_isUniformZmodule`
+  + structure `UniformZmodule`
+  + factory `PreUniformNmodule_isUniformZmodule`
+  + lemma `sub_unif_continuous`
+
+- in `tvs.v`:
+  + structure `ConvexTvs` now inherits from `UniformZmodule`
+
+- move to `pseudometric_structure.v`:
+  + definitions `closed_ball_`, `closed_ball`
+  + lemmas `closure_ballE`, `closed_ballxx`, `closed_ball_closed`, `subset_closed_ball`,
+    `subset_closure_half`, `le_closed_ball`
+
 ### Renamed
 
 - in `sequences.v`:
   + `limn_einf_shift` -> `limn_einf_addl`
   + `series_le_cvg` -> `series_squeeze_is_cvgn`
+- in `pseudometric_normed_Zmodule.v`:
+  + `PseudoMetricNormedZmod0` -> `PseudoMetricNormedZmodule`
+  + `pseudoMetricNormedZmodType` -> `metricNormedZmodType`
+  + `PseudoMetricNormedZmod` -> `MetricNormedZmodule`
+
+- in `normed_module.v`:
+  + `PseudoMetricNormedZmod_ConvexTvs_isNormedModule` -> `MetricNormedZmod_ConvexTvs_isNormedModule`
 
 ### Generalized
 
+- in `pseudometric_normed_Zmodule.v`:
+  + from `pseudoMetricNormedZmodType` to `PseudoMetricNormedZmod0.type`:
+    * lemma `le0_ball0`
+    * lemma `cvg_bounded`
+    * lemma `bounded_cst`
+  + from `realFieldType` to `numFieldType`
+    * lemma `bounded_funN`
+    * lemma `bounded_funD`
+
+- in `pseudometric_normed_Zmodule.v`:
+  + lemmas `cvgD`, `cvg0D`, `cvgD0`, `cvgN`, `cvgNP`, `cvgB`, `cvg0B`, `cvgB0`, `cvgN0`,
+    `cvg_sub0`, `cvg0`, `subr_cvg0`
+  + lemmas `within_continuousD`, `within_continuousB`, `within_continuousN`
+  + lemmas `le_closed_ball`, `closed_ball0`
+
 ### Deprecated
 
+- in `pseudometric_normed_Zmodule.v`:
+  + lemma `fun_cvgD` (use `cvgD` instead)
+  + lemma `fun_cvgN` (use `cvgN` instead)
+
 ### Removed
 
+- in `tvs.v`:
+  + structure `PreUniformLmodule`
+  + mixin `PreUniformLmodule_isUniformLmodule`
+  + structure `UniformLmodule`
+  + factory `UniformNmodule_isUniformLmodule`
+  + lemma `prod_add_continuous` (remains accessible via the generic `add_continuous` of `TopologicalNmodule.type`)
+
+- in `pseudometric_normred_Zmodule.v`:
+  + lemma `pseudoMetricNormedZModType_hausdorff` (deprecated since 1.10.0)
+
 ### Infrastructure
 
 ### Misc

theories/esum.v

@@ -1016,7 +1016,7 @@ suff: ((fun n => C_ n - (A - B)) @ \oo --> (0 : R^o))%R.
   rewrite [X in  X - _]esummable_nneseries_lim//; first exact/esummable_funepos.
   rewrite [X in _ - X]esummable_nneseries_lim//; first exact/esummable_funeneg.
   rewrite -EFinB; apply/cvg_lim => //; apply/fine_cvgP; split; last first.
-    exact: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB).
+    exact: (@cvg_sub0 _ _ _ _ _ (cst (A - B)%R)).
   apply: nearW => n; rewrite fin_num_abs; apply: le_lt_trans Pf => /=.
   by rewrite -nneseries_esum// (le_trans (lee_abs_sum _ _ _))// nneseries_lim_ge.
 have : ((fun x => A_ x - B_ x) @ \oo --> A - B)%R.

theories/ftc.v

@@ -592,7 +592,7 @@ have GacFa : G x @[x --> a^'+] --> (- c + F a)%R.
     apply/cvgrPdist_le => /= e e0; near=> t.
     rewrite opprB GFc; first by rewrite in_itv/=; apply/andP.
     by rewrite addNr normr0 ltW.
-  have := @cvgD _ _ _ _ Fap _ _ _ _ GFac Fa.
+  have := @cvgD _ _ _ Fap _ _ _ _ GFac Fa.
   rewrite (_ : (G \- F) + F = G)%R//.
   by apply/funext => x/=; rewrite subrK.
 have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R.
@@ -601,7 +601,7 @@ have GbcFb : G x @[x --> b^'-] --> (- c + F b)%R.
     apply/cvgrPdist_le => /= e e0; near=> t.
     rewrite opprB GFc; first by rewrite in_itv/=; apply/andP.
     by rewrite addNr normr0 ltW.
-  have := @cvgD _ _ _ _ Fbn _ _ _ _ GFbc Fb.
+  have := @cvgD _ _ _ Fbn _ _ _ _ GFbc Fb.
   rewrite (_ : G \- F + F = G)%R //.
   by apply/funext => x/=; rewrite subrK.
 have contF : {within `[a, b], continuous F}.

theories/normedtype_theory/matrix_normedtype.v

@@ -286,6 +286,20 @@ elim/big_ind2 : _ => // [|a b c d bE dE]; first by rewrite mulr0.
 by rewrite !num_max bE dE maxr_pMr.
 Qed.
 
+HB.instance Definition _ (K : numFieldType) (m n : nat) :=
+  Uniform.on ('M[K]_(m, n)).
+
+Section matrix_UniformNZmodule.
+Context {K : numFieldType} {m n : nat}.
+
+HB.instance Definition _ := PreUniformNmodule_isUniformNmodule.Build
+  'M[K]_(m, n) (@PseudoMetricNormedZmodule_add_unif_continuous _ _).
+
+HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build
+  'M[K]_(m, n) (@PseudoMetricNormedZmodule_opp_unif_continuous _ _).
+
+End matrix_UniformNZmodule.
+
 HB.instance Definition _ (K : numFieldType) m n :=
   PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m, n)
     (@mx_normZ K m n).

theories/normedtype_theory/normed_module.v

@@ -74,7 +74,6 @@ Reserved Notation "k .-lipschitz f" (at level 2, format "k .-lipschitz  f").
 Reserved Notation "[ 'lipschitz' E | x 'in' A ]"
   (at level 0, x name, format "[ 'lipschitz'  E  |  x  'in'  A ]").
 
-Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -87,36 +86,41 @@ Local Open Scope ring_scope.
 
 (** Modules with a norm depending on a numDomain *)
 
-HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule K V
-    & PseudoMetricNormedZmod K V & ConvexTvs K V := {
+HB.mixin Record MetricNormedZmod_ConvexTvs_isNormedModule
+    (K : numDomainType) V & MetricNormedZmodule K V & ConvexTvs K V := {
   normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |;
 }.
 
+#[deprecated(since="mathcomp-analysis 1.19.0",
+             use=MetricNormedZmod_ConvexTvs_isNormedModule)]
+Notation PseudoMetricNormedZmod_ConvexTvs_isNormedModule x1 x2 :=
+  (MetricNormedZmod_ConvexTvs_isNormedModule x1 x2).
+
+Module PseudoMetricNormedZmod_ConvexTvs_isNormedModule.
+#[deprecated(since="mathcomp-analysis 1.19.0",
+             use=MetricNormedZmod_ConvexTvs_isNormedModule.Build)]
+Notation Build x1 x2 x3 :=
+  (MetricNormedZmod_ConvexTvs_isNormedModule.Build x1 x2 x3) (only parsing).
+End PseudoMetricNormedZmod_ConvexTvs_isNormedModule.
+
 #[short(type="normedModType")]
 HB.structure Definition NormedModule (K : numDomainType) :=
-  {T of PseudoMetricNormedZmod K T & ConvexTvs K T
-   & PseudoMetricNormedZmod_ConvexTvs_isNormedModule K T}.
+  {T of MetricNormedZmodule K T & ConvexTvs K T
+     & MetricNormedZmod_ConvexTvs_isNormedModule K T}.
 
 #[short(type="subNormedModType")]
 HB.structure Definition SubNormedModule (R : numDomainType)
-  (V : normedModType R) (S : pred V) :=
+    (V : normedModType R) (S : pred V) :=
   { U of SubChoice V S U & NormedModule R U & @GRing.SubLmodule R V S U
-       & @Num.SubNormedZmodule(*Zmodule_isSubSemiNormed*) R V S U &
-       @SubConvexTvs R V S U}.
+       & @Num.SubNormedZmodule R V S U & @SubConvexTvs R V S U}.
 
 HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule
-  (K : numFieldType) V & PseudoMetricNormedZmod K V & GRing.Lmodule K V := {
+  (K : numFieldType) V & MetricNormedZmodule K V & GRing.Lmodule K V := {
  normrZ : forall (l : K) (x : V), `| l *: x | = `| l | * `| x |;
 }.
 
 HB.builders Context K V & PseudoMetricNormedZmod_Lmodule_isNormedModule K V.
 
-(**md `add_continuous` has been moved to `pseudometric_normed_Zmodule.v`,
-  `scale_continuous` is proved but is not proved again anymore later in this
-  file. *)
-Let add_continuous : continuous (fun x : V * V => x.1 + x.2).
-Proof. exact: add_continuous. Qed.
-
 (** NB: we have almost the same proof in `tvs.v` *)
 Let scale_continuous : continuous (fun z : K^o * V => z.1 *: z.2).
 Proof.
@@ -157,27 +161,34 @@ move=> x B; rewrite -nbhs_ballE/= => -[r] r0 Bxr /=.
 by exists (ball x r) => //; split; [exists x, r|exact: ballxx].
 Qed.
 
-HB.instance Definition _ :=
-  PreTopologicalNmodule_isTopologicalNmodule.Build V add_continuous.
+(* NB: was needed until version 1.18.0 *)
+(*HB.instance Definition _ :=
+  PreTopologicalNmodule_isTopologicalNmodule.Build V add_continuous.*)
 HB.instance Definition _ :=
   TopologicalNmodule_isTopologicalLmodule.Build K V scale_continuous.
 HB.instance Definition _ := Uniform_isConvexTvs.Build K V locally_convex_set.
+
 HB.instance Definition _ :=
-  PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build K V normrZ.
+  MetricNormedZmod_ConvexTvs_isNormedModule.Build K V normrZ.
 
 HB.end.
 
 #[short(type="normedVectType")]
 HB.structure Definition NormedVector (K : numDomainType) :=
   {T of NormedModule K T & Vector K T}.
 
-(**md see also `Section standard_topology_pseudoMetricNormedZmod` in
+(**md see also `Section standard_topology_metricNormedZmod` in
   `pseudometric_normed_Zmodule.v` *)
 Section standard_topology_normedMod.
 Variable R : numFieldType.
 
+(* NB: was need until version 1.18.0
+HB.instance Definition _ := TopologicalZmodule_isTopologicalLmodule.Build
+  R^o R^o (@standard_scale_continuous R).
+*)
+
 HB.instance Definition _ :=
-  PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build R R^o (@normrM _).
+  MetricNormedZmod_ConvexTvs_isNormedModule.Build R R^o (@normrM _).
 
 End standard_topology_normedMod.
 
@@ -257,7 +268,7 @@ End numFieldNormedType.
 Import numFieldNormedType.Exports.
 
 Lemma within_continuous_compN {R : realFieldType} {K : numDomainType}
-    {U : pseudoMetricNormedZmodType K} (f : R -> U) (a b : R) :
+    {U : metricNormedZmodType K} (f : R -> U) (a b : R) :
   {within `[- b, - a], continuous f} -> {within `[a, b], continuous f \o -%R}.
 Proof.
 have [ab|ba _ |-> _] := ltgtP a b; last 2 first.
@@ -373,6 +384,12 @@ HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R M erefl.
 
 HB.instance Definition _ := isPseudoMetricNormedZmodule.Build R M.
 
+HB.instance Definition _ := PreUniformNmodule_isUniformNmodule.Build
+  M (@PseudoMetricNormedZmodule_add_unif_continuous _ M).
+
+HB.instance Definition _ := UniformNmodule_isUniformZmodule.Build
+  M (@PseudoMetricNormedZmodule_opp_unif_continuous _ M).
+
 HB.instance Definition _ :=
   PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R M normrZ.
 
@@ -1757,17 +1774,16 @@ apply/connected_intervalP/connected_continuous_connected => //.
 exact: segment_connected.
 Qed.
 
-Section prod_NormedModule.
+Section prod_normedModType.
 Context {K : numFieldType} {U V : normedModType K}.
 
 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 _ :=
-  PseudoMetricNormedZmod_ConvexTvs_isNormedModule.Build K (U * V)%type
-  prod_norm_scale.
+HB.instance Definition _ := MetricNormedZmod_ConvexTvs_isNormedModule.Build
+  K (U * V)%type prod_norm_scale.
 
-End prod_NormedModule.
+End prod_normedModType.
 
 (* Local properties in R *)
 
@@ -2662,6 +2678,14 @@ HB.instance Definition _ (V : vectType R) :=
 HB.instance Definition _ (V : vectType R) :=
   isPseudoMetricNormedZmodule.Build _ (max_space V).
 
+HB.instance Definition _ (V : vectType R) :=
+    PreUniformNmodule_isUniformNmodule.Build (max_space V)
+  (@PseudoMetricNormedZmodule_add_unif_continuous _ (max_space V)).
+
+HB.instance Definition _ (V : vectType R) :=
+    UniformNmodule_isUniformZmodule.Build (max_space V)
+  (@PseudoMetricNormedZmodule_opp_unif_continuous _ (max_space V)).
+
 HB.instance Definition _ (V : vectType R) :=
   PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V)
     (@Norm.normZ _ _ (@max_norm V)).