bernoulli probability measure (math-comp#895)

* bernoulli, binomial, uniform distr

Co-authored-by: Takafumi Saikawa <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -34,6 +34,40 @@
 - in `normedtype.v`:
   + lemma `not_near_at_leftP`
 
+- in `lebesgue_measure.v`:
+  + lemma `measurable_fun_ler`
+
+- in `measure.v`:
+  + lemma `measurable_and`
+
+- in `signed.v`:
+  + lemma `onem_nonneg_proof`, definition `onem_nonneg`
+
+- in `esum.v`:
+  + lemma `nneseries_sum_bigcup`
+
+- in `lebesgue_measurable.v`:
+  + lemmas `measurable_natmul`, `measurable_fun_pow`
+
+- in `probability.v`:
+  + definition `bernoulli_pmf`
+  + lemmas `bernoulli_pmf_ge0`, `bernoulli_pmf1`, `measurable_bernoulli_pmf`
+  + definition  `bernoulli` (equipped with the `probability` structure)
+  + lemmas `bernoulli_dirac`, `bernoulliE`, `integral_bernoulli`, `measurable_bernoulli`,
+    `measurable_bernoulli2`
+  + definition `binomial_pmf`
+  + lemmas `binomial_pmf_ge0`, `measurable_binomial_pmf`
+  + definitions `binomial_prob` (equipped with the `probability` structure), `bin_prob`
+  + lemmas `bin_prob0`, `bin_prob1`, `binomial_msum`, `binomial_probE`, `integral_binomial`,
+    `integral_binomial_prob`, `measurable_binomial_prob`
+  + definition `uniform_pdf`
+  + lemmas `measurable_uniform_pdf`, `integral_uniform_pdf`, `integral_uniform_pdf1`
+  + definition `uniform_prob` (equipped with the `probability` structure)
+  + lemmas `dominates_uniform_prob`, `integral_uniform`
+
+- in `measure.v`:
+  + lemma `measurableID`
+
 ### Changed
 
 - in `forms.v`:
@@ -44,6 +78,9 @@
 - in `sequences.v`:
   + definition `expR` is now HB.locked
 
+- in `measure.v`:
+  + change the hypothesis of `measurable_fun_bool`
+
 ### Renamed
 
 - in `constructive_ereal.v`:
@@ -110,6 +147,9 @@
 	(from `measurableType` to `semiRingOfSetsType`)
   + lemmas ` measurable_prod_measurableType`, `measurable_prod_g_measurableTypeR` (from `measurableType` to `algebraOfSetsType`)
 
+- in `lebesgue_integral.v`:
+  + lemma `ge0_emeasurable_fun_sum`
+
 ### Deprecated
 
 - in `classical_sets.v`:

theories/charge.v

@@ -1467,7 +1467,7 @@ have muAP_gt0 : 0 < mu AP.
 pose h x := if x \in AP then f x + (epsRN mA abs)%:num%:E else f x.
 have mh : measurable_fun setT h.
   apply: measurable_fun_if => //.
-  - by apply: (measurable_fun_bool true); rewrite preimage_mem_true.
+  - by apply: (measurable_fun_bool true); rewrite setTI preimage_mem_true.
   - by apply: measurable_funTS; apply: emeasurable_funD => //; exact: mf.
   - by apply: measurable_funTS; exact: mf.
 have hge0 x : 0 <= h x.
@@ -1559,7 +1559,7 @@ pose f_ j x := if x \in E j then g_ j x else 0.
 have f_ge0 k x : 0 <= f_ k x by rewrite /f_; case: ifP.
 have mf_ k : measurable_fun setT (f_ k).
   apply: measurable_fun_if => //.
-  - by apply: (measurable_fun_bool true); rewrite preimage_mem_true.
+  - by apply: (measurable_fun_bool true); rewrite setTI preimage_mem_true.
   - rewrite preimage_mem_true.
     by apply: measurable_funTS => //; have /integrableP[] := ig_ k.
 have if_T k : integrable mu setT (f_ k).

theories/esum.v

@@ -451,6 +451,15 @@ End esum_bigcup.
 Arguments esum_bigcupT {R T K} J a.
 Arguments esum_bigcup {R T K} J a.
 
+Lemma nneseries_sum_bigcup {R : realType} (T : choiceType) (F : (set T)^nat)
+    (f : T -> \bar R) : trivIset [set: nat] F -> (forall i, 0 <= f i)%E ->
+  (\esum_(i in \bigcup_n F n) f i = \sum_(0 <= i <oo) (\esum_(j in F i) f j))%E.
+Proof.
+move=> tF f0; rewrite esum_bigcupT// nneseries_esum//; last first.
+  by move=> k _; exact: esum_ge0.
+by rewrite fun_true; apply: eq_esum => /= i _.
+Qed.
+
 Definition summable (T : choiceType) (R : realType) (D : set T)
   (f : T -> \bar R) := (\esum_(x in D) `| f x | < +oo)%E.
 

theories/kernel.v

@@ -132,7 +132,7 @@ Lemma measurable_fun_kseries (U : set Y) :
   measurable U -> measurable_fun [set: X] (kseries ^~ U).
 Proof.
 move=> mU.
-by apply: ge0_emeasurable_fun_sum => // n; exact/measurable_kernel.
+by apply: ge0_emeasurable_fun_sum => // n _; exact/measurable_kernel.
 Qed.
 
 HB.instance Definition _ :=
@@ -506,7 +506,7 @@ Variable k : X * Y -> \bar R.
 
 Lemma measurable_fun_xsection_integral
     (l : X -> {measure set Y -> \bar R})
-    (k_ : ({nnsfun [the measurableType _ of X * Y] >-> R})^nat)
+    (k_ : {nnsfun (X * Y) >-> R}^nat)
     (ndk_ : nondecreasing_seq (k_ : (X * Y -> R)^nat))
     (k_k : forall z, (k_ n z)%:E @[n --> \oo] --> k z) :
   (forall n r,
@@ -585,7 +585,7 @@ have [l_ hl_] := sfinite_kernel l.
 rewrite (_ : (fun x => _) = (fun x =>
     mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first.
   by apply/funext => x; rewrite hl_//; exact/measurable_xsection.
-apply: ge0_emeasurable_fun_sum => // m.
+apply: ge0_emeasurable_fun_sum => // m _.
 by apply: measurable_fun_xsection_finite_kernel => // /[!inE].
 Qed.
 
@@ -614,7 +614,7 @@ Qed.
 HB.instance Definition _ := isKernel.Build _ _ _ _ _ (kdirac mf)
   measurable_fun_kdirac.
 
-Let kdirac_prob x : kdirac mf x setT = 1.
+Let kdirac_prob x : kdirac mf x [set: Y] = 1.
 Proof. by rewrite /kdirac/= diracT. Qed.
 
 HB.instance Definition _ := Kernel_isProbability.Build _ _ _ _ _
@@ -717,46 +717,14 @@ HB.instance Definition _ t :=
   Kernel_isFinite.Build _ _ _ _ R (kadd k1 k2) kadd_finite_uub.
 End fkadd.
 
-Lemma measurable_fun_mnormalize d d' (X : measurableType d)
-    (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) :
-  measurable_fun [set: X] (fun x =>
-    [the probability _ _ of mnormalize (k x) point] : pprobability Y R).
-Proof.
-apply: (@measurability _ _ _ _ _ _
-  (@pset _ _ _ : set (set (pprobability Y R)))) => //.
-move=> _ -[_ [r r01] [Ys mYs <-]] <-.
-rewrite /mnormalize /mset /preimage/=.
-apply: emeasurable_fun_infty_o => //.
-rewrite /mnormalize/=.
-rewrite (_ : (fun x => _) = (fun x => if (k x setT == 0) || (k x setT == +oo)
-    then \d_point Ys else k x Ys * ((fine (k x setT))^-1)%:E)); last first.
-  by apply/funext => x/=; case: ifPn.
-apply: measurable_fun_if => //.
-- apply: (measurable_fun_bool true) => //.
-  rewrite (_ : _ @^-1` _ = [set t | k t setT == 0] `|`
-                           [set t | k t setT == +oo]); last first.
-    by apply/seteqP; split=> x /= /orP//.
-  by apply: measurableU; exact: kernel_measurable_eq_cst.
-- apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel.
-  apply/EFin_measurable_fun; rewrite setTI.
-  apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]).
-  + exact: open_measurable.
-  + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey.
-  + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0.
-    exact: inv_continuous.
-  + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel.
-Qed.
-
 Section knormalize.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variable f : R.-ker X ~> Y.
 
 Definition knormalize (P : probability Y R) : X -> {measure set Y -> \bar R} :=
