Module mathcomp.analysis.probability_theory.uniform_distribution
From HB Require Import structures.From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval.
From mathcomp Require Import archimedean finmap.
From mathcomp Require Import boolp classical_sets functions cardinality fsbigop.
From mathcomp Require Import reals interval_inference ereal topology normedtype.
From mathcomp Require Import sequences measure numfun lebesgue_measure.
From mathcomp Require Import lebesgue_integral.
# Uniform distribution
```
uniform_pdf a b == uniform pdf over the interval [a,b]
uniform_prob a b ab == uniform probability over the interval [a,b]
where ab0 a proof that 0 < b - a
```
Set SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Section uniform_probability.
Local Open Scope ring_scope.
Context (R : realType) (a b : R).
Definition uniform_pdf x := if a <= x <= b then (b - a)^-1 else 0.
Lemma uniform_pdf_ge0 x : a < b -> 0 <= uniform_pdf x.
Proof.
Lemma measurable_uniform_pdf : measurable_fun setT uniform_pdf.
Proof.
rewrite /uniform_pdf /=; apply: measurable_fun_if => //=.
by apply: measurable_and => //; exact: measurable_fun_ler.
Qed.
by apply: measurable_and => //; exact: measurable_fun_ler.
Qed.
Local Notation mu := lebesgue_measure.
Lemma integral_uniform_pdf U :
(\int[mu]_(x in U) (uniform_pdf x)%:E =
\int[mu]_(x in U `&` `[a, b]) (uniform_pdf x)%:E)%E.
Proof.
rewrite [RHS]integral_mkcondr/=; apply: eq_integral => x xU.
rewrite patchE; case: ifPn => //.
rewrite notin_setE/= in_itv/= => /negP/negbTE xab.
by rewrite /uniform_pdf xab.
Qed.
rewrite patchE; case: ifPn => //.
rewrite notin_setE/= in_itv/= => /negP/negbTE xab.
by rewrite /uniform_pdf xab.
Qed.
Lemma integral_uniform_pdf1 A (ab : a < b) : `[a, b] `<=` A ->
(\int[mu]_(x in A) (uniform_pdf x)%:E = 1)%E.
Proof.
move=> abA; rewrite integral_uniform_pdf setIidr//.
rewrite (eq_integral (fun=> (b - a)^-1%:E)); last first.
by move=> x; rewrite inE/= in_itv/= /uniform_pdf => ->.
rewrite integral_cst//= lebesgue_measure_itv/= lte_fin.
by rewrite ab -EFinD -EFinM mulVf// gt_eqF// subr_gt0.
Qed.
rewrite (eq_integral (fun=> (b - a)^-1%:E)); last first.
by move=> x; rewrite inE/= in_itv/= /uniform_pdf => ->.
rewrite integral_cst//= lebesgue_measure_itv/= lte_fin.
by rewrite ab -EFinD -EFinM mulVf// gt_eqF// subr_gt0.
Qed.
Definition uniform_prob (ab : a < b) : set _ -> \bar R :=
fun U => (\int[mu]_(x in U) (uniform_pdf x)%:E)%E.
Hypothesis ab : (a < b)%R.
Let uniform0 : uniform_prob ab set0 = 0.
Proof.
Let uniform_ge0 U : (0 <= uniform_prob ab U)%E.
Proof.
Lemma integrable_uniform_pdf :
mu.-integrable setT (fun x => (uniform_pdf x)%:E).
Proof.
apply/integrableP; split.
by apply: measurableT_comp => //; exact: measurable_uniform_pdf.
under eq_integral.
move=> x _; rewrite gee0_abs//; last by rewrite lee_fin uniform_pdf_ge0.
over.
by rewrite /= integral_uniform_pdf1 ?ltry// -subr_gt0.
Qed.
by apply: measurableT_comp => //; exact: measurable_uniform_pdf.
under eq_integral.
move=> x _; rewrite gee0_abs//; last by rewrite lee_fin uniform_pdf_ge0.
over.
by rewrite /= integral_uniform_pdf1 ?ltry// -subr_gt0.
Qed.
Let uniform_sigma_additive : semi_sigma_additive (uniform_prob ab).
Proof.
move=> /= F mF tF mUF; rewrite /uniform_prob; apply: cvg_toP.
apply: ereal_nondecreasing_is_cvgn => m n mn.
apply: lee_sum_nneg_natr => // k _ _.
by apply: integral_ge0 => /= x Fkx; rewrite lee_fin uniform_pdf_ge0.
rewrite ge0_integral_bigcup//=.
- apply: measurable_funTS; apply: measurableT_comp => //.
exact: measurable_uniform_pdf.
- by move=> x _; rewrite lee_fin uniform_pdf_ge0.
Qed.
apply: ereal_nondecreasing_is_cvgn => m n mn.
apply: lee_sum_nneg_natr => // k _ _.
by apply: integral_ge0 => /= x Fkx; rewrite lee_fin uniform_pdf_ge0.
rewrite ge0_integral_bigcup//=.
- apply: measurable_funTS; apply: measurableT_comp => //.
exact: measurable_uniform_pdf.
- by move=> x _; rewrite lee_fin uniform_pdf_ge0.
Qed.
HB.instance Definition _ := isMeasure.Build _ _ _ (uniform_prob ab)
uniform0 uniform_ge0 uniform_sigma_additive.
Let uniform_setT : uniform_prob ab [set: _] = 1%:E.
Proof.
HB.instance Definition _ := @Measure_isProbability.Build _ _ R
(uniform_prob ab) uniform_setT.
Lemma dominates_uniform_prob : uniform_prob ab `<< mu.
Proof.
apply/null_content_dominatesP.
move=> A mA muA0; rewrite /uniform_prob integral_uniform_pdf.
apply/eqP; rewrite eq_le; apply/andP; split; last first.
apply: integral_ge0 => x [Ax /=]; rewrite in_itv /= => xab.
by rewrite lee_fin uniform_pdf_ge0.
apply: (@le_trans _ _
(\int[mu]_(x in A `&` `[a, b]%classic) (b - a)^-1%:E))%E; last first.
rewrite integral_cst//= ?mul1e//.
by rewrite pmule_rle0 ?lte_fin ?invr_gt0// ?subr_gt0// -muA0 measureIl.
exact: measurableI.
apply: ge0_le_integral => //=.
- exact: measurableI.
- by move=> x [Ax]; rewrite /= in_itv/= => axb; rewrite lee_fin uniform_pdf_ge0.
- by apply/measurable_EFinP/measurable_funTS; exact: measurable_uniform_pdf.
- by move=> x [Ax]; rewrite in_itv/= /uniform_pdf => ->.
Qed.
move=> A mA muA0; rewrite /uniform_prob integral_uniform_pdf.
apply/eqP; rewrite eq_le; apply/andP; split; last first.
apply: integral_ge0 => x [Ax /=]; rewrite in_itv /= => xab.
by rewrite lee_fin uniform_pdf_ge0.
apply: (@le_trans _ _
(\int[mu]_(x in A `&` `[a, b]%classic) (b - a)^-1%:E))%E; last first.
rewrite integral_cst//= ?mul1e//.
by rewrite pmule_rle0 ?lte_fin ?invr_gt0// ?subr_gt0// -muA0 measureIl.
exact: measurableI.
apply: ge0_le_integral => //=.
- exact: measurableI.
- by move=> x [Ax]; rewrite /= in_itv/= => axb; rewrite lee_fin uniform_pdf_ge0.
- by apply/measurable_EFinP/measurable_funTS; exact: measurable_uniform_pdf.
- by move=> x [Ax]; rewrite in_itv/= /uniform_pdf => ->.
Qed.
Let integral_uniform_indic E : measurable E ->
(\int[uniform_prob ab]_x (\1_E x)%:E =
(b - a)^-1%:E * \int[mu]_(x in `[a, b]) (\1_E x)%:E)%E.
Proof.
move=> mE; rewrite integral_indic//= /uniform_prob setIT -ge0_integralZl//=.
- rewrite [LHS]integral_mkcond/= [RHS]integral_mkcond/=.
apply: eq_integral => x _; rewrite !patchE; case: ifPn => xE.
case: ifPn.
rewrite inE/= in_itv/= => xab.
by rewrite /uniform_pdf xab indicE xE mule1.
by rewrite notin_setE/= in_itv/= => /negP/negbTE; rewrite /uniform_pdf => ->.
case: ifPn => //.
by rewrite inE/= in_itv/= => axb; rewrite indicE (negbTE xE) mule0.
- exact/measurable_EFinP/measurable_indic.
- by rewrite lee_fin invr_ge0// ltW// subr_gt0.
Qed.
- rewrite [LHS]integral_mkcond/= [RHS]integral_mkcond/=.
apply: eq_integral => x _; rewrite !patchE; case: ifPn => xE.
case: ifPn.
rewrite inE/= in_itv/= => xab.
by rewrite /uniform_pdf xab indicE xE mule1.
by rewrite notin_setE/= in_itv/= => /negP/negbTE; rewrite /uniform_pdf => ->.
case: ifPn => //.
by rewrite inE/= in_itv/= => axb; rewrite indicE (negbTE xE) mule0.
- exact/measurable_EFinP/measurable_indic.
- by rewrite lee_fin invr_ge0// ltW// subr_gt0.
Qed.
Import HBNNSimple.
Let integral_uniform_nnsfun (f : {nnsfun _ >-> R}) :
(\int[uniform_prob ab]_x (f x)%:E =
(b - a)^-1%:E * \int[mu]_(x in `[a, b]) (f x)%:E)%E.
Proof.
under [LHS]eq_integral do rewrite fimfunE -fsumEFin//.
rewrite [LHS]ge0_integral_fsum//; last 2 first.
- by move=> r; exact/measurable_EFinP/measurableT_comp.
- by move=> n x _; rewrite EFinM nnfun_muleindic_ge0.
rewrite -[RHS]ge0_integralZl//; last 3 first.
- exact/measurable_EFinP/measurable_funTS.
- by move=> x _; rewrite lee_fin.
- by rewrite lee_fin invr_ge0// ltW// subr_gt0.
under [RHS]eq_integral.
move=> x xD; rewrite fimfunE -fsumEFin// ge0_mule_fsumr; last first.
by move=> r; rewrite EFinM nnfun_muleindic_ge0.
over.
rewrite [RHS]ge0_integral_fsum//; last 2 first.
- by move=> r; apply/measurable_EFinP; do 2 apply/measurableT_comp => //.
- move=> n x _; rewrite EFinM mule_ge0//; last by rewrite nnfun_muleindic_ge0.
by rewrite lee_fin invr_ge0// ltW// subr_gt0.
apply: eq_fsbigr => r _; rewrite ge0_integralZl//.
- by rewrite !integralZl_indic_nnsfun//= integral_uniform_indic// muleCA.
- exact/measurable_EFinP/measurableT_comp.
- by move=> t _; rewrite nnfun_muleindic_ge0.
- by rewrite lee_fin invr_ge0// ltW// subr_gt0.
Qed.
rewrite [LHS]ge0_integral_fsum//; last 2 first.
- by move=> r; exact/measurable_EFinP/measurableT_comp.
- by move=> n x _; rewrite EFinM nnfun_muleindic_ge0.
rewrite -[RHS]ge0_integralZl//; last 3 first.
- exact/measurable_EFinP/measurable_funTS.
- by move=> x _; rewrite lee_fin.
- by rewrite lee_fin invr_ge0// ltW// subr_gt0.
under [RHS]eq_integral.
move=> x xD; rewrite fimfunE -fsumEFin// ge0_mule_fsumr; last first.
by move=> r; rewrite EFinM nnfun_muleindic_ge0.
over.
rewrite [RHS]ge0_integral_fsum//; last 2 first.
- by move=> r; apply/measurable_EFinP; do 2 apply/measurableT_comp => //.
- move=> n x _; rewrite EFinM mule_ge0//; last by rewrite nnfun_muleindic_ge0.
by rewrite lee_fin invr_ge0// ltW// subr_gt0.
apply: eq_fsbigr => r _; rewrite ge0_integralZl//.
- by rewrite !integralZl_indic_nnsfun//= integral_uniform_indic// muleCA.
- exact/measurable_EFinP/measurableT_comp.
- by move=> t _; rewrite nnfun_muleindic_ge0.
- by rewrite lee_fin invr_ge0// ltW// subr_gt0.
Qed.
Lemma integral_uniform (f : _ -> \bar R) :
measurable_fun setT f -> (forall x, 0 <= f x)%E ->
(\int[uniform_prob ab]_x f x = (b - a)^-1%:E * \int[mu]_(x in `[a, b]) f x)%E.
Proof.
move=> mf f0.
pose f_ := nnsfun_approx measurableT mf.
transitivity (lim (\int[uniform_prob ab]_x (f_ n x)%:E @[n --> \oo])%E).
rewrite -monotone_convergence//=.
- apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //=.
exact: cvg_nnsfun_approx.
- by move=> n; exact/measurable_EFinP/measurable_funTS.
- by move=> n ? _; rewrite lee_fin.
- by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
rewrite [X in _ = (_ * X)%E](_ : _ = lim
(\int[mu]_(x in `[a, b]) (f_ n x)%:E @[n --> \oo])%E); last first.
rewrite -monotone_convergence//=.
- apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //.
exact: cvg_nnsfun_approx.
- by move=> n; exact/measurable_EFinP/measurable_funTS.
- by move=> n ? _; rewrite lee_fin.
- by move=> ? _ ? ? ?; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
rewrite -limeMl//.
by apply: congr_lim; apply/funext => n /=; exact: integral_uniform_nnsfun.
apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=.
- by move=> ? _; rewrite lee_fin.
- exact/measurable_EFinP/measurable_funTS.
- exact/measurable_EFinP/measurable_funTS.
- by move=> ? _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
Qed.
pose f_ := nnsfun_approx measurableT mf.
transitivity (lim (\int[uniform_prob ab]_x (f_ n x)%:E @[n --> \oo])%E).
rewrite -monotone_convergence//=.
- apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //=.
exact: cvg_nnsfun_approx.
- by move=> n; exact/measurable_EFinP/measurable_funTS.
- by move=> n ? _; rewrite lee_fin.
- by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
rewrite [X in _ = (_ * X)%E](_ : _ = lim
(\int[mu]_(x in `[a, b]) (f_ n x)%:E @[n --> \oo])%E); last first.
rewrite -monotone_convergence//=.
- apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //.
exact: cvg_nnsfun_approx.
- by move=> n; exact/measurable_EFinP/measurable_funTS.
- by move=> n ? _; rewrite lee_fin.
- by move=> ? _ ? ? ?; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
rewrite -limeMl//.
by apply: congr_lim; apply/funext => n /=; exact: integral_uniform_nnsfun.
apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=.
- by move=> ? _; rewrite lee_fin.
- exact/measurable_EFinP/measurable_funTS.
- exact/measurable_EFinP/measurable_funTS.
- by move=> ? _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
Qed.
End uniform_probability.