sampling_lemma

bernoulli probability measure
wise_inde_weak
complete pairwise_independentM
mutually_independent_weak
bayes
binomial_mmt_gen_fun
generalizing discrete random variables
bernoulli RVs are discrete
bernoulli_mmt_gen_fun

Co-authored-by: @affeldt-aist
Co-authored-by: @t6s

CHANGELOG_UNRELEASED.md

@@ -131,6 +131,14 @@
     `independent_RVs2_funrpospos`
   + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`,
     ` expectation_prod`
+- in `lebesgue_integral.v`:
+  + lemma `abse_integralP`
+- in `signed.v`:
+  + definition `onem_NngNum`
+- in `measure.v`:
+  + definition `bernoulli`, declared as a probability measure instance
+- in `itv.v`:
+  + canonical `onem_itv01`
 
 ### Changed
 

reals/itv.v

@@ -850,6 +850,9 @@ Lemma inum_lt : {mono inum : x y / (x < y)%O}. Proof. by []. Qed.
 
 End Morph.
 
+Canonical onem_itv01 {R : realDomainType} (p : {i01 R}) : {i01 R} :=
+  @Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].
+
 Section Test1.
 
 Variable R : numDomainType.
@@ -893,8 +896,6 @@ apply/val_inj => /=.
 by rewrite subr0 mulr1 opprB addrCA subrr addr0.
 Qed.
 
-Canonical onem_itv01 (p : {i01 R}) : {i01 R} :=
-  @Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].
 
 Definition s_of_pq' (p q : {i01 R}) : {i01 R} :=
   (`1- (`1-(p%:inum) * `1-(q%:inum)))%:i01.

reals/signed.v

@@ -123,6 +123,7 @@ From mathcomp Require Import mathcomp_extra.
 (* Canonical instances are also provided according to types, as a             *)
 (* fallback when no known operator appears in the expression. Look to         *)
 (* nat_snum below for an example on how to add your favorite type.            *)
+(*                                                                            *)
 (******************************************************************************)
 
 Reserved Notation "{ 'compare' x0 & nz & cond }"

theories/lebesgue_integral.v

@@ -4958,19 +4958,16 @@ Variable m2 : {sigma_finite_measure set T2 -> \bar R}.
 Implicit Types A : set (T1 * T2).
 
 Let pm10 : (m1 \x m2) set0 = 0.
-Proof. by rewrite [LHS]integral0_eq// => x/= _; rewrite xsection0 measure0. Qed.
+Proof. by rewrite [LHS]integral0_eq// => x/= _; rewrite xsection0. Qed.
 
 Let pm1_ge0 A : 0 <= (m1 \x m2) A.
-Proof.
-by apply: integral_ge0 => // *; exact/measure_ge0/measurable_xsection.
-Qed.
+Proof. by apply: integral_ge0 => // *. Qed.
 
 Let pm1_sigma_additive : semi_sigma_additive (m1 \x m2).
 Proof.
 move=> F mF tF mUF.
 rewrite [X in _ --> X](_ : _ = \sum_(n <oo) (m1 \x m2) (F n)).
-  apply/cvg_closeP; split; last by rewrite closeE.
-  by apply: is_cvg_nneseries => *; exact: integral_ge0.
+  by apply/cvg_closeP; split; [exact: is_cvg_nneseries|rewrite closeE].
 rewrite -integral_nneseries//; last by move=> n; exact: measurable_fun_xsection.
 apply: eq_integral => x _; apply/esym/cvg_lim => //=; rewrite xsection_bigcup.
 apply: (measure_sigma_additive _ (trivIset_xsection tF)) => ?.
@@ -5029,8 +5026,7 @@ HB.instance Definition _ := Measure_isSigmaFinite.Build _ _ _ (m1 \x m2)
 
 Lemma product_measure_unique
     (m' : {measure set [the semiRingOfSetsType _ of T1 * T2] -> \bar R}) :
-    (forall A1 A2, measurable A1 -> measurable A2 ->
-      m' (A1 `*` A2) = m1 A1 * m2 A2) ->
+    (forall A B, measurable A -> measurable B -> m' (A `*` B) = m1 A * m2 B) ->
   forall X : set (T1 * T2), measurable X -> (m1 \x m2) X = m' X.
 Proof.
 move=> m'E.