-  fun x => [the measure _ _ of mnormalize (f x) P].
-
-Variable P : probability Y R.
+  fun x => mnormalize (f x) P.
 
-Let measurable_fun_knormalize U :
+Let measurable_knormalize (P : probability Y R) U :
   measurable U -> measurable_fun [set: X] (knormalize P ^~ U).
 Proof.
 move=> mU; rewrite /knormalize/= /mnormalize /=.
@@ -773,7 +741,7 @@ apply: measurable_fun_if => //.
 - apply: (@measurable_funS _ _ _ _ setT) => //.
   exact: kernel_measurable_fun_eq_cst.
 - apply: emeasurable_funM.
-    by have := measurable_kernel f U mU; exact: measurable_funS.
+    exact: measurable_funS (measurable_kernel f U mU).
   apply/EFin_measurable_fun.
   apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]) => //.
   + exact: open_measurable.
@@ -786,17 +754,48 @@ apply: measurable_fun_if => //.
     by have := measurable_kernel f _ measurableT; exact: measurable_funS.
 Qed.
 
-HB.instance Definition _ := isKernel.Build _ _ _ _ R (knormalize P)
-  measurable_fun_knormalize.
+HB.instance Definition _ (P : probability Y R) :=
+  isKernel.Build _ _ _ _ R (knormalize P) (measurable_knormalize P).
 
