From 6ebcb056945cb10e476e54012927825d309f1d5d Mon Sep 17 00:00:00 2001
From: Yosuke-Ito-345 <glacier345@gmail.com>
Date: Sat, 28 Feb 2026 13:55:02 +0900
Subject: [PATCH] add expectation_cdf_ccdf

---
 CHANGELOG_UNRELEASED.md                       |  2 +-
 theories/probability_theory/random_variable.v | 31 +++++++++++++++++++
 2 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 1e4237cb4..94b52fad9 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -43,7 +43,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`
diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v
index 07ad1f329..005e2ba59 100644
--- a/theories/probability_theory/random_variable.v
+++ b/theories/probability_theory/random_variable.v
@@ -687,6 +687,37 @@ rewrite setDitv1r; congr -%E; apply: eq_integral => r _.
 by rewrite (@comp_preimage _ _ _ _ _ -%R)/= opp_preimage_itvbndy/= opprK.
 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.
+pose Xp := (cst 0%R) \max X.
+pose Xm := (cst 0%R) \min X.
+have Xp_leX x : setT x -> `|(Xp x)%:E| <= `|(X x)%:E|.
+  by rewrite lee_tofin// ger0_norm ?le_max ?lexx// ge_max normr_ge0 ler_norm.
+have Xm_leX x : setT x -> `|(Xm x)%:E| <= `|(X x)%:E|.
+  rewrite /Xm lee_tofin//=.
+  by have [//=| Xle0 |] := (@real_le0P _ (X x));
+    [rewrite ler0_norm | rewrite normr0; exact: ltW].
+have XpP1 : Xp \in Lfun P 1.
+  by rewrite Lfun1_integrable; apply: (le_integrable _ _ Xp_leX);
+    [| apply/measurable_EFinP | rewrite -Lfun1_integrable].
+have XmP1: Xm \in Lfun P 1.
+  by rewrite Lfun1_integrable; apply: (le_integrable _ _ Xm_leX);
+    [| apply/measurable_EFinP | rewrite -Lfun1_integrable].
+rewrite (_ :  MeasurableFun.sort X = (Xp \+ Xm)%R) ?expectationD//;
+  last by apply: funext => x; rewrite /= addr_max_min add0r.
+rewrite (_ : 'E_P[Xp] = \int[mu]_(r in `[0%R, +oo[) ccdf X r); last first.
+  rewrite ge0_expectation_ccdf/= => [|x]; last by case: ler0P; last exact: ltW.
+  apply: eq_integral => r; rewrite inE/= in_itv/= andbT => r_ge0; congr (P _).
+  by apply: eq_set => x/=; rewrite !in_itv/= !andbT lt_max ltNge r_ge0.
+rewrite (_ : 'E_P[Xm] = - \int[mu]_(r in `]-oo, 0%R[) cdf X r)//.
+rewrite le0_expectation_cdf/= => [|x]; last by rewrite ge_min ?lexx.
+congr -%E; apply: eq_integral => r; rewrite inE/= in_itv/= => r_le0.
+by congr (P _); apply: eq_set => x/=; rewrite !in_itv/= ge_min leNgt r_le0.
+Qed.
+
 End tail_expectation_formula.
 
 HB.lock Definition covariance {d} {T : measurableType d} {R : realType}