Module mathcomp.analysis.probability_theory.exponential_distribution
From HB Require Import structures.From mathcomp Require Import boot order ssralg ssrnum interval archimedean.
From mathcomp Require Import interval_inference finmap.
From mathcomp Require Import boolp classical_sets functions.
From mathcomp Require Import reals ereal topology normedtype sequences derive.
From mathcomp Require Import measure exp numfun real_measure lebesgue_integral.
From mathcomp Require Import ftc.
# Exponential distribution
`exponential_pdf r`
: pdf of the exponential distribution with rate r
`exponential_prob r`
: exponential probability measure
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 exponential_pdf.
Context {RSource code : realType}.
Notation muSource code := lebesgue_measure.
Variable rateSource code : R.
Hypothesis rate_ge0Source code : 0 <= rate.
Let exponential_pdfTSource code xSource code := rate * expR (- rate * x).
Definition exponential_pdf
exponential_pdf : forall {R : realType}, R -> join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_POrder (join_Num_POrderZmodule_between_Algebra_BaseZmodule_and_Num_POrderNmodule R) -> numFieldTopology.Real_sort__canonical__classical_sets_Pointed R exponential_pdf is not universe polymorphic Arguments exponential_pdf {R} rate%_ring_scope u exponential_pdf is transparent Expands to: Constant mathcomp.analysis.probability_theory.exponential_distribution.exponential_pdf Declared in library mathcomp.analysis.probability_theory.exponential_distribution, line 38, characters 11-26
Source code := exponential_pdfT \_ `[0, +oo[.
Lemma exponential_pdf_ge0Source code xSource code : 0 <= exponential_pdf x.
Proof.
Lemma lt0_exponential_pdfSource code xSource code : x < 0 -> exponential_pdf x = 0.
Proof.
Let continuous_exponential_pdfTSource code : continuous exponential_pdfT.
Proof.
move=> x.
apply: (@continuousM _ R^o (fun=> rate) (fun xSource code => expR (- rate * x))).
exact: cst_continuous.
apply: continuous_comp; last exact: continuous_expR.
by apply: continuousM => //; apply: (@continuousN _ R^o); exact: cst_continuous.
Qed.
apply: (@continuousM _ R^o (fun=> rate) (fun xSource code => expR (- rate * x))).
exact: cst_continuous.
apply: continuous_comp; last exact: continuous_expR.
by apply: continuousM => //; apply: (@continuousN _ R^o); exact: cst_continuous.
Qed.
Import MeasurableR.
Lemma measurable_exponential_pdfSource code : measurable_fun [set: R] exponential_pdf.
Proof.
Lemma exponential_pdfESource code xSource code : 0 <= x -> exponential_pdf x = exponential_pdfT x.
Proof.
Lemma in_continuous_exponential_pdfSource code :
{in `]0, +oo[%R, continuous exponential_pdf}.
Proof.
move=> x; rewrite in_itv/= andbT => x0.
apply/(@cvgrPdist_lt _ R^o) => e e0; near=> y.
rewrite 2?(exponential_pdfE (ltW _))//; first by near: y; exact: lt_nbhsr.
near: y; move: e e0; apply/(@cvgrPdist_lt _ R^o).
by apply: continuous_comp => //; exact: continuous_exponential_pdfT.
Unshelve. end_near. Qed.
apply/(@cvgrPdist_lt _ R^o) => e e0; near=> y.
rewrite 2?(exponential_pdfE (ltW _))//; first by near: y; exact: lt_nbhsr.
near: y; move: e e0; apply/(@cvgrPdist_lt _ R^o).
by apply: continuous_comp => //; exact: continuous_exponential_pdfT.
Unshelve. end_near. Qed.
Lemma within_continuous_exponential_pdfSource code :
{within `[0, +oo[%classic, continuous exponential_pdf}.
Proof.
apply/continuous_within_itvcyP; split.
exact: in_continuous_exponential_pdf.
apply/(@cvgrPdist_le _ R^o) => e e0; near=> t.
rewrite 2?exponential_pdfE//.
near: t; move: e e0; apply/cvgrPdist_le.
by apply: cvg_at_right_filter; exact: continuous_exponential_pdfT.
Unshelve. end_near. Qed.
exact: in_continuous_exponential_pdf.
apply/(@cvgrPdist_le _ R^o) => e e0; near=> t.
rewrite 2?exponential_pdfE//.
near: t; move: e e0; apply/cvgrPdist_le.
by apply: cvg_at_right_filter; exact: continuous_exponential_pdfT.
Unshelve. end_near. Qed.
End exponential_pdf.
Section exponential_prob.
Context {RSource code : realType}.
Local Open Scope ring_scope.
Notation muSource code := lebesgue_measure.
Variable rateSource code : R.
Import MeasurableR.
Definition exponential_prob
exponential_prob : forall {R : realType}, R -> set Real_sort__canonical__measurable_structure_Measurable -> GRing.BaseAddMagma.sort \bar R exponential_prob is not universe polymorphic Arguments exponential_prob {R} rate%_ring_scope V%_classical_set_scope exponential_prob is transparent Expands to: Constant mathcomp.analysis.probability_theory.exponential_distribution.exponential_prob Declared in library mathcomp.analysis.probability_theory.exponential_distribution, line 102, characters 11-27
Source code (rateSource code : R) :=
fun VSource code => (\int[lebesgue_measure]_(xSource code in V) (exponential_pdf rate x)%:E)%E.
Lemma derive1_exponential_pdfSource code :
{in `]0, +oo[%R, (fun xSource code => - expR (- rate * x))^`()%classic
=1 exponential_pdf rate}.
Proof.
move=> z; rewrite in_itv/= andbT => z0.
rewrite derive1_comp// derive1N// derive1_id mulN1r derive1_comp// derive1E.
have /funeqP -> := @derive_expR R.
by rewrite derive1Ml// derive1_id mulr1 mulrN opprK mulrC exponential_pdfE ?ltW.
Qed.
rewrite derive1_comp// derive1N// derive1_id mulN1r derive1_comp// derive1E.
have /funeqP -> := @derive_expR R.
by rewrite derive1Ml// derive1_id mulr1 mulrN opprK mulrC exponential_pdfE ?ltW.
Qed.
Let cexpNMSource code : continuous (fun zSource code : R^o => expR (- rate * z)).
Proof.
move=> z; apply: continuous_comp; last exact: continuous_expR.
by apply: continuousM => //; apply: (@continuousN _ R^o); exact: cst_continuous.
Qed.
by apply: continuousM => //; apply: (@continuousN _ R^o); exact: cst_continuous.
Qed.
Lemma exponential_prob_itv0cSource code (xSource code : R) : 0 < x ->
exponential_prob rate `[0, x] = (1 - (expR (- rate * x))%:E)%E.
Proof.
move=> x0.
rewrite (_ : 1 = - (- expR (- rate * 0))%:E)%E.
by rewrite mulr0 expR0 EFinN oppeK.
rewrite addeC.
apply: (@continuous_FTC2 _ _ (fun xSource code => - expR (- rate * x))) => //.
- apply: (@continuous_subspaceW R^o _ _ [set` `[0, +oo[%R]).
+ exact: subset_itvl.
+ exact: within_continuous_exponential_pdf.
- split.
+ by move=> z _; exact: ex_derive.
+ by apply/cvg_at_right_filter; apply: cvgN; exact: cexpNM.
+ by apply/cvg_at_left_filter; apply: cvgN; exact: cexpNM.
- move=> z; rewrite in_itv/= => /andP[z0 _].
by apply: derive1_exponential_pdf; rewrite in_itv/= andbT.
Qed.
rewrite (_ : 1 = - (- expR (- rate * 0))%:E)%E.
by rewrite mulr0 expR0 EFinN oppeK.
rewrite addeC.
apply: (@continuous_FTC2 _ _ (fun xSource code => - expR (- rate * x))) => //.
- apply: (@continuous_subspaceW R^o _ _ [set` `[0, +oo[%R]).
+ exact: subset_itvl.
+ exact: within_continuous_exponential_pdf.
- split.
+ by move=> z _; exact: ex_derive.
+ by apply/cvg_at_right_filter; apply: cvgN; exact: cexpNM.
+ by apply/cvg_at_left_filter; apply: cvgN; exact: cexpNM.
- move=> z; rewrite in_itv/= => /andP[z0 _].
by apply: derive1_exponential_pdf; rewrite in_itv/= andbT.
Qed.
Lemma integral_exponential_pdfSource code : 0 < rate ->
(\int[mu]_xSource code (exponential_pdf rate x)%:E = 1)%E.
Proof.
move=> rate0.
have mEex : measurable_fun setT (EFin \o exponential_pdf rate).
by apply/measurable_EFinP; exact: measurable_exponential_pdf.
rewrite -(setUv `[0, +oo[%classic) ge0_integral_setU//=.
exact: measurableC.
by rewrite setUv.
by move=> x _; rewrite lee_fin exponential_pdf_ge0// ltW.
exact/disj_setPCl.
rewrite [X in _ + X]integral0_eq ?adde0.
by move=> x x0; rewrite /exponential_pdf patchE ifF// memNset.
rewrite (@ge0_continuous_FTC2y _ _
(fun xSource code => - (expR (- rate * x))) _ 0)//.
- by move=> x _; apply: exponential_pdf_ge0; exact: ltW.
- exact: within_continuous_exponential_pdf.
- rewrite -oppr0; apply: cvgN.
rewrite (_ : (fun xSource code => expR (- rate * x)) =
(fun zSource code => expR (- z)) \o (fun zSource code => rate * z)).
by apply: eq_fun => x; rewrite mulNr.
apply: (@cvg_comp _ _ _ _ _ _ (pinfty_nbhs R)); last exact: cvgr_expR.
exact: gt0_cvgMry.
- by apply: cvgN; apply/cvg_at_right_filter; exact: cexpNM.
- exact: derive1_exponential_pdf.
- by rewrite mulr0 expR0 EFinN oppeK add0e.
Qed.
have mEex : measurable_fun setT (EFin \o exponential_pdf rate).
by apply/measurable_EFinP; exact: measurable_exponential_pdf.
rewrite -(setUv `[0, +oo[%classic) ge0_integral_setU//=.
exact: measurableC.
by rewrite setUv.
by move=> x _; rewrite lee_fin exponential_pdf_ge0// ltW.
exact/disj_setPCl.
rewrite [X in _ + X]integral0_eq ?adde0.
by move=> x x0; rewrite /exponential_pdf patchE ifF// memNset.
rewrite (@ge0_continuous_FTC2y _ _
(fun xSource code => - (expR (- rate * x))) _ 0)//.
- by move=> x _; apply: exponential_pdf_ge0; exact: ltW.
- exact: within_continuous_exponential_pdf.
- rewrite -oppr0; apply: cvgN.
rewrite (_ : (fun xSource code => expR (- rate * x)) =
(fun zSource code => expR (- z)) \o (fun zSource code => rate * z)).
by apply: eq_fun => x; rewrite mulNr.
apply: (@cvg_comp _ _ _ _ _ _ (pinfty_nbhs R)); last exact: cvgr_expR.
exact: gt0_cvgMry.
- by apply: cvgN; apply/cvg_at_right_filter; exact: cexpNM.
- exact: derive1_exponential_pdf.
- by rewrite mulr0 expR0 EFinN oppeK add0e.
Qed.
Lemma integrable_exponential_pdfSource code : 0 < rate ->
mu.-integrable setT (EFin \o (exponential_pdf rate)).
Proof.
move=> rate0.
have mEex : measurable_fun setT (EFin \o exponential_pdf rate).
by apply/measurable_EFinP; exact: measurable_exponential_pdf.
apply/integrableP; split => //.
under eq_integral do rewrite /= ger0_norm ?(exponential_pdf_ge0 (ltW _))//.
by rewrite /= integral_exponential_pdf// ltry.
Qed.
have mEex : measurable_fun setT (EFin \o exponential_pdf rate).
by apply/measurable_EFinP; exact: measurable_exponential_pdf.
apply/integrableP; split => //.
under eq_integral do rewrite /= ger0_norm ?(exponential_pdf_ge0 (ltW _))//.
by rewrite /= integral_exponential_pdf// ltry.
Qed.
Hypothesis rate_gt0Source code : 0 < rate.
Local Notation exponentialSource code := (exponential_prob rate).
Let exponential0Source code : exponential set0 = 0%E.
Proof.
Let exponential_ge0Source code ASource code : (0 <= exponential A)%E.
Proof.
Let exponential_sigma_additiveSource code : semi_sigma_additive exponential.
Proof.
move=> /= F mF tF mUF; rewrite /exponential; apply: cvg_toP.
apply: ereal_nondecreasing_is_cvgn => m n mn.
apply: lee_sum_nneg_natr => // k _ _; apply: integral_ge0 => /= x Fkx.
by rewrite lee_fin exponential_pdf_ge0// ltW.
rewrite ge0_integral_bigcup//=.
- apply/measurable_funTS/measurableT_comp => //.
exact: measurable_exponential_pdf.
- by move=> x _; rewrite lee_fin exponential_pdf_ge0// ltW.
Qed.
apply: ereal_nondecreasing_is_cvgn => m n mn.
apply: lee_sum_nneg_natr => // k _ _; apply: integral_ge0 => /= x Fkx.
by rewrite lee_fin exponential_pdf_ge0// ltW.
rewrite ge0_integral_bigcup//=.
- apply/measurable_funTS/measurableT_comp => //.
exact: measurable_exponential_pdf.
- by move=> x _; rewrite lee_fin exponential_pdf_ge0// ltW.
Qed.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isMeasureSource code.Build _ _ _
exponential exponential0 exponential_ge0 exponential_sigma_additive.
Let exponential_setTSource code : exponential [set: R] = 1%E.
Proof.
HBSource code.instanceSource code DefinitionSource code _Source code :=Source code
@Measure_isProbabilitySource code.Build _ _ R exponential exponential_setT.
End exponential_prob.