Skip to content

Tail expectation formula for a non-negative random variable #1731

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Oct 21, 2025
Merged

Tail expectation formula for a non-negative random variable #1731

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d169e5b
tail expectation formula for non-negative RV
Yosuke-Ito-345 Oct 5, 2025
96ce77d
rm redundancies
affeldt-aist Oct 20, 2025
dfc8aea
modify name
Yosuke-Ito-345 Oct 21, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@

- in `probability.v`:
+ definition `ccdf`
+ lemmas `cdf_fin_num`, `lebesgue_stieltjes_cdf_id`, `cdf_ccdf_1`, `ccdf_fin_num`, `ccdf_nonincreasing`, `cvg_ccdfy0`, `cvg_ccdfNy1`, `ccdf_right_continuous`
+ lemmas `lebesgue_stieltjes_cdf_id`, `cdf_ccdf_1`, `ccdf_nonincreasing`, `cvg_ccdfy0`, `cvg_ccdfNy1`, `ccdf_right_continuous`, `expectation_nonneg_tail`
+ corollaries `ccdf_cdf_1`, `ccdf_1_cdf`, `cdf_1_ccdf`

- in `num_normedtype.v`:
Expand Down
91 changes: 77 additions & 14 deletions theories/probability.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,11 +173,6 @@ Lemma cdf_ge0 r : 0 <= cdf X r. Proof. by []. Qed.

Lemma cdf_le1 r : cdf X r <= 1. Proof. exact: probability_le1. Qed.

Lemma cdf_fin_num r : cdf X r \is a fin_num.
Proof.
by rewrite ge0_fin_numE ?cdf_ge0//; exact/(le_lt_trans (cdf_le1 r))/ltry.
Qed.

Lemma cdf_nondecreasing : nondecreasing_fun (cdf X).
Proof. by move=> r s rs; rewrite le_measure ?inE//; exact: subitvPr. Qed.

Expand Down Expand Up @@ -305,13 +300,13 @@ Let fcdf r := fine (cdf (idTR : {RV P >-> R}) r).

Let fcdf_nd : nondecreasing fcdf.
Proof.
by move=> *; apply: fine_le; [exact: cdf_fin_num.. | exact: cdf_nondecreasing].
by move=> *; rewrite fine_le ?fin_num_measure// cdf_nondecreasing.
Qed.

Let fcdf_rc : right_continuous fcdf.
Proof.
move=> a; apply: fine_cvg.
by rewrite fineK; [exact: cdf_right_continuous | exact: cdf_fin_num].
by rewrite fineK ?fin_num_measure//; exact: cdf_right_continuous.
Qed.

#[local] HB.instance Definition _ :=
Expand All @@ -335,7 +330,7 @@ rewrite /lebesgue_stieltjes_measure /measure_extension/=.
rewrite measurable_mu_extE/=; last exact: is_ocitv.
have [ab | ba] := leP a b; last first.
by rewrite set_itv_ge ?wlength0 ?measure0// bnd_simp -leNgt ltW.
rewrite wlength_itv_bnd// EFinB !fineK ?cdf_fin_num//.
rewrite wlength_itv_bnd// EFinB !fineK ?fin_num_measure//.
rewrite /cdf /distribution /pushforward !preimage_id.
have : `]a, b]%classic = `]-oo, b] `\` `]-oo, a] => [|->].
by rewrite -[RHS]setCK setCD setCitvl setUC -[LHS]setCK setCitv.
Expand All @@ -355,21 +350,18 @@ Local Open Scope ereal_scope.

Lemma cdf_ccdf_1 r : cdf X r + ccdf X r = 1.
Proof.
rewrite /cdf/ccdf -measureU//= -eq_opE; last exact: disjoint_rays.
rewrite /cdf /ccdf -measureU//= -eq_opE; last exact: disjoint_rays.
by rewrite itv_setU_setT probability_setT.
Qed.

Corollary ccdf_cdf_1 r : ccdf X r + cdf X r = 1.
Proof. by rewrite -(cdf_ccdf_1 r) addeC. Qed.

Corollary ccdf_1_cdf r : ccdf X r = 1 - cdf X r.
Proof. by rewrite -(ccdf_cdf_1 r) addeK ?cdf_fin_num. Qed.

Lemma ccdf_fin_num r : ccdf X r \is a fin_num.
Proof. by rewrite ccdf_1_cdf fin_numB cdf_fin_num -fine1. Qed.
Proof. by rewrite -(ccdf_cdf_1 r) addeK ?fin_num_measure. Qed.

Corollary cdf_1_ccdf r : cdf X r = 1 - ccdf X r.
Proof. by rewrite -(cdf_ccdf_1 r) addeK ?ccdf_fin_num. Qed.
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.
Expand Down Expand Up @@ -483,6 +475,77 @@ End expectation_lemmas.
#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to `expectationZl`")]
Notation expectationM := expectationZl (only parsing).

Section tail_expectation_formula.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (P : probability T R).

