add poisson distribution (#1668)

* add poisson_prob

---------

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

Author: IshiguroYoshihiro

CHANGELOG_UNRELEASED.md

@@ -101,6 +101,14 @@
 
 - in `lebesgue_integral_nonneg.v`:
   + lemma `ge0_integral_ereal_sup` (was a `Let`)
+- in `esum.v`:
+  + lemma `nneseries_esumT`
+
+- in `probability.v`:
+  + Definition `poisson_pmf`, `poisson_prob`
+  + lemmas `poisson_pmf_ge0`, `measurable_poisson_pmf`,
+           `measurable_poisson_prob`
+  + instance `poisson_prob`
 
 ### Changed
 
@@ -186,6 +194,12 @@
 - in `constructive_ereal.v`:
   + lemmas `div1e`, `divee`, `inve_eq1`, `Nyconjugate`
 
+- in `measure.v`:
+  + change the implicit arguments of lemma `measurability`
+
+- in `sequences.v`:
+  + change the implicit arguments of lemma `is_cvg_series_exp_coeff`
+
 ### Changed
 
 - in `measure.v`:

theories/esum.v

@@ -324,6 +324,10 @@ rewrite fsbig_finite//= -(big_rmcond_in P)/=; first exact: lee_sum_fset_lim.
 by move=> k; rewrite in_fset_set// inE => /PF ->.
 Qed.
 
+Lemma nneseries_esumT {R : realType} (a : nat -> \bar R) :
+  (forall n, 0 <= a n) -> \sum_(i <oo) a i = \esum_(i in [set: nat]) a i.
+Proof. by move=> a0; rewrite nneseries_esum// set_true. Qed.
+
 Lemma reindex_esum (R : realType) (T T' : choiceType)
     (P : set T) (Q : set T') (e : T -> T') (a : T' -> \bar R) :
     set_bij P Q e ->

theories/kernel.v

@@ -448,12 +448,12 @@ have kE i : k i x U = \sum_(j <oo) p i j x U.
 transitivity (\esum_(l in [set: nat] `*` [set: nat]) p l.1 l.2 x U).
   rewrite (_ : _ `*` _ = setT `*`` (fun=> setT)); last by apply/seteqP; split.
   rewrite -(@esum_esum _ _ _ _ _ (fun i j => p i j x U))//.
-  rewrite nneseries_esum// -fun_true; apply: eq_esum => i _.
-  by rewrite kE// nneseries_esum.
+  rewrite nneseries_esumT//; apply: eq_esum => i _.
+  by rewrite kE// nneseries_esumT.
 rewrite (reindex_esum [set: nat] _ f)//; last first.
   have := @bijTT _ _ f.
   by rewrite -setTT_bijective/= -[in X in set_bij _ X _ -> _](@setXTT nat nat).
-by rewrite nneseries_esum// fun_true; exact: eq_esum.
+by rewrite nneseries_esumT//; exact: eq_esum.
 Qed.
 
 HB.instance Definition _ :=
@@ -795,7 +795,7 @@ Let measurable_fun_kprobability U : measurable U ->
   measurable_fun [set: X] (kprobability mP ^~ U).
 Proof.
 move=> mU.
-apply: (measurability (ErealGenInftyO.measurableE R)) => _ /= -[_ [r ->] <-].
+apply: (measurability _ (ErealGenInftyO.measurableE R)) => _ /= -[_ [r ->] <-].
 rewrite setTI preimage_itvNyo -/(P @^-1` mset U r).
 have [r0|r0] := leP 0%R r; last by rewrite lt0_mset// preimage_set0.
 have [r1|r1] := leP r 1%R; last by rewrite gt1_mset// preimage_setT.
@@ -930,8 +930,7 @@ 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 => mnormalize (k x) point : pprobability Y R).
 Proof.
-apply: (@measurability _ _ _ _ _ _
-  (@pset _ _ _ : set (set (pprobability Y R)))) => //.
+apply: (measurability (@pset _ _ _ : set (set (pprobability Y R)))) => //.
 move=> _ -[_ [r r01] [Ys mYs <-]] <-.
 rewrite /mnormalize /mset /preimage/=.
 apply: emeasurable_fun_infty_o => //.
@@ -1061,7 +1060,7 @@ have [kl hkl] : exists kl : (R.-fker X ~> Z) ^nat, forall x U,
   have /ppcard_eqP[f] : ([set: nat] #= [set: nat * nat])%card.
     by rewrite card_eq_sym; exact: card_nat2.
   exists (fun i => l_ (f i).2 \; k_ (f i).1) => x U.
-  by rewrite (reindex_esum [set: nat] _ f)// nneseries_esum// fun_true.
+  by rewrite (reindex_esum [set: nat] _ f)// nneseries_esumT.
 exists kl => x U mU.
 transitivity ((kseries l_ \; kseries k_) x U).
   rewrite /= /kcomp [in RHS](eq_measure_integral (l x)); last first.
@@ -1075,8 +1074,8 @@ transitivity (\sum_(i <oo) \sum_(j <oo) (l_ j \; k_ i) x U).
 rewrite /mseries -hkl/=.
 rewrite (_ : setT = setT `*`` (fun=> setT)); last by apply/seteqP; split.
 rewrite -(@esum_esum _ _ _ _ _ (fun i j => (l_ j \; k_ i) x U))//.
-rewrite nneseries_esum; last by move=> n _; exact: nneseries_ge0.
-by rewrite fun_true; apply: eq_esum => /= i _; rewrite nneseries_esum// fun_true.
+rewrite nneseries_esumT; last by move=> *; exact: nneseries_ge0.
+by apply: eq_esum => /= i _; rewrite nneseries_esumT.
 Qed.
 
 Lemma measurable_fun_mkcomp_sfinite U : measurable U ->

theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v

@@ -1157,7 +1157,7 @@ Lemma ae_measurable_fun : ae_eq mu D f g ->
   measurable_fun D f -> measurable_fun D g.
 Proof.
 move=> [N [mN N0 subN]] mf B mB mD.
-apply: (measurability (ErealGenOInfty.measurableE R)) => // _ [_ [x ->] <-].
+apply: (measurability _ (ErealGenOInfty.measurableE R)) => // _ [_ [x ->] <-].
 rewrite [X in measurable X](_ : _ = D `&` ~` N `&` (f @^-1` `]x%:E, +oo[)
     `|` (D `&` N `&` g @^-1` `]x%:E, +oo[)); last first.
   apply/seteqP; split=> [y /= [Dy gyxoo]|y /= [[[Dy Ny] fyxoo]|]].

theories/lebesgue_measure.v

@@ -1174,7 +1174,7 @@ have finite_set_F i : finite_set (F i).
       exact/(@bigcup_sup _ _ _ _ (closure \o B))/CsubFi.
   have Fir2 : mu (\bigcup_(j in F i) closure (B j)) <=
               mu (ball (0:R) (r%:num + 2))%R.
-    rewrite (le_trans _ EBr2)// -(set_mem_set E) -nneseries_esum //.
+    rewrite (le_trans _ EBr2)// -(set_mem_set E) -nneseries_esum//.
     rewrite E_partition -measure_bigcup//=; last 2 first.
       by move=> ? _; exact: measurable_closure.
       apply: trivIset_bigcup => //.
@@ -1207,7 +1207,7 @@ have FE : \sum_(n <oo) \esum_(i in F n) mu (closure (B i)) =
     by apply/(trivIset_mkcond _ _).1; apply: sub_trivIset tDB => x [[]].
     rewrite -bigcup_mkcond; apply: bigcup_measurable => k _.
     exact: measurable_closure.
-  rewrite esum_mkcond//= nneseries_esum// -fun_true//=.
+  rewrite esum_mkcond//= nneseries_esumT//.
   by under eq_esum do rewrite (fun_if mu) (measure0 mu).
 apply/eqP; rewrite -measure_le0.
 apply/lee_addgt0Pr => _ /posnumP[e]; rewrite add0e.

theories/measurable_realfun.v

@@ -860,7 +860,7 @@ Qed.
 Lemma subspace_continuous_measurable_fun (D : set R) (f : subspace D -> R) :
   measurable D -> continuous f -> measurable_fun D f.
 Proof.
-move=> mD /continuousP cf; apply: (measurability (RGenOpens.measurableE R)).
+move=> mD /continuousP cf; apply: (measurability _ (RGenOpens.measurableE R)).
 move=> _ [_ [a [b ->] <-]]; apply: open_measurable_subspace => //.
 exact/cf/interval_open.
 Qed.
@@ -883,7 +883,7 @@ End coutinuous_measurable.
 Lemma lower_semicontinuous_measurable {R : realType} (f : R -> \bar R) :
   lower_semicontinuous f -> measurable_fun setT f.
 Proof.
-move=> scif; apply: (measurability (ErealGenOInfty.measurableE R)).
+move=> scif; apply: (measurability _ (ErealGenOInfty.measurableE R)).
 move=> /= _ [_ [a ->]] <-; apply: measurableI => //; apply: open_measurable.
 by rewrite preimage_itvoy; move/lower_semicontinuousP : scif; exact.
 Qed.
@@ -900,7 +900,7 @@ Qed.
 
 Lemma normr_measurable D : measurable_fun D (@normr _ R).
 Proof.
-move=> mD; apply: (measurability (RGenOInfty.measurableE R)) => //.
+move=> mD; apply: (measurability _ (RGenOInfty.measurableE R)) => //.
 move=> /= _ [_ [x ->] <-]; apply: measurableI => //.
 have [x0|x0] := leP 0 x.
   rewrite [X in measurable X](_ : _ = `]-oo, (- x)[ `|` `]x, +oo[)%classic.
@@ -962,7 +962,7 @@ Implicit Types (D : set T) (f g : T -> R).
 Lemma measurable_funD D f g :
   measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g).
 Proof.
-move=> mf mg mD; apply: (measurability (RGenOInfty.measurableE R)) => //.
+move=> mf mg mD; apply: (measurability _ (RGenOInfty.measurableE R)) => //.
 move=> /= _ [_ [a ->] <-]; rewrite preimage_itvoy.
 rewrite [X in measurable X](_ : _ = \bigcup_(q : rat)
   ((D `&` [set x | ratr q < f x]) `&` (D `&` [set x | a - ratr q < g x]))).
@@ -1042,7 +1042,7 @@ Lemma measurable_fun_sups D (h : (T -> R)^nat) n :
   (forall m, measurable_fun D (h m)) ->
   measurable_fun D (fun x => sups (h ^~ x) n).
 Proof.
-move=> f_ub mf mD; apply: (measurability (RGenOInfty.measurableE R)) => //.
+move=> f_ub mf mD; apply: (measurability _ (RGenOInfty.measurableE R)) => //.
 move=> _ [_ [x ->] <-]; rewrite sups_preimage // setI_bigcupr.
 by apply: bigcup_measurable => k /= nk; apply: mf => //; exact: measurable_itv.
 Qed.
@@ -1052,7 +1052,7 @@ Lemma measurable_fun_infs D (h : (T -> R)^nat) n :
   (forall n, measurable_fun D (h n)) ->
   measurable_fun D (fun x => infs (h ^~ x) n).
 Proof.
-move=> lb_f mf mD; apply: (measurability (RGenInftyO.measurableE R)) =>//.
+move=> lb_f mf mD; apply: (measurability _ (RGenInftyO.measurableE R)) => //.
 move=> _ [_ [x ->] <-]; rewrite infs_preimage // setI_bigcupr.
 by apply: bigcup_measurable => k /= nk; apply: mf => //; exact: measurable_itv.
 Qed.
@@ -1228,7 +1228,7 @@ Implicit Types (D : set T) (f g : T -> nat).
 Lemma measurable_fun_addn D f g : measurable_fun D f -> measurable_fun D g ->
   measurable_fun D (fun x => f x + g x)%N.
 Proof.
-move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
+move=> mf mg mD; apply: (measurability _ NGenCInfty.measurableE) => //.
 move=> /= _ [_ [a ->] <-]; rewrite preimage_itvcy.
 rewrite [X in measurable X](_ : _ = \bigcup_q
   ((D `&` [set x | q <= f x]%O) `&` (D `&` [set x | (a - q)%N <= g x]%O))).
@@ -1247,7 +1247,7 @@ Qed.
 Lemma measurable_fun_maxn D f g : measurable_fun D f -> measurable_fun D g ->
   measurable_fun D (fun x => maxn (f x) (g x)).
 Proof.
-move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
+move=> mf mg mD; apply: (measurability _ NGenCInfty.measurableE) => //.
 move=> /= _ [_ [a ->] <-]; rewrite [X in measurable X](_ : _ =
   ((D `&` [set x | a <= f x]%O) `|` (D `&` [set x | a <= g x]%O))).
   apply: measurableU.
@@ -1266,7 +1266,7 @@ Let measurable_fun_subn' D f g : (forall t, g t <= f t)%N ->
   measurable_fun D f -> measurable_fun D g ->
   measurable_fun D (fun x => f x - g x)%N.
 Proof.
-move=> gf mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
+move=> gf mf mg mD; apply: (measurability _ NGenCInfty.measurableE) => //.
 move=> /= _ [_ [a ->] <-]; rewrite preimage_itvcy.
 rewrite [X in measurable X](_ : _ = \bigcup_q
   ((D `&` [set x | maxn a q <= f x]%O) `&`
@@ -1366,14 +1366,14 @@ Variable R : realType.
 
 Lemma EFin_measurable (D : set R) : measurable_fun D EFin.
 Proof.
-move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //.
+move=> mD; apply: (measurability _ (ErealGenOInfty.measurableE R)) => //.
 move=> /= _ [_ [x ->]] <-; apply: measurableI => //.
 by rewrite preimage_itvoy EFin_itv; exact: measurable_itv.
 Qed.
 
 Lemma abse_measurable (D : set (\bar R)) : measurable_fun D abse.
 Proof.
-move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //.
+move=> mD; apply: (measurability _ (ErealGenOInfty.measurableE R)) => //.
 move=> /= _ [_ [x ->] <-].
 rewrite [X in _ @^-1` X](punct_eitv_bndy _ x) preimage_setU setIUr.
 apply: measurableU; last first.
@@ -1390,7 +1390,7 @@ Qed.
 Lemma oppe_measurable (D : set (\bar R)) :
   measurable_fun D (-%E : \bar R -> \bar R).
 Proof.
-move=> mD; apply: (measurability (ErealGenCInfty.measurableE R)) => //.
+move=> mD; apply: (measurability _ (ErealGenCInfty.measurableE R)) => //.
 move=> _ [_ [x ->] <-]; rewrite (_ : _ @^-1` _ = `]-oo, (- x)%:E]%classic).
   by apply: measurableI => //; exact: emeasurable_itv.
 by rewrite predeqE => y; rewrite preimage_itv !in_itv/= andbT in_itv leeNr.
@@ -1452,7 +1452,7 @@ Lemma measurable_fun_einfs D (f : (T -> \bar R)^nat) :
   forall n, measurable_fun D (fun x => einfs (f ^~ x) n).
 Proof.
 move=> mf n mD.
-apply: (measurability (ErealGenCInfty.measurableE R)) => //.
+apply: (measurability _ (ErealGenCInfty.measurableE R)) => //.
 move=> _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n =>/=.
 by apply: bigcap_measurableType => ? ?; exact/mf/emeasurable_itv.
 Qed.
@@ -1461,7 +1461,7 @@ Lemma measurable_fun_esups D (f : (T -> \bar R)^nat) :
   (forall n, measurable_fun D (f n)) ->
   forall n, measurable_fun D (fun x => esups (f ^~ x) n).
 Proof.
-move=> mf n mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //.
+move=> mf n mD; apply: (measurability _ (ErealGenOInfty.measurableE R)) => //.
 move=> _ [_ [x ->] <-];rewrite esups_preimage setI_bigcupr.
 by apply: bigcup_measurable => ? ?; exact/mf/emeasurable_itv.
 Qed.
@@ -1470,7 +1470,7 @@ Lemma measurable_maxe D (f g : T -> \bar R) :
   measurable_fun D f -> measurable_fun D g ->
   measurable_fun D (fun x => maxe (f x) (g x)).
 Proof.
-move=> mf mg mD; apply: (measurability (ErealGenCInfty.measurableE R)) => //.
+move=> mf mg mD; apply: (measurability _ (ErealGenCInfty.measurableE R)) => //.
 move=> _ [_ [x ->] <-]; rewrite [X in measurable X](_ : _ =
     (D `&` f @^-1` `[x%:E, +oo[) `|` (D `&` g @^-1` `[x%:E, +oo[)); last first.
   rewrite predeqE => t /=; split.

theories/measure.v

@@ -1850,6 +1850,7 @@ Notation sigma_algebra_image_class := sigma_algebra_image (only parsing).
 
 #[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `g_sigma_preimageE`")]
 Notation sigma_algebra_preimage_classE := g_sigma_preimageE (only parsing).
+Arguments measurability {d d' aT rT D f} _.
 
 Local Open Scope ereal_scope.
 
@@ -2463,9 +2464,7 @@ Let mseries0 : mseries set0 = 0.
 Proof. by rewrite /mseries ereal_series eseries0. Qed.
 
 Let mseries_ge0 B : 0 <= mseries B.
-Proof.
-by rewrite /mseries ereal_series nneseries_esum//; exact: esum_ge0.
-Qed.
+Proof. by rewrite /mseries ereal_series nneseries_esum//; exact: esum_ge0. Qed.
 
 Let mseries_sigma_additive : semi_sigma_additive mseries.
 Proof.
@@ -3198,7 +3197,7 @@ rewrite esum_bigcup//; last first.
    move=> /(decomp_neq0 DUBiN0) [y Yy].
    apply: (@trivIset_seqDU _ B) => //; exists y.
    by split => //; [exact: YBi|exact: YBj].
-rewrite nneseries_esum// set_true le_esum// => i _.
+rewrite nneseries_esumT// le_esum// => i _.
 rewrite [leLHS](_ : _ = \sum_(j \in decomp (seqDU B i)) mu j); last first.
   by rewrite esum_fset//; exact: decomp_finite_set.
 rewrite -SetRing.Rmu_fin_bigcup//=; last 3 first.
@@ -4939,7 +4938,7 @@ pose g i := (f^-1%FUN i).2; exists g; first split.
   exact: decomp_measurable.
 - move=> i /XS [k _]; rewrite -[F k]cover_decomp => -[D /= DFk Di].
   by exists (f (k, D)) => //; rewrite /g invK// inE.
-rewrite !nneseries_esum//= /measure ?set_true.
+rewrite !nneseries_esumT//= /measure.
 transitivity (\esum_(i in setT) \sum_(X0 \in decomp (F i)) mu X0); last first.
   by apply: eq_esum => /= k _; rewrite fsbig_finite//; exact: decomp_finite_set.
 rewrite -(eq_esum (fun _ _ => esum_fset _ _))//; last first.