measurable types are not pointed by default any more (#1949)

* measurable types are not pointed by default any more

---------

Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -78,6 +78,8 @@
 
 - in `measure_extension.v`:
   + definition `caratheodory_measure`
+- in `measurable_structure.v`:
+  + structure `PMeasurable`, notation `pmeasurableType`
 
 ### Changed
 
@@ -163,6 +165,29 @@
 - in `measurable_structure.v`:
   + lemma `sigma_algebra_measurable` (not specialized to `setT` anymore)
 
+- in `measurable_function.v`:
+  + lemma `preimage_set_system_measurable_fun`
+
+- in `measurable_structure.v`
+  + structure `SemiRingOfSets`, mixin `isSigmaRing`, factories `isRingOfSets`,
+    `isRingOfSets_setY`, `isAlgebraOfSets`, `isAlgebraOfSets_setD`, `isMeasurable`
+    are not required to be pointed anymore
+  + lemmas `measurable_g_measurableTypeE`, `g_sigma_algebra_preimageType`,
+    `g_sigma_algebra_preimage`, `g_sigma_preimageE`, `g_sigma_preimageE`,
+    `g_sigma_algebra_rectangle` are  generalized from `pointedType` to `choiceType`
+    (the list might not be exhaustive)
+
+- in `ereal.v`:
+  + lemma `funID` generalized from `pointedType` to `Type`
+
+- in `numfun.v`:
+  + lemma `indic_restrict` generalized from `pointedType` to `Type`
+  + factory `FiniteDecomp` generalized from `pointedType`/`nzRingType` to
+    `Type/pzRingType`
+
+- in `simple_functions.v`:
+  + lemmas `fctD`, `fctN`, `fctM`, `fctZ`
+
 ### Deprecated
 
 ### Removed

theories/ereal.v

@@ -353,7 +353,7 @@ End DualAddTheory.
 
 HB.instance Definition _ (R : numDomainType) := isPointed.Build (\bar R) 0%E.
 
-Lemma funID {aT : pointedType} (D : set aT) {R : numDomainType}
+Lemma funID {aT : Type} (D : set aT) {R : numDomainType}
   (f : aT -> \bar R) : f = (f \_ (~` D)) \+ (f \_ D).
 Proof.
 by apply/funext => x; rewrite !patchE in_setC; case: ifPn => [xD|/negPn ->];

theories/kernel.v

@@ -195,8 +195,10 @@ Lemma measure_fam_uubP : measure_fam_uub <->
   exists r : {posnum R}, forall x, k x [set: Y] < r%:num%:E.
 Proof.
 split => [|] [r kr]; last by exists r%:num.
-suff r_gt0 : (0 < r)%R by exists (PosNum r_gt0).
-by rewrite -lte_fin; exact: le_lt_trans (kr point).
+have [[point _]|/forallNP empty] := pselect (exists r : X, True).
+  suff r_gt0 : (0 < r)%R by exists (PosNum r_gt0).
+  rewrite -lte_fin; exact: le_lt_trans (kr point).
+by exists (PosNum ltr01) => x; have := empty x.
 Qed.
 
 End measure_fam_uub.
@@ -925,7 +927,7 @@ HB.instance Definition _ (P : probability Y R):=
 End knormalize.
 
 Lemma measurable_fun_mnormalize d d' (X : measurableType d)
-    (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) :
+    (Y : pmeasurableType d') (R : realType) (k : R.-ker X ~> Y) :
   measurable_fun [set: X] (fun x => mnormalize (k x) point : pprobability Y R).
 Proof.
 apply: (measurability (@pset _ _ _ : set (set (pprobability Y R)))) => //.
@@ -1123,9 +1125,11 @@ HB.instance Definition _ n := @isMeasurableFun.Build _ _ _ _ _ (mk_2 n).
 
 Let fk_2 n : finite_set (range (k_2 n)).
 Proof.
-have := fimfunP (k_ n).
-suff : range (k_ n) = range (k_2 n) by move=> <-.
-by apply/seteqP; split => r [y ?] <-; [exists (point, y)|exists y.2].
+have [[point _]|/forallNP empty] := pselect (exists point : X, True).
+  have := fimfunP (k_ n).
+  suff : range (k_ n) = range (k_2 n) by move=> <-.
+  by apply/seteqP; split => r [y ?] <-; [exists (point, y)|exists y.2].
+by rewrite (_ : range _ = set0)// -subset0 => r [[x]]; have := empty x.
 Qed.
 
 HB.instance Definition _ n := @FiniteImage.Build _ _ _ (fk_2 n).

theories/lebesgue_integral_theory/simple_functions.v

@@ -29,6 +29,7 @@ From mathcomp Require Import lebesgue_measure numfun realfun measurable_realfun.
 (* Detailed contents:                                                         *)
 (* ````                                                                       *)
 (*         {sfun T >-> R} == type of simple functions                         *)
+(*                           They form a (potentially zero) ring.             *)
 (*       {nnsfun T >-> R} == type of non-negative simple functions            *)
 (*          indic_sfun mD := mindic _ mD                                      *)
 (*             cst_sfun r == constant simple function                         *)
@@ -149,13 +150,13 @@ Lemma cst_sfunE x : @cst_sfun x =1 cst x. Proof. by []. Qed.
 End sfun.
 
 (* a better way to refactor function stuffs *)
-Lemma fctD (T : pointedType) (K : pzRingType) (f g : T -> K) : f + g = f \+ g.
+Lemma fctD (T : Type) (K : pzRingType) (f g : T -> K) : f + g = f \+ g.
 Proof. by []. Qed.
-Lemma fctN (T : pointedType) (K : pzRingType) (f : T -> K) : - f = \- f.
+Lemma fctN (T : Type) (K : pzRingType) (f : T -> K) : - f = \- f.
 Proof. by []. Qed.
-Lemma fctM (T : pointedType) (K : pzRingType) (f g : T -> K) : f * g = f \* g.
+Lemma fctM (T : Type) (K : pzRingType) (f g : T -> K) : f * g = f \* g.
 Proof. by []. Qed.
-Lemma fctZ (T : pointedType) (K : pzRingType) (L : lmodType K) k (f : T -> L) :
+Lemma fctZ (T : Type) (K : pzRingType) (L : lmodType K) k (f : T -> L) :
    k *: f = k \*: f.
 Proof. by []. Qed.
 Arguments cst _ _ _ _ /.
@@ -172,7 +173,7 @@ Qed.
 
 HB.instance Definition _ := GRing.isSubringClosed.Build _ sfun
   sfun_subring_closed.
-HB.instance Definition _ := [SubChoice_isSubComNzRing of {sfun aT >-> rT} by <:].
+HB.instance Definition _ := [SubChoice_isSubComPzRing of {sfun aT >-> rT} by <:].
 
 Implicit Types (f g : {sfun aT >-> rT}).
 

theories/measurable_realfun.v

@@ -1071,6 +1071,12 @@ HB.instance Definition _ :=
 
 End mfun_realType.
 
+(* NB: should appear in MathComp 2.6.0 (PR #1586) *)
+Notation "[ 'SubChoice_isSubComPzRing' 'of' U 'by' <: ]" :=
+  (GRing.SubChoice_isSubComPzRing.Build _ _ U (subringClosedP _))
+  (format "[ 'SubChoice_isSubComPzRing'  'of'  U  'by'  <: ]")
+  : form_scope.
+
 Section ring.
 Context d (aT : measurableType d) (rT : realType).
 
@@ -1083,7 +1089,8 @@ split=> [|f g|f g]; rewrite !inE/=.
 Qed.
 HB.instance Definition _ := GRing.isSubringClosed.Build _
   (@mfun d default_measure_display aT rT) mfun_subring_closed.
-HB.instance Definition _ := [SubChoice_isSubComNzRing of {mfun aT >-> rT} by <:].
+
+HB.instance Definition _ := [SubChoice_isSubComPzRing of {mfun aT >-> rT} by <:].
 
 Implicit Types (f g : {mfun aT >-> rT}).
 

theories/measure_theory/measurable_function.v

@@ -210,19 +210,11 @@ HB.instance Definition _ x := isMeasurableFun.Build d _ aT rT (cst x)
 
 End mfun.
 
-Section measurable_fun_measurableType.
-Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2)
-        (T3 : measurableType d3).
+Section measurable_fun_restrict.
+Context d1 d2 d3 (T1 : measurableType d1) (T2 : pmeasurableType d2)
+  (T3 : measurableType d3).
 Implicit Type D E : set T1.
 
-Lemma measurableT_comp (f : T2 -> T3) E (g : T1 -> T2) :
-  measurable_fun [set: T2] f -> measurable_fun E g -> measurable_fun E (f \o g).
-Proof. exact: measurable_comp. Qed.
-
-Lemma measurable_funTS D (f : T1 -> T2) :
-  measurable_fun [set: T1] f -> measurable_fun D f.
-Proof. exact: measurable_funS. Qed.
-
 Lemma measurable_restrict D E (f : T1 -> T2) : measurable D -> measurable E ->
   measurable_fun (E `&` D) f <-> measurable_fun E (f \_ D).
 Proof.
@@ -244,6 +236,21 @@ Proof.
 by move=> mD; have := measurable_restrict f mD measurableT; rewrite setTI.
 Qed.
 
+End measurable_fun_restrict.
+
+Section measurable_fun_measurableType.
+Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2)
+  (T3 : measurableType d3).
+Implicit Type D E : set T1.
+
+Lemma measurableT_comp (f : T2 -> T3) E (g : T1 -> T2) :
+  measurable_fun [set: T2] f -> measurable_fun E g -> measurable_fun E (f \o g).
+Proof. exact: measurable_comp. Qed.
+
+Lemma measurable_funTS D (f : T1 -> T2) :
+  measurable_fun [set: T1] f -> measurable_fun D f.
+Proof. exact: measurable_funS. Qed.
+
 Lemma measurable_fun_ifT (g h : T1 -> T2) (f : T1 -> bool)
     (mf : measurable_fun [set: T1] f) :
   measurable_fun [set: T1] g -> measurable_fun [set: T1] h ->
@@ -360,7 +367,7 @@ Arguments g_sigma_algebra_preimage_comp {d T d1 T1 d2 T2 X} f.
 Section measurability.
 
 (* f is measurable on the sigma-algebra generated by itself *)
-Lemma preimage_set_system_measurable_fun d (aT : pointedType)
+Lemma preimage_set_system_measurable_fun d (aT : choiceType)
     (rT : measurableType d) (D : set aT) (f : aT -> rT) :
   measurable_fun
     (D : set (g_sigma_algebraType (preimage_set_system D f measurable))) f.

theories/measure_theory/measurable_structure.v

@@ -35,6 +35,8 @@ From mathcomp Require Import ereal topology normedtype sequences.
 (*                            The HB class is AlgebraOfsets.                  *)
 (*          measurableType == the type of sigma-algebras                      *)
 (*                            The HB class is Measurable.                     *)
+(*         pmeasurableType == the type of pointed sigma-algebras              *)
+(*                            The HB class is PMeasurable.                    *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* ## Instances of mathematical structures                                    *)
@@ -856,7 +858,7 @@ HB.mixin Record isSemiRingOfSets (d : measure_display) T := {
 
 #[short(type="semiRingOfSetsType")]
 HB.structure Definition SemiRingOfSets d :=
-  {T of Pointed T & isSemiRingOfSets d T}.
+  {T of Choice T & isSemiRingOfSets d T}.
 
 Arguments measurable {d}%_measure_display_scope {s} _%_classical_set_scope.
 
@@ -906,7 +908,7 @@ HB.end.
 HB.structure Definition SigmaRing d :=
   {T of SemiRingOfSets d T & hasMeasurableCountableUnion d T}.
 
-HB.factory Record isSigmaRing (d : measure_display) T & Pointed T := {
+HB.factory Record isSigmaRing (d : measure_display) T & Choice T := {
   measurable : set (set T) ;
   measurable0 : measurable set0 ;
   measurableD : setD_closed measurable ;
@@ -934,7 +936,10 @@ HB.end.
 HB.structure Definition Measurable d :=
   {T of AlgebraOfSets d T & hasMeasurableCountableUnion d T }.
 
-HB.factory Record isRingOfSets (d : measure_display) T & Pointed T := {
+#[short(type="pmeasurableType")]
+HB.structure Definition PMeasurable d := {T of Pointed T & Measurable d T}.
+
+HB.factory Record isRingOfSets (d : measure_display) T & Choice T := {
   measurable : set (set T) ;
   measurable0 : measurable set0 ;
   measurableU : setU_closed measurable;
@@ -958,7 +963,7 @@ HB.instance Definition _ := SemiRingOfSets_isRingOfSets.Build d T measurableU.
 HB.end.
 
 HB.factory Record isRingOfSets_setY (d : measure_display) T
-    & Pointed T := {
+    & Choice T := {
   measurable : set (set T) ;
   measurable_nonempty : measurable !=set0 ;
   measurable_setY : setY_closed measurable ;
@@ -989,7 +994,7 @@ HB.instance Definition _ := isRingOfSets.Build d T m0 mU mD.
 
 HB.end.
 
-HB.factory Record isAlgebraOfSets (d : measure_display) T & Pointed T := {
+HB.factory Record isAlgebraOfSets (d : measure_display) T & Choice T := {
   measurable : set (set T) ;
   measurable0 : measurable set0 ;
   measurableU : setU_closed measurable;
@@ -1014,7 +1019,7 @@ HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.
 
 HB.end.
 
-HB.factory Record isAlgebraOfSets_setD (d : measure_display) T & Pointed T := {
+HB.factory Record isAlgebraOfSets_setD (d : measure_display) T & Choice T := {
   measurable : set (set T) ;
   measurableT : measurable [set: T] ;
   measurableD : setD_closed measurable
@@ -1038,7 +1043,7 @@ HB.instance Definition _ := RingOfSets_isAlgebraOfSets.Build d T measurableT.
 
 HB.end.
 
-HB.factory Record isMeasurable (d : measure_display) T & Pointed T := {
+HB.factory Record isMeasurable (d : measure_display) T & Choice T := {
   measurable : set (set T) ;
   measurable0 : measurable set0 ;
   measurableC : forall A, measurable A -> measurable (~` A) ;
@@ -1282,12 +1287,12 @@ Proof. exact. Qed.
 Definition g_sigma_algebraType {T} (G : set (set T)) := T.
 
 Section g_salgebra_instance.
-Variables (T : pointedType) (G : set (set T)).
+Variables (T : choiceType) (G : set (set T)).
 
 Lemma sigma_algebraC (A : set T) : <<s G >> A -> <<s G >> (~` A).
 Proof. by move=> sGA; rewrite -setTD; exact: sigma_algebraCD. Qed.
 
-HB.instance Definition _ := Pointed.on (g_sigma_algebraType G).
+HB.instance Definition _ := Choice.on (g_sigma_algebraType G).
 HB.instance Definition _ := @isMeasurable.Build (sigma_display G)
   (g_sigma_algebraType G)
   <<s G >> (@sigma_algebra0 _ setT G) (@sigma_algebraC)
@@ -1299,7 +1304,7 @@ Notation "G .-sigma" := (sigma_display G) : measure_display_scope.
 Notation "G .-sigma.-measurable" :=
   (measurable : set (set (g_sigma_algebraType G))) : classical_set_scope.
 
-Lemma measurable_g_measurableTypeE (T : pointedType) (G : set (set T)) :
+Lemma measurable_g_measurableTypeE (T : choiceType) (G : set (set T)) :
   sigma_algebra setT G -> G.-sigma.-measurable = G.
 Proof. exact: sigma_algebra_id. Qed.
 
@@ -1326,15 +1331,15 @@ Qed.
 Definition preimage_display {T T'} : (T -> T') -> measure_display.
 Proof. exact. Qed.
 
-Definition g_sigma_algebra_preimageType d' (T : pointedType)
+Definition g_sigma_algebra_preimageType d' (T : choiceType)
   (T' : measurableType d') (f : T -> T') : Type := T.
 
-Definition g_sigma_algebra_preimage d' (T : pointedType)
+Definition g_sigma_algebra_preimage d' (T : choiceType)
     (T' : measurableType d') (f : T -> T') :=
   preimage_set_system setT f (@measurable _ T').
 
 Section preimage_generated_sigma_algebra.
-Context {d'} (T : pointedType) (T' : measurableType d').
+Context {d'} (T : choiceType) (T' : measurableType d').
 Variable f : T -> T'.
 
 Let preimage_set0 : g_sigma_algebra_preimage f set0.
@@ -1363,7 +1368,7 @@ rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _.
 by case: (mg k) => _; rewrite setTI.
 Qed.
 
-HB.instance Definition _ := Pointed.on (g_sigma_algebra_preimageType f).
+HB.instance Definition _ := Choice.on (g_sigma_algebra_preimageType f).
 
 HB.instance Definition _ := @isMeasurable.Build (preimage_display f)
   (g_sigma_algebra_preimageType f) (g_sigma_algebra_preimage f)
@@ -1393,7 +1398,7 @@ move=> [G0 GC GU]; split; rewrite /image_set_system.
 - by move=> F /= mF; rewrite preimage_bigcup setI_bigcupr; exact: GU.
 Qed.
 
-Lemma g_sigma_preimageE aT (rT : pointedType) (D : set aT)
+Lemma g_sigma_preimageE aT (rT : choiceType) (D : set aT)
     (f : aT -> rT) (G' : set (set rT)) :
   <<s D, preimage_set_system D f G' >> =
     preimage_set_system D f (G'.-sigma.-measurable).
@@ -1539,7 +1544,7 @@ move=> sA sB; split=> [AB|AB]; last by rewrite AB.
 by apply/seteqP; split; exact/AB.
 Qed.
 
-Lemma g_sigma_algebra_cross {T1 T2 : pointedType} (X : set_system T1)
+Lemma g_sigma_algebra_cross {T1 T2 : choiceType} (X : set_system T1)
     (Y : set_system T2) :
   <<s X `x` <<s Y >> >> = <<s X `x` Y >>.
 Proof.
@@ -1562,7 +1567,7 @@ Notation preimage_classes := g_sigma_preimageU (only parsing).
 
 Section product_lemma.
 Context d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2).
-Variables (T : pointedType) (f1 : T -> T1) (f2 : T -> T2).
+Variables (T : choiceType) (f1 : T -> T1) (f2 : T -> T2).
 Variables (T3 : Type) (g : T3 -> T).
 
 Lemma g_sigma_preimageU_comp : g_sigma_preimageU (f1 \o g) (f2 \o g) =
@@ -1604,7 +1609,7 @@ Let prod_salgebra_bigcup (F : _^nat) :
   g_sigma_preimageU f1 f2 (\bigcup_i (F i)).
 Proof. exact: sigma_algebra_bigcup. Qed.
 
-HB.instance Definition _ := Pointed.on (T1 * T2)%type.
+HB.instance Definition _ := Choice.on (T1 * T2)%type.
 HB.instance Definition prod_salgebra_mixin :=
   @isMeasurable.Build (measure_prod_display (d1, d2))
     (T1 * T2)%type (g_sigma_preimageU f1 f2)
@@ -1626,7 +1631,7 @@ rewrite -(setIT A) -(setTI B) setXI setXT setTX; apply: measurableI.
 - by apply: sub_sigma_algebra; right; exists B => //; rewrite setTI.
 Qed.
 
-Lemma g_sigma_algebra_rectangle {T1 T2 : pointedType} (X : set_system T1)
+Lemma g_sigma_algebra_rectangle {T1 T2 : choiceType} (X : set_system T1)
     (Y : set_system T2) : X [set: T1] -> Y [set: T2] ->
   <<s rectangle X Y >> = <<s X `x` Y >>.
 Proof.
@@ -1657,7 +1662,7 @@ End product_salgebra_algebraOfSetsType.
 Notation measurable_prod_measurableType := prod_measurable_rectangle (only parsing).
 
 Section product_salgebra_g_measurableTypeR.
-Context d1 (T1 : algebraOfSetsType d1) (T2 : pointedType) (C2 : set (set T2)).
+Context d1 (T1 : algebraOfSetsType d1) (T2 : choiceType) (C2 : set (set T2)).
 Hypothesis setTC2 : setT `<=` C2.
 
 #[deprecated(since="mathcomp-analysis 1.17.0")]
@@ -1674,7 +1679,7 @@ Qed.
 End product_salgebra_g_measurableTypeR.
 
 Section product_salgebra_g_measurableType.
-Variables (T1 T2 : pointedType) (C1 : set (set T1)) (C2 : set (set T2)).
+Variables (T1 T2 : choiceType) (C1 : set (set T1)) (C2 : set (set T2)).
 Hypotheses (setTC1 : setT `<=` C1) (setTC2 : setT `<=` C2).
 
 #[deprecated(since="mathcomp-analysis 1.17.0")]
@@ -1695,7 +1700,7 @@ Definition g_sigma_preimage d (rT : semiRingOfSetsType d) (aT : Type)
   <<s \big[setU/set0]_(i < n) preimage_set_system setT (f i) measurable >>.
 
 Lemma g_sigma_preimage_comp d1 {T1 : semiRingOfSetsType d1} n
-    {T : pointedType} (f : 'I_n -> T -> T1) {T2 : Type} (g : T2 -> T) :
+    {T : choiceType} (f : 'I_n -> T -> T1) {T2 : Type} (g : T2 -> T) :
   g_sigma_preimage (fun i => f i \o g) =
   preimage_set_system [set: T2] g (g_sigma_preimage f).
 Proof.