From 45b0e368ffa0983e7b8a7509645a891a799c8579 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 24 Apr 2026 16:12:14 +0900 Subject: [PATCH 1/2] measurable types are not pointed by default any more Co-authored-by: Takafumi Saikawa --- theories/ereal.v | 2 +- theories/kernel.v | 16 +++--- .../simple_functions.v | 10 ++-- theories/measurable_realfun.v | 9 +++- theories/measure_theory/measurable_function.v | 31 +++++++----- .../measure_theory/measurable_structure.v | 49 ++++++++++--------- theories/measure_theory/measure_extension.v | 6 +-- theories/measure_theory/measure_function.v | 2 +- theories/measure_theory/probability_measure.v | 4 +- theories/numfun.v | 26 +++++++--- theories/probability_theory/random_variable.v | 6 +-- 11 files changed, 98 insertions(+), 63 deletions(-) diff --git a/theories/ereal.v b/theories/ereal.v index 738ec1037..76dfc1b72 100644 --- a/theories/ereal.v +++ b/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 ->]; diff --git a/theories/kernel.v b/theories/kernel.v index 5edc7088e..c8cd1d767 100644 --- a/theories/kernel.v +++ b/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). diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 7b1f64d0e..e7aeb3b67 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -149,13 +149,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 +172,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}). diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 779cea070..75565ec05 100644 --- a/theories/measurable_realfun.v +++ b/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}). diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v index 30f404155..48f7b5067 100644 --- a/theories/measure_theory/measurable_function.v +++ b/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. diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index 89a6957a0..fe676545a 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/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) : <> A -> <> (~` 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) <> (@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)) : <> = 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) : <> >> = <>. 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] -> <> = <>. 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) <>. 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. diff --git a/theories/measure_theory/measure_extension.v b/theories/measure_theory/measure_extension.v index 46efc6837..cc4158357 100644 --- a/theories/measure_theory/measure_extension.v +++ b/theories/measure_theory/measure_extension.v @@ -403,9 +403,9 @@ Proof. exact. Qed. Notation "mu .-cara" := (caratheodory_display mu) : measure_display_scope. Section caratheodory_sigma_algebra. -Variables (R : realType) (T : pointedType) (mu : {outer_measure set T -> \bar R}). +Variables (R : realType) (T : choiceType) (mu : {outer_measure set T -> \bar R}). -HB.instance Definition _ := Pointed.on (caratheodory_type mu). +HB.instance Definition _ := Choice.on (caratheodory_type mu). HB.instance Definition _ := @isMeasurable.Build (caratheodory_display mu) (caratheodory_type mu) mu.-caratheodory (caratheodory_measurable_set0 mu) @@ -416,7 +416,7 @@ End caratheodory_sigma_algebra. Section caratheodory_measure. Local Open Scope ereal_scope. -Variables (R : realType) (T : pointedType). +Variables (R : realType) (T : choiceType). Variable mu : {outer_measure set T -> \bar R}. Let U := caratheodory_type mu. diff --git a/theories/measure_theory/measure_function.v b/theories/measure_theory/measure_function.v index 5ab442498..d8a4ac072 100644 --- a/theories/measure_theory/measure_function.v +++ b/theories/measure_theory/measure_function.v @@ -696,7 +696,7 @@ Context d {T : semiRingOfSetsType d}. Notation rT := (type T). #[export] -HB.instance Definition _ := Pointed.on rT. +HB.instance Definition _ := Choice.on rT. #[export] HB.instance Definition _ := isRingOfSets.Build (display d) rT (@setring0 T measurable) (@setringU T measurable) (@setringD T measurable). diff --git a/theories/measure_theory/probability_measure.v b/theories/measure_theory/probability_measure.v index 1e76ec5c7..42aae61f2 100644 --- a/theories/measure_theory/probability_measure.v +++ b/theories/measure_theory/probability_measure.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* 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 boolp classical_sets functions cardinality reals. @@ -189,7 +189,7 @@ apply/funext => x; rewrite /mnormalize/= probability_setT. by rewrite onee_eq0/= invr1 mule1. Qed. -HB.instance Definition _ d (T : measurableType d) (R : realType) := +HB.instance Definition _ d (T : pmeasurableType d) (R : realType) := isPointed.Build (probability T R) (dirac point). Section dist_sigma_algebra_instance. diff --git a/theories/numfun.v b/theories/numfun.v index c64d4d7d5..8252cd299 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -1117,7 +1117,7 @@ Proof. by exists 1; split => // r r1 t At/=; rewrite indicE mem_set//= normr1 ltW. Qed. -Lemma indic_restrict {T : pointedType} {R : numFieldType} (A : set T) : +Lemma indic_restrict {T : Type} {R : numFieldType} (A : set T) : \1_A = (1 : T -> R) \_ A. Proof. by apply/funext => x; rewrite indicE /patch; case: ifP. Qed. @@ -1144,9 +1144,14 @@ rewrite -ltrBrDr distrC (lt_le_trans h)//. 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 _)) + (format "[ 'SubZmodule_isSubPzRing' 'of' U 'by' <: ]") + : form_scope. + Section ring. -(* TODO: generalize to the potentially-zero case? *) -Context (aT : pointedType) (rT : nzRingType). +Context (aT : Type) (rT : pzRingType). Lemma fimfun_mulr_closed : mulr_closed (@fimfun aT rT). Proof. @@ -1156,7 +1161,7 @@ Qed. HB.instance Definition _ := @GRing.isMulClosed.Build _ (@fimfun aT rT) fimfun_mulr_closed. -HB.instance Definition _ := [SubZmodule_isSubNzRing of {fimfun aT >-> rT} by <:]. +HB.instance Definition _ := [SubZmodule_isSubPzRing of {fimfun aT >-> rT} by <:]. Implicit Types f g : {fimfun aT >-> rT}. @@ -1190,16 +1195,23 @@ Definition scale_fimfun k f : {fimfun aT >-> rT} := k \o* f. End ring. Arguments indic_fimfun {aT rT} _. +(* NB: this notation will be taken by MathComp 2.6.0, + will become [SubSemiRing_isSubComSemiRing of U by <: ] but might require more *) +Notation "[ 'SubPzRing_isSubComPzRing' 'of' U 'by' <: ]" := + (GRing.SubPzRing_isSubComPzRing.Build _ _ U) + (format "[ 'SubPzRing_isSubComPzRing' 'of' U 'by' <: ]") + : form_scope. + Section comring. -Context (aT : pointedType) (rT : comNzRingType). +Context (aT : Type) (rT : comPzRingType). HB.instance Definition _ := - [SubNzRing_isSubComNzRing of {fimfun aT >-> rT} by <:]. + [SubPzRing_isSubComPzRing of {fimfun aT >-> rT} by <:]. Implicit Types (f g : {fimfun aT >-> rT}). HB.instance Definition _ f g := FImFun.copy (f \* g) (f * g). End comring. -HB.factory Record FiniteDecomp (T : pointedType) (R : nzRingType) (f : T -> R) := +HB.factory Record FiniteDecomp (T : Type) (R : pzRingType) (f : T -> R) := { fimfunE : exists (r : seq R) (A_ : R -> set T), forall x, f x = \sum_(y <- r) (y * \1_(A_ y) x) }. HB.builders Context T R f & @FiniteDecomp T R f. diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index 8db246610..e4f11c0af 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -1160,7 +1160,7 @@ Notation "{ 'dRV' P >-> T }" := (@discrete_random_variable _ _ _ T _ P) : form_scope. Section dRV_definitions. -Context {d} {d'} {T : measurableType d} {T' : measurableType d'} {R : realType} +Context {d} {d'} {T : pmeasurableType d} {T' : pmeasurableType d'} {R : realType} (P : probability T R). Lemma dRV_dom_enum (X : {dRV P >-> T'}) : @@ -1183,7 +1183,7 @@ End dRV_definitions. Section distribution_dRV. Local Open Scope ereal_scope. -Context d d' (T : measurableType d) (T' : measurableType d') (R : realType) +Context d d' (T : pmeasurableType d) (T' : pmeasurableType d') (R : realType) (P : probability T R). Variable X : {dRV P >-> T'}. @@ -1242,7 +1242,7 @@ End distribution_dRV. Section discrete_distribution. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) (P : probability T R). +Context d (T : pmeasurableType d) (R : realType) (P : probability T R). Lemma dRV_expectation (X : {dRV P >-> R}) : P.-integrable [set: T] (EFin \o X) -> From 363ef70c0d18c8994aaffedfb1c7d0a4c47c73d8 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 24 Apr 2026 16:29:56 +0900 Subject: [PATCH 2/2] changelog and doc --- CHANGELOG_UNRELEASED.md | 26 +++++++++++++++++++ .../simple_functions.v | 1 + theories/numfun.v | 5 ++-- 3 files changed, 30 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4c7a5478f..72983be6c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -76,6 +76,9 @@ - in `ereal.v`: + lemma `ge0_addBefctE` +- in `measurable_structure.v`: + + structure `PMeasurable`, notation `pmeasurableType` + ### Changed - moved from `measurable_structure.v` to `classical_sets.v`: @@ -160,6 +163,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 diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index e7aeb3b67..0029be157 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/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 *) diff --git a/theories/numfun.v b/theories/numfun.v index 8252cd299..534f7ce69 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -11,8 +11,9 @@ From mathcomp Require Import topology normedtype sequences. (**md**************************************************************************) (* # Numerical functions *) (* *) -(* This file provides definitions and lemmas about numerical functions and *) -(* theorems such as Tietze's extension theorem. *) +(* This file provides definitions and lemmas about numerical functions (e.g., *) +(* the fact that numerical functions with a finite image from a (potentially *) +(* zero) ring) and theorems such as Tietze's extension theorem. *) (* *) (* ``` *) (* nondecreasing_fun f == the function f is non-decreasing *)