rm dup sections normal_density and normal_probability

Author: affeldt-aist

theories/probability.v

@@ -73,9 +73,6 @@ From mathcomp Require Import charge ftc gauss_integral hoelder.
 (*             beta_pdf == probability density function for beta              *)
 (*            beta_prob == beta probability measure                           *)
 (* div_beta_fun a b c d := beta_fun (a + c) (b + d) / beta_fun a b            *)
-(*       poisson_pmf r  == a pmf of Poisson distribution with parameter r : R *)
-(*       poisson_prob r == probability measure of Poisson distribution when   *)
-(*                         0 <= r and \d_0%N otherwise                        *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -2303,159 +2300,6 @@ Qed.
 
 End exp_coeff_properties.
 
-Section normal_density.
-Context {R : realType}.
-Local Open Scope ring_scope.
-Local Import Num.ExtraDef.
-Implicit Types m s x : R.
-
-Definition normal_pdf0 m s x : R := normal_peak s * normal_fun m s x.
-
-Lemma normal_pdf0_center m s : normal_pdf0 m s = normal_pdf0 0 s \o center m.
-Proof. by rewrite /normal_pdf0 normal_fun_center. Qed.
-
-Lemma normal_pdf0_ge0 m s x : 0 <= normal_pdf0 m s x.
-Proof. by rewrite mulr_ge0 ?normal_peak_ge0 ?expR_ge0. Qed.
-
-Lemma normal_pdf0_gt0 m s x : s != 0 -> 0 < normal_pdf0 m s x.
-Proof. by move=> s0; rewrite mulr_gt0 ?expR_gt0// normal_peak_gt0. Qed.
-
-Lemma measurable_normal_pdf0 m s : measurable_fun setT (normal_pdf0 m s).
-Proof. by apply: measurable_funM => //=; exact: measurable_normal_fun. Qed.
-
-Lemma continuous_normal_pdf0 m s : continuous (normal_pdf0 m s).
-Proof.
-move=> x; apply: cvgM; first exact: cvg_cst.
-apply: (@cvg_comp _ R^o _ _ _ _
-   (nbhs (- (x - m) ^+ 2 / (s ^+ 2 *+ 2)))); last exact: continuous_expR.
-apply: cvgM; last exact: cvg_cst; apply: (@cvgN _ R^o).
-apply: (@cvg_comp _ _ _ _ (@GRing.exp R^~ 2) _ (nbhs (x - m))).
-  apply: (@cvgB _ R^o) => //; exact: cvg_cst.
-exact: sqr_continuous.
-Qed.
-
-Lemma normal_pdf0_ub m s x : normal_pdf0 m s x <= normal_peak s.
-Proof.
-rewrite /normal_pdf0 ler_piMr ?normal_peak_ge0//.
-rewrite -[leRHS]expR0 ler_expR mulNr oppr_le0 mulr_ge0// ?sqr_ge0//.
-by rewrite invr_ge0 mulrn_wge0// sqr_ge0.
-Qed.
-
-End normal_density.
-
-Section normal_probability.
-Variables (R : realType) (m sigma : R).
-Local Open Scope ring_scope.
-Notation mu := lebesgue_measure.
-
-Local Notation normal_peak := (normal_peak sigma).
-Local Notation normal_fun := (normal_fun m sigma).
-
-Let measurable_normal_fun : measurable_fun setT normal_fun.
-Proof.
-apply: measurableT_comp => //=; apply: measurable_funM => //=.
-apply: measurableT_comp => //=; apply: measurable_funX => //=.
-exact: measurable_funD.
-Qed.
-
-Let F (x : R^o) := (x - m) / (Num.sqrt (sigma ^+ 2 *+ 2)).
-Lemma F'E : F^`()%classic = cst (Num.sqrt (sigma ^+ 2 *+ 2))^-1.
-Proof.
-apply/funext => x; rewrite /F derive1E deriveM// deriveD// derive_cst scaler0.
-by rewrite add0r derive_id derive_cst addr0 scaler1.
-Qed.
-
-Let int_gaussFE : sigma != 0 ->
-  (\int[mu]_x ((((gauss_fun \o F) *
-     (F^`())%classic) x)%:E * (Num.sqrt (sigma ^+ 2 *+ 2))%:E))%E =
-  (Num.sqrt (sigma ^+ 2 * pi *+ 2))%:E.
-Proof.
-move=> s0.
-rewrite -mulrnAr -[in RHS]mulr_natr sqrtrM ?(sqrtrM 2) ?sqr_ge0 ?pi_ge0// !EFinM.
-rewrite muleCA ge0_integralZr//=; last first.
-  by move=> x _; rewrite lee_fin mulr_ge0//= ?gauss_fun_ge0// F'E/= invr_ge0.
-  rewrite F'E; apply/measurable_EFinP/measurable_funM => //.
-  apply/measurableT_comp => //; first exact: measurable_gauss_fun.
-  by apply: measurable_funM => //; exact: measurable_funD.
-congr *%E.
-rewrite -increasing_ge0_integration_by_substitutionT//; first last.
-- by move=> x; rewrite gauss_fun_ge0.
-- exact: continuous_gauss_fun.
-- apply/gt0_cvgMly; last exact: cvg_addrr.
-  by rewrite invr_gt0// sqrtr_gt0 -mulr_natr mulr_gt0// exprn_even_gt0.
-- apply/gt0_cvgMlNy; last exact: cvg_addrr_Ny.
-  by rewrite invr_gt0// sqrtr_gt0 -mulr_natr mulr_gt0// exprn_even_gt0.
-- by rewrite F'E; exact: is_cvg_cst.
-- by rewrite F'E; exact: is_cvg_cst.
-- by rewrite F'E => ?; exact: cvg_cst.
-- move=> x y xy; rewrite /F ltr_pM2r ?ltr_leB//.
-  rewrite invr_gt0 ?sqrtr_gt0 ?pmulrn_lgt0 ?exprn_even_gt0//.
-apply: integralT_gauss.
-by rewrite -(mulr_natr (_ ^+ 2)) sqrtrM ?sqr_ge0.
-Qed.
-
-Let integral_normal_pdf_part : sigma != 0 ->
-  (\int[mu]_x (normal_fun x)%:E =
-  (Num.sqrt (sigma ^+ 2 * pi *+ 2))%:E)%E.
-Proof.
-move=> s0; rewrite -int_gaussFE//; apply: eq_integral => /= x _.
-rewrite F'E !fctE/= EFinM -muleA -EFinM mulVf ?mulr1; last first.
-  by rewrite gt_eqF// sqrtr_gt0 pmulrn_lgt0// exprn_even_gt0.
-congr (expR _)%:E; rewrite mulNr exprMn exprVn; congr (- (_ * _^-1)%R).
-by rewrite sqr_sqrtr// pmulrn_lge0// sqr_ge0.
-Qed.
-
-Let integrable_normal_pdf_part : sigma != 0 ->
-  mu.-integrable setT (EFin \o normal_fun).
-Proof.
-move=> s0; apply/integrableP; split.
-  by apply/measurable_EFinP; apply: measurable_normal_fun.
-under eq_integral do rewrite /= ger0_norm ?expR_ge0//.
-by rewrite /= integral_normal_pdf_part// ltry.
-Qed.
-
-Local Notation normal_pdf := (normal_pdf m sigma).
-Local Notation normal_prob := (normal_prob m sigma).
-
-Let normal0 : normal_prob set0 = 0%E.
-Proof. by rewrite /normal_prob integral_set0. Qed.
-
-Let normal_ge0 A : (0 <= normal_prob A)%E.
-Proof.
-rewrite /normal_prob integral_ge0//= => x _.
-by rewrite lee_fin normal_pdf_ge0 ?ltW.
-Qed.
-
-Let normal_sigma_additive : semi_sigma_additive normal_prob.
-Proof.
-move=> /= A mA tA mUA.
-rewrite /normal_prob/= integral_bigcup//=; last first.
-  apply: (integrableS _ _ (@subsetT _ _)) => //; exact: integrable_normal_pdf.
-apply: is_cvg_ereal_nneg_natsum_cond => n _ _.
-by apply: integral_ge0 => /= x ?; rewrite lee_fin normal_pdf_ge0 ?ltW.
-Qed.
-
-HB.instance Definition _ := isMeasure.Build _ _ _
-  normal_prob normal0 normal_ge0 normal_sigma_additive.
-
-Let normal_setT : normal_prob [set: _] = 1%E.
-Proof. by rewrite /normal_prob integral_normal_pdf. Qed.
-
-HB.instance Definition _ :=
-  @Measure_isProbability.Build _ _ R normal_prob normal_setT.
-
-Lemma integrable_indic_itv (a b : R) (b0 b1 : bool) : a < b ->
-  mu.-integrable setT (EFin \o \1_[set` (Interval (BSide b0 a) (BSide b1 b))]).
-Proof.
-move=> ab.
-apply/integrableP; split; first by apply/measurable_EFinP/measurable_indic.
-apply/abse_integralP => //; first by apply/measurable_EFinP/measurable_indic.
-rewrite integral_indic// setIT/= lebesgue_measure_itv/=.
-by rewrite lte_fin ab -EFinD/= ltry.
-Qed.
-
-End normal_probability.
-
 (* TODO: move *)
 Section shift_properties.
 Variable R : realType.
@@ -3914,147 +3758,3 @@ by rewrite -!EFin_beta_fun -EFinM divff// gt_eqF// beta_fun_gt0.
 Qed.
 
 End beta_prob_bernoulliE.
-
-Section poisson_pmf.
-Local Open Scope ring_scope.
-Context {R : realType}.
-Implicit Types (rate : R) (k : nat).
-
-Definition poisson_pmf (rate : R) (k : nat) : R :=
-          (rate ^+ k) * k`!%:R^-1 * expR (- rate).
-
-Lemma poisson_pmf_ge0 rate k (rate0 : 0 <= rate) : 0 <= poisson_pmf rate k.
-Proof.
-by rewrite /poisson_pmf 2?mulr_ge0// exprn_ge0.
-Qed.
-
-End poisson_pmf.
-
-Lemma measurable_poisson_pmf {R : realType} D (rate : R) k :
-  measurable_fun D (@poisson_pmf R ^~ k).
-Proof.
-apply: measurable_funM; first exact: measurable_funM.
-by apply: measurable_funTS; exact: measurableT_comp.
-Qed.
-
-Definition poisson_prob {R : realType} (rate : R) (k : nat)
-   : set nat -> \bar R :=
-  fun U => if (0 <= rate)%R then
-    \esum_(k in U) (poisson_pmf rate k)%:E else \d_0%N U.
-
-Section poisson.
-Context {R : realType} (rate : R) (k : nat).
-Local Open Scope ereal_scope.
-
-Local Notation poisson := (poisson_prob rate k).
-
-Let poisson0 : poisson set0 = 0.
-Proof. by rewrite /poisson measure0; case: ifPn => //; rewrite esum_set0. Qed.
-
-Let poisson_ge0 U : 0 <= poisson U.
-Proof.
-rewrite /poisson; case: ifPn => // rate0; apply: esum_ge0 => /= n Un.
-by rewrite lee_fin poisson_pmf_ge0.
-Qed.
-
-Let poisson_sigma_additive : semi_sigma_additive poisson.
-Proof.
-move=> F mF tF mUF; rewrite /poisson; case: ifPn => rate0; last first.
-  exact: measure_semi_sigma_additive.
-apply: cvg_toP.
-  apply: ereal_nondecreasing_is_cvgn => a b ab.
-  apply: lee_sum_nneg_natr => // n _ _.
-  by apply: esum_ge0 => /= ? _; exact: poisson_pmf_ge0.
-by rewrite nneseries_sum_bigcup// => i; rewrite lee_fin poisson_pmf_ge0.
-Qed.
-
-HB.instance Definition _ := isMeasure.Build _ _ _ poisson
-  poisson0 poisson_ge0 poisson_sigma_additive.
-
-Let poisson_setT : poisson [set: _] = 1.
-Proof.
-rewrite /poisson; case: ifPn; last by move=> _; rewrite probability_setT.
-move=> rate0; rewrite /poisson_pmf.
-have pkn n : 0%R <= (rate ^+ n / n`!%:R * expR (- rate))%:E.
-  by rewrite lee_fin poisson_pmf_ge0.
-apply/esym.
-rewrite [LHS](_ : _ = (expR rate)%:E * (expR (- rate))%:E); last first.
-  by rewrite -EFinM expRN divff// gt_eqF ?expR_gt0.
-transitivity
-  ((\esum_(k0 in setT) (rate ^+ k0 / k0`!%:R)%:E) * (expR (- rate))%:E).
-  congr *%E.
-  rewrite -EFin_lim; last exact: is_cvg_series_exp_coeff.
-  transitivity (ereal_sup (range (EFin \o (fun n : nat => (\sum_(0 <= k0 < n) rate ^+ k0 / k0`!%:R)%R)))).
-    apply: cvg_lim => //.
-    rewrite /esum/series/exp_coeff/=.
-    apply: ereal_nondecreasing_cvgn.
-    apply: nondecreasing_series => n _ _.
-    exact: exp_coeff_ge0.
-  apply/eqP; rewrite eq_le; apply/andP; split.
-    apply: le_ereal_sup => _ [n _ <-]/=.
-    exists `I_n => //.
-    rewrite -fsbig_ord/=.
-    rewrite big_mkord.
-    by rewrite sumEFin.
-  apply: ub_ereal_sup.
-  move=> /= e/= [S [fS _] <-].
-  apply: ereal_sup_ge.
-  have /finite_fsetP[X SX] := fS.
-  set N : nat := \max_(x <- X) x.
-  exists ((\sum_(0 <= k0 < N.+1) rate ^+ k0 / k0`!%:R)%:E) => //.
-  rewrite fsbig_finite//=.
-  rewrite -sumEFin.
-  rewrite [leRHS](_ : _ =
-     (\sum_(i <- fset_set `I_N.+1) (rate ^+ i / i`!%:R)%:E)%R); last first.
-    rewrite -Iiota.
-    rewrite -fsbig_finite//=.
-    rewrite -fsbig_seq//.
-    rewrite -/(iota 0 N.+1).
-    apply: iota_uniq.
-  apply: lee_sum_nneg_subfset => /=.
-    apply/subsetP.
-    move=> n; rewrite 2!inE.
-    rewrite 2?in_fset_set// 2!inE => Sn/=.
-    rewrite ltnS.
-    apply: leq_bigmax_seq => //.
-    by rewrite SX in Sn.
-  move=> n _ _.
-  by rewrite lee_fin mulr_ge0// exprn_ge0.
-(* TODO: lemma *)
-under [RHS]eq_esum do rewrite mulrC.
-rewrite muleC -ereal_sup_pZl; last exact: expR_gt0.
-apply/eqP; rewrite eq_le; apply/andP; split => /=.
-  apply: le_ereal_sup => _ [_ [N fN <-] <-]; exists N => //.
-  rewrite ge0_mule_fsumr//.
-  by move=> ?; exact: exp_coeff_ge0.
-apply: le_ereal_sup => _ [N fN <-]/=.
-exists (\sum_(x1 \in N) (rate ^+ x1 / x1`!%:R)%:E)%R; first by exists N.
-rewrite ge0_mule_fsumr//.
-by move=> ?; exact: exp_coeff_ge0.
-Qed.
-
-HB.instance Definition _ :=
-  @Measure_isProbability.Build _ _ R poisson poisson_setT.
-
-End poisson.
-
-Lemma measurable_poisson_prob (R : realType) (n : nat) :
-  measurable_fun setT (poisson_prob ^~ n : R -> pprobability _ _).
-Proof.
-apply: (@measurability _ _ _ _ _ _
-  (@pset _ _ _ : set (set (pprobability _ R)))) => //.
-move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=.
-rewrite /poisson_prob/=.
-set f := (X in measurable_fun _ X).
-apply: measurable_fun_if => //=.
-  by exact: measurable_fun_ler.
-apply: (eq_measurable_fun (fun t =>
-    \sum_(k <oo | k \in Ys) (poisson_pmf t k)%:E))%E.
-  move=> x /set_mem[_/= x01].
-  rewrite nneseries_esum// -1?[in RHS](set_mem_set Ys)// => k kYs.
-  by rewrite lee_fin poisson_pmf_ge0.
-apply: ge0_emeasurable_sum.
-  by move=> k x/= [_ x01] _; rewrite lee_fin poisson_pmf_ge0.
-move=> k Ysk; apply/measurableT_comp => //.
-exact: measurable_poisson_pmf.
-Qed.