diff --git a/CHANGELOG_UNRELEASED_new.md b/CHANGELOG_UNRELEASED_new.md new file mode 100644 index 000000000..7b2c00c7a --- /dev/null +++ b/CHANGELOG_UNRELEASED_new.md @@ -0,0 +1,19 @@ +# Changelog (unreleased) + +## [Unreleased] + +### Added + +- in lebesgue_integral_nonneg.v + + lemmas `lebesgue_measure_oppr`, `ge0_integral_oppr` + +- in measurable_realfun.v + + lemma `min_mfun_subproof` + + definition `min_mfun` + +- in random_variable.v + + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`, `ge0_expectation_prob_ge`, `le0_expectation_cdf` + + + + diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index a6ad41e9f..a84ca5fc4 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -568,6 +568,38 @@ Qed. End ge0_transfer. +Section change_of_variable. +Open Scope ereal_scope. +Context {R : realType}. + +Let mu : {measure set _ -> \bar R} := @lebesgue_measure R. + +Lemma lebesgue_measureN A (mA : measurable A) : + pushforward(T2 := measurableTypeR R) mu -%R A = mu A. +Proof. +apply /esym/lebesgue_stieltjes_measure_unique => //= _ [[a b]] _ <-. +rewrite /lebesgue_stieltjes_measure/measure_extension. +rewrite measurable_mu_extE /pushforward/preimage/=; last exact: is_ocitv. +have ->: [set r | (-r)%R \in `]a, b]] = `[(-b)%R, (-a)%R[%classic. + by apply: eq_set => r; rewrite oppr_itvoc. +rewrite lebesgue_measure_itv/= lte_fin ltrN2. +have [ab | ba] := (ltP a b). +- by rewrite wlength_itv_bnd ?ltW// opprK EFinD addeC. +- by rewrite set_itv_ge ?wlength0// bnd_simp -leNgt. +Qed. + +Lemma ge0_integral_pushforwardN (f : R -> \bar R) + (mf : measurable_fun setT f) (ge0 : forall r, 0 <= f r) : + \int[mu]_(r in `[0%R, +oo[) f r = \int[mu]_(r in `]-oo, 0%R]) f (- r)%R. +Proof. +rewrite (eq_measure_integral (pushforward(T2 := measurableTypeR R) mu -%R)) + => [| A mA /=]; rewrite ?lebesgue_measureN//. +rewrite ge0_integral_pushforward //; last exact: measurable_funS mf. +by congr integral; apply: eq_set => r/=; rewrite !in_itv/= oppr_ge0 andbT. +Qed. + +End change_of_variable. + Section integral_dirac. Local Open Scope ereal_scope. Context d (T : measurableType d) (a : T) (R : realType). diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 7f0d773d3..ede44a2ca 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -46,6 +46,7 @@ From mathcomp Require Export lebesgue_stieltjes_measure. (* indic_mfun mD := mindic mD *) (* scale_mfun k f := k \o* f *) (* max_mfun f g := f \max g *) +(* min_mfun f g := f \min g *) (* ``` *) (******************************************************************************) @@ -1182,6 +1183,13 @@ HB.instance Definition _ f g := max_mfun_subproof f g. Definition max_mfun f g : {mfun aT >-> _} := f \max g. +Lemma min_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \min g). +Proof. by split; apply: measurable_minr. Qed. + +HB.instance Definition _ f g := min_mfun_subproof f g. + +Definition min_mfun f g : {mfun aT >-> _} := f \min g. + End ring. Arguments indic_mfun {d aT rT} _. (* TODO: move earlier?*) diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index 992f0e127..a6cb2ad54 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -136,6 +136,107 @@ Proof. by move=> mf intf; rewrite integral_pushforward. Qed. End transfer_probability. +Section pmf_definition. +Context {d} {T : measurableType d} {R : realType}. +Variables (P : probability T R). + +Definition pmf (X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])). + +Lemma pmf_ge0 (X : {RV P >-> R}) (r : R) : 0 <= pmf X r. +Proof. by rewrite fine_ge0. Qed. + +End pmf_definition. + +Section pmf_measurable. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) + (P : probability T R) (X : {RV P >-> R}). + +Lemma pmf_gt0_countable : countable [set r | 0 < pmf X r]%R. +Proof. +rewrite [X in countable X](_ : _ = + \bigcup_n [set r | n.+1%:R^-1 < pmf X r]%R); last first. + by apply/seteqP; split=> [r/= /ltr_add_invr[k /[!add0r] kXr]|r/= [k _]]; + [exists k|exact: lt_trans]. +apply: bigcup_countable => // n _; apply: finite_set_countable. +apply: contrapT => /infiniteP/pcard_leP/injfunPex[/= q q_fun q_inj]. +have /(probability_le1 P) : measurable (\bigcup_k X @^-1` [set q k]). + by apply: bigcup_measurable => k _; exact: measurable_funPTI. +rewrite leNgt => /negP; apply. +rewrite [ltRHS](_ : _ = \sum_(0 <= k // i; rewrite in_setT. + rewrite (trivIset_comp (fun r => X@^-1` [set r]))//. + exact: trivIset_preimage1. +apply: (lt_le_trans _ (nneseries_lim_ge n.+1 _)) => //. +rewrite -EFin_sum_fine//; last by move=> ? _; rewrite fin_num_measure. +under eq_bigr do rewrite -/(pmf X (q _)). +rewrite lte_fin (_ : 1%R = (\sum_(0 <= k < n.+1) n.+1%:R^-1:R)%R); last first. + by rewrite sumr_const_nat subn0 -[RHS]mulr_natr mulVf. +by apply: ltr_sum => // k _; exact: q_fun. +Qed. + +Lemma pmf_measurable : measurable_fun [set: R] (pmf X). +Proof. +have /countable_bijP[S] := pmf_gt0_countable. +rewrite card_eq_sym => /pcard_eqP/bijPex[/= h h_bij]. +have pmf1_ge0 k s : 0 <= (pmf X (h k) * \1_[set h k] s)%:E. + by rewrite EFinM mule_ge0// lee_fin pmf_ge0. +pose sfun r := \sum_(0 <= k [r _|]; last first. + by apply: ge0_emeasurable_sum => // *; exact/measurable_EFinP/measurable_funM. +have [rS|nrS] := boolP (r \in [set h k | k in S]). +- pose kr := pinv S h r. + have neqh k : k \in S /\ k != kr -> r != h k. + move=> [Sk]; apply: contra_neq. + by rewrite /kr => ->; rewrite pinvKV//; exact: (set_bij_inj h_bij). + rewrite /sfun (@nneseriesD1 _ _ kr)//; last by rewrite inE; exact/invS/set_mem. + by rewrite eseries0 => [| k k_ge0 /andP/neqh]; rewrite indicE in_set1_eq; + [rewrite pinvK// eqxx mulr1 addr0|move/negPf => ->; rewrite mulr0]. +- rewrite /sfun eseries0 => [|k k_ge0 Sk]/=. + apply: le_anti; rewrite !lee_fin pmf_ge0/= leNgt; apply: contraNN nrS. + by rewrite (surj_image_eq _ (set_bij_surj h_bij)) ?inE//; exact:set_bij_sub. + rewrite indicE in_set1_eq (_ : (r == h k) = false) ?mulr0//. + by apply: contraNF nrS => /eqP ->; exact/image_f. +Qed. + +End pmf_measurable. + +Section lebesgue_integral_pmf. +Context d (T : measurableType d) (R : realType) + (P : probability T R) (X : {RV P >-> R}). +Local Open Scope ereal_scope. + +Lemma lebesgue_integral_pmf : + \int[lebesgue_measure]_r (pmf X r)%:E = 0. +Proof. +pose mu := @lebesgue_measure R. +pose pmfP := [set r | (0 < pmf X r)%R]. +pose pmf0 := [set r | (0 = pmf X r)%R]. +have Upmf : pmfP `|` pmf0 = setT. + rewrite -subTset => r /= _. + by case: (ltrgt0P (pmf X r)); [left | rewrite ltNge fine_ge0 | right]. +have Ipmf : [disjoint pmfP & pmf0]. + rewrite disj_set2E; apply/eqP. + by rewrite -subset0 setIC /pmfP/pmf0 => r /= [] ->; rewrite ltxx. +have pmf0NP : pmf0 = ~`pmfP. + rewrite /pmf0 /pmfP seteqP; split=> r /= => [-> | /negP]; rewrite ?ltxx//. + by rewrite -real_leNgt//= => pmfN; apply: le_anti; rewrite pmfN fine_ge0. +have cpmfP : countable pmfP by exact: pmf_gt0_countable. +have mpmfP : measurable pmfP by exact: countable_measurable. +have mupmfP : mu pmfP = 0 by exact: countable_lebesgue_measure0. +have mpmf : measurable_fun setT (fun r => (pmf X r)%:E). + by apply/measurable_EFinP; exact: pmf_measurable. +transitivity + (\int[mu]_(r in pmfP) (pmf X r)%:E + \int[mu]_(r in pmf0) (pmf X r)%:E). + by rewrite -ge0_integral_setU ?Upmf// ?pmf0NP => [| r _]; + [exact: measurableC | exact: fine_ge0]. +rewrite (_ : \int[mu]_(r in pmf0) (pmf X r)%:E = 0) ?addr0; + last by apply: integral0_eq => r <-. +by apply: null_set_integral; [| exact: (measurable_funS(E:=setT)) |]. +Qed. + +End lebesgue_integral_pmf. + Definition cdf d (T : measurableType d) (R : realType) (P : probability T R) (X : {RV P >-> R}) (r : R) := distribution P X `]-oo, r]. @@ -151,6 +252,15 @@ Lemma cdf_le1 r : cdf X r <= 1. Proof. exact: probability_le1. Qed. Lemma cdf_nondecreasing : nondecreasing_fun (cdf X). Proof. by move=> r s rs; rewrite le_measure ?inE//; exact: subitvPr. Qed. +Lemma cdf_measurable : measurable_fun setT (cdf X). +Proof. +suff : measurable_fun setT (fine \o (cdf X)) => [/measurable_EFinP |]. + apply: eq_measurable_fun => r _. + by rewrite /comp fineK; last exact: fin_num_measure. +apply: nondecreasing_measurable => // r s rs. +by apply: fine_le; [rewrite fin_num_measure .. | exact: cdf_nondecreasing]. +Qed. + Lemma cvg_cdfy1 : cdf X @ +oo%R --> 1. Proof. pose s : \bar R := ereal_sup (range (cdf X)). @@ -341,6 +451,13 @@ Proof. by rewrite -(cdf_ccdf_1 r) addeK ?fin_num_measure. Qed. Lemma ccdf_nonincreasing : nonincreasing_fun (ccdf X). Proof. by move=> r s rs; rewrite le_measure ?inE//; exact: subitvPl. Qed. +Lemma ccdf_measurable : measurable_fun setT (ccdf X). +Proof. +apply: (eq_measurable_fun (fun r => 1 - cdf X r)) => [r _|]. + by rewrite ccdf_1_cdf. +by apply: emeasurable_funB; last exact: cdf_measurable. +Qed. + Lemma cvg_ccdfy0 : ccdf X @ +oo%R --> 0. Proof. have : 1 - cdf X r @[r --> +oo%R] --> 1 - 1. @@ -519,6 +636,72 @@ rewrite [X in measurable X](_ : _ = fgts @^-1` [set true]). by apply: eq_set => r; rewrite in_itv/= s_ge0. Qed. +Let ge0_expectation_prob_ge (X : {RV P >-> R}) : (forall x, 0 <= X x)%R -> + 'E_P[X] = \int[mu]_(r in `[0%R, +oo[) P [set x | (r <= X x)%R]. +Proof. +have gtpre r : [set x | (r < X x)%R] = X @^-1` `]r, +oo[. + by apply: eq_set => x/=; rewrite in_itv andbT. +have mPeqr : measurable_fun setT (fun r => P [set x | X x = r]). + apply: (eq_measurable_fun (EFin \o (pmf X))) => [r |]. + by rewrite /comp fineK ?fin_num_measure. + by apply/measurable_EFinP; exact: pmf_measurable. +have mPgtr : measurable_fun setT (fun r:R => P [set x | (r < X x)%R]). + apply: (eq_measurable_fun (ccdf X)) => [r _|]; rewrite ?gtpre//. + exact: ccdf_measurable. +move=> X_ge0; rewrite ge0_expectation_ccdf//. +transitivity + (\int[mu]_(r in `[0%R, +oo[) (P [set x | X x = r] + P [set x | (r < X x)%R])). + rewrite ge0_integralD//=; [| exact: measurable_funTS ..]. + rewrite (_ : \int[mu]_(r in `[0%R, +oo[) P [set x | X x = r] = 0). + by rewrite add0e; apply: eq_integral => r; rewrite gtpre. + rewrite -(lebesgue_integral_pmf X) integral_mkcond; apply: eq_integral => r _. + rewrite patchE; case/asboolP: (r \in `[0%R, +oo[) => [r_ge0 | r_lt0]. + - by rewrite ifT ?inE// fineK ?fin_num_measure. + - rewrite ifF; [rewrite fineK ?fin_num_measure// | exact: asboolF]. + suff ->: X @^-1` [set r] = set0; first by rewrite measure0. + rewrite -nonemptyPn; apply: contra_not r_lt0. + by case=> x <-; rewrite in_itv/= andbT. +apply: eq_integral =>/= r _; rewrite -measureU. +- congr (P _); rewrite seteqP; split=> x/=; first by case=> [->//|]; exact: ltW. + by rewrite le_eqVlt; case/orP => [/eqP|]; [left | right]. +- by rewrite (_ : [set x | X x = r] = X @^-1` [set r]). +- by rewrite gtpre; exact: (measurable_funPTI X). +- by rewrite -subset0 => x []/= ->; rewrite ltxx. +Qed. + +Lemma le0_expectation_cdf (X : {RV P >-> R}) : (forall x, X x <= 0)%R -> + 'E_P[X] = - \int[mu]_(r in `]-oo, 0%R[) cdf X r. +Proof. +pose Y : {RV P >-> R} := (- X)%R. +pose fPleY r := fine (P [set x | (r <= Y x)%R]). +have mgeY r : d.-measurable [set x | (r <= Y x)%R]. + by rewrite -(setTI (mkset _)); exact: measurable_fun_le. +have mfPleY : measurable_fun setT fPleY. + apply: nonincreasing_measurable => // r s rs. + apply: fine_le; rewrite ?fin_num_measure//. + by apply: le_measure; rewrite ?inE// => x /=; exact: (le_trans rs). +move=> X_le0. +have Y_ge0 x : (0 <= Y x)%R by rewrite oppr_ge0/=. +transitivity (- 'E_P[Y]). + rewrite !expectation_def -integral_ge0N/= => [| x]. + by apply: eq_integral => x _; rewrite opprK. + by rewrite lee_tofin//; exact: Y_ge0. +transitivity (- \int[mu]_(s in `]-oo, 0%R]) P [set x | (- s <= Y x)%R]). + rewrite ge0_expectation_prob_ge ?ge0_integral_pushforwardN//. + by apply: (eq_measurable_fun (fun r:R => (fine (P [set x | (r <= Y x)%R]))%:E)) + => [r _|]; [rewrite fineK ?fin_num_measure | apply/measurable_EFinP]. +transitivity (- \int[mu]_(s in `]-oo, 0%R] `\ 0%R) P [set x | (- s <= Y x)%R]). + congr oppe. + under[LHS] eq_integral => s _ do + rewrite -(@fineK _ (P [set x | (- s <= Y x)%R])) ?fin_num_measure//. + under[RHS] eq_integral => s _ do + rewrite -(@fineK _ (P [set x | (- s <= Y x)%R])) ?fin_num_measure//. + rewrite integral_setD1_EFin//; first exact: measurableD. + by apply: measurable_funTS; exact: (measurableT_comp mfPleY). +rewrite setDitv1r; congr oppe; apply: eq_integral => r _. +by congr (P _); apply: eq_set => x; rewrite lerN2. +Qed. + End tail_expectation_formula. HB.lock Definition covariance {d} {T : measurableType d} {R : realType} @@ -1039,71 +1222,6 @@ Qed. End distribution_dRV. -Section pmf_definition. -Context {d} {T : measurableType d} {R : realType}. -Variables (P : probability T R). - -Definition pmf (X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])). - -Lemma pmf_ge0 (X : {RV P >-> R}) (r : R) : 0 <= pmf X r. -Proof. by rewrite fine_ge0. Qed. - -End pmf_definition. - -Section pmf_measurable. -Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) - (P : probability T R) (X : {RV P >-> R}). - -Lemma pmf_gt0_countable : countable [set r | 0 < pmf X r]%R. -Proof. -rewrite [X in countable X](_ : _ = - \bigcup_n [set r | n.+1%:R^-1 < pmf X r]%R); last first. - by apply/seteqP; split=> [r/= /ltr_add_invr[k /[!add0r] kXr]|r/= [k _]]; - [exists k|exact: lt_trans]. -apply: bigcup_countable => // n _; apply: finite_set_countable. -apply: contrapT => /infiniteP/pcard_leP/injfunPex[/= q q_fun q_inj]. -have /(probability_le1 P) : measurable (\bigcup_k X @^-1` [set q k]). - by apply: bigcup_measurable => k _; exact: measurable_funPTI. -rewrite leNgt => /negP; apply. -rewrite [ltRHS](_ : _ = \sum_(0 <= k // i; rewrite in_setT. - rewrite (trivIset_comp (fun r => X@^-1` [set r]))//. - exact: trivIset_preimage1. -apply: (lt_le_trans _ (nneseries_lim_ge n.+1 _)) => //. -rewrite -EFin_sum_fine//; last by move=> ? _; rewrite fin_num_measure. -under eq_bigr do rewrite -/(pmf X (q _)). -rewrite lte_fin (_ : 1%R = (\sum_(0 <= k < n.+1) n.+1%:R^-1:R)%R); last first. - by rewrite sumr_const_nat subn0 -[RHS]mulr_natr mulVf. -by apply: ltr_sum => // k _; exact: q_fun. -Qed. - -Lemma pmf_measurable : measurable_fun [set: R] (pmf X). -Proof. -have /countable_bijP[S] := pmf_gt0_countable. -rewrite card_eq_sym => /pcard_eqP/bijPex[/= h h_bij]. -have pmf1_ge0 k s : 0 <= (pmf X (h k) * \1_[set h k] s)%:E. - by rewrite EFinM mule_ge0// lee_fin pmf_ge0. -pose sfun r := \sum_(0 <= k [r _|]; last first. - by apply: ge0_emeasurable_sum => // *; exact/measurable_EFinP/measurable_funM. -have [rS|nrS] := boolP (r \in [set h k | k in S]). -- pose kr := pinv S h r. - have neqh k : k \in S /\ k != kr -> r != h k. - move=> [Sk]; apply: contra_neq. - by rewrite /kr => ->; rewrite pinvKV//; exact: (set_bij_inj h_bij). - rewrite /sfun (@nneseriesD1 _ _ kr)//; last by rewrite inE; exact/invS/set_mem. - by rewrite eseries0 => [| k k_ge0 /andP/neqh]; rewrite indicE in_set1_eq; - [rewrite pinvK// eqxx mulr1 addr0|move/negPf => ->; rewrite mulr0]. -- rewrite /sfun eseries0 => [|k k_ge0 Sk]/=. - apply: le_anti; rewrite !lee_fin pmf_ge0/= leNgt; apply: contraNN nrS. - by rewrite (surj_image_eq _ (set_bij_surj h_bij)) ?inE//; exact:set_bij_sub. - rewrite indicE in_set1_eq (_ : (r == h k) = false) ?mulr0//. - by apply: contraNF nrS => /eqP ->; exact/image_f. -Qed. - -End pmf_measurable. - Section discrete_distribution. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R).