Add lemma le0_expectation_cdf

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`
+
+
+
+

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).

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?*)

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 <oo) P (X @^-1` [set q k])); last first.
+  rewrite measure_bigcup//; first by apply: eq_eseriesl =>// 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 <oo | k \in S) (pmf X (h k) * \1_[set h k] r)%:E.
+apply/measurable_EFinP; apply: (eq_measurable_fun sfun) => [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 <oo) P (X @^-1` [set q k])); last first.
-  rewrite measure_bigcup//; first by apply: eq_eseriesl =>// 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 <oo | k \in S) (pmf X (h k) * \1_[set h k] r)%:E.
-apply/measurable_EFinP; apply: (eq_measurable_fun sfun) => [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).