exponential distribution (#1635)

Co-authored-by: IshiguroYoshihiro <jb.15r.1213@s.thers.ac.jp>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -55,6 +55,17 @@
 - in `normed_module.v`:
   + definition `pseudoMetric_normed`
   + factory `Lmodule_isNormed`
+- in `num_normedtype.v`:
+  + lemmas `gt0_cvgMrNy`, `gt0_cvgMry`
+
+- in `probability.v`:
+  + definition `exponential_pdf`
+  + lemmas `exponential_pdf_ge0`, `lt0_exponential_pdf`,
+    `measurable_exponential_pdf`, `exponential_pdfE`,
+    `in_continuous_exponential_pdf`, `within_continuous_exponential_pdf`
+  + definition `exponential_prob`
+  + lemmas `derive1_exponential_pdf`, `exponential_prob_itv0c`,
+    `integral_exponential_pdf`, `integrable_exponential_pdf`
 
 ### Changed
 

theories/normedtype_theory/num_normedtype.v

@@ -505,22 +505,31 @@ rewrite pmulrn ceil_le_int// [ceil _]intEsign.
 by rewrite le_gtF ?expr0 ?mul1r ?lez_nat ?ceil_ge0//; near: n; apply: Foo.
 Unshelve. all: by end_near. Qed.
 
-Lemma gt0_cvgMlNy {R : realFieldType} {F : set_system R} {FF : Filter F} (M : R)
-  (f : R -> R) :
-  (0 < M)%R -> (f r) @[r --> F] --> -oo -> (f r * M)%R @[r --> F] --> -oo.
+Section gt0_cvg.
+Context {R : realFieldType} {F : set_system R} {FF : Filter F}.
+Variables (M : R) (f : R -> R).
+Hypothesis M0 : 0 < M.
+
+Lemma gt0_cvgMlNy : (f r) @[r --> F] --> -oo -> (f r * M)%R @[r --> F] --> -oo.
 Proof.
-move=> M0 /cvgrNyPle fy; apply/cvgrNyPle => A.
+move=> /cvgrNyPle fy; apply/cvgrNyPle => A.
 by apply: filterS (fy (A / M)) => x; rewrite ler_pdivlMr.
 Qed.
 
-Lemma gt0_cvgMly {R : realFieldType} {F : set_system R} {FF : Filter F} (M : R)
-  (f : R -> R) :
-  (0 < M)%R -> f r @[r --> F] --> +oo -> (f r * M)%R @[r --> F] --> +oo.
+Lemma gt0_cvgMrNy : (f r) @[r --> F] --> -oo -> (M * f r)%R @[r --> F] --> -oo.
+Proof. by move=> fy; under eq_fun do rewrite mulrC; exact: gt0_cvgMlNy. Qed.
+
+Lemma gt0_cvgMly : f r @[r --> F] --> +oo -> (f r * M)%R @[r --> F] --> +oo.
 Proof.
-move=> M0 /cvgryPge fy; apply/cvgryPge => A.
+move=> /cvgryPge fy; apply/cvgryPge => A.
 by apply: filterS (fy (A / M)) => x; rewrite ler_pdivrMr.
 Qed.
 
+Lemma gt0_cvgMry : f r @[r --> F] --> +oo -> (M * f r)%R @[r --> F] --> +oo.
+Proof. by move=> fy; under eq_fun do rewrite mulrC; exact: gt0_cvgMly. Qed.
+
+End gt0_cvg.
+
 Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
     (l : set_system T) :
   f x @[x --> -oo] --> l <-> (f \o -%R) x @[x --> +oo] --> l.
@@ -539,7 +548,6 @@ have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
 by rewrite (eq_cvg +oo _ f_opp) fmap_comp ninfty.
 Qed.
 
-
 Section monotonic_itv_bigcup.
 Context {R : realType}.
 Implicit Types (F : R -> R) (a : R).

theories/probability.v

@@ -59,6 +59,8 @@ From mathcomp Require Import ftc gauss_integral.
 (*                         standard deviation s                               *)
 (*                         Using normal_peak and normal_pdf.                  *)
 (*      normal_prob m s == normal probability measure                         *)
+(*    exponential_pdf r == pdf of the exponential distribution with rate r    *)
+(*   exponential_prob r == exponential probability measure                    *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -1731,3 +1733,181 @@ apply: ge0_le_integral => //=.
 Qed.
 
 End normal_probability.
+
+Section exponential_pdf.
+Context {R : realType}.
+Notation mu := lebesgue_measure.
+Variable rate : R.
+Hypothesis rate_gt0 : 0 < rate.
+
+Let exponential_pdfT x := rate * expR (- rate * x).
+Definition exponential_pdf := exponential_pdfT \_ `[0%R, +oo[.
+
+Lemma exponential_pdf_ge0 x : 0 <= exponential_pdf x.
+Proof.
+by apply: restrict_ge0 => {}x _; apply: mulr_ge0; [exact: ltW|exact: expR_ge0].
+Qed.
+
+Lemma lt0_exponential_pdf x : x < 0 -> exponential_pdf x = 0.
+Proof.
+move=> x0; rewrite /exponential_pdf patchE ifF//.
+by apply/negP; rewrite inE/= in_itv/= andbT; apply/negP; rewrite -ltNge.
+Qed.
+
+Let continuous_exponential_pdfT : continuous exponential_pdfT.
+Proof.
+move=> x.
+apply: (@continuousM _ R^o (fun=> rate) (fun x => expR (- rate * x))).
+  exact: cst_continuous.
+apply: continuous_comp; last exact: continuous_expR.
+by apply: continuousM => //; apply: (@continuousN _ R^o); exact: cst_continuous.
+Qed.
+
+Lemma measurable_exponential_pdf : measurable_fun [set: R] exponential_pdf.
+Proof.
+apply/measurable_restrict => //; apply: measurable_funTS.
+exact: continuous_measurable_fun.
+Qed.
+
+Lemma exponential_pdfE x : 0 <= x -> exponential_pdf x = exponential_pdfT x.
+Proof.
+by move=> x0; rewrite /exponential_pdf patchE ifT// inE/= in_itv/= x0.
+Qed.
+
+Lemma in_continuous_exponential_pdf :
+  {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 _))//; last 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_pdf :
+  {within [set` `[0, +oo[%R], 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.
+
+End exponential_pdf.
+
+Definition exponential_prob {R : realType} (rate : R) :=
+  fun V => (\int[lebesgue_measure]_(x in V) (exponential_pdf rate x)%:E)%E.
+
+Section exponential_prob.
+Context {R : realType}.
+Local Open Scope ring_scope.
+Notation mu := lebesgue_measure.
+Variable rate : R.
+Hypothesis rate_gt0 : 0 < rate.
+
+Lemma derive1_exponential_pdf :
+  {in `]0, +oo[%R, (fun x => - (expR : R^o -> R^o) (- 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.
+
+Let cexpNM : continuous (fun z : 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.
+
+Lemma exponential_prob_itv0c (x : R) : 0 < x ->
+  exponential_prob rate `[0, x] = (1 - (expR (- rate * x))%:E)%E.
+Proof.
+move=> x0.
+rewrite (_: 1 = - (- expR (- rate * 0))%:E)%E; last first.
+  by rewrite mulr0 expR0 EFinN oppeK.
+rewrite addeC.
+apply: (@continuous_FTC2 _ _ (fun x => - 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_pdf : (\int[mu]_x (exponential_pdf rate x)%:E = 1)%E.
+Proof.
+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//=; last 4 first.
+  exact: measurableC.
+  by rewrite setUv.
+  by move=> x _; rewrite lee_fin exponential_pdf_ge0.
+  exact/disj_setPCl.
+rewrite [X in _ + X]integral0_eq ?adde0; last first.
+  by move=> x x0; rewrite /exponential_pdf patchE ifF// memNset.
+rewrite (@ge0_continuous_FTC2y _ _
+  (fun x => - (expR (- rate * x))) _ 0)//.
+- by rewrite mulr0 expR0 EFinN oppeK add0e.
+- by move=> x _; apply: exponential_pdf_ge0.
+- exact: within_continuous_exponential_pdf.
+- rewrite -oppr0; apply: (@cvgN _ R^o).
+  rewrite (_ : (fun x => expR (- rate * x)) =
+               (fun z => expR (- z)) \o (fun z => rate * z)); last first.
+    by apply: eq_fun => x; rewrite mulNr.
+  apply: (@cvg_comp _ R^o _ _ _ _ (pinfty_nbhs R)); last exact: cvgr_expR.
+  exact: gt0_cvgMry.
+- by apply: (@cvgN _ R^o); apply: cvg_at_right_filter; exact: cexpNM.
+- exact: derive1_exponential_pdf.
+Qed.
+
+Lemma integrable_exponential_pdf :
+  mu.-integrable setT (EFin \o (exponential_pdf rate)).
+Proof.
+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//.
+by rewrite /= integral_exponential_pdf ltry.
+Qed.
+
+Local Notation exponential := (exponential_prob rate).
+
+Let exponential0 : exponential set0 = 0%E.
+Proof. by rewrite /exponential integral_set0. Qed.
+
+Let exponential_ge0 A : (0 <= exponential A)%E.
+Proof.
+rewrite /exponential integral_ge0//= => x _.
+by rewrite lee_fin exponential_pdf_ge0.
+Qed.
+
+Let exponential_sigma_additive : 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; apply: exponential_pdf_ge0.
+rewrite ge0_integral_bigcup//=.
+- apply/measurable_funTS/measurableT_comp => //.
+  exact: measurable_exponential_pdf.
+- by move=> x _; rewrite lee_fin exponential_pdf_ge0.
+Qed.
+
+HB.instance Definition _ := isMeasure.Build _ _ _
+  exponential exponential0 exponential_ge0 exponential_sigma_additive.
+
+Let exponential_setT : exponential [set: R] = 1%E.
+Proof. by rewrite /exponential integral_exponential_pdf. Qed.
+
+HB.instance Definition _ :=
+  @Measure_isProbability.Build _ _ R exponential exponential_setT.
+
+End exponential_prob.