From 6e7a1c83ee30b82550cf61f4e427c7e9b726b6c1 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Mon, 27 May 2024 10:04:41 +0900 Subject: [PATCH] bernoulli probability measure (#895) * bernoulli, binomial, uniform distr Co-authored-by: Takafumi Saikawa --- CHANGELOG_UNRELEASED.md | 40 +++ theories/charge.v | 4 +- theories/esum.v | 9 + theories/kernel.v | 87 +++--- theories/lebesgue_integral.v | 37 ++- theories/lebesgue_measure.v | 43 ++- theories/measure.v | 56 +++- theories/probability.v | 563 +++++++++++++++++++++++++++++++++-- theories/signed.v | 6 + 9 files changed, 741 insertions(+), 104 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8acf8ff949..b8287296e4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -34,6 +34,40 @@ - in `normedtype.v`: + lemma `not_near_at_leftP` +- in `lebesgue_measure.v`: + + lemma `measurable_fun_ler` + +- in `measure.v`: + + lemma `measurable_and` + +- in `signed.v`: + + lemma `onem_nonneg_proof`, definition `onem_nonneg` + +- in `esum.v`: + + lemma `nneseries_sum_bigcup` + +- in `lebesgue_measurable.v`: + + lemmas `measurable_natmul`, `measurable_fun_pow` + +- in `probability.v`: + + definition `bernoulli_pmf` + + lemmas `bernoulli_pmf_ge0`, `bernoulli_pmf1`, `measurable_bernoulli_pmf` + + definition `bernoulli` (equipped with the `probability` structure) + + lemmas `bernoulli_dirac`, `bernoulliE`, `integral_bernoulli`, `measurable_bernoulli`, + `measurable_bernoulli2` + + definition `binomial_pmf` + + lemmas `binomial_pmf_ge0`, `measurable_binomial_pmf` + + definitions `binomial_prob` (equipped with the `probability` structure), `bin_prob` + + lemmas `bin_prob0`, `bin_prob1`, `binomial_msum`, `binomial_probE`, `integral_binomial`, + `integral_binomial_prob`, `measurable_binomial_prob` + + definition `uniform_pdf` + + lemmas `measurable_uniform_pdf`, `integral_uniform_pdf`, `integral_uniform_pdf1` + + definition `uniform_prob` (equipped with the `probability` structure) + + lemmas `dominates_uniform_prob`, `integral_uniform` + +- in `measure.v`: + + lemma `measurableID` + ### Changed - in `forms.v`: @@ -44,6 +78,9 @@ - in `sequences.v`: + definition `expR` is now HB.locked +- in `measure.v`: + + change the hypothesis of `measurable_fun_bool` + ### Renamed - in `constructive_ereal.v`: @@ -110,6 +147,9 @@ (from `measurableType` to `semiRingOfSetsType`) + lemmas ` measurable_prod_measurableType`, `measurable_prod_g_measurableTypeR` (from `measurableType` to `algebraOfSetsType`) +- in `lebesgue_integral.v`: + + lemma `ge0_emeasurable_fun_sum` + ### Deprecated - in `classical_sets.v`: diff --git a/theories/charge.v b/theories/charge.v index 6c6fb76f55..780a4e0637 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1467,7 +1467,7 @@ have muAP_gt0 : 0 < mu AP. pose h x := if x \in AP then f x + (epsRN mA abs)%:num%:E else f x. have mh : measurable_fun setT h. apply: measurable_fun_if => //. - - by apply: (measurable_fun_bool true); rewrite preimage_mem_true. + - by apply: (measurable_fun_bool true); rewrite setTI preimage_mem_true. - by apply: measurable_funTS; apply: emeasurable_funD => //; exact: mf. - by apply: measurable_funTS; exact: mf. have hge0 x : 0 <= h x. @@ -1559,7 +1559,7 @@ pose f_ j x := if x \in E j then g_ j x else 0. have f_ge0 k x : 0 <= f_ k x by rewrite /f_; case: ifP. have mf_ k : measurable_fun setT (f_ k). apply: measurable_fun_if => //. - - by apply: (measurable_fun_bool true); rewrite preimage_mem_true. + - by apply: (measurable_fun_bool true); rewrite setTI preimage_mem_true. - rewrite preimage_mem_true. by apply: measurable_funTS => //; have /integrableP[] := ig_ k. have if_T k : integrable mu setT (f_ k). diff --git a/theories/esum.v b/theories/esum.v index 63250f50f5..95e7d038eb 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -451,6 +451,15 @@ End esum_bigcup. Arguments esum_bigcupT {R T K} J a. Arguments esum_bigcup {R T K} J a. +Lemma nneseries_sum_bigcup {R : realType} (T : choiceType) (F : (set T)^nat) + (f : T -> \bar R) : trivIset [set: nat] F -> (forall i, 0 <= f i)%E -> + (\esum_(i in \bigcup_n F n) f i = \sum_(0 <= i tF f0; rewrite esum_bigcupT// nneseries_esum//; last first. + by move=> k _; exact: esum_ge0. +by rewrite fun_true; apply: eq_esum => /= i _. +Qed. + Definition summable (T : choiceType) (R : realType) (D : set T) (f : T -> \bar R) := (\esum_(x in D) `| f x | < +oo)%E. diff --git a/theories/kernel.v b/theories/kernel.v index 74b2a03428..88b70b7b73 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -132,7 +132,7 @@ Lemma measurable_fun_kseries (U : set Y) : measurable U -> measurable_fun [set: X] (kseries ^~ U). Proof. move=> mU. -by apply: ge0_emeasurable_fun_sum => // n; exact/measurable_kernel. +by apply: ge0_emeasurable_fun_sum => // n _; exact/measurable_kernel. Qed. HB.instance Definition _ := @@ -506,7 +506,7 @@ Variable k : X * Y -> \bar R. Lemma measurable_fun_xsection_integral (l : X -> {measure set Y -> \bar R}) - (k_ : ({nnsfun [the measurableType _ of X * Y] >-> R})^nat) + (k_ : {nnsfun (X * Y) >-> R}^nat) (ndk_ : nondecreasing_seq (k_ : (X * Y -> R)^nat)) (k_k : forall z, (k_ n z)%:E @[n --> \oo] --> k z) : (forall n r, @@ -585,7 +585,7 @@ have [l_ hl_] := sfinite_kernel l. rewrite (_ : (fun x => _) = (fun x => mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first. by apply/funext => x; rewrite hl_//; exact/measurable_xsection. -apply: ge0_emeasurable_fun_sum => // m. +apply: ge0_emeasurable_fun_sum => // m _. by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. Qed. @@ -614,7 +614,7 @@ Qed. HB.instance Definition _ := isKernel.Build _ _ _ _ _ (kdirac mf) measurable_fun_kdirac. -Let kdirac_prob x : kdirac mf x setT = 1. +Let kdirac_prob x : kdirac mf x [set: Y] = 1. Proof. by rewrite /kdirac/= diracT. Qed. HB.instance Definition _ := Kernel_isProbability.Build _ _ _ _ _ @@ -717,46 +717,14 @@ HB.instance Definition _ t := Kernel_isFinite.Build _ _ _ _ R (kadd k1 k2) kadd_finite_uub. End fkadd. -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 => - [the probability _ _ of mnormalize (k x) point] : pprobability Y R). -Proof. -apply: (@measurability _ _ _ _ _ _ - (@pset _ _ _ : set (set (pprobability Y R)))) => //. -move=> _ -[_ [r r01] [Ys mYs <-]] <-. -rewrite /mnormalize /mset /preimage/=. -apply: emeasurable_fun_infty_o => //. -rewrite /mnormalize/=. -rewrite (_ : (fun x => _) = (fun x => if (k x setT == 0) || (k x setT == +oo) - then \d_point Ys else k x Ys * ((fine (k x setT))^-1)%:E)); last first. - by apply/funext => x/=; case: ifPn. -apply: measurable_fun_if => //. -- apply: (measurable_fun_bool true) => //. - rewrite (_ : _ @^-1` _ = [set t | k t setT == 0] `|` - [set t | k t setT == +oo]); last first. - by apply/seteqP; split=> x /= /orP//. - by apply: measurableU; exact: kernel_measurable_eq_cst. -- apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel. - apply/EFin_measurable_fun; rewrite setTI. - apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]). - + exact: open_measurable. - + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey. - + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0. - exact: inv_continuous. - + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel. -Qed. - Section knormalize. Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). Variable f : R.-ker X ~> Y. Definition knormalize (P : probability Y R) : X -> {measure set Y -> \bar R} := - fun x => [the measure _ _ of mnormalize (f x) P]. - -Variable P : probability Y R. + fun x => mnormalize (f x) P. -Let measurable_fun_knormalize U : +Let measurable_knormalize (P : probability Y R) U : measurable U -> measurable_fun [set: X] (knormalize P ^~ U). Proof. move=> mU; rewrite /knormalize/= /mnormalize /=. @@ -773,7 +741,7 @@ apply: measurable_fun_if => //. - apply: (@measurable_funS _ _ _ _ setT) => //. exact: kernel_measurable_fun_eq_cst. - apply: emeasurable_funM. - by have := measurable_kernel f U mU; exact: measurable_funS. + exact: measurable_funS (measurable_kernel f U mU). apply/EFin_measurable_fun. apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]) => //. + exact: open_measurable. @@ -786,17 +754,48 @@ apply: measurable_fun_if => //. by have := measurable_kernel f _ measurableT; exact: measurable_funS. Qed. -HB.instance Definition _ := isKernel.Build _ _ _ _ R (knormalize P) - measurable_fun_knormalize. +HB.instance Definition _ (P : probability Y R) := + isKernel.Build _ _ _ _ R (knormalize P) (measurable_knormalize P). -Let knormalize1 x : knormalize P x [set: Y] = 1. +Let knormalize1 (P : probability Y R) x : knormalize P x [set: Y] = 1. Proof. by rewrite /knormalize/= probability_setT. Qed. -HB.instance Definition _ := - @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) knormalize1. +HB.instance Definition _ (P : probability Y R):= + @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) (knormalize1 P). End knormalize. +(* TODO: useful? *) +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 => + [the probability _ _ of mnormalize (k x) point] : pprobability Y R). +Proof. +apply: (@measurability _ _ _ _ _ _ + (@pset _ _ _ : set (set (pprobability Y R)))) => //. +move=> _ -[_ [r r01] [Ys mYs <-]] <-. +rewrite /mnormalize /mset /preimage/=. +apply: emeasurable_fun_infty_o => //. +rewrite /mnormalize/=. +rewrite (_ : (fun x => _) = (fun x => if (k x setT == 0) || (k x setT == +oo) + then \d_point Ys else k x Ys * ((fine (k x setT))^-1)%:E)); last first. + by apply/funext => x/=; case: ifPn. +apply: measurable_fun_if => //. +- apply: (measurable_fun_bool true) => //. + rewrite (_ : _ @^-1` _ = [set t | k t setT == 0] `|` + [set t | k t setT == +oo]); last first. + by apply/seteqP; split=> x /= /orP. + by rewrite setTI; apply: measurableU; exact: kernel_measurable_eq_cst. +- apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel. + apply/EFin_measurable_fun; rewrite setTI. + apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]). + + exact: open_measurable. + + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey. + + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0. + exact: inv_continuous. + + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel. +Qed. + Section kcomp_def. Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2) (Z : measurableType d3) (R : realType). diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 488b4b0059..f59201b046 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1969,15 +1969,30 @@ move=> fs mh; under eq_fun do rewrite fsbig_finite//. exact: emeasurable_fun_sum. Qed. -Lemma ge0_emeasurable_fun_sum D (h : nat -> (T -> \bar R)) : - (forall k x, 0 <= h k x) -> (forall k, measurable_fun D (h k)) -> - measurable_fun D (fun x => \sum_(i h0 mh; rewrite [X in measurable_fun _ X](_ : _ = - (fun x => limn_esup (fun n => \sum_(0 <= i < n) h i x))); last first. +Lemma ge0_emeasurable_fun_sum D (h : nat -> (T -> \bar R)) (P : pred nat) : + (forall k x, D x -> P k -> 0 <= h k x) -> (forall k, P k -> measurable_fun D (h k)) -> + measurable_fun D (fun x => \sum_(i h0 mh. +move=> mD; move: (mD). +apply/(@measurable_restrict _ _ _ _ _ setT) => //. +rewrite [X in measurable_fun _ X](_ : _ = + (fun x => \sum_(0 <= i x/=; rewrite /patch; case: ifPn => // xD. + by rewrite eseries0. +rewrite [X in measurable_fun _ X](_ : _ = + (fun x => limn_esup (fun n => \sum_(0 <= i < n | P i) (h i) \_ D x))); last first. apply/funext=> x; rewrite is_cvg_limn_esupE//. - exact: is_cvg_ereal_nneg_natsum. -by apply: measurable_fun_limn_esup => k; exact: emeasurable_fun_sum. + apply: is_cvg_nneseries_cond => n Pn; rewrite patchE. + by case: ifPn => // xD; rewrite h0//; exact/set_mem. +apply: measurable_fun_limn_esup => k. +under eq_fun do rewrite big_mkcond. +apply: emeasurable_fun_sum => n. +have [|] := boolP (n \in P). + rewrite /in_mem/= => Pn; rewrite Pn. + by apply/(measurable_restrict (h n)) => //; exact: mh. +by rewrite /in_mem/= => /negbTE ->. Qed. Lemma emeasurable_funB D f g : @@ -5262,7 +5277,7 @@ rewrite ge0_integralZl//; last by rewrite lee_fin. - by move=> y _; rewrite lee_fin. Qed. -Lemma sfun_measurable_fun_fubini_tonelli_F : measurable_fun setT F. +Lemma sfun_measurable_fun_fubini_tonelli_F : measurable_fun [set: T1] F. Proof. rewrite sfun_fubini_tonelli_FE//; apply: emeasurable_fun_fsum => // r. exact/measurable_funeM/measurable_fun_xsection. @@ -5703,8 +5718,8 @@ transitivity (\sum_(n \sum_(n x. by rewrite ge0_integral_measure_series//; exact/measurableT_comp. - apply: ge0_emeasurable_fun_sum; first by move=> k x; exact: integral_ge0. - by move=> k; apply: measurable_fun_fubini_tonelli_F. + apply: ge0_emeasurable_fun_sum; first by move=> k x *; exact: integral_ge0. + by move=> k _; exact: measurable_fun_fubini_tonelli_F. apply: eq_eseriesr => n _; apply: eq_integral => x _. by rewrite ge0_integral_measure_series//; exact/measurableT_comp. transitivity (\sum_(n measurable_fun D g -> measurable_fun D (fun x => f x < g x). Proof. -move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. -- under eq_fun do rewrite -subr_gt0. - rewrite preimage_true -preimage_itv_o_infty. - by apply: (measurable_funB mg mf) => //; exact: measurable_itv. -- under eq_fun do rewrite ltNge -subr_ge0. - rewrite preimage_false set_predC setCK -preimage_itv_c_infty. - by apply: (measurable_funB mf mg) => //; exact: measurable_itv. -- by rewrite preimage_set0 setI0. -- by rewrite preimage_setT setIT. +move=> mf mg mD; apply: (measurable_fun_bool true) => //. +under eq_fun do rewrite -subr_gt0. +by rewrite preimage_true -preimage_itv_o_infty; exact: measurable_funB. +Qed. + +Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x <= g x). +Proof. +move=> mf mg mD; apply: (measurable_fun_bool true) => //. +under eq_fun do rewrite -subr_ge0. +by rewrite preimage_true -preimage_itv_c_infty; exact: measurable_funB. Qed. Lemma measurable_maxr D f g : @@ -1672,11 +1674,26 @@ Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed. #[global] Hint Extern 0 (measurable_fun _ expR) => solve [apply: measurable_expR] : core. +Lemma measurable_natmul {R : realType} D n : + measurable_fun D ((@GRing.natmul R)^~ n). +Proof. +under eq_fun do rewrite -mulr_natr. +by do 2 apply: measurable_funM => //. +Qed. + +Lemma measurable_fun_pow {R : realType} D (f : R -> R) n : measurable_fun D f -> + measurable_fun D (fun x => f x ^+ n). +Proof. +move=> mf. +exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). +Qed. + Lemma measurable_powR (R : realType) p : measurable_fun [set: R] (@powR R ^~ p). Proof. apply: measurable_fun_if => //. -- apply: (measurable_fun_bool true); rewrite (_ : _ @^-1` _ = [set 0])//. +- apply: (measurable_fun_bool true). + rewrite (_ : _ @^-1` _ = [set 0]) ?setTI//. by apply/seteqP; split => [_ /eqP ->//|_ -> /=]; rewrite eqxx. - rewrite setTI; apply: measurableT_comp => //. rewrite (_ : _ @^-1` _ = [set~ 0]); first exact: measurableT_comp. @@ -1760,9 +1777,7 @@ move=> mf;rewrite (_ : er_map _ = fun x => if x \is a fin_num then (f (fine x))%:E else x); last first. by apply: funext=> -[]. apply: measurable_fun_ifT => //=. -+ apply: (measurable_fun_bool true). - rewrite /preimage/= -[X in measurable X]setTI. - exact/emeasurable_fin_num. ++ by apply: (measurable_fun_bool true); exact/emeasurable_fin_num. + exact/EFin_measurable_fun/measurableT_comp. Qed. #[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_er_map`")] @@ -1779,7 +1794,7 @@ Lemma measurable_fun_einfs D (f : (T -> \bar R)^nat) : Proof. move=> mf n mD. apply: (measurability (ErealGenCInfty.measurableE R)) => //. -move=> _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n => /=. +move=> _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n =>/=. by apply: bigcap_measurable => ? ?; exact/mf/emeasurable_itv. Qed. diff --git a/theories/measure.v b/theories/measure.v index 259b796dcc..3865b13544 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -920,6 +920,13 @@ rewrite -bigsetI_fset_set// big_seq; apply: bigsetI_measurable => i. by rewrite in_fset_set ?inE// => *; apply: Fm. Qed. +Lemma measurableID A B : measurable A -> measurable (A `&` B) -> + measurable (A `\` B). +Proof. +move=> mA /measurableC; rewrite setCI => /(measurableI A) => /(_ mA). +by rewrite setIUr setICr set0U. +Qed. + End algebraofsets_lemmas. Section measurable_lemmas. @@ -1160,23 +1167,46 @@ by move=> mx my; apply: measurable_fun_if => //; [exact: measurable_funS mx|exact: measurable_funS my]. Qed. -Lemma measurable_fun_bool D (f : T1 -> bool) b : - measurable (f @^-1` [set b]) -> measurable_fun D f. -Proof. -have FNT : [set false] = [set~ true] by apply/seteqP; split => -[]//=. -wlog {b}-> : b / b = true. - case: b => [|h]; first exact. - by rewrite FNT -preimage_setC => /measurableC; rewrite setCK; exact: h. -move=> mfT mD /= Y; have := @subsetT _ Y; rewrite setT_bool => YT. -have [-> _|-> _|-> _ |-> _] := subset_set2 YT. +Section measurable_fun_bool. + +Let measurable_fun_TF D (f : T1 -> bool) : + measurable (D `&` f @^-1` [set true]) -> + measurable (D `&` f @^-1` [set false]) -> + measurable_fun D f. +Proof. +move=> mT mF mD /= Y mY. +have := @subsetT _ Y; rewrite setT_bool => YT. +move: mY; have [-> _|-> _|-> _ |-> _] := subset_set2 YT. - by rewrite preimage0 ?setI0. -- by apply: measurableI => //; exact: mfT. -- rewrite -[X in measurable X]setCK; apply: measurableC; rewrite setCI. - apply: measurableU; first exact: measurableC. - by rewrite FNT preimage_setC setCK; exact: mfT. +- exact: mT. +- exact: mF. - by rewrite -setT_bool preimage_setT setIT. Qed. +Lemma measurable_fun_bool D (f : T1 -> bool) b : + measurable (D `&` f @^-1` [set b]) -> measurable_fun D f. +Proof. +move=> mb mD; have mDb : measurable (D `&` f @^-1` [set ~~ b]). + rewrite (_ : [set ~~ b] = [set~ b]); last first. + by apply/seteqP; split=> -[] /=; case: b {mb}. + by rewrite -preimage_setC; exact: measurableID. +by case: b => /= in mb mDb *; exact: measurable_fun_TF. +Qed. + +End measurable_fun_bool. +Arguments measurable_fun_bool {D f} _. + +Lemma measurable_and D (f : T1 -> bool) (g : T1 -> bool) : + measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x && g x). +Proof. +move=> mf mg mD; apply: (measurable_fun_bool true) => //. +- rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `&` + (D `&` g @^-1` [set true])); last first. + by rewrite setIACA setIid; congr (_ `&` _); apply/seteqP; split => x /andP. + by apply: measurableI; [exact: mf|exact: mg]. +Qed. + End measurable_fun. #[global] Hint Extern 0 (measurable_fun _ (fun=> _)) => solve [apply: measurable_cst] : core. diff --git a/theories/probability.v b/theories/probability.v index c471b1b424..0ab1ddf266 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -2,11 +2,11 @@ From mathcomp Require Import all_ssreflect. From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality. +From mathcomp Require Import cardinality fsbigop. From HB Require Import structures. Require Import exp numfun lebesgue_measure lebesgue_integral. Require Import reals ereal signed topology normedtype sequences esum measure. -Require Import exp numfun lebesgue_measure lebesgue_integral. +Require Import exp numfun lebesgue_measure lebesgue_integral kernel. (**md**************************************************************************) (* # Probability *) @@ -15,24 +15,39 @@ Require Import exp numfun lebesgue_measure lebesgue_integral. (* the type probability T R (a measure that sums to 1). *) (* *) (* ``` *) -(* {RV P >-> R} == real random variable: a measurable function from *) -(* the measurableType of the probability P to R *) -(* distribution P X == measure image of the probability measure P by the *) -(* random variable X : {RV P -> R} *) -(* P as type probability T R with T of type *) -(* measurableType. *) -(* Declared as an instance of probability measure. *) -(* 'E_P[X] == expectation of the real measurable function X *) -(* covariance X Y == covariance between real random variable X and Y *) -(* 'V_P[X] == variance of the real random variable X *) -(* mmt_gen_fun X == moment generating function of the random variable *) -(* X *) -(* {dmfun T >-> R} == type of discrete real-valued measurable functions *) -(* {dRV P >-> R} == real-valued discrete random variable *) -(* dRV_dom X == domain of the discrete random variable X *) -(* dRV_enum X == bijection between the domain and the range of X *) -(* pmf X r := fine (P (X @^-1` [set r])) *) -(* enum_prob X k == probability of the kth value in the range of X *) +(* {RV P >-> R} == real random variable: a measurable function from *) +(* the measurableType of the probability P to R *) +(* distribution P X == measure image of the probability measure P by the *) +(* random variable X : {RV P -> R} *) +(* P as type probability T R with T of type *) +(* measurableType. *) +(* Declared as an instance of probability measure. *) +(* 'E_P[X] == expectation of the real measurable function X *) +(* covariance X Y == covariance between real random variable X and Y *) +(* 'V_P[X] == variance of the real random variable X *) +(* mmt_gen_fun X == moment generating function of the random variable *) +(* X *) +(* {dmfun T >-> R} == type of discrete real-valued measurable functions *) +(* {dRV P >-> R} == real-valued discrete random variable *) +(* dRV_dom X == domain of the discrete random variable X *) +(* dRV_enum X == bijection between the domain and the range of X *) +(* pmf X r := fine (P (X @^-1` [set r])) *) +(* enum_prob X k == probability of the kth value in the range of X *) +(* ``` *) +(* *) +(* ``` *) +(* bernoulli_pmf p == Bernoulli pmf *) +(* bernoulli p == Bernoulli probability measure when 0 <= p <= 1 *) +(* and \d_false otherwise *) +(* binomial_pmf n p == binomial pmf *) +(* binomial_prob n p == binomial probability measure when 0 <= p <= 1 *) +(* and \d_0%N otherwise *) +(* bin_prob n k p == $\binom{n}{k}p^k (1-p)^(n-k)$ *) +(* Computes a binomial distribution term for *) +(* k successes in n trials with success rate p *) +(* uniform_pdf a b == uniform pdf *) +(* uniform_prob a b ab == uniform probability over the interval [a,b] *) +(* with ab0 a proof that 0 < b - a *) (* ``` *) (* *) (******************************************************************************) @@ -828,3 +843,511 @@ by rewrite /pmf fineK// fin_num_measure. Qed. End discrete_distribution. + +Section bernoulli_pmf. +Context {R : realType} (p : R). +Local Open Scope ring_scope. + +Definition bernoulli_pmf b := if b then p else 1 - p. + +Lemma bernoulli_pmf_ge0 (p01 : 0 <= p <= 1) b : 0 <= bernoulli_pmf b. +Proof. +rewrite /bernoulli_pmf. +by move: p01 => /andP[p0 p1]; case: ifPn => // _; rewrite subr_ge0. +Qed. + +Lemma bernoulli_pmf1 (p01 : 0 <= p <= 1) : + \sum_(i \in [set: bool]) (bernoulli_pmf i)%:E = 1%E. +Proof. +rewrite setT_bool fsbigU//=; last by move=> x [/= ->]. +by rewrite !fsbig_set1/= -EFinD addrCA subrr addr0. +Qed. + +End bernoulli_pmf. + +Lemma measurable_bernoulli_pmf {R : realType} D n : + measurable_fun D (@bernoulli_pmf R ^~ n). +Proof. +by apply/measurable_funTS/measurable_fun_if => //=; exact: measurable_funB. +Qed. + +Definition bernoulli {R : realType} (p : R) : set bool -> \bar R := fun A => + if (0 <= p <= 1)%R then \sum_(b \in A) (bernoulli_pmf p b)%:E else \d_false A. + +Section bernoulli. +Context {R : realType} (p : R). + +Local Notation bernoulli := (bernoulli p). + +Let bernoulli0 : bernoulli set0 = 0. +Proof. +by rewrite /bernoulli; case: ifPn => // p01; rewrite fsbig_set0. +Qed. + +Let bernoulli_ge0 U : (0 <= bernoulli U)%E. +Proof. +rewrite /bernoulli; case: ifPn => // p01. +rewrite fsbig_finite//= sumEFin lee_fin. +by apply: sumr_ge0 => /= b _; exact: bernoulli_pmf_ge0. +Qed. + +Let bernoulli_sigma_additive : semi_sigma_additive bernoulli. +Proof. +move=> F mF tF mUF; rewrite /bernoulli; case: ifPn => p01; last first. + exact: measure_semi_sigma_additive. +apply: cvg_toP. + apply: ereal_nondecreasing_is_cvgn => m n mn. + apply: lee_sum_nneg_natr => // k _ _. + rewrite fsbig_finite//= sumEFin lee_fin. + by apply: sumr_ge0 => /= b _; exact: bernoulli_pmf_ge0. +transitivity (\sum_(0 <= i k _; rewrite esum_fset//= => b _. + by rewrite lee_fin bernoulli_pmf_ge0. +rewrite -nneseries_sum_bigcup//=; last first. + by move=> b; rewrite lee_fin bernoulli_pmf_ge0. +by rewrite esum_fset//= => b _; rewrite lee_fin bernoulli_pmf_ge0. +Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ bernoulli + bernoulli0 bernoulli_ge0 bernoulli_sigma_additive. + +Let bernoulli_setT : bernoulli [set: _] = 1%E. +Proof. +rewrite /bernoulli/=; case: ifPn => p01; last by rewrite probability_setT. +by rewrite bernoulli_pmf1. +Qed. + +HB.instance Definition _ := + @Measure_isProbability.Build _ _ R bernoulli bernoulli_setT. + +End bernoulli. + +Section bernoulli_measure. +Context {R : realType}. +Variables (p : R) (p0 : (0 <= p)%R) (p1 : ((NngNum p0)%:num <= 1)%R). + +Lemma bernoulli_dirac : bernoulli p = measure_add + (mscale (NngNum p0) \d_true) (mscale (onem_nonneg p1) \d_false). +Proof. +apply/funext => U; rewrite /bernoulli; case: ifPn => [p01|]; last first. + by rewrite p0/= p1. +rewrite measure_addE/= /mscale/=. +have := @subsetT _ U; rewrite setT_bool => UT. +have [->|->|->|->] /= := subset_set2 UT. +- rewrite -esum_fset//=; last by move=> b; rewrite lee_fin bernoulli_pmf_ge0. + by rewrite esum_set0 2!measure0 2!mule0 adde0. +- rewrite -esum_fset//=; last by move=> b; rewrite lee_fin bernoulli_pmf_ge0. + rewrite esum_set1/= ?lee_fin// 2!diracE mem_set//= memNset//= mule0 adde0. + by rewrite mule1. +- rewrite -esum_fset//=; last by move=> b; rewrite lee_fin bernoulli_pmf_ge0. + rewrite esum_set1/= ?lee_fin ?subr_ge0// 2!diracE memNset//= mem_set//=. + by rewrite mule0 add0e mule1. +- rewrite fsbigU//=; last by move=> x [->]. + by rewrite 2!fsbig_set1/= -setT_bool 2!diracT !mule1. +Qed. + +End bernoulli_measure. +Arguments bernoulli {R}. + +Section integral_bernoulli. +Context {R : realType}. +Variables (p : R) (p01 : (0 <= p <= 1)%R). +Local Open Scope ereal_scope. + +Lemma bernoulliE A : bernoulli p A = p%:E * \d_true A + (`1-p)%:E * \d_false A. +Proof. by case/andP : p01 => p0 p1; rewrite bernoulli_dirac// measure_addE. Qed. + +Lemma integral_bernoulli (f : bool -> \bar R) : (forall x, 0 <= f x) -> + \int[bernoulli p]_y (f y) = p%:E * f true + (`1-p)%:E * f false. +Proof. +move=> f0; case/andP : p01 => p0 p1; rewrite bernoulli_dirac/=. +rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. +by rewrite !ge0_integral_mscale//= !integral_dirac//= !diracT !mul1e. +Qed. + +End integral_bernoulli. + +Section measurable_bernoulli. +Local Open Scope ring_scope. +Variable R : realType. +Implicit Type p : R. + +Lemma measurable_bernoulli : + measurable_fun setT (bernoulli : R -> pprobability bool R). +Proof. +apply: (@measurability _ _ _ _ _ _ + (@pset _ _ _ : set (set (pprobability _ R)))) => //. +move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=. +apply: measurable_fun_if => //=. + by apply: measurable_and => //; exact: measurable_fun_ler. +apply: (eq_measurable_fun (fun t => + \sum_(b <- fset_set Ys) (bernoulli_pmf t b)%:E)). + move=> x /set_mem[_/= x01]. + by rewrite fsbig_finite//=. +apply: emeasurable_fun_sum => n. +move=> k Ysk; apply/measurableT_comp => //. +exact: measurable_bernoulli_pmf. +Qed. + +Lemma measurable_bernoulli2 U : measurable U -> + measurable_fun setT (bernoulli ^~ U : R -> \bar R). +Proof. +by move=> ?; exact: (measurable_kernel (kprobability measurable_bernoulli)). +Qed. + +End measurable_bernoulli. +Arguments measurable_bernoulli {R}. + +Section binomial_pmf. +Local Open Scope ring_scope. +Context {R : realType} (n : nat) (p : R). + +Definition binomial_pmf k := p ^+ k * (`1-p) ^+ (n - k) *+ 'C(n, k). + +Lemma binomial_pmf_ge0 k (p01 : (0 <= p <= 1)%R) : 0 <= binomial_pmf k. +Proof. +move: p01 => /andP[p0 p1]; rewrite mulrn_wge0// mulr_ge0// ?exprn_ge0//. +exact: onem_ge0. +Qed. + +End binomial_pmf. + +Lemma measurable_binomial_pmf {R : realType} D n k : + measurable_fun D (@binomial_pmf R n ^~ k). +Proof. +apply: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x *+ 'C(n, k))%R) => /=. + exact: measurable_natmul. +apply: measurable_funM => //=; apply: measurable_fun_pow. +exact: measurable_funB. +Qed. + +Definition binomial_prob {R : realType} (n : nat) (p : R) : set nat -> \bar R := + fun U => if (0 <= p <= 1)%R then + \esum_(k in U) (binomial_pmf n p k)%:E else \d_0%N U. + +Section binomial. +Context {R : realType} (n : nat) (p : R). +Local Open Scope ereal_scope. + +Local Notation binomial := (binomial_prob n p). + +Let binomial0 : binomial set0 = 0. +Proof. by rewrite /binomial measure0; case: ifPn => //; rewrite esum_set0. Qed. + +Let binomial_ge0 U : 0 <= binomial U. +Proof. +rewrite /binomial; case: ifPn => // p01; apply: esum_ge0 => /= k Uk. +by rewrite lee_fin binomial_pmf_ge0. +Qed. + +Let binomial_sigma_additive : semi_sigma_additive binomial. +Proof. +move=> F mF tF mUF; rewrite /binomial; case: ifPn => p01; last first. + exact: measure_semi_sigma_additive. +apply: cvg_toP. + apply: ereal_nondecreasing_is_cvgn => a b ab. + apply: lee_sum_nneg_natr => // k _ _. + by apply: esum_ge0 => /= ? _; exact: binomial_pmf_ge0. +by rewrite nneseries_sum_bigcup// => i; rewrite lee_fin binomial_pmf_ge0. +Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ binomial + binomial0 binomial_ge0 binomial_sigma_additive. + +Let binomial_setT : binomial [set: _] = 1. +Proof. +rewrite /binomial; case: ifPn; last by move=> _; rewrite probability_setT. +move=> p01; rewrite /binomial_pmf. +have pkn k : 0%R <= (p ^+ k * `1-p ^+ (n - k) *+ 'C(n, k))%:E. + case/andP : p01 => p0 p1. + by rewrite lee_fin mulrn_wge0// mulr_ge0 ?exprn_ge0 ?subr_ge0. +rewrite (esumID `I_n.+1)// [X in _ + X]esum1 ?adde0; last first. + by move=> /= k [_ /negP]; rewrite -leqNgt => nk; rewrite bin_small. +rewrite setTI esum_fset// -fsbig_ord//=. +under eq_bigr do rewrite mulrC. +rewrite sumEFin -exprDn_comm; last exact: mulrC. +by rewrite addrC add_onemK expr1n. +Qed. + +HB.instance Definition _ := + @Measure_isProbability.Build _ _ R binomial binomial_setT. + +End binomial. + +Section binomial_probability. +Local Open Scope ring_scope. +Context {R : realType} (n : nat) (p : R) + (p0 : (0 <= p)%R) (p1 : ((NngNum p0)%:num <= 1)%R). + +Definition bin_prob (k : nat) : {nonneg R} := + ((NngNum p0)%:num ^+ k * (NngNum (onem_ge0 p1))%:num ^+ (n - k)%N *+ 'C(n, k))%:nng. + +Lemma bin_prob0 : bin_prob 0 = ((NngNum (onem_ge0 p1))%:num^+n)%:nng. +Proof. +rewrite /bin_prob bin0 subn0/=; apply/val_inj => /=. +by rewrite expr0 mul1r mulr1n. +Qed. + +Lemma bin_prob1 : bin_prob 1 = + ((NngNum p0)%:num * (NngNum (onem_ge0 p1))%:num ^+ n.-1 *+ n)%:nng. +Proof. +by rewrite /bin_prob bin1/=; apply/val_inj => /=; rewrite expr1 subn1. +Qed. + +Lemma binomial_msum : + binomial_prob n p = msum (fun k => mscale (bin_prob k) \d_k) n.+1. +Proof. +apply/funext => U. +rewrite /binomial_prob; case: ifPn => [_|]; last by rewrite p1 p0. +rewrite /msum/= /mscale/= /binomial_pmf. +have pkn k : (0%R <= (p ^+ k * `1-p ^+ (n - k) *+ 'C(n, k))%:E)%E. + by rewrite lee_fin mulrn_wge0// mulr_ge0 ?exprn_ge0 ?subr_ge0. +rewrite (esumID `I_n.+1)//= [X in _ + X]esum1 ?adde0; last first. + by move=> /= k [_ /negP]; rewrite -leqNgt => nk; rewrite bin_small. +rewrite esum_mkcondl esum_fset//; last by move=> i /= _; case: ifPn. +rewrite -fsbig_ord//=; apply: eq_bigr => i _. +by rewrite diracE; case: ifPn => /= iU; [rewrite mule1|rewrite mule0]. +Qed. + +Lemma binomial_probE U : binomial_prob n p U = + (\sum_(k < n.+1) (bin_prob k)%:num%:E * (\d_(nat_of_ord k) U))%E. +Proof. by rewrite binomial_msum. Qed. + +Lemma integral_binomial (f : nat -> \bar R) : (forall x, 0 <= f x)%E -> + (\int[binomial_prob n p]_y (f y) = + \sum_(k < n.+1) (bin_prob k)%:num%:E * f k)%E. +Proof. +move=> f0; rewrite binomial_msum ge0_integral_measure_sum//=. +apply: eq_bigr => i _. +by rewrite ge0_integral_mscale//= integral_dirac//= diracT mul1e. +Qed. + +End binomial_probability. + +Lemma integral_binomial_prob (R : realType) n p U : (0 <= p <= 1)%R -> + (\int[binomial_prob n p]_y \d_(0 < y)%N U = + bernoulli (1 - `1-p ^+ n) U :> \bar R)%E. +Proof. +move=> /andP[p0 p1]; rewrite bernoulliE//=; last first. + rewrite subr_ge0 exprn_ile1//=; [|exact/onem_ge0|exact/onem_le1]. + by rewrite lerBlDr addrC -lerBlDr subrr; exact/exprn_ge0/onem_ge0. +rewrite (@integral_binomial _ n p _ _ (fun y => \d_(1 <= y)%N U))//. +rewrite !big_ord_recl/=. +rewrite expr0 mul1r subn0 bin0 ltnn mulr1n addrC. +rewrite onemD opprK onem1 add0r; congr +%E. +rewrite /bump; under eq_bigr do rewrite leq0n add1n ltnS leq0n. +rewrite -ge0_sume_distrl; last first. + move=> i _. + by apply/mulrn_wge0/mulr_ge0; apply/exprn_ge0 => //; exact/onem_ge0. +congr *%E. +transitivity (\sum_(i < n.+1) (`1-p ^+ (n - i) * p ^+ i *+ 'C(n, i))%:E - + (`1-p ^+ n)%:E)%E. + rewrite big_ord_recl/=. + rewrite expr0 mulr1 subn0 bin0 mulr1n addrAC -EFinD subrr add0e. + by rewrite /bump; under [RHS]eq_bigr do rewrite leq0n add1n mulrC. +rewrite sumEFin -(@exprDn_comm _ `1-p p n)//. + by rewrite subrK expr1n. +by rewrite /GRing.comm/onem mulrC. +Qed. + +Lemma measurable_binomial_prob (R : realType) (n : nat) : + measurable_fun setT (binomial_prob n : R -> pprobability _ _). +Proof. +apply: (@measurability _ _ _ _ _ _ + (@pset _ _ _ : set (set (pprobability _ R)))) => //. +move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=. +rewrite /binomial_prob/=. +set f := (X in measurable_fun _ X). +apply: measurable_fun_if => //=. + by apply: measurable_and => //; exact: measurable_fun_ler. +apply: (eq_measurable_fun (fun t => + \sum_(k x /set_mem[_/= x01]. + rewrite nneseries_esum// -1?[in RHS](set_mem_set Ys)// => k kYs. + by rewrite lee_fin binomial_pmf_ge0. +apply: ge0_emeasurable_fun_sum. + by move=> k x/= [_ x01] _; rewrite lee_fin binomial_pmf_ge0. +move=> k Ysk; apply/measurableT_comp => //. +exact: measurable_binomial_pmf. +Qed. + +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. +move=> ab; rewrite /uniform_pdf; case: ifPn => // axb. +by rewrite invr_ge0// ltW// subr_gt0. +Qed. + +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. + +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. + +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. + +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. by rewrite /uniform_prob integral_set0. Qed. + +Let uniform_ge0 U : (0 <= uniform_prob ab U)%E. +Proof. +by apply: integral_ge0 => /= x Ux; rewrite lee_fin uniform_pdf_ge0. +Qed. + +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. + +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. + +HB.instance Definition _ := isMeasure.Build _ _ _ (uniform_prob ab) + uniform0 uniform_ge0 uniform_sigma_additive. + +Let uniform_setT : uniform_prob ab [set: _] = 1%:E. +Proof. by rewrite /uniform_prob /mscale/= integral_uniform_pdf1. Qed. + +HB.instance Definition _ := @Measure_isProbability.Build _ _ R + (uniform_prob ab) uniform_setT. + +Lemma dominates_uniform_prob : uniform_prob ab `<< mu. +Proof. +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/EFin_measurable_fun/measurable_funTS; exact: measurable_uniform_pdf. +- by move=> x [Ax _]; rewrite lee_fin invr_ge0// ltW// subr_gt0. +- 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/EFin_measurable_fun/measurable_indic. +- by move=> x _; rewrite lee_fin. +- by rewrite lee_fin invr_ge0// ltW// subr_gt0. +Qed. + +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/EFin_measurable_fun/measurableT_comp. + - by move=> n x _; rewrite EFinM nnfun_muleindic_ge0. +rewrite -[RHS]ge0_integralZl//; last 3 first. + - exact/EFin_measurable_fun/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/EFin_measurable_fun; 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/EFin_measurable_fun/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. +have [f_ [ndf_ f_f]] := approximation measurableT mf (fun y _ => f0 y). +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: f_f. + - by move=> n; exact/EFin_measurable_fun/measurable_funTS. + - by move=> n ? _; rewrite lee_fin. + - by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/ndf_. +rewrite [X in _ = (_ * X)%E](_ : _ = lim + (\int[mu]_(x in `[a, b]) (f_ n x)%:E @[n --> \oo])%E); last first. + rewrite -monotone_convergence//=. + - by apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //; exact: f_f. + - by move=> n; exact/EFin_measurable_fun/measurable_funTS. + - by move=> n ? _; rewrite lee_fin. + - by move=> ? _ ? ? /ndf_ /lefP; rewrite lee_fin. +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/EFin_measurable_fun/measurable_funTS. +- by move=> ? _; rewrite lee_fin. +- exact/EFin_measurable_fun/measurable_funTS. +- by move=> ? _; rewrite lee_fin; move/ndf_ : xy => /lefP. +Qed. + +End uniform_probability. diff --git a/theories/signed.v b/theories/signed.v index de3932d30d..84fc0d8db3 100644 --- a/theories/signed.v +++ b/theories/signed.v @@ -1225,4 +1225,10 @@ Lemma onemX_NngNum r (r1 : r <= 1) (r0 : 0 <= r) n : `1-(r ^+ n) = (NngNum (onemX_ge0 n r0 r1))%:num. Proof. by []. Qed. +Lemma onem_nonneg_proof (p : {nonneg R}) : p%:num <= 1 -> 0 <= `1-(p%:num). +Proof. by rewrite /onem/= subr_ge0. Qed. + +Definition onem_nonneg (p : {nonneg R}) (p1 : p%:num <= 1) := + NngNum (onem_nonneg_proof p1). + End onem_signed.