Tail expectation formula for L1 random variable

CHANGELOG_UNRELEASED.md

@@ -47,7 +47,7 @@
 
 - in `random_variable.v`
   + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`,
-    `le0_expectation_cdf`
+    `le0_expectation_cdf`, `expectation_cdf_ccdf`
 
 - in `lebesgue_integral_nonneg.v`:
   + lemma `integral_setU`
@@ -84,6 +84,23 @@
 - in `separation_axioms.v`:
   + lemmas `limit_point_closed`
 
+- in `functions.v`:
+  + lemma `addBrfctE`
+
+- in `numfun.v`:
+  + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-`
+  + lemmas `funrpos_ge0`, `funrneg_ge0`, `funrposN`, `funrnegN`, `ge0_funrposE`,
+    `ge0_funrnegE`, `le0_funrposE`, `le0_funrnegE`, `ge0_funrposM`, `ge0_funrnegM`,
+    `le0_funrposM`, `le0_funrnegM`, `funrposDneg`, `funrposBneg`,
+    `funrD_posD`, `funrpos_le`, `funrneg_le`
+  + lemmas `funerpos`, `funerneg`
+
+- in `lebesgue_integrable.v`:
+  + lemmas `integrable_funrpos`, `integrable_funrneg`
+
+- in `measurable_realfun.v`:
+  + lemmas `measurable_funrpos`, `measurable_funrneg`
+
 ### Changed
 
 - in `constructive_ereal.v`: fixed the infamous `%E` scope bug.

classical/functions.v

@@ -2719,6 +2719,10 @@ Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed.
 Lemma opprfctE (T : Type) (K : zmodType) (f : T -> K) : - f = (fun x => - f x).
 Proof. by []. Qed.
 
+Lemma addBrfctE (U : Type) (K : zmodType) :
+  @interchange (U -> K) (fun a b => a - b) (fun a b => a + b).
+Proof. by move=> a b c d; apply/funext => x; rewrite addrACA -opprD. Qed.
+
 Lemma mulrfctE (T : Type) (K : pzRingType) (f g : T -> K) :
   f * g = (fun x => f x * g x).
 Proof. by []. Qed.

theories/lebesgue_integral_theory/lebesgue_integrable.v

@@ -372,6 +372,14 @@ have [M [_ mrt]] := bdA; apply: le_lt_trans.
 by rewrite lte_mul_pinfty.
 Qed.
 
+Lemma integrable_funrpos A f : measurable A ->
+  mu.-integrable A (EFin \o f) -> mu.-integrable A (EFin \o f^\+).
+Proof. by move/integrable_funepos => /[apply]; rewrite funerpos. Qed.
+
+Lemma integrable_funrneg A f : measurable A ->
+  mu.-integrable A (EFin \o f) -> mu.-integrable A (EFin \o f^\-).
+Proof. by move/integrable_funeneg => /[apply]; rewrite funerneg. Qed.
+
 End Rintegrable.
 
 Lemma integrable_indic_itv {R : realType} (a b : R) (b0 b1 : bool) :

theories/measurable_realfun.v

@@ -907,6 +907,12 @@ by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //;
   [exact: measurable_fun_ltr|exact: measurable_funS mg|exact: measurable_funS mf].
 Qed.
 
+Lemma measurable_funrpos D f : measurable_fun D f -> measurable_fun D f^\+.
+Proof. by move=> mf; exact: measurable_maxr. Qed.
+
+Lemma measurable_funrneg D f : measurable_fun D f -> measurable_fun D f^\-.
+Proof. by move=> mf; apply: measurable_maxr => //; exact: measurableT_comp. Qed.
+
 Lemma measurable_minr D f g :
   measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \min g).
 Proof.
@@ -999,6 +1005,19 @@ Qed.
 
 End measurable_fun_realType.
 
