probability measure HB instances for product measure

CHANGELOG_UNRELEASED.md

@@ -196,6 +196,9 @@
 - in `lebesgue_integral_differentiation.v`:
   + definition `iavg` (to use `inve`)
 
+- in `measure.v`:
+  + fourth argument of `probability_setT` is now explicit
+
 ### Renamed
 
 - in `measure.v`

theories/lebesgue_integral_theory/lebesgue_integral_fubini.v

@@ -430,6 +430,33 @@ Qed.
 
 End product_measure2E.
 
+Section product_probability_measures.
+Context {d1} {T1 : measurableType d1} {d2} {T2 : measurableType d2}
+  (R : realType) (P1 : probability T1 R) (P2 : probability T2 R).
+Local Open Scope ereal_scope.
+
+Local Notation pro1 := (P1 \x P2).
+
+Let pro1_setT : pro1 [set: T1 * T2] = 1.
+Proof.
+rewrite -setXTT product_measure1E// -[RHS]mule1.
+by rewrite -{1}(probability_setT P1) -(probability_setT P2).
+Qed.
+
+HB.instance Definition _ := Measure_isProbability.Build _ _ _ pro1 pro1_setT.
+
+Local Notation pro2 := (P1 \x^ P2).
+
+Let pro2_setT : pro2 setT = 1.
+Proof.
+rewrite -setXTT product_measure2E// -[RHS]mule1.
+by rewrite -{1}(probability_setT P1) -(probability_setT P2).
+Qed.
+
+HB.instance Definition _ := Measure_isProbability.Build _ _ _ pro2 pro2_setT.
+
+End product_probability_measures.
+
 Section fubini_functions.
 Local Open Scope ereal_scope.
 Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).

theories/measure.v

@@ -3578,6 +3578,8 @@ HB.mixin Record isProbability d (T : measurableType d) (R : realType)
 HB.structure Definition Probability d (T : measurableType d) (R : realType) :=
   {P of @SubProbability d T R P & isProbability d T R P }.
 
+Arguments probability_setT {d T R} s.
+
 HB.instance Definition _ d (T : measurableType d) (R : realType) :=
   gen_eqMixin (probability T R).
 HB.instance Definition _ d (T : measurableType d) (R : realType) :=
@@ -3587,15 +3589,11 @@ Section probability_lemmas.
 Context d (T : measurableType d) (R : realType) (P : probability T R).
 
 Lemma probability_le1 (A : set T) : measurable A -> P A <= 1.
-Proof.
-move=> mA; rewrite -(@probability_setT _ _ _ P).
-by apply: le_measure => //; rewrite ?in_setE.
-Qed.
+Proof. by move=> mA; rewrite -(probability_setT P) ?le_measure ?in_setE. Qed.
 
 Lemma probability_setC (A : set T) : measurable A -> P (~` A) = 1 - P A.
 Proof.
-move=> mA.
-rewrite -(@probability_setT _ _ _ P) -(setvU A) measureU ?addeK ?setICl//.
+move=> mA; rewrite -(probability_setT P) -(setvU A) measureU ?addeK ?setICl//.
 - by rewrite fin_num_measure.
 - exact: measurableC.
 Qed.

theories/probability.v

@@ -177,7 +177,7 @@ have cdf_s : cdf X r @[r --> +oo%R] --> s.
 have cdf_ns : cdf X n%:R @[n --> \oo%R] --> s.
   by move/cvge_pinftyP : cdf_s; apply; exact/cvgryPge/nbhs_infty_ger.
 have cdf_n1 : cdf X n%:R @[n --> \oo] --> 1.
-  rewrite -(@probability_setT _ _ _ P).
+  rewrite -(probability_setT P).
   pose F n := X @^-1` `]-oo, n%:R].
   have <- : \bigcup_n F n = setT.
     rewrite -preimage_bigcup -subTset => t _/=.
@@ -986,7 +986,7 @@ Lemma eq_bernoulli (P : probability bool R) :
 Proof.
 move=> Ptrue sb; rewrite /bernoulli /bernoulli_pmf.
 have Pfalse: P [set false] = (1 - p%:E)%E.
-  rewrite -Ptrue -(@probability_setT _ _ _ P) setT_bool measureU//; last first.
+  rewrite -Ptrue -(probability_setT P) setT_bool measureU//; last first.
     by rewrite disjoints_subset => -[]//.
   by rewrite addeAC subee ?add0e//= Ptrue.
 have: (0 <= p%:E <= 1)%E by rewrite -Ptrue measure_ge0 probability_le1.
@@ -1031,7 +1031,7 @@ Lemma eq_bernoulliV2 {R : realType} (P : probability bool R) :
   P [set true] = P [set false] -> P =1 bernoulli 2^-1.
 Proof.
 move=> Ptrue_eq_false; apply/eq_bernoulli.
-have : P [set: bool] = 1%E := probability_setT.
+have : P [set: bool] = 1%E := probability_setT P.
 rewrite setT_bool measureU//=; last first.
   by rewrite disjoints_subset => -[]//.
 rewrite Ptrue_eq_false -mule2n; move/esym/eqP.