Bernoulli trials and central limit theorem

CHANGELOG_UNRELEASED.md

@@ -48,6 +48,12 @@
 
 - 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
 

classical/classical_sets.v

@@ -1058,7 +1058,7 @@ apply/predeqP => x; split=> [[a ? [b ? <-]]|[[a b] [? ? <-]]]/=;
 by [exists (a, b) | exists a => //; exists b].
 Qed.
 
-Lemma set_nil (T : choiceType) : [set` [::]] = @set0 T.
+Lemma set_nil (T : eqType) : [set` [::]] = @set0 T.
 Proof. by rewrite predeqP. Qed.
 
 Lemma set_seq_eq0 (T : eqType) (S : seq T) : ([set` S] == set0) = (S == [::]).

theories/itv.v

@@ -843,6 +843,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.
@@ -882,8 +885,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.

theories/lebesgue_integral.v

@@ -4617,7 +4617,7 @@ End measurable_fun_ysection.
 
 Section product_measures.
 Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
-Context (m1 : {measure set T1 -> \bar R}) (m2 : {measure set T2 -> \bar R}).
+Context (m1 : set T1 -> \bar R) (m2 : set T2 -> \bar R).
 
 Definition product_measure1 := (fun A => \int[m1]_x (m2 \o xsection A) x)%E.
 Definition product_measure2 := (fun A => \int[m2]_x (m1 \o ysection A) x)%E.
@@ -4635,19 +4635,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)) => ?.
@@ -4686,41 +4683,53 @@ Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType).
 Variable m1 : {sigma_finite_measure set T1 -> \bar R}.
 Variable m2 : {sigma_finite_measure set T2 -> \bar R}.
 
+Let product_measure_sigma_finite : sigma_finite setT (m1 \x m2).
+Proof.
+have /sigma_finiteP[F TF [ndF Foo]] := sigma_finiteT m1.
+have /sigma_finiteP[G TG [ndG Goo]] := sigma_finiteT m2.
+exists (fun n => F n `*` G n).
+ rewrite -setMTT TF TG predeqE => -[x y]; split.
+    move=> [/= [n _ Fnx] [k _ Gky]]; exists (maxn n k) => //; split.
+    - by move: x Fnx; exact/subsetPset/ndF/leq_maxl.
+    - by move: y Gky; exact/subsetPset/ndG/leq_maxr.
+  by move=> [n _ []/= ? ?]; split; exists n.
+move=> k; have [? ?] := Foo k; have [? ?] := Goo k.
+split; first exact: measurableM.
+by rewrite product_measure1E// lte_mul_pinfty// ge0_fin_numE.
+Qed.
+
+HB.instance Definition _ := Measure_isSigmaFinite.Build _ _ _ (m1 \x m2)
+  product_measure_sigma_finite.
+
 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; pose m := product_measure1 m1 m2.
-have /sigma_finiteP [F1 F1_T [F1_nd F1_oo]] := sigma_finiteT m1.
-have /sigma_finiteP [F2 F2_T [F2_nd F2_oo]] := sigma_finiteT m2.
-have UF12T : \bigcup_k (F1 k `*` F2 k) = setT.
-  rewrite -setMTT F1_T F2_T predeqE => -[x y]; split.
+move=> m'E.
+have /sigma_finiteP[F TF [ndF Foo]] := sigma_finiteT m1.
+have /sigma_finiteP[G TG [ndG Goo]] := sigma_finiteT m2.
+have UFGT : \bigcup_k (F k `*` G k) = setT.
+  rewrite -setMTT TF TG predeqE => -[x y]; split.
     by move=> [n _ []/= ? ?]; split; exists n.
-  move=> [/= [n _ F1nx] [k _ F2ky]]; exists (maxn n k) => //; split.
-  - by move: x F1nx; apply/subsetPset/F1_nd; rewrite leq_maxl.
-  - by move: y F2ky; apply/subsetPset/F2_nd; rewrite leq_maxr.
-have mF1F2 n : measurable (F1 n `*` F2 n) /\ m (F1 n `*` F2 n) < +oo.
-  have [? ?] := F1_oo n; have [? ?] := F2_oo n.
-  split; first exact: measurableM.
-  by rewrite /m product_measure1E // lte_mul_pinfty// ge0_fin_numE.
-have sm : sigma_finite setT m by exists (fun n => F1 n `*` F2 n).
-pose C : set (set (T1 * T2)) := [set C |
-  exists A1, measurable A1 /\ exists A2, measurable A2 /\ C = A1 `*` A2].
+  move=> [/= [n _ Fnx] [k _ Gky]]; exists (maxn n k) => //; split.
+  - by move: x Fnx; exact/subsetPset/ndF/leq_maxl.
+  - by move: y Gky; exact/subsetPset/ndG/leq_maxr.
+pose C : set (set (T1 * T2)) :=
+  [set C | exists A, measurable A /\ exists B, measurable B /\ C = A `*` B].
 have CI : setI_closed C.
   move=> /= _ _ [X1 [mX1 [X2 [mX2 ->]]]] [Y1 [mY1 [Y2 [mY2 ->]]]].
   rewrite -setMI; exists (X1 `&` Y1); split; first exact: measurableI.
   by exists (X2 `&` Y2); split => //; exact: measurableI.
-move=> X mX; apply: (measure_unique C (fun n => F1 n `*` F2 n)) => //.
+move=> X mX; apply: (measure_unique C (fun n => F n `*` G n)) => //.
 - rewrite measurable_prod_measurableType //; congr (<<s _ >>).
-  rewrite predeqE; split => [[A1 mA1 [A2 mA2 <-]]|[A1 [mA1 [A2 [mA2 ->]]]]].
-    by exists A1; split => //; exists A2; split.
-  by exists A1 => //; exists A2.
-- move=> n; rewrite /C /=; exists (F1 n); split; first by have [] := F1_oo n.
-  by exists (F2 n); split => //; have [] := F2_oo n.
+  rewrite predeqE; split => [[A mA [B mB <-]]|[A [mA [B [mB ->]]]]].
+    by exists A; split => //; exists B.
+  by exists A => //; exists B.
+- move=> n; rewrite /C /=; exists (F n); split; first by have [] := Foo n.
+  by exists (G n); split => //; have [] := Goo n.
 - by move=> A [A1 [mA1 [A2 [mA2 ->]]]]; rewrite m'E//= product_measure1E.
-- move=> k; have [? ?] := F1_oo k; have [? ?] := F2_oo k.
+- move=> k; have [? ?] := Foo k; have [? ?] := Goo k.
   by rewrite /= product_measure1E// lte_mul_pinfty// ge0_fin_numE.
 Qed.
 

theories/lebesgue_measure.v

@@ -341,6 +341,8 @@ Definition lebesgue_measure {R : realType} :
 HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R).
 HB.instance Definition _ (R : realType) :=
   SigmaFiniteContent.on (@lebesgue_measure R).
+HB.instance Definition _ (R : realType) :=
+  SigmaFiniteMeasure.on (@lebesgue_measure R).
 
 Section ps_infty.
 Context {T : Type}.

theories/lebesgue_stieltjes_measure.v

@@ -497,7 +497,7 @@ Lemma sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R) :
   sigma_finite setT (lebesgue_stieltjes_measure f).
 Proof. exact/measure_extension_sigma_finite/wlength_sigma_finite. Qed.
 
-HB.instance Definition _ (f : cumulative R) := @isSigmaFinite.Build _ _ _
+HB.instance Definition _ (f : cumulative R) := @Measure_isSigmaFinite.Build _ _ _
   (lebesgue_stieltjes_measure f) (sigmaT_finite_lebesgue_stieltjes_measure f).
 
 End wlength_extension.

theories/measure.v

@@ -3,6 +3,7 @@ From mathcomp Require Import all_ssreflect all_algebra finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop .
 Require Import reals ereal signed topology normedtype sequences esum numfun.
+Require Import itv.
 From HB Require Import structures.
 
 (******************************************************************************)
@@ -178,6 +179,7 @@ From HB Require Import structures.
 (*     probability T R == probability measure over the measurableType T with  *)
 (*                        value in R : realType                               *)
 (*     Measure_isProbability == factor for probability measures               *)
+(*     bernoulli p == the p-Bernoulli probability where p : {i01 R}           *)
 (*                                                                            *)
 (*      monotone_class D G == G is a monotone class of subsets of D           *)
 (*             <<m D, G >> == monotone class generated by G on D              *)
@@ -2994,6 +2996,26 @@ HB.instance Definition _ x :=
 
 End pdirac.
 
+Section bernoulli.
+Variables (R : realType) (p : {i01 R}).
+
+Definition bernoulli : set _ -> \bar R := measure_add
+  (mscale (NngNum (itv_ge0 p)) (dirac true))
+  (mscale (NngNum (itv_ge0 ((`1-(p%:inum))%:i01))) (dirac false)).
+
+HB.instance Definition _ := Measure.on bernoulli.
+
+Let bernoulli_setT : bernoulli [set: _] = 1.
+Proof.
+rewrite /bernoulli/= /measure_add/= /msum 2!big_ord_recr/= big_ord0 add0e/=.
+by rewrite /mscale/= !diracT !mule1 -EFinD add_onemK.
+Qed.
+
+HB.instance Definition _ :=
+  @Measure_isProbability.Build _ _ R bernoulli bernoulli_setT.
+
+End bernoulli.
+
 Lemma sigma_finite_counting (R : realType) :
   sigma_finite [set: nat] (@counting _ R).
 Proof.