-Let knormalize1 x : knormalize P x [set: Y] = 1.
+Let knormalize1 (P : probability Y R) x : knormalize P x [set: Y] = 1.
 Proof. by rewrite /knormalize/= probability_setT. Qed.
 
-HB.instance Definition _ :=
-  @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) knormalize1.
+HB.instance Definition _ (P : probability Y R):=
+  @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) (knormalize1 P).
 
 End knormalize.
 
+(* TODO: useful? *)
+Lemma measurable_fun_mnormalize d d' (X : measurableType d)
+    (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) :
+  measurable_fun [set: X] (fun x =>
+    [the probability _ _ of mnormalize (k x) point] : pprobability Y R).
+Proof.
+apply: (@measurability _ _ _ _ _ _
+  (@pset _ _ _ : set (set (pprobability Y R)))) => //.
+move=> _ -[_ [r r01] [Ys mYs <-]] <-.
+rewrite /mnormalize /mset /preimage/=.
+apply: emeasurable_fun_infty_o => //.
+rewrite /mnormalize/=.
+rewrite (_ : (fun x => _) = (fun x => if (k x setT == 0) || (k x setT == +oo)
+    then \d_point Ys else k x Ys * ((fine (k x setT))^-1)%:E)); last first.
+  by apply/funext => x/=; case: ifPn.
+apply: measurable_fun_if => //.
+- apply: (measurable_fun_bool true) => //.
+  rewrite (_ : _ @^-1` _ = [set t | k t setT == 0] `|`
+                           [set t | k t setT == +oo]); last first.
+    by apply/seteqP; split=> x /= /orP.
+  by rewrite setTI; apply: measurableU; exact: kernel_measurable_eq_cst.
+- apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel.
+  apply/EFin_measurable_fun; rewrite setTI.
+  apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]).
+  + exact: open_measurable.
+  + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey.
+  + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0.
+    exact: inv_continuous.
+  + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel.
+Qed.
+
 Section kcomp_def.
 Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2)
   (Z : measurableType d3) (R : realType).

theories/lebesgue_integral.v

@@ -1969,15 +1969,30 @@ move=> fs mh; under eq_fun do rewrite fsbig_finite//.
 exact: emeasurable_fun_sum.
 Qed.
 
-Lemma ge0_emeasurable_fun_sum D (h : nat -> (T -> \bar R)) :
-  (forall k x, 0 <= h k x) -> (forall k, measurable_fun D (h k)) ->
-  measurable_fun D (fun x => \sum_(i <oo) h i x).
-Proof.
-move=> h0 mh; rewrite [X in measurable_fun _ X](_ : _ =
-    (fun x => limn_esup (fun n => \sum_(0 <= i < n) h i x))); last first.
+Lemma ge0_emeasurable_fun_sum D (h : nat -> (T -> \bar R)) (P : pred nat) :
+  (forall k x, D x -> P k -> 0 <= h k x) -> (forall k, P k -> measurable_fun D (h k)) ->
+  measurable_fun D (fun x => \sum_(i <oo | i \in P) h i x).
+Proof.
+Proof.
+move=> h0 mh.
+move=> mD; move: (mD).
+apply/(@measurable_restrict _ _ _ _ _ setT) => //.
+rewrite [X in measurable_fun _ X](_ : _ =
+  (fun x => \sum_(0 <= i <oo | i \in P) (h i \_ D) x)); last first.
+  apply/funext => x/=; rewrite /patch; case: ifPn => // xD.
+  by rewrite eseries0.
+rewrite [X in measurable_fun _ X](_ : _ =
+    (fun x => limn_esup (fun n => \sum_(0 <= i < n | P i) (h i) \_ D x))); last first.
   apply/funext=> x; rewrite is_cvg_limn_esupE//.
-  exact: is_cvg_ereal_nneg_natsum.
-by apply: measurable_fun_limn_esup => k; exact: emeasurable_fun_sum.
+  apply: is_cvg_nneseries_cond => n Pn; rewrite patchE.
+  by case: ifPn => // xD; rewrite h0//; exact/set_mem.
+apply: measurable_fun_limn_esup => k.
+under eq_fun do rewrite big_mkcond.
+apply: emeasurable_fun_sum => n.
+have [|] := boolP (n \in P).
+  rewrite /in_mem/= => Pn; rewrite Pn.
+  by apply/(measurable_restrict (h n)) => //; exact: mh.
+by rewrite /in_mem/= => /negbTE ->.
 Qed.
 
 Lemma emeasurable_funB D f g :
@@ -5262,7 +5277,7 @@ rewrite ge0_integralZl//; last by rewrite lee_fin.
 - by move=> y _; rewrite lee_fin.
 Qed.
 
-Lemma sfun_measurable_fun_fubini_tonelli_F : measurable_fun setT F.
+Lemma sfun_measurable_fun_fubini_tonelli_F : measurable_fun [set: T1] F.
 Proof.
 rewrite sfun_fubini_tonelli_FE//; apply: emeasurable_fun_fsum => // r.
 exact/measurable_funeM/measurable_fun_xsection.
@@ -5703,8 +5718,8 @@ transitivity (\sum_(n <oo) \int[s1 n]_x \sum_(m <oo) \int[s2 m]_y f (x, y)).
         fun x => \sum_(n <oo) \int[s2 n]_y f (x, y)); last first.
       apply/funext => x.
       by rewrite ge0_integral_measure_series//; exact/measurableT_comp.
-    apply: ge0_emeasurable_fun_sum; first by move=> k x; exact: integral_ge0.
-    by move=> k; apply: measurable_fun_fubini_tonelli_F.
+    apply: ge0_emeasurable_fun_sum; first by move=> k x *; exact: integral_ge0.
+    by move=> k _; exact: measurable_fun_fubini_tonelli_F.
   apply: eq_eseriesr => n _; apply: eq_integral => x _.
   by rewrite ge0_integral_measure_series//; exact/measurableT_comp.
 transitivity (\sum_(n <oo) \sum_(m <oo) \int[s1 n]_x \int[s2 m]_y f (x, y)).

theories/lebesgue_measure.v

@@ -1566,15 +1566,17 @@ Qed.
 Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g ->
   measurable_fun D (fun x => f x < g x).
 Proof.
-move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->.
-- under eq_fun do rewrite -subr_gt0.
-  rewrite preimage_true -preimage_itv_o_infty.
-  by apply: (measurable_funB mg mf) => //; exact: measurable_itv.
-- under eq_fun do rewrite ltNge -subr_ge0.
-  rewrite preimage_false set_predC setCK -preimage_itv_c_infty.
-  by apply: (measurable_funB mf mg) => //; exact: measurable_itv.
-- by rewrite preimage_set0 setI0.
-- by rewrite preimage_setT setIT.
+move=> mf mg mD; apply: (measurable_fun_bool true) => //.
+under eq_fun do rewrite -subr_gt0.
+by rewrite preimage_true -preimage_itv_o_infty; exact: measurable_funB.
+Qed.
+
+Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g ->
+  measurable_fun D (fun x => f x <= g x).
+Proof.
+move=> mf mg mD; apply: (measurable_fun_bool true) => //.
+under eq_fun do rewrite -subr_ge0.
+by rewrite preimage_true -preimage_itv_c_infty; exact: measurable_funB.
 Qed.
 
 Lemma measurable_maxr D f g :
@@ -1672,11 +1674,26 @@ Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed.
 #[global] Hint Extern 0 (measurable_fun _ expR) =>
   solve [apply: measurable_expR] : core.
 
+Lemma measurable_natmul {R : realType} D n :
+  measurable_fun D ((@GRing.natmul R)^~ n).
+Proof.
+under eq_fun do rewrite -mulr_natr.
+by do 2 apply: measurable_funM => //.
+Qed.
+
+Lemma measurable_fun_pow {R : realType} D (f : R -> R) n : measurable_fun D f ->
+  measurable_fun D (fun x => f x ^+ n).
+Proof.
+move=> mf.
+exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f).
+Qed.
+
 Lemma measurable_powR (R : realType) p :
   measurable_fun [set: R] (@powR R ^~ p).
 Proof.
 apply: measurable_fun_if => //.
-- apply: (measurable_fun_bool true); rewrite (_ : _ @^-1` _ = [set 0])//.
+- apply: (measurable_fun_bool true).
+  rewrite (_ : _ @^-1` _ = [set 0]) ?setTI//.
   by apply/seteqP; split => [_ /eqP ->//|_ -> /=]; rewrite eqxx.
 - rewrite setTI; apply: measurableT_comp => //.
   rewrite (_ : _ @^-1` _ = [set~ 0]); first exact: measurableT_comp.
@@ -1760,9 +1777,7 @@ move=> mf;rewrite (_ : er_map _ =
   fun x => if x \is a fin_num then (f (fine x))%:E else x); last first.
   by apply: funext=> -[].
 apply: measurable_fun_ifT => //=.
-+ apply: (measurable_fun_bool true).
-  rewrite /preimage/= -[X in measurable X]setTI.
-  exact/emeasurable_fin_num.
++ by apply: (measurable_fun_bool true); exact/emeasurable_fin_num.
 + exact/EFin_measurable_fun/measurableT_comp.
 Qed.
 #[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_er_map`")]
@@ -1779,7 +1794,7 @@ Lemma measurable_fun_einfs D (f : (T -> \bar R)^nat) :
 Proof.
 move=> mf n mD.
 apply: (measurability (ErealGenCInfty.measurableE R)) => //.
-move=> _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n => /=.
+move=> _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n =>/=.
 by apply: bigcap_measurable => ? ?; exact/mf/emeasurable_itv.
 Qed.