Let mu : {measure set _ -> \bar R} := @lebesgue_measure R.

Lemma expectation_nonneg_tail (X : {RV P >-> R}) : (forall x, 0 <= X x)%R ->
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe it is better if this lemma bears the identifier ccdf with a name such as ge0_expectation_ccdf? (The prefix ge0_ is to mark that there is a non-negativity hypothesis.)

'E_P[X] = \int[mu]_(r in `[0%R, +oo[) ccdf X r.
Proof.
pose GR := measurableTypeR R.
pose distrX := distribution P X.
pose D : set R := `[0%R, +oo[%classic.
move=> X_ge0.
transitivity (\int[P]_x ((EFin \_ D) \o X) x).
rewrite expectation_def; apply: eq_integral => x _ /=.
by rewrite /D patchE ifT// set_itvE inE /=.
transitivity (\int[distrX]_r (EFin \_ D) r).
rewrite ge0_integral_distribution// -?measurable_restrictT /D// => r.
by apply: erestrict_ge0 => s /=; rewrite in_itv/= andbT lee_fin.
transitivity (\int[distrX]_r (\int[mu]_(s in D) (\1_`]-oo, r[ s)%:E)).
apply: eq_integral => r _.
rewrite integral_indic /D//= setIC -(set_itv_splitI `[0%R, r[).
rewrite lebesgue_measure_itv/= lte_fin patchE.
have [r_pos | r_neg | <-] := ltgtP.
- by rewrite mem_set ?EFinN ?sube0//= in_itv/= ltW.
- by rewrite memNset//= in_itv/= leNgt r_neg.
- by rewrite mem_set//= in_itv/= lexx.
transitivity (\int[distrX]_r (\int[mu]_s (\1_`[0, r[ s)%:E)).
apply: eq_integral => r _; rewrite /D integral_mkcond.
apply: eq_integral => /= s _.
have [s_ge0 | s_lt0] := leP 0%R s.
- have [s_ltr | s_ger] := ltP s r.
+ rewrite indicE mem_set/=; last by rewrite in_itv/= s_ge0 s_ltr.
by rewrite patchE/= ifT ?indicE mem_set//= in_itv/= andbT.
+ rewrite indicE memNset/=; last by rewrite in_itv/= s_ge0 ltNge s_ger.
rewrite patchE ifT//; last by rewrite mem_set//= in_itv/= andbT.
by rewrite indicE memNset//= in_itv/= ltNge s_ger.
- rewrite indicE memNset/=; last by rewrite in_itv/= leNgt s_lt0.
by rewrite patchE/= ifF// memNset//= in_itv/= andbT leNgt s_lt0.
transitivity (\int[mu]_s (\int[distrX]_r (\1_`[0, r[ s)%:E)).
rewrite (fubini_tonelli (fun p : R * GR => (\1_`[0, p.1[ p.2)%:E))//=.
apply/measurable_EFinP/measurable_indic => /=.
pose fsnd (p : R * GR) := (0 <= p.2)%R.
pose f21 (p : R * GR) := (p.2 < p.1)%R.
rewrite [X in measurable X](_ : _ =
fsnd @^-1` [set true] `&` f21 @^-1` [set true]); last first.
by apply/seteqP; split => p; rewrite in_itv/= => /andP.
apply: measurableI.
- have : measurable_fun setT fsnd by exact: measurable_fun_ler.
by move=> /(_ measurableT [set true]); rewrite setTI; exact.
- have : measurable_fun setT f21 by exact: measurable_fun_ltr.
by move=> /(_ measurableT [set true]); rewrite setTI; exact.
transitivity (\int[mu]_(s in D) (\int[distrX]_r (\1_`[0, r[ s)%:E)).
rewrite [in RHS]integral_mkcond/=.
apply: eq_integral => s _; rewrite patchE /D.
have [s0|s0] := leP 0%R s; first by rewrite mem_set//= in_itv/= s0.
rewrite memNset//= ?in_itv/= ?leNgt ?s0//.
by apply: integral0_eq => r _; rewrite indicE/= memNset//= in_itv/= leNgt s0.
apply: eq_integral => s; rewrite /D inE/= in_itv/= andbT => s_ge0.
rewrite integral_indic//=.
rewrite /ccdf setIT set_itvoy; congr distribution.
by apply/funext => r/=; rewrite in_itv/= s_ge0.
pose fgts (r : R) := (s < r)%R.
have : measurable_fun setT fgts by exact: measurable_fun_ltr.
rewrite [X in measurable X](_ : _ = fgts @^-1` [set true]).
by move=> /(_ measurableT [set true]); rewrite setTI; exact.
by apply: eq_set => r; rewrite in_itv/= s_ge0.
Qed.

End tail_expectation_formula.

HB.lock Definition covariance {d} {T : measurableType d} {R : realType}
(P : probability T R) (X Y : T -> R) :=
'E_P[(X \- cst (fine 'E_P[X])) * (Y \- cst (fine 'E_P[Y]))]%E.
Expand Down
Loading