minor generalizations (#977)

CHANGELOG_UNRELEASED.md

@@ -152,6 +152,12 @@
   + lemmas `is_cvg_nneseries`, `is_cvg_npeseries`
   + lemmas `nneseries_ge0`, `npeseries_le0`
 
+- in `measure.v`:
+  + lemmas `measureDI`, `measureD`, `measureUfinl`, `measureUfinr`,
+    `null_set_setU`, `measureU0`
+    (from measure to content)
+  + lemma `subset_measure0` (from `realType` to `realFieldType`)
+
 ### Deprecated
 
 ### Removed

theories/kernel.v

@@ -509,7 +509,7 @@ rewrite [X in measurable_fun _ X](_ : _ = (fun x => r%:E *
     \int[l x]_y (\1_(k_ n @^-1` [set r]) (x, y))%:E)); last first.
   apply/funext => x; under eq_integral do rewrite EFinM.
   have [r0|r0] := leP 0%R r.
-    rewrite ge0_integralM//; last by move=> y _; rewrite lee_fin.
+    rewrite ge0_integralZl//; last by move=> y _; rewrite lee_fin.
     exact/EFin_measurable_fun/measurableT_comp.
   rewrite integral0_eq; last first.
     by move=> y _; rewrite preimage_nnfun0// indic0 mule0.
@@ -1086,7 +1086,7 @@ under [in RHS]eq_integral.
     - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0.
   under eq_fsbigr.
     move=> r _.
-    rewrite (integralM_indic _ (fun r => f @^-1` [set r]))//; last first.
+    rewrite (integralZl_indic _ (fun r => f @^-1` [set r]))//; last first.
       by move=> r0; rewrite preimage_nnfun0.
     rewrite integral_indic// setIT.
     over.
@@ -1098,11 +1098,11 @@ rewrite /= ge0_integral_fsum//; last 2 first.
     have := mulemu_ge0 (fun n => f @^-1` [set n]).
     by apply; exact: preimage_nnfun0.
 apply: eq_fsbigr => r _.
-rewrite (integralM_indic _ (fun r => f @^-1` [set r]))//; last first.
+rewrite (integralZl_indic _ (fun r => f @^-1` [set r]))//; last first.
   exact: preimage_nnfun0.
 rewrite /= integral_kcomp_indic; last exact/measurable_sfunP.
 have [r0|r0] := leP 0%R r.
-  rewrite ge0_integralM//; last first.
+  rewrite ge0_integralZl//; last first.
     exact: measurableT_comp (measurable_kernel k (f @^-1` [set r]) _) _.
   by congr (_ * _); apply: eq_integral => y _; rewrite integral_indic// setIT.
 rewrite integral0_eq ?mule0; last first.

theories/measure.v

@@ -2955,28 +2955,28 @@ Qed.
 HB.instance Definition _ R :=
   @isSigmaFinite.Build _ _ _ (@counting _ R) (sigma_finite_counting R).
 
-Lemma measureIl d (R : realFieldType) (T : semiRingOfSetsType d)
-    (mu : {content set T -> \bar R}) (A B : set T) :
-  measurable A -> measurable B -> (mu (A `&` B) <= mu A)%E.
-Proof. by move=> mA mB; rewrite le_measure ?inE//; apply: measurableI. Qed.
+Section content_semiRingOfSetsType.
+Context d (T : semiRingOfSetsType d) (R : realFieldType).
+Variables (mu : {content set T -> \bar R}) (A B : set T).
+Hypotheses (mA : measurable A) (mB : measurable B).
+
+Lemma measureIl : mu (A `&` B) <= mu A.
+Proof. by rewrite le_measure ?inE//; apply: measurableI. Qed.
 
-Lemma measureIr d (R : realFieldType) (T : semiRingOfSetsType d)
-    (mu : {content set T -> \bar R}) (A B : set T) :
-  measurable A -> measurable B -> (mu (A `&` B) <= mu B)%E.
-Proof. by move=> mA mB; rewrite le_measure ?inE//; apply: measurableI. Qed.
+Lemma measureIr : mu (A `&` B) <= mu B.
+Proof. by rewrite le_measure ?inE//; apply: measurableI. Qed.
 
-Lemma subset_measure0 d (T : semiRingOfSetsType d) (R : realType)
-  (mu : {content set T -> \bar R}) (A B : set T) :
-  measurable A -> measurable B -> A `<=` B ->
-  mu B = 0%E -> mu A = 0%E.
+Lemma subset_measure0 : A `<=` B -> mu B = 0 -> mu A = 0.
 Proof.
-move=> mA mB AB B0; apply/eqP; rewrite eq_le measure_ge0// ?andbT -?B0.
-by apply: le_measure; rewrite ?inE.
+by move=> AB B0; apply/eqP; rewrite eq_le measure_ge0// -B0 le_measure// inE.
 Qed.
 
-Section measureD.
+End content_semiRingOfSetsType.
+
+Section content_ringOfSetsType.
 Context d (T : ringOfSetsType d) (R : realFieldType).
 Variable mu : {content set T -> \bar R}.
+Implicit Types A B : set T.
 
 Lemma measureDI A B : measurable A -> measurable B ->
   mu A = mu (A `\` B) + mu (A `&` B).
@@ -2998,12 +2998,6 @@ rewrite (measureDI mA mB) addeK// fin_numE 1?gt_eqF 1?lt_eqF//.
 - by rewrite (lt_le_trans _ (measure_ge0 _ _)).
 Qed.
 
-End measureD.
-
-Section measureU2.
-Context d (T : ringOfSetsType d) (R : realFieldType).
-Variable mu : {content set T -> \bar R}.
-
 Lemma measureU2 A B : measurable A -> measurable B ->
   mu (A `|` B) <= mu A + mu B.
 Proof.
@@ -3014,7 +3008,7 @@ by apply: bigsetU_measurable => -[] [//|[//|[|]]].
 by rewrite big_ord_recr/= big_ord_recr/= big_ord0 add0e.
 Qed.
 
-End measureU2.
+End content_ringOfSetsType.
 
 Section measureU.
 Context d (T : ringOfSetsType d) (R : realFieldType).
@@ -3034,6 +3028,20 @@ Lemma measureUfinl A B : measurable A -> measurable B -> mu A < +oo ->
   mu (A `|` B) = mu A + mu B - mu (A `&` B).
 Proof. by move=> *; rewrite setUC measureUfinr// setIC [mu B + _]addeC. Qed.
 
+Lemma null_set_setU A B : measurable A -> measurable B ->
+  mu A = 0 -> mu B = 0 -> mu (A `|` B) = 0.
+Proof.
+move=> mA mB A0 B0; rewrite measureUfinl/= ?A0//= ?B0 ?add0e.
+by apply/eqP; rewrite oppe_eq0 -measure_le0/= -A0 measureIl.
+Qed.
+
+Lemma measureU0 A B : measurable A -> measurable B -> mu B = 0 ->
+  mu (A `|` B) = mu A.
+Proof.
+move=> mA mB B0; rewrite measureUfinr/= ?B0// adde0.
+by rewrite (@subset_measure0 _ _ _ _ (A `&` B) B) ?sube0//; exact: measurableI.
+Qed.
+
 End measureU.
 
 Lemma eq_measureU d (T : ringOfSetsType d) (R : realFieldType) (A B : set T)
@@ -3043,29 +3051,12 @@ Lemma eq_measureU d (T : ringOfSetsType d) (R : realFieldType) (A B : set T)
   mu (A `|` B) = mu' (A `|` B).
 Proof.
 move=> mA mB muA muB muAB; have [mu'ANoo|] := ltP (mu' A) +oo.
-  by rewrite !measureUfinl ?muA ?muB ?muAB.
+  by rewrite !measureUfinl/= ?muA ?muB ?muAB.
 rewrite leye_eq => /eqP mu'A; transitivity (+oo : \bar R); apply/eqP.
   by rewrite -leye_eq -mu'A -muA le_measure ?inE//=; apply: measurableU.
 by rewrite eq_sym -leye_eq -mu'A le_measure ?inE//=; apply: measurableU.
 Qed.
 
-Lemma null_set_setU d (R : realFieldType) (T : ringOfSetsType d)
-  (mu : {measure set T -> \bar R}) (A B : set T) :
-  measurable A -> measurable B -> mu A = 0%E -> mu B = 0%E -> mu (A `|` B) = 0%E.
-Proof.
-move=> mA mB A0 B0; rewrite measureUfinl ?A0//= ?B0 ?add0e.
-apply/eqP; rewrite oppe_eq0 -measure_le0/=; do ?exact: measurableI.
-by rewrite -A0 measureIl.
-Qed.
-
-Lemma measureU0 d (R : realType) (T : ringOfSetsType d)
-  (mu : {measure set T -> \bar R}) (A B : set T) :
-  measurable A -> measurable B -> mu B = 0 -> mu (A `|` B) = mu A.
-Proof.
-move=> mA mB B0; rewrite measureUfinr ?B0// adde0.
-by rewrite (@subset_measure0 _ _ _ _ (A `&` B) B) ?sube0//; exact: measurableI.
-Qed.
-
 Section measure_continuity.
 
 Local Open Scope ereal_scope.
@@ -4276,8 +4267,8 @@ Qed.
 
 Lemma measurable_pair2 (y : T2) : measurable_fun [set: T1] (pair^~ y).
 Proof.
-have m1pairy : measurable_fun [set: T1] (fst \o pair^~ y) by exact/measurable_id.
-have m2pairy: measurable_fun [set: T1] (snd \o pair^~ y) by exact/measurable_cst.
+have m1pairy : measurable_fun [set: T1] (fst \o pair^~y) by exact/measurable_id.
+have m2pairy : measurable_fun [set: T1] (snd \o pair^~y) by exact/measurable_cst.
 exact/(prod_measurable_funP _).
 Qed.
 

theories/probability.v

@@ -138,7 +138,7 @@ Lemma expectationM (X : {RV P >-> R}) (iX : P.-integrable [set: T] (EFin \o X))
   (k : R) : 'E_P[k \o* X] = k%:E * 'E_P [X].
 Proof.
 rewrite unlock; under eq_integral do rewrite EFinM.
-by rewrite -integralM//; under eq_integral do rewrite muleC.
+by rewrite -integralZl//; under eq_integral do rewrite muleC.
 Qed.
 
 Lemma expectation_ge0 (X : {RV P >-> R}) :
@@ -212,11 +212,11 @@ rewrite unlock [X in 'E_P[X]](_ : _ = (X \* Y \- fine 'E_P[X] \o* Y
   apply/funeqP => x /=; rewrite mulrDr !mulrDl/= mul1r fineM// mulrNN addrA.
   by rewrite mulrN mulNr [Z in (X x * Y x - Z)%R]mulrC.
 have ? : P.-integrable [set: T] (EFin \o (X \* Y \- fine 'E_P[X] \o* Y)%R).
-  by rewrite compreBr ?integrableB// compre_scale ?integrablerM.
+  by rewrite compreBr ?integrableB// compre_scale ?integrableZl.
 rewrite expectationD/=; last 2 first.
-  - by rewrite compreBr// integrableB// compre_scale ?integrablerM.
-  - by rewrite compre_scale// integrablerM// finite_measure_integrable_cst.
-rewrite 2?expectationB//= ?compre_scale// ?integrablerM//.
+  - by rewrite compreBr// integrableB// compre_scale ?integrableZl.
+  - by rewrite compre_scale// integrableZl// finite_measure_integrable_cst.
+rewrite 2?expectationB//= ?compre_scale// ?integrableZl//.
 rewrite 3?expectationM//= ?finite_measure_integrable_cst//.
 by rewrite expectation_cst mule1 fineM// EFinM !fineK// muleC subeK ?fin_numM.
 Qed.
@@ -255,8 +255,8 @@ move=> X1 Y1 XY1.
 have aXY : (a \o* X * Y = a \o* (X * Y))%R.
   by apply/funeqP => x; rewrite mulrAC.
 rewrite [LHS]covarianceE => [||//|] /=; last 2 first.
-- by rewrite compre_scale ?integrablerM.
-- by rewrite aXY compre_scale ?integrablerM.
+- by rewrite compre_scale ?integrableZl.
+- by rewrite aXY compre_scale ?integrableZl.
 rewrite covarianceE// aXY !expectationM//.
 by rewrite -muleA -muleBr// fin_num_adde_defr// expectation_fin_num.
 Qed.
@@ -392,10 +392,10 @@ Lemma varianceZ a (X : {RV P >-> R}) :
 Proof.
 move=> X1 X2; rewrite /variance covarianceZl//=.
 - by rewrite covarianceZr// muleA.
-- by rewrite compre_scale// integrablerM.
+- by rewrite compre_scale// integrableZl.
 - rewrite [X in EFin \o X](_ : _ = (a \o* X ^+ 2)%R); last first.
     by apply/funeqP => x; rewrite mulrA.
-  by rewrite compre_scale// integrablerM.
+  by rewrite compre_scale// integrableZl.
 Qed.
 
 Lemma varianceN (X : {RV P >-> R}) :
@@ -416,7 +416,7 @@ have XY : P.-integrable [set: T] (EFin \o (X \+ Y)%R).
 rewrite covarianceDl//=; last 3 first.
 - rewrite -expr2 sqrrD compreDr ?integrableD// compreDr// integrableD//.
   rewrite -mulr_natr -[(_ * 2)%R]/(2 \o* (X * Y))%R compre_scale//.
-  exact: integrablerM.
+  exact: integrableZl.
 - by rewrite mulrDr compreDr ?integrableD.
 - by rewrite mulrDr mulrC compreDr ?integrableD.
 rewrite covarianceDr// covarianceDr ?(mulrC Y X)//.
@@ -445,8 +445,8 @@ Proof.
 move=> X1 X2.
 rewrite varianceD//=; last 3 first.
 - exact: finite_measure_integrable_cst.
-- by rewrite compre_scale// integrablerM// finite_measure_integrable_cst.
-- by rewrite mulrC compre_scale ?integrablerM.
+- by rewrite compre_scale// integrableZl// finite_measure_integrable_cst.
+- by rewrite mulrC compre_scale ?integrableZl.
 by rewrite variance_cst add0e covariance_cst_l mule0 adde0.
 Qed.
 
@@ -494,10 +494,10 @@ apply: deg_le2_ge0 => r; rewrite -lee_fin !EFinD.
 rewrite EFinM fineK ?variance_fin_num// muleC -varianceZ//.
 rewrite -mulrA EFinM mulrC EFinM ?fineK ?covariance_fin_num// -covarianceZl//.
 rewrite addeAC -varianceD ?variance_ge0//=.
-- by rewrite compre_scale ?integrablerM.
+- by rewrite compre_scale ?integrableZl.
 - rewrite [X in EFin \o X](_ : _ = r ^+2 \o* X ^+ 2)%R 1?mulrACA//.
-  by rewrite compre_scale ?integrablerM.
-- by rewrite -mulrAC compre_scale// integrablerM.
+  by rewrite compre_scale ?integrableZl.
+- by rewrite -mulrAC compre_scale// integrableZl.
 Qed.
 
 End variance.
@@ -569,7 +569,7 @@ have Y2 : P.-integrable [set: T] (EFin \o (Y ^+ 2)%R).
   rewrite compreDr => [|//]; apply: integrableD X2 _ => [//|].
   rewrite [X in EFin \o X](_ : _ = (- fine 'E_P[X] * 2) \o* X)%R; last first.
     by apply/funeqP => x /=; rewrite -mulr_natl mulrC mulrA.
-  by rewrite compre_scale => [|//]; apply: integrablerM X1.
+  by rewrite compre_scale => [|//]; apply: integrableZl X1.
 have EY : 'E_P[Y] = 0.
   rewrite expectationB/= ?finite_measure_integrable_cst//.
   rewrite expectation_cst finEK subee//.
@@ -590,7 +590,7 @@ have le (u : R) : (0 <= u)%R ->
     rewrite compreDr => [|//]; apply: integrableD Y2 _ => [//|].
     rewrite [X in EFin \o X](_ : _ = (2 * u) \o* Y)%R; last first.
       by apply/funeqP => x /=; rewrite -mulr_natl mulrCA.
-    by rewrite compre_scale => [|//]; apply: integrablerM Y1.
+    by rewrite compre_scale => [|//]; apply: integrableZl Y1.
   have -> : (fine 'V_P[X] + u^2)%:E = 'E_P[(Y \+ cst u)^+2]%R.
     rewrite -VY -[RHS](@subeK _ _ (('E_P[(Y \+ cst u)%R])^+2)); last first.
       by rewrite fin_numX ?unlock ?integral_fune_fin_num.
@@ -773,7 +773,7 @@ transitivity (\sum_(i <oo)
 transitivity (\sum_(i <oo) (dRV_enum X i)%:E *
   \int[P]_(x in (if i \in dRV_dom X then X @^-1` [set dRV_enum X i] else set0))
     1).
-  apply: eq_eseriesr => i _; rewrite -integralM//; last 2 first.
+  apply: eq_eseriesr => i _; rewrite -integralZl//; last 2 first.
     - by case: ifPn.
     - apply/integrableP; split => //.
       rewrite (eq_integral (cst 1%E)); last by move=> x _; rewrite abse1.