mv contents of file prodnormedzmodule

CHANGELOG_UNRELEASED.md

@@ -89,6 +89,10 @@
 
 - in `normed_module.v`:
   + implicit arguments of `squeeze_cvge` and `sequeeze_fin`
+- moved from `prodnormedzmodule.v` to `unstable.v`
+  + module `ProdNormedZmodule`
+    * definition `norm`
+    * lemmas `normD`, `norm_eq0`, `normMn`, `normrN`, `prod_normE`
 
 ### Renamed
 
@@ -174,6 +178,8 @@
     `setringDI`, `preimage_classes`, `preimage_classes_comp`
     (deprecated since 1.9.0)
 
+- file `prodnormedzmodule.v`
+
 ### Infrastructure
 
 ### Misc

classical/unstable.v

@@ -674,3 +674,46 @@ HB.instance Definition _ :=
 
 End max_nng_comlaw.
 End MaxNngComLaw.
+
+(* This module equips the product of two normedZmodTypes with a canonical
+   normedZmodType structure. *)
+Module ProdNormedZmodule.
+Section ProdNormedZmodule.
+Context {R : numDomainType} {U V : normedZmodType R}.
+
+Definition norm (x : U * V) : R := Num.max `|x.1| `|x.2|.
+
+Lemma normD x y : norm (x + y) <= norm x + norm y.
+Proof.
+rewrite /norm num_ge_max !(le_trans (ler_normD _ _)) ?lerD//;
+by rewrite comparable_le_max ?lexx ?orbT// real_comparable.
+Qed.
+
+Lemma norm_eq0 x : norm x = 0 -> x = 0.
+Proof.
+case: x => x1 x2 /eqP; rewrite eq_le num_ge_max 2!normr_le0 -andbA/=.
+by case/and3P => /eqP -> /eqP ->.
+Qed.
+
+Lemma normMn x n : norm (x *+ n) = (norm x) *+ n.
+Proof. by rewrite /norm pairMnE -mulr_natl maxr_pMr ?mulr_natl ?normrMn. Qed.
+
+Lemma normrN x : norm (- x) = norm x.
+Proof. by rewrite /norm/= !normrN. Qed.
+
+#[export]
+HB.instance Definition _ := Num.Zmodule_isNormed.Build R (U * V)%type
+  normD norm_eq0 normMn normrN.
+
+Lemma prod_normE (x : U * V) : `|x| = Num.max `|x.1| `|x.2|.
+Proof. by []. Qed.
+
+End ProdNormedZmodule.
+
+Module Exports.
+HB.reexport.
+Definition prod_normE := @prod_normE.
+End Exports.
+
+End ProdNormedZmodule.
+Export ProdNormedZmodule.Exports.

reals/prodnormedzmodule.v

@@ -4,72 +4,5 @@ From mathcomp Require Import boot order fingroup ssralg poly ssrnum.
 From mathcomp Require Import all_classical.
 From mathcomp Require Import interval_inference.
 
-(**md**************************************************************************)
-(* This file equips the product of two normedZmodTypes with a canonical       *)
-(* normedZmodType structure. It is a short file that has been added here for  *)
-(* convenience during the rebase of MathComp-Analysis on top of MathComp 1.1. *)
-(* The contents is likely to be moved elsewhere.                              *)
-(******************************************************************************)
-
-Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-
-Local Open Scope ring_scope.
-Import Order.TTheory GRing.Theory Num.Theory.
-
-Section Linear1.
-Context (R : pzRingType) (U : lmodType R) (V : zmodType) (s : R -> V -> V).
-(*HB.instance Definition _ := gen_eqMixin {linear U -> V | s}.*)
-(*Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]*)
-(*HB.instance Definition _ := gen_choiceMixin {linear U -> V | s}.*)
-(*Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]*)
-End Linear1.
-Section Linear2.
-Context (R : pzRingType) (U : lmodType R) (V : zmodType) (s : GRing.Scale.law R V).
-(*HB.instance Definition _ :=
-  isPointed.Build {linear U -> V | GRing.Scale.Law.sort s} \0.*)
-(*Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default]*)
-End Linear2.
-
-Module ProdNormedZmodule.
-Section ProdNormedZmodule.
-Context {R : numDomainType} {U V : normedZmodType R}.
-
-Definition norm (x : U * V) : R := Num.max `|x.1| `|x.2|.
-
-Lemma normD x y : norm (x + y) <= norm x + norm y.
-Proof.
-rewrite /norm num_ge_max !(le_trans (ler_normD _ _)) ?lerD//;
-by rewrite comparable_le_max ?lexx ?orbT// real_comparable.
-Qed.
-
-Lemma norm_eq0 x : norm x = 0 -> x = 0.
-Proof.
-case: x => x1 x2 /eqP; rewrite eq_le num_ge_max 2!normr_le0 -andbA/=.
-by case/and3P => /eqP -> /eqP ->.
-Qed.
-
-Lemma normMn x n : norm (x *+ n) = (norm x) *+ n.
-Proof. by rewrite /norm pairMnE -mulr_natl maxr_pMr ?mulr_natl ?normrMn. Qed.
-
-Lemma normrN x : norm (- x) = norm x.
-Proof. by rewrite /norm/= !normrN. Qed.
-
-#[export]
-HB.instance Definition _ := Num.Zmodule_isNormed.Build R (U * V)%type
-  normD norm_eq0 normMn normrN.
-
-Lemma prod_normE (x : U * V) : `|x| = Num.max `|x.1| `|x.2|.
-Proof. by []. Qed.
-
-End ProdNormedZmodule.
-
-Module Exports.
-HB.reexport.
-Definition prod_normE := @prod_normE.
-End Exports.
-
-End ProdNormedZmodule.
-Export ProdNormedZmodule.Exports.
+Attributes deprecated(since="mathcomp-analysis 1.18.0",
+  note="The contents have been moved to `unstable.v`").

