Fixes 1998

CHANGELOG_UNRELEASED.md

@@ -303,6 +303,10 @@
 - in `measurable_structure.v`:
   + lemmas `measurable_prod_g_measurableType`, `measurable_prod_g_measurableTypeR`
 
+- file `measurable_structure.v`:
+  + notations `preimage_class`, `image_class`, `sigma_algebra_preimage_class`,
+    `sigma_algebra_image_class`, `sigma_algebra_preimage_classE` (deprecated since 1.9.0)
+
 ### Infrastructure
 
 ### Misc

classical/classical_sets.v

@@ -108,6 +108,8 @@ From mathcomp Require Import mathcomp_extra boolp wochoice.
 (*               rectangle X Y := [set U `*` V | U in X & V in Y]             *)
 (*   preimage_set_system D f G == set system of the preimages by f of sets    *)
 (*                                in G                                        *)
+(*      image_set_system D f G == set system of the sets with a preimage      *)
+(*                                by f in G                                   *)
 (*               cross f g X Y := preimage_set_system setT f X                *)
 (*                                `|` preimage_set_system setT g Y            *)
 (*                     X `x` Y := cross fst snd X Y                           *)
@@ -1717,6 +1719,10 @@ Lemma preimage_set_systemS {T1 T2} (A B : set_system T2) (f : T1 -> T2) :
   preimage_set_system [set: _] f A `<=` preimage_set_system [set: _] f B.
 Proof. by move=> AB _ [C ? <-]; exists C => //; exact: AB. Qed.
 