+Section funrposneg_measurable.
+Context {d} {aT : measurableType d} {rT : realType}.
+
+HB.instance Definition _ (f : {mfun aT >-> rT}) :=
+  @isMeasurableFun.Build d _ _ _ f^\+
+    (measurable_funrpos (@measurable_funPT _ _ _ _ f)).
+
+HB.instance Definition _ (f : {mfun aT >-> rT}) :=
+  @isMeasurableFun.Build d _ _ _ f^\-
+    (measurable_funrneg (@measurable_funPT _ _ _ _ f)).
+
+End funrposneg_measurable.
+
 Section mono_measurable.
 Context {R : realType}.
 

theories/numfun.v

@@ -27,12 +27,15 @@ From mathcomp Require Import topology normedtype sequences.
 (* bounded_variation a b f == all variations of f are bounded                 *)
 (*         {nnfun T >-> R} == type of non-negative functions                  *)
 (*                   f ^\+ == the function formed by the non-negative outputs *)
-(*                            of f (from a type to the type of extended real  *)
-(*                            numbers) and 0 otherwise                        *)
-(*                            rendered as f ⁺ with company-coq (U+207A)       *)
+(*                            of f and 0 otherwise                            *)
+(*                            The codomain of f is the real numbers in scope  *)
+(*                            ring_scope and the extended real numbers in     *)
+(*                            scope ereal_scope.                              *)
+(*                            Rendered as f ⁺ with company-coq (U+207A).      *)
 (*                   f ^\- == the function formed by the non-positive outputs *)
 (*                            of f and 0 o.w.                                 *)