theories/all_analysis.v

@@ -2,7 +2,6 @@ From mathcomp Require Export ereal.
 From mathcomp Require Export landau.
 From mathcomp Require Export topology.
 From mathcomp Require Export cantor.
-From mathcomp Require Export prodnormedzmodule.
 From mathcomp Require Export normedtype.
 From mathcomp Require Export realfun.
 From mathcomp Require Export sequences.

theories/derive.v

@@ -6,7 +6,7 @@ From mathcomp Require Import poly sesquilinear.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp contra classical_sets functions reals.
-From mathcomp Require Import topology prodnormedzmodule tvs normedtype landau.
+From mathcomp Require Import topology tvs normedtype landau.
 
 (**md**************************************************************************)
 (* # Differentiation                                                          *)

theories/exp.v

@@ -55,8 +55,7 @@ Proof. by rewrite qualifE/=. Qed.
 (* /PR to mathcomp in progress *)
 
 Section PseriesDiff.
-
-Variable R : realType.
+Context {R : realType}.
 
 Definition pseries f (x : R) := [series f i * x ^+ i]_i.
 
@@ -306,7 +305,7 @@ Qed.
 End PseriesDiff.
 
 Section expR.
-Variable R : realType.
+Context {R : realType}.
 Implicit Types x : R.
 
 Lemma expR0 : expR 0 = 1 :> R.
@@ -684,7 +683,7 @@ Notation ltr_expeR := lte_expeR (only parsing).
 Notation ler_expeR := lee_expeR (only parsing).
 
 Section Ln.
-Variable R : realType.
+Context {R : realType}.
 Implicit Types x : R.
 
 Notation exp := (@expR R).
@@ -822,7 +821,7 @@ Unshelve. end_near. Qed.
 End Ln.
 
 Section PowR.
-Variable R : realType.
+Context {R : realType}.
 Implicit Types a x y z r : R.
 
 Definition powR a x := if a == 0 then (x == 0)%:R else expR (x * ln a).
@@ -1146,7 +1145,7 @@ End PowR.
 Notation "a `^ x" := (powR a x) : ring_scope.
 
 Section Lne.
-Variable R : realType.
+Context {R : realType}.
 Implicit Types (x : \bar R) (r : R).
 Local Open Scope ereal_scope.
 
@@ -1454,7 +1453,7 @@ End poweR.
 Notation "a `^ x" := (poweR a x) : ereal_scope.
 
 Section riemannR_series.
-Variable R : realType.
+Context {R : realType}.
 Implicit Types a : R.
 Local Open Scope real_scope.
 

theories/landau.v

@@ -2,7 +2,7 @@
 From HB Require Import structures.
 From mathcomp Require Import boot order ssralg interval_inference ssrnum.
 From mathcomp Require Import boolp classical_sets functions reals.
-From mathcomp Require Import ereal topology normedtype prodnormedzmodule.
+From mathcomp Require Import ereal topology normedtype.
 
 (**md**************************************************************************)
 (* # Bachmann-Landau notations: $f=o(e)$, $f=O(e)$                            *)

theories/lebesgue_integral_theory/lebesgue_integral_definition.v

@@ -2,8 +2,6 @@
 From HB Require Import structures.
 From mathcomp Require Import boot order ssralg ssrnum ssrint interval.
 From mathcomp Require Import interval_inference finmap.
-#[warning="-warn-library-file-internal-analysis"]
-From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
 From mathcomp Require Import reals real_interval topology ereal tvs.
 From mathcomp Require Import normedtype sequences esum measure.

theories/normedtype_theory/matrix_normedtype.v

@@ -5,8 +5,7 @@ From mathcomp Require Import interval interval_inference.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp contra classical_sets reals topology.
-From mathcomp Require Import prodnormedzmodule tvs pseudometric_normed_Zmodule.
-From mathcomp Require Import normed_module.
+From mathcomp Require Import tvs pseudometric_normed_Zmodule normed_module.
 
 (**md**************************************************************************)
 (* # Normed topological Abelian group of matrices                             *)

theories/normedtype_theory/normed_module.v

@@ -7,8 +7,7 @@ From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets filter functions cardinality
   set_interval.
 From mathcomp Require Import reals real_interval ereal topology convex
-  prodnormedzmodule tvs num_normedtype ereal_normedtype
-  pseudometric_normed_Zmodule.
+  tvs num_normedtype ereal_normedtype pseudometric_normed_Zmodule.
 
 (**md**************************************************************************)
 (* # Normed modules                                                           *)

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -2,9 +2,11 @@
 From HB Require Import structures.
 From mathcomp Require Import boot order finmap ssralg ssrnum ssrint.
 From mathcomp Require Import interval interval_inference archimedean.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions cardinality.
 From mathcomp Require Import set_interval ereal reals topology.
-From mathcomp Require Import prodnormedzmodule num_normedtype.
+From mathcomp Require Import num_normedtype.
 
 (**md**************************************************************************)
 (* # Normed topological abelian groups                                        *)

theories/realfun.v

@@ -6,7 +6,7 @@ From mathcomp Require Import archimedean interval interval_inference.
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions cardinality contra.
 From mathcomp Require Import reals convex.
-From mathcomp Require Import topology ereal prodnormedzmodule tvs normedtype.
+From mathcomp Require Import topology ereal tvs normedtype.
 From mathcomp Require Import derive sequences real_interval numfun.
 
 (**md**************************************************************************)