+Definition image_set_system (aT rT : Type) (D : set aT) (f : aT -> rT)
+    (G : set (set aT)) : set (set rT) :=
+  [set B : set rT | G (D `&` f @^-1` B)].
+
 Section cross.
 Context {T T1 T2 : Type}.
 Implicit Types (X : set_system T1) (Y : set_system T2).

classical/filter.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
+From mathcomp Require Import all_ssreflect_compat algebra finmap.
 From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
 

classical/functions.v

@@ -2656,7 +2656,7 @@ Let mulrC : commutative (@GRing.mul (T -> M)).
 Proof. by move=> f g; rewrite funeqE => x; rewrite /GRing.mul/= mulrC. Qed.
 
 HB.instance Definition _ :=
-  GRing.PzRing_hasCommutativeMul.Build (T -> M) mulrC.
+  GRing.SemiRing_hasCommutativeMul.Build (T -> M) mulrC.
 
 End fct_comPzRingType.
 

classical/mathcomp_extra.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat finmap all_algebra.
+From mathcomp Require Import all_ssreflect_compat finmap algebra.
 
 (**md**************************************************************************)
 (* # MathComp extra                                                           *)

experimental_reals/discrete.v

@@ -6,7 +6,7 @@
 (* -------------------------------------------------------------------- *)
 From Corelib Require Setoid.
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp.classical Require Import boolp.
 From mathcomp Require Import xfinmap reals.
 

experimental_reals/distr.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp.classical Require Import boolp classical_sets mathcomp_extra.
 From mathcomp Require Import xfinmap constructive_ereal reals discrete.
 From mathcomp Require Import realseq realsum.

experimental_reals/realseq.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp Require Import bigenough.
 From mathcomp.classical Require Import boolp classical_sets functions.
 From mathcomp.classical Require Import mathcomp_extra.

experimental_reals/realsum.v

@@ -3,7 +3,7 @@
 (* Copyright (c) - 2015--2018 - Inria                                   *)
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp.classical Require Import boolp.

experimental_reals/xfinmap.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp Require Export finmap.
 
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)

reals/constructive_ereal.v

@@ -10,7 +10,7 @@
    incorporate it into mathcomp proper where it could then be used for
    bounds of intervals*)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
+From mathcomp Require Import all_ssreflect_compat algebra finmap.
 From mathcomp Require Import mathcomp_extra interval_inference.
 
 (**md**************************************************************************)

reals/reals.v

@@ -44,7 +44,7 @@
 (******************************************************************************)
 
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.

reals_stdlib/Rstruct.v

@@ -106,7 +106,7 @@ HB.instance Definition _ := GRing.Zmodule_isNzRing.Build R
   RmultA Rmult_1_l Rmult_1_r Rmult_plus_distr_r Rmult_plus_distr_l R1_neq_0.
 
 #[hnf]
-HB.instance Definition _ := GRing.PzRing_hasCommutativeMul.Build R Rmult_comm.
+HB.instance Definition _ := GRing.SemiRing_hasCommutativeMul.Build R Rmult_comm.
 
 Import Monoid.
 

theories/borel_hierarchy.v

@@ -1,5 +1,5 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp Require Import boolp classical_sets functions cardinality.
 From mathcomp Require Import reals topology normedtype sequences.
 From mathcomp Require Import measure lebesgue_measure measurable_realfun.

theories/ereal.v

@@ -5,7 +5,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
+From mathcomp Require Import all_ssreflect_compat algebra finmap.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.

theories/ess_sup_inf.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp Require Import boolp classical_sets functions cardinality.
 From mathcomp Require Import reals ereal topology normedtype sequences.
 From mathcomp Require Import measure lebesgue_measure measurable_realfun.

theories/hoelder.v

@@ -884,7 +884,7 @@ Proof. by move=> a/= f; rewrite !inE; exact: measurable_funM. Qed.
 HB.instance Definition _ := GRing.isScaleClosed.Build _ _ (@mfun _ _ T R)
   mfun_scaler_closed.
 
-HB.instance Definition _ := [SubZmodule_isSubLmodule of {mfun T >-> R} by <:].
+HB.instance Definition _ := [SubNmodule_isSubLSemiModule of {mfun T >-> R} by <:].
 
 End mfun_extra.
 
@@ -962,7 +962,7 @@ HB.instance Definition _ := GRing.isOppClosed.Build _ Lfun
   Lfun_oppr_closed.
 
 (* NB: not used directly by HB.instance *)
-Lemma Lfun_addr_closed : addr_closed Lfun.
+Lemma Lfun_addr_closed : Algebra.nmod_closed Lfun.
 Proof.
 split.
   by rewrite inE rpred0/= inE/=; exact: finite_norm_cst0.

theories/homotopy_theory/continuous_path.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat generic_quotient all_algebra.
+From mathcomp Require Import all_ssreflect_compat generic_quotient algebra.
 From mathcomp Require Import finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop reals topology wedge_sigT.

theories/homotopy_theory/wedge_sigT.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra generic_quotient.
+From mathcomp Require Import all_ssreflect_compat algebra generic_quotient.
 From mathcomp Require Import finmap.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.

theories/lebesgue_integral_theory/giry.v

@@ -1,5 +1,5 @@
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra boolp classical_sets.
+From mathcomp Require Import all_ssreflect_compat algebra boolp classical_sets.
 From mathcomp Require Import fsbigop functions reals topology separation_axioms.
 From mathcomp Require Import ereal sequences numfun measure measurable_realfun.
 From mathcomp Require Import lebesgue_measure lebesgue_integral.

theories/measure_theory/counting_measure.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
+From mathcomp Require Import all_ssreflect_compat algebra finmap.
 From mathcomp Require Import boolp classical_sets functions cardinality reals.
 From mathcomp Require Import interval_inference ereal topology normedtype.
 From mathcomp Require Import sequences measurable_structure measure_function.

theories/measure_theory/dirac_measure.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
+From mathcomp Require Import all_ssreflect_compat algebra finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets.
 From mathcomp Require Import functions cardinality fsbigop reals.
 From mathcomp Require Import interval_inference ereal topology normedtype.

theories/measure_theory/measurable_function.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions cardinality reals.

theories/measure_theory/measurable_structure.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
+From mathcomp Require Import all_ssreflect_compat algebra finmap.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions cardinality reals.
@@ -98,8 +98,6 @@ From mathcomp Require Import ereal topology normedtype sequences.
 (*                                   This is an HB alias.                     *)
 (*      f.-preimage.-measurable A == A is measurable for                      *)
 (*                                   g_sigma_algebra_preimage f               *)
-(*         image_set_system D f G == set system of the sets with a preimage   *)
-(*                                   by f in G                                *)
 (*    subset_sigma_subadditive mu == alternative predicate defining           *)
 (*                                   sigma-subadditivity                      *)
 (* ```                                                                        *)
@@ -1380,10 +1378,6 @@ Notation "f .-preimage" := (preimage_display f) : measure_display_scope.
 Notation "f .-preimage.-measurable" :=
   (measurable : set (set (g_sigma_algebra_preimageType f))) : classical_set_scope.
 
-Definition image_set_system (aT rT : Type) (D : set aT) (f : aT -> rT)
-    (G : set (set aT)) : set (set rT) :=
-  [set B : set rT | G (D `&` f @^-1` B)].
-
 Lemma sigma_algebra_image (aT rT : Type) (D : set aT) (f : aT -> rT)
     (G : set (set aT)) :
   sigma_algebra D G -> sigma_algebra setT (image_set_system D f G).
@@ -1423,17 +1417,6 @@ by move=> _ [B mB <-]; exact: sG'sfun.
 Qed.
 
 End measurability.
-#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `preimage_set_system`")]
-Notation preimage_class := preimage_set_system (only parsing).
-#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `image_set_system`")]
-Notation image_class := image_set_system (only parsing).
-#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sigma_algebra_preimage`")]
-Notation sigma_algebra_preimage_class := sigma_algebra_preimage (only parsing).
-#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `sigma_algebra_image`")]
-Notation sigma_algebra_image_class := sigma_algebra_image (only parsing).
-
-#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `g_sigma_preimageE`")]
-Notation sigma_algebra_preimage_classE := g_sigma_preimageE (only parsing).
 
 (** This predicate is used also by `measure_function.v` *)
 Definition subset_sigma_subadditive {T} {R : numFieldType}

theories/measure_theory/measure_extension.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
 From mathcomp Require Import reals interval_inference ereal topology normedtype.
 From mathcomp Require Import sequences esum.

theories/measure_theory/measure_function.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
+From mathcomp Require Import all_ssreflect_compat algebra finmap.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.

theories/measure_theory/measure_negligible.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions cardinality reals.

theories/measure_theory/probability_measure.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat all_algebra.
+From mathcomp Require Import all_ssreflect_compat algebra.
 From mathcomp Require Import boolp classical_sets functions cardinality reals.
 From mathcomp Require Import interval_inference ereal topology normedtype.
 From mathcomp Require Import measurable_structure measure_function dirac_measure.

theories/normedtype_theory/normed_module.v

@@ -186,7 +186,7 @@ Module numFieldNormedType.
 Section realType.
 Variable (R : realType).
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ := GRing.ComAlgebra.copy R R^o.
+HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o.
 #[export, non_forgetful_inheritance]
 HB.instance Definition _ := Vector.copy R R^o.
 #[export, non_forgetful_inheritance]
@@ -196,7 +196,7 @@ End realType.
 Section rcfType.
 Variable (R : rcfType).
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ := GRing.ComAlgebra.copy R R^o.
+HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o.
 #[export, non_forgetful_inheritance]
 HB.instance Definition _ := Vector.copy R R^o.
 #[export, non_forgetful_inheritance]
@@ -206,7 +206,7 @@ End rcfType.
 Section archiFieldType.
 Variable (R : archiRealFieldType).
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ := GRing.ComAlgebra.copy R R^o.
+HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o.
 #[export, non_forgetful_inheritance]
 HB.instance Definition _ := Vector.copy R R^o.
 #[export, non_forgetful_inheritance]
@@ -216,7 +216,7 @@ End archiFieldType.
 Section realFieldType.
 Variable (R : realFieldType).
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ := GRing.ComAlgebra.copy R R^o.
+HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o.
 #[export, non_forgetful_inheritance]
 HB.instance Definition _ := Vector.copy R R^o.
 #[export, non_forgetful_inheritance]
@@ -228,7 +228,7 @@ End realFieldType.
 Section numClosedFieldType.
 Variable (R : numClosedFieldType).
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ := GRing.ComAlgebra.copy R R^o.
+HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o.
 #[export, non_forgetful_inheritance]
 HB.instance Definition _ := Vector.copy R R^o.
 #[export, non_forgetful_inheritance]
@@ -240,7 +240,7 @@ End numClosedFieldType.
 Section numFieldType.
 Variable (R : numFieldType).
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ := GRing.ComAlgebra.copy R R^o.
+HB.instance Definition _ := GRing.ComNzAlgebra.copy R R^o.
 #[export, non_forgetful_inheritance]
 HB.instance Definition _ := Vector.copy R R^o.
 #[export, non_forgetful_inheritance]
@@ -2727,7 +2727,7 @@ have NC0 : continuous (N : max_space V -> R).
   by near: y; apply: cvgr_dist_le; [exact: cvg_id|exact: divr_gt0].
 have: compact [set x : max_space V | `|x| = 1].
   apply: (subclosed_compact _ (@sup_closed_ball_compact V)).
-  - apply: (@closed_comp _ _ _ [set 1 : R]); last exact: closed_eq.
+  - apply: (@preimage_closed _ _ _ [set 1 : R]); last exact: closed_eq.
     by move=> *; exact: norm_continuous.
   - by move => x/=; rewrite closed_ballE// /closed_ball_/= sub0r normrN => ->.
 move=> /(@continuous_compact _ _ (N : max_space V -> R)) -/(_ _)/wrap[].

theories/normedtype_theory/tvs.v

@@ -472,7 +472,7 @@ exists [set a | exists2 b, B b & \val @^-1` b = a].
   - by move: ra; rewrite -ba !inE.
   - by move: sa; rewrite -ba !inE.
 split => /=.
-  move=> a/= [b Bb <-]; rewrite /open/= /wopen/=; exists b => //.
+  move=> a/= [b Bb <-]; rewrite /open/= /initial_open/=; exists b => //.
   exact: openB.
 move=> x a [/= b [[/=c openc] cb bx ba]].
 rewrite /nbhs/= /filter_from/=.

theories/numfun.v

@@ -1146,10 +1146,10 @@ by rewrite ler_pdivrMr//= ler_pMr// ?subr_gt0// ler1n.
 Unshelve. all: by end_near. Qed.
 
 (* NB: should appear in MathComp 2.6.0 (PR #1586) *)
-Notation "[ 'SubZmodule_isSubPzRing' 'of' U 'by' <: ]" :=
-  (GRing.SubZmodule_isSubPzRing.Build _ _ U (subringClosedP _))
+(*Notation "[ 'SubZmodule_isSubPzRing' 'of' U 'by' <: ]" :=
+  (GRing.SubNmodule_isSubPzSemiRing.Build _ _ U (subringClosedP _))
   (format "[ 'SubZmodule_isSubPzRing'  'of'  U  'by'  <: ]")
-  : form_scope.
+  : form_scope.*)
 
 Section ring.
 Context (aT : Type) (rT : pzRingType).
@@ -1162,7 +1162,7 @@ Qed.
 
 HB.instance Definition _ :=
    @GRing.isMulClosed.Build _ (@fimfun aT rT) fimfun_mulr_closed.
-HB.instance Definition _ := [SubZmodule_isSubPzRing of {fimfun aT >-> rT} by <:].
+HB.instance Definition _ := [SubNmodule_isSubPzSemiRing of {fimfun aT >-> rT} by <:].
 
 Implicit Types f g : {fimfun aT >-> rT}.