-(*                            rendered as f ⁻ with company-coq (U+207B)       *)
+(*                            Similar to ^\+.                                 *)
+(*                            Rendered as f ⁻ with company-coq (U+207B).      *)
 (*                   \1_ A == indicator function 1_A                          *)
 (* ```                                                                        *)
 (*                                                                            *)
@@ -682,6 +685,133 @@ Proof. by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?mule0. Qed.
 
 End erestrict_lemmas.
 
+Section funrposneg.
+Local Open Scope ring_scope.
+
+Definition funrpos T (R : realDomainType) (f : T -> R) :=
+  fun x => Num.max (f x) 0.
+Definition funrneg T (R : realDomainType) (f : T -> R) :=
+  fun x => Num.max (- f x) 0.
+
+End funrposneg.
+
+Notation "f ^\+" := (funrpos f) : ring_scope.
+Notation "f ^\-" := (funrneg f) : ring_scope.
+
+Section funrposneg_lemmas.
+Local Open Scope ring_scope.
+Variables (T : Type) (R : realDomainType) (D : set T).
+Implicit Types (f g : T -> R) (r : R).
+
+Lemma funrpos_ge0 f x : 0 <= f^\+ x.
+Proof. by rewrite /funrpos /= le_max lexx orbT. Qed.
+
+Lemma funrneg_ge0 f x : 0 <= f^\- x.
+Proof. by rewrite /funrneg le_max lexx orbT. Qed.
+
+Lemma funrposN f : (\- f)^\+ = f^\-. Proof. exact/funext. Qed.
+
+Lemma funrnegN f : (\- f)^\- = f^\+.
+Proof. by apply/funext => x; rewrite /funrneg opprK. Qed.
+
+(* TODO: the following lemmas require a pointed type and realDomainType does
+not seem to be at this point
+
+Lemma funrpos_restrict f : (f \_ D)^\+ = (f^\+) \_ D.
+Proof.
+by apply/funext => x; rewrite /patch/_^\+; case: ifP; rewrite //= maxxx.
+Qed.
+
+Lemma funrneg_restrict f : (f \_ D)^\- = (f^\-) \_ D.
+Proof.
+by apply/funext => x; rewrite /patch/_^\-; case: ifP; rewrite //= oppr0 maxxx.
+Qed.*)
+
+Lemma ge0_funrposE f : (forall x, D x -> 0 <= f x) -> {in D, f^\+ =1 f}.
+Proof. by move=> f0 x; rewrite inE => Dx; apply/max_idPl/f0. Qed.
+
+Lemma ge0_funrnegE f : (forall x, D x -> 0 <= f x) -> {in D, f^\- =1 cst 0}.
+Proof.
+by move=> f0 x; rewrite inE => Dx; apply/max_idPr; rewrite lerNl oppr0 f0.
+Qed.
+
+Lemma le0_funrposE f : (forall x, D x -> f x <= 0) -> {in D, f^\+ =1 cst 0}.
+Proof. by move=> f0 x; rewrite inE => Dx; exact/max_idPr/f0. Qed.
+
+Lemma le0_funrnegE f : (forall x, D x -> f x <= 0) -> {in D, f^\- =1 \- f}.
+Proof.
+by move=> f0 x; rewrite inE => Dx; apply/max_idPl; rewrite lerNr oppr0 f0.
+Qed.
+
+Lemma ge0_funrposM r f : (0 <= r)%R ->
+  (fun x => r * f x)^\+ = (fun x => r * (f^\+ x)).
+Proof. by move=> ?; rewrite funeqE => x; rewrite /funrpos maxr_pMr// mulr0. Qed.
+
+Lemma ge0_funrnegM r f : (0 <= r)%R ->
+  (fun x => r * f x)^\- = (fun x => r * (f^\- x)).
+Proof.
+by move=> r0; rewrite funeqE => x; rewrite /funrneg -mulrN maxr_pMr// mulr0.
+Qed.
+
+Lemma le0_funrposM r f : (r <= 0)%R ->
+  (fun x => r * f x)^\+ = (fun x => - r * (f^\- x)).
+Proof.
+move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr.
+by rewrite funrposN ge0_funrnegM ?oppr_ge0.
+Qed.
+
+Lemma le0_funrnegM r f : (r <= 0)%R ->
+  (fun x => r * f x)^\- = (fun x => - r * (f^\+ x)).
+Proof.
+move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr.
+by rewrite funrnegN ge0_funrposM ?oppr_ge0.
+Qed.
+
+Lemma funrposDneg f : f^\+ + f^\- = Num.norm \o f.
+Proof.
+rewrite funeqE => x /=; rewrite !fctE/=; have [fx0|/ltW fx0] := leP (f x) 0.
+- rewrite ler0_norm// /funrpos /funrneg.
+  move/max_idPr : (fx0) => ->; rewrite add0r.
+  by move: fx0; rewrite -{1}oppr0 lerNr => /max_idPl ->.
+- rewrite ger0_norm// /funrpos /funrneg; move/max_idPl : (fx0) => ->.
+  by move: fx0; rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0.
+Qed.
+
+Lemma funrposBneg f : f^\+ - f^\- = f.
+Proof.
+apply/funext => x.
+rewrite /funrpos /funrneg/= !fctE; have [|/ltW] := leP (f x) 0.
+  by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r.
+by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0.
+Qed.
+
+Lemma funrDB f g : (f^\+ + g^\+) - (f^\- + g^\-) = f + g.
+Proof. by rewrite addBrfctE !funrposBneg. Qed.
+
+Lemma funrpos_le f g :
+  {in D, forall x, f x <= g x} -> {in D, forall x, f^\+ x <= g^\+ x}.
+Proof.
+move=> fg x Dx; rewrite /funrpos /Num.max; case: ifPn => fx; case: ifPn => gx//.
+- by rewrite leNgt.
+- by move: fx; rewrite -leNgt => /(lt_le_trans gx); rewrite ltNge fg.
+- exact: fg.
+Qed.
+
+Lemma funrneg_le f g :
+  {in D, forall x, f x <= g x} -> {in D, forall x, g^\- x <= f^\- x}.
+Proof.
+move=> fg x Dx; rewrite /funrneg /Num.max; case: ifPn => gx; case: ifPn => fx//.
+- by rewrite leNgt.
+- by move: gx; rewrite -leNgt => /(lt_le_trans fx); rewrite ltrN2 ltNge fg.
+- by rewrite lerN2; exact: fg.
+Qed.
+
+End funrposneg_lemmas.
+#[global]
+Hint Extern 0 (is_true (0%R <= _ ^\+ _)%R) => solve [apply: funrpos_ge0] : core.
+#[global]
+Hint Extern 0 (is_true (0%R <= _ ^\- _)%R) => solve [apply: funrneg_ge0] : core.
+
 HB.lock
 Definition funepos T (R : realDomainType) (f : T -> \bar R) :=
   fun x => maxe (f x) 0.
@@ -847,6 +977,17 @@ Hint Extern 0 (is_true (0%R <= _ ^\+ _)%E) => solve [apply: funepos_ge0] : core.
 #[global]
 Hint Extern 0 (is_true (0%R <= _ ^\- _)%E) => solve [apply: funeneg_ge0] : core.
 
+Section funrpos_funepos_lemmas.
+Context {T : Type} {R : realDomainType}.
+
+Lemma funerpos (f : T -> R) : (EFin \o f)^\+%E = (EFin \o f^\+).
+Proof. by apply/funext => x; rewrite funeposE /funrpos/= EFin_max. Qed.
+
+Lemma funerneg (f : T -> R) : (EFin \o f)^\-%E = (EFin \o f^\-).
+Proof. by apply/funext => x; rewrite funenegE /funrneg/= EFin_max. Qed.
+
+End funrpos_funepos_lemmas.
+
 Definition indic {T} {R : pzRingType} (A : set T) (x : T) : R := (x \in A)%:R.
 Reserved Notation "'\1_' A" (at level 8, A at level 2, format "'\1_' A") .
 Notation "'\1_' A" := (indic A) : ring_scope.

theories/probability_theory/random_variable.v

@@ -688,6 +688,39 @@ rewrite setDitv1r; congr -%E; apply: eq_integral => r _.
 by rewrite (@comp_preimage _ _ _ _ _ -%R)/= opp_preimage_itvbndy/= opprK.
 Qed.
 
+Let preimage_funrpos (f : T -> R) r : (0 <= r)%R ->
+  (f^\+)%R @^-1` `]r, +oo[ = f @^-1` `]r, +oo[.
+Proof.
+move=> r0; apply: eq_set => a/=.
+by rewrite !in_itv/= !andbT lt_max (ltNge r 0%R) r0 orbF.
+Qed.
+
+Let preimage_funrneg (f : T -> R) r : (r < 0)%R ->
+  (- f^\-)%R @^-1` `]-oo, r] = (f)%R @^-1` `]-oo, r].
+Proof.
+move=> r0; apply: eq_set => a/=.
+by rewrite !in_itv/= lerNl le_max lerN2 (leNgt _ 0%R) oppr_gt0 r0 orbF.
+Qed.
+
+Lemma expectation_cdf_ccdf (X : {RV P >-> R}) : Lfun P 1 X ->
+  'E_P[X] = \int[mu]_(r in `[0%R, +oo[) ccdf X r
+            - \int[mu]_(r in `]-oo, 0%R[) cdf X r.
+Proof.
+move=> L1X.
+rewrite -[in LHS](funrposBneg X) expectationD; last 2 first.
+- exact/Lfun1_integrable/integrable_funrpos/Lfun1_integrable.
+- rewrite rpredN/=.
+  exact/Lfun1_integrable/integrable_funrneg/Lfun1_integrable.
+rewrite (_ : 'E_P[X^\+] = \int[mu]_(r in `[0%R, +oo[) ccdf X r); last first.
+  rewrite ge0_expectation_ccdf/= => [|?]; last by rewrite funrpos_ge0.
+  apply: eq_integral => r; rewrite inE/= in_itv/= andbT => r0; congr (P _).
+  by rewrite preimage_funrpos.
+rewrite (_ : 'E_P[- X^\-] = - \int[mu]_(r in `]-oo, 0%R[) cdf X r)//.
+rewrite le0_expectation_cdf/= => [|x]; last by rewrite oppr_le0 funrneg_ge0.
+congr -%E; apply: eq_integral => r; rewrite inE/= in_itv/= => r0; congr (P _).
+by rewrite preimage_funrneg.
+Qed.
+
 End tail_expectation_formula.
 
 HB.lock Definition covariance {d} {T : measurableType d} {R : realType}