diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 318217cd50..05d8a5fe35 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -21,6 +21,32 @@
   + lemma `pmf_ge0`
   + lemmas `pmf_gt0_countable`, `pmf_measurable`
 
+- in `unstable.v`:
+  + lemmas `oppr_itvNy`, `oppr_itvy`
+
+- in `set_interval.v`:
+  + lemmas `opp_preimage_itvbndy`, `opp_preimage_itvbndbnd`
+
+- in `lebesgue_measure.v`:
+  + lemma `lebesgue_measure_unique`
+
+- in `lebesgue_integral_nonneg.v`:
+  + lemmas `lebesgue_measureN`, `ge0_integration_by_substitution0`
+
+- in `measurable_realfun.v`:
+  + definition `min_mfun`
+
+- in `random_variable.v`
+  + lemmas `lebesgue_integral_pmf`, `cdf_measurable`, `ccdf_measurable`,
+    `le0_expectation_cdf`
+
+- in `lebesgue_integral_nonneg.v`:
+  + lemma `integral_setU`
+
+- in `measurable_realfun.v`:
+  + lemmas `emeasurable_fun_itv_obnd_cbndP`, `emeasurable_fun_itv_bndo_bndcP`,
+    `emeasurable_fun_itv_cc`
+
 ### Changed
 - in set_interval.v
   + `itv_is_closed_unbounded` (fix the definition)
@@ -163,10 +189,20 @@
   + `weak_sep_openE` -> `initial_sep_openE`
   + `join_product_weak` -> `join_product_initial`
 
+- in `lebesgue_integral_nonneg.v`:
+  + `integral_setD1_EFin` -> `integral_setD1`
+
 ### Generalized
 
+- in `lebesgue_integral_nonneg.v`:
+  + lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd`,
+    `integral_itv_bndoo`
+
 ### Deprecated
 
+- in `lebesgue_integral_nonneg.v`:
+  + lemma `integral_setU_EFin`
+
 ### Removed
 
 - in `weak_topology.v`:
@@ -175,6 +211,15 @@
     `weak_pseudo_metric_entourageE`
     (now `Let`'s in `initial_topology.v`)
 
+- in `measurable_realfun.v`:
+  + lemma `max_mfun_subproof` (has become a `Let`)
+
+- in `simple_functions.v`:
+  + definition `max_sfun`
+
+- in `lebesgue_integral_nonneg.v`:
+  + lemma `integral_setU` (was deprecated since version 1.0.1)
+
 ### Infrastructure
 
 ### Misc
diff --git a/classical/set_interval.v b/classical/set_interval.v
index 7008aadd0f..3d1c4da994 100644
--- a/classical/set_interval.v
+++ b/classical/set_interval.v
@@ -505,6 +505,16 @@ rewrite predeqE => /= r; split => [[{}r + <-]|].
 by exists (- r); rewrite ?opprK// !in_itv/= ltrNl ltrNr andbC.
 Qed.
 
+Lemma opp_preimage_itvbndy (R : numDomainType) ba (a : R) (bb : bool):
+  -%R @^-1` [set` Interval (BSide ba a) (BInfty _ bb)] =
+  [set` Interval (BInfty _ (~~ bb)) (BSide (~~ ba) (- a))].
+Proof. by apply/seteqP; split => [x/=|x/=]; rewrite oppr_itvy. Qed.
+
+Lemma opp_preimage_itvbndbnd (R : numDomainType) ba (a : R) bb (b : R) :
+  -%R @^-1` [set` Interval (BSide ba a) (BSide bb b)] =
+  [set` Interval (BSide (~~ bb) (- b)) (BSide (~~ ba) (- a))].
+Proof. by apply/seteqP; split => [x/=|x/=]; rewrite oppr_itv. Qed.
+
 (** lemmas between itv and set-theoretic operations *)
 Section set_itv_porderType.
 Variables (d : Order.disp_t) (T : porderType d).
diff --git a/classical/unstable.v b/classical/unstable.v
index da4e0b8087..a18a730d09 100644
--- a/classical/unstable.v
+++ b/classical/unstable.v
@@ -37,6 +37,27 @@ Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
+Section IntervalNumDomain.
+Variable R : numDomainType.
+Implicit Types x : R.
+
+(* TODO: PR to num_domain.v *)
+Lemma oppr_itvNy ba bb (xa xb x : R) :
+  (- x \in Interval (BInfty _ ba) (BSide bb xb)) =
+  (x \in Interval (BSide (~~ bb) (- xb)) (BInfty _ (~~ ba))).
+Proof.
+by rewrite !itv_boundlr /<=%O /= !implybF if_neg lteifNl andbC.
+Qed.
+
+Lemma oppr_itvy ba bb (xa x : R) :
+  (- x \in Interval (BSide ba xa) (BInfty _ bb)) =
+  (x \in Interval (BInfty _ (~~ bb)) (BSide (~~ ba) (- xa))).
+Proof.
+by rewrite !itv_boundlr /<=%O /= !implybF if_neg lteifNr negbK andbC.
+Qed.
+
+End IntervalNumDomain.
+
 Lemma coprime_prodr (I : Type) (r : seq I) (P : {pred I}) (F : I -> nat) (a : I)
     (l : seq I) :
   all (coprime (F a)) [seq F i | i <- [seq i <- l | P i]] ->
diff --git a/theories/ftc.v b/theories/ftc.v
index b83b6a397f..ad662b422e 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -109,25 +109,22 @@ apply: cvg_at_right_left_dnbhs.
   have ixdf n : \int[mu]_(t in [set` Interval a (BRight (x + d n))]) (f t)%:E -
                 \int[mu]_(t in [set` Interval a (BRight x)]) (f t)%:E =
                 \int[mu]_(y in E x n) (f y)%:E.
-    rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first.
-      by case: locf => + _ _; exact: measurable_funS.
+    rewrite -[in X in X - _]integral_itv_bndo_bndc; last first.
+      by case: locf => /measurable_EFinP + _ _; exact: measurable_funS.
     rewrite (@itv_bndbnd_setU _ _ _ (BLeft x))//=; last 2 first.
       by case: a ax F => [[|] a|[|]]// /ltW.
       by rewrite bnd_simp lerDl ltW.
-    rewrite integral_setU_EFin//=.
-    - rewrite addeAC -[X in _ - X]integral_itv_bndo_bndc//=; last first.
-        by case: locf => + _ _; exact: measurable_funS.
+    rewrite integral_setU//=.
+    - rewrite addeAC -[X in _ - X]integral_itv_bndo_bndc; last first.
+        by case: locf => /measurable_EFinP + _ _; exact: measurable_funS.
       rewrite subee ?add0e//.
       by apply: integrable_fin_num => //; exact: integrableS intf.
-    - by case: locf => + _ _; exact: measurable_funS.
-    - apply/disj_setPRL => z/=.
-      rewrite /E /= !in_itv/= => /andP[xz zxdn].
+    - by case: locf => /measurable_EFinP + _ _; exact: measurable_funS.
+    - apply/disj_setPRL => z/= zxxdn.
       move: a ax {F} => [[|] t/=|[_ /=|//]].
-      - rewrite lte_fin => tx.
-        by apply/negP; rewrite negb_and -leNgt xz orbT.
-      - rewrite lte_fin => tx.
-        by apply/negP; rewrite negb_and -!leNgt xz orbT.
-      - by apply/negP; rewrite -leNgt.
+      - by rewrite lte_fin in_itv/= => tx; rewrite (itvP zxxdn) andbF.
+      - by rewrite lte_fin in_itv/= => tx; rewrite (itvP zxxdn) andbF.
+      - by rewrite in_itv/= (itvP zxxdn).
   rewrite [f in f n @[n --> _] --> _](_ : _ =
       fun n => (d n)^-1 *: fine (\int[mu]_(t in E x n) (f t)%:E)); last first.
     apply/funext => n; congr (_ *: _); rewrite -fineB/=.
@@ -170,8 +167,8 @@ apply: cvg_at_right_left_dnbhs.
     case: a ax {F}; last first.
       move=> [_|//].
       apply: nearW => n.
-      rewrite -[in LHS]integral_itv_bndo_bndc//=; last first.
-        by case: locf => + _ _; exact: measurable_funS.
+      rewrite -[in LHS]integral_itv_bndo_bndc; last first.
+        by case: locf => /measurable_EFinP + _ _; exact: measurable_funS.
       rewrite -/mu -[LHS]oppeK; congr oppe.
       rewrite oppeB; last first.
         rewrite fin_num_adde_defl// fin_numN//.
@@ -179,24 +176,22 @@ apply: cvg_at_right_left_dnbhs.
       rewrite addeC.
       rewrite (_ : `]-oo, x] = `]-oo, (x + d n)%R] `|` E x n)%classic; last first.
         by rewrite -itv_bndbnd_setU//= bnd_simp ler_wnDr// ltW.
-      rewrite integral_setU_EFin//=.
-      - rewrite addeAC.
-        rewrite -[X in X - _]integral_itv_bndo_bndc//; last first.
-          by case: locf => + _ _; exact: measurable_funS.
+      rewrite integral_setU//=.
+      - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc; last first.
+          by case: locf => /measurable_EFinP + _ _; exact: measurable_funS.
         rewrite subee ?add0e//.
         by apply: integrable_fin_num => //; exact: integrableS intf.
       - exact: (nice_E _).1.
-      - by case: locf => + _ _; exact: measurable_funS.
-      - apply/disj_setPLR => z/=.
-        rewrite /E /= !in_itv/= leNgt => xdnz.
-        by apply/negP; rewrite negb_and xdnz.
+      - by case: locf => /measurable_EFinP + _ _; exact: measurable_funS.
+      - apply/disj_setPLR => z/= zNyxdn.
+        by rewrite /E /= !in_itv/= (itvP zNyxdn).
     move=> b a ax.
     move/cvgrPdist_le : d0.
     move/(_ (x - a)%R); rewrite subr_gt0 => /(_ ax)[m _ /=] h.
     near=> n.
     have mn : (m <= n)%N by near: n; exists m.
-    rewrite -[in X in X - _]integral_itv_bndo_bndc//=; last first.
-      by case: locf => + _ _; exact: measurable_funS.
+    rewrite -[in X in X - _]integral_itv_bndo_bndc; last first.
+      by case: locf => /measurable_EFinP + _ _; exact: measurable_funS.
     rewrite -/mu -[LHS]oppeK; congr oppe.
     rewrite oppeB; last first.
       rewrite fin_num_adde_defl// fin_numN//.
@@ -209,14 +204,14 @@ apply: cvg_at_right_left_dnbhs.
       rewrite lerBrDl -lerBrDr.
       by have := h _ mn; rewrite sub0r gtr0_norm.
       by rewrite opprK bnd_simp -lerBrDl subrr ltW.
-    rewrite integral_setU_EFin//=.
-    - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc//; last first.
-        by case: locf => + _ _; exact: measurable_funS.
+    rewrite integral_setU//=.
+    - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc; last first.
+        by case: locf => /measurable_EFinP + _ _; exact: measurable_funS.
       rewrite opprK subee ?add0e//.
       by apply: integrable_fin_num => //; exact: integrableS intf.
-    - by case: locf => + _ _; exact: measurable_funS.
+    - by case: locf => /measurable_EFinP + _ _; exact: measurable_funS.
     - apply/disj_setPLR => z/=.
-      rewrite /E /= !in_itv/= => /andP[az zxdn].
+      rewrite !in_itv/= => /andP[az zxdn].
       by apply/negP; rewrite negb_and -leNgt zxdn.
   suff: ((d n)^-1 * - fine (\int[mu]_(y in E x n) (f y)%:E))%R
           @[n --> \oo] --> f x.
@@ -446,9 +441,9 @@ have xbab : `]x, b] `<=` `[a, b].
 rewrite -addrA subrKC (le_trans (le_normr_Rintegral _ _))//.
   exact: integrableS intf.
 rewrite [leLHS](_ : _ = (\int[mu]_(t in `]x, b]) `|fab t|))//; last first.
-  apply: eq_Rintegral => //= z; rewrite inE/= in_itv/= => /andP[xz zb].
-  rewrite /fab patchE ifT// inE/= in_itv/= zb andbT (le_trans _ (ltW xz))//.
-  by near: x; exact: nbhs_left_ge.
+  apply: eq_Rintegral => //= z; rewrite inE/= => zxb.
+  rewrite /fab patchE ifT// inE/=.
+  by apply: subset_itv (zxb); rewrite bnd_simp// ltW// (itvP zxb).
 apply/ltW/int_normr_cont => //.
 rewrite lebesgue_measure_itv/= lte_fin.
 rewrite ifT// -EFinD lte_fin.
@@ -576,8 +571,8 @@ have [k FGk] : exists k : R, {in `]a, b[, (F - G =1 cst k)%R}.
     have [| |] := @MVT _ (F \- G)%R (F^`() - G^`())%R x y xy.
     - move=> z zxy; have zab : z \in `]a, b[.
         move: z zxy; apply: subset_itvW => //.
-        + by move: xab; rewrite in_itv/= => /andP[/ltW].
-        + by move: yab; rewrite in_itv/= => /andP[_ /ltW].
+        + by rewrite ltW// (itvP xab).
+        + by rewrite ltW// (itvP yab).
       have Fz1 : derivable F z 1.
         by case: dF => /= + _ _; apply; rewrite inE in zab.
       have Gz1 : derivable G z 1 by have [|] := G'f z.
@@ -587,17 +582,17 @@ have [k FGk] : exists k : R, {in `]a, b[, (F - G =1 cst k)%R}.
     - apply: derivable_within_continuous => z zxy.
       apply: derivableB.
       + case: dF => /= + _ _; apply.
-        apply: subset_itvSoo zxy => //.
-        by move: xab; rewrite in_itv/= => /andP[].
-        by move: yab; rewrite in_itv/= => /andP[].
-      + apply: (G'f _ _).2; apply: subset_itvSoo zxy => //.
-        by move: xab; rewrite in_itv/= => /andP[].
-        by move: yab; rewrite in_itv/= => /andP[].
+        apply: subset_itvSoo zxy => //; rewrite bnd_simp.
+        by rewrite (itvP xab).
+        by rewrite (itvP yab).
+      + apply: (G'f _ _).2; apply: subset_itvSoo zxy => //; rewrite bnd_simp.
+        by rewrite (itvP xab).
+        by rewrite (itvP yab).
     - move=> z zxy; rewrite F'G'0.
         by rewrite /cst/= mul0r => /eqP; rewrite subr_eq0 => /eqP.
       apply: subset_itvSoo zxy => //=; rewrite bnd_simp.
-      * by move: xab; rewrite in_itv/= => /andP[/ltW].
-      * by move: yab; rewrite in_itv/= => /andP[_ /ltW].
+      + by rewrite (itvP xab).
+      + by rewrite (itvP yab).
   move=> H; pose c := ((a + b) / 2)%R.
   exists (F c - G c)%R => u /(H u c); apply.
   by rewrite in_itv/= midf_lt//= midf_lt.
@@ -659,7 +654,8 @@ move=> f_ge0 cf Fxl dF Fa dFE.
 have mf : measurable_fun `]a, +oo[ f.
   apply: open_continuous_measurable_fun => //.
   by move: cf => /continuous_within_itvcyP[/in_continuous_mksetP cf _].
-rewrite -integral_itv_obnd_cbnd// itv_bndy_bigcup_BRight seqDU_bigcup_eq.
+rewrite -integral_itv_obnd_cbnd//; last exact/measurable_EFinP.
+rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq.
 rewrite ge0_integral_bigcup//=; last 3 first.
 - by move=> k; apply: measurableD => //; exact: bigsetU_measurable.
 - by rewrite -seqDU_bigcup_eq -itv_bndy_bigcup_BRight; exact: measurableT_comp.
@@ -687,7 +683,7 @@ transitivity (\sum_(0 <= i <oo) ((F (a + i.+1%:R))%:E - (F (a + i%:R))%:E)).
     by rewrite lee_fin; exact: f_ge0.
   apply: eq_eseriesr => n _.
   rewrite seqDUE/= integral_itv_obnd_cbnd; last first.
-    apply/measurable_fun_itv_bndo_bndcP.
+    apply/measurable_EFinP/measurable_fun_itv_bndo_bndcP.
     apply: open_continuous_measurable_fun => //.
     move: cf => /continuous_within_itvcyP[cf _] x.
     rewrite inE/= in_itv/= => /andP[anx _].
@@ -781,7 +777,7 @@ rewrite (@ge0_continuous_FTC2y (- f)%R (- F)%R _ (- l)%R).
 - exact: cvgN.
 - move=> x ax; rewrite derive1E deriveN.
     by rewrite -derive1E dFE.
-  by apply: dF; move: ax; rewrite in_itv/= andbT.
+  by apply: dF; rewrite (itvP ax).
 Qed.
 
 End corollary_FTC1.
@@ -879,8 +875,7 @@ Lemma increasing_image_oo F (a b : R) : (a < b)%R ->
   F @` `]a, b[ `<=` `]F a, F b[.
 Proof.
 move=> ab iF ? [x /= xab <-].
-move: xab; rewrite !in_itv/= => /andP[ax xb].
-by apply/andP; split; apply: iF; rewrite // in_itv/= ?lexx !ltW.
+by apply/andP; split; apply: iF; rewrite ?(itvP xab)//; exact: subset_itv_oo_cc.
 Qed.
 
 Lemma decreasing_image_oo F (a b : R) : (a < b)%R ->
@@ -888,8 +883,7 @@ Lemma decreasing_image_oo F (a b : R) : (a < b)%R ->
   F @` `]a, b[ `<=` `]F b, F a[.
 Proof.
 move=> ab iF ? [x /= xab <-].
-move: xab; rewrite !in_itv/= => /andP[ax xb].
-by apply/andP; split; apply: iF; rewrite // in_itv/= ?lexx !ltW.
+by apply/andP; split; apply: iF; rewrite ?(itvP xab)//; exact: subset_itv_oo_cc.
 Qed.
 
 Lemma increasing_cvg_at_right_comp F G a (b : itv_bound R) (l : R) :
@@ -1084,7 +1078,7 @@ pose PG x := parameterized_integral mu (F b) x G.
 have PGFbFa : derivable_oo_LRcontinuous PG (F b) (F a).
   have [/= dF rF lF] := Fab; split => /=.
   - move=> x xFbFa /=.
-    have xFa : (x < F a)%R by move: xFbFa; rewrite in_itv/= => /andP[].
+    have xFa : (x < F a)%R. by move: xFbFa; rewrite in_itv/= => /andP[].
     apply: (continuous_FTC1 xFa intG _ _).1 => /=.
       by move: xFbFa; rewrite lte_fin in_itv/= => /andP[].
     exact: (within_continuous_continuous _ _ xFbFa).
@@ -1261,7 +1255,8 @@ have mGF : measurable_fun `]a, b[ (G \o F).
 have mF' : measurable_fun `]a, b[ F^`().
   apply: subspace_continuous_measurable_fun => //.
   by apply: continuous_in_subspaceT => x /[!inE] xab; exact: cF'.
-rewrite integral_itv_bndoo//; last first.
+rewrite integral_itv_bndoo; last first.
+  apply/measurable_EFinP.
   rewrite compA -(compA G -%R) (_ : -%R \o -%R = id); last first.
     by apply/funext => y; rewrite /= opprK.
   apply: measurable_funM => //; apply: measurableT_comp => //.
@@ -1269,7 +1264,7 @@ rewrite integral_itv_bndoo//; last first.
     move=> x /[!inE] xab; rewrite [in RHS]derive1E deriveN -?derive1E//.
     by case: Fab => + _ _; apply.
   exact: measurableT_comp.
-rewrite [in RHS]integral_itv_bndoo//; last exact: measurable_funM.
+rewrite [in RHS]integral_itv_bndoo; last exact/measurable_EFinP/measurable_funM.
 apply: eq_integral => x /[!inE] xab; rewrite !fctE !opprK derive1E deriveN.
 - by rewrite opprK -derive1E.
 - by case: Fab => + _ _; exact.
@@ -1306,7 +1301,7 @@ have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R.
     by apply; rewrite inE/= in_itv/= andbT.
   by apply: cG; rewrite in_itv/=; apply: decrF; rewrite ?in_itv/= ?lexx ?ltW.
 rewrite -integral_itv_bndo_bndc; last first.
-  apply: open_continuous_measurable_fun => // x.
+  apply/measurable_EFinP;  apply: open_continuous_measurable_fun => // x.
   by rewrite inE => /cG.
 transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a[) (G x)%:E)).
   rewrite (decreasing_itvNyo_bigcup decrF Fny).
@@ -1338,7 +1333,7 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a[) (G x)%:E)).
     rewrite -(bigcup_mkord _ (fun k => `]F (a + k.+1%:R), F a[%classic)).
     by move: x; apply: bigcup_sub => k/= nk; exact: subset_itvr.
   rewrite -integral_itv_obnd_cbnd; last first.
-    case: n => [|n].
+    apply/measurable_EFinP; case: n => [|n].
       by rewrite addr0 set_itvoo0; exact: measurable_fun_set0.
     by apply: measurable_funS (mG n) => //; exact: subset_itvW.
   congr (integral _).
@@ -1348,6 +1343,7 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a[) (G x)%:E)).
 transitivity (limn (fun n =>
     \int[mu]_(x in `]a, (a + n%:R)%R[) (((G \o F) * - F^`()) x)%:E)); last first.
   rewrite -integral_itv_obnd_cbnd; last first.
+    apply/measurable_EFinP.
     rewrite (@itv_bndy_bigcup_BLeft_shift _ _ _ 1).
     under eq_bigcupr do rewrite addn1.
     apply/measurable_fun_bigcup => // n.
@@ -1396,33 +1392,34 @@ transitivity (limn (fun n =>
 apply: congr_lim; apply/funext => -[|n].
   by rewrite addr0 set_itvco0 set_itvoo0 !integral_set0.
 rewrite integral_itv_bndo_bndc; last first.
+  apply/measurable_EFinP.
   apply/measurable_fun_itv_obnd_cbndP; apply: measurable_funS (mG n) => //.
   by apply: subset_itvl; rewrite bnd_simp.
 rewrite integration_by_substitution_decreasing.
-- rewrite integral_itv_bndo_bndc// ?integral_itv_obnd_cbnd//.
-  + rewrite -setUitv1; last by rewrite bnd_simp ltrDl.
-    rewrite measurable_funU//; split; last exact: measurable_fun_set1.
+- rewrite integral_itv_bndo_bndc; last first.
+    apply/measurable_EFinP.
     by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co.
-  + by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co.
+  rewrite integral_itv_obnd_cbnd//.
+  apply/measurable_EFinP.
+  rewrite -setUitv1; last by rewrite bnd_simp ltrDl.
+  rewrite measurable_funU//; split; last exact: measurable_fun_set1.
+  by apply: measurable_funS (mGFNF' n) => //; exact: subset_itv_oo_co.
 - by rewrite lerDl.
-- move=> x y /=; rewrite !in_itv/= => /andP[ax _] /andP[ay _] yx.
-  by apply: decrF; rewrite //in_itv/= ?ax ?ay.
-- move=> x; rewrite in_itv/= => /andP[ax _].
-  by apply: cdF; rewrite in_itv/= ax.
+- move=> x y /= xaa yaa yx.
+  by apply: decrF; rewrite ?in_itv ?andbT/= ?(itvP xaa) ?(itvP yaa).
+- by move=> x xaa; apply: cdF; rewrite in_itv/= (itvP xaa).
 - exact: (cvgP dFa).
 - apply: (cvgP (F^`() (a + n.+1%:R))); apply/cvg_at_left_filter/cdF.
   by rewrite in_itv/= andbT ltr_pwDr.
 - split.
-  + move=> x; rewrite in_itv/= => /andP[ax _].
-    by apply: dF; rewrite in_itv/= ax.
+  + by move=> x xaa; apply: dF; rewrite in_itv/= (itvP xaa).
   + exact: cFa.
   + apply/cvg_at_left_filter/differentiable_continuous/derivable1_diffP/dF.
     by rewrite in_itv/= andbT ltr_pwDr.
 - apply/continuous_within_itvP.
   + by rewrite decrF ?ltr_pwDr ?in_itv ?andbT//= lerDl.
   + split.
-    * move=> y; rewrite in_itv/= => /andP[_ yFa].
-      by apply: cG; rewrite in_itv/= yFa.
+    * by move=> y yFaFa; apply: cG; rewrite in_itv/= (itvP yFaFa).
     * apply/cvg_at_right_filter/cG.
       by rewrite in_itv/= decrF ?in_itv/= ?andbT ?lerDl// ltr_pwDr.
     * exact: cGFa.
@@ -1511,8 +1508,8 @@ rewrite (@decreasing_ge0_integration_by_substitutiony (- F)%R); first last.
 - by move=> x y ax ay yx; rewrite ltrN2; exact: incrF.
 have mGF : measurable_fun `]a, +oo[ (G \o F).
   apply: (@measurable_comp _ _ _ _ _ _ `]F a, +oo[%classic) => //.
-  - move=> /= _ [x] /[!in_itv]/= /andP[ax xb] <-.
-    by rewrite incrF ?incrF// in_itv/= ?lexx/= ?(ltW ab)//= ?(ltW ax) ?(ltW xb).
+  - move=> /= _ [x] xab <-.
+    by rewrite in_itv/= incrF ?incrF ?in_itv/= ?lexx//= (itvP xab).
   - apply: open_continuous_measurable_fun; first exact: interval_open.
     by move=> x; rewrite inE/= => Fax; exact: cG.
   - apply: subspace_continuous_measurable_fun => //.
@@ -1531,14 +1528,13 @@ have mF' : measurable_fun `]a, +oo[ (- F)%R^`().
   rewrite near_nbhs.
   exact: near_in_itvoy.
 rewrite -!integral_itv_obnd_cbnd; last 2 first.
-  apply: measurable_funM => //.
+  apply/measurable_EFinP; apply: measurable_funM => //.
   apply: open_continuous_measurable_fun; first exact: interval_open.
   by move=> x; rewrite inE/=; exact: cF'.
-  apply: measurable_funM; last exact: measurableT_comp.
+  apply/measurable_EFinP; apply: measurable_funM; last exact: measurableT_comp.
   apply: (measurable_comp (measurable_itv `]-oo, (- F a)%R[)).
-  - move=> _ /= [x + <-].
-    rewrite !in_itv/= andbT=> ax.
-    by rewrite ltrN2 incrF// ?in_itv/= ?andbT// ltW.
+  - move=> _ /= [x + <-] => ax.
+    by rewrite in_itv/= ltrN2 incrF ?in_itv/= ?lexx//= (itvP ax).
   - apply: open_continuous_measurable_fun; first exact: interval_open.
     by move=> x; rewrite inE/=; exact: cGN.
   - apply: measurableT_comp => //.
@@ -1685,7 +1681,7 @@ have mF : measurable_fun `]-oo, b[ F.
   move/derivable_within_continuous : dF.
   by rewrite continuous_open_subspace; [exact|exact: interval_open].
 rewrite -[RHS]integral_itv_obnd_cbnd; last first.
-  apply: (@measurable_comp _ _ _ _ _ _ `]-oo, b]) => //=.
+  apply/measurable_EFinP/(@measurable_comp _ _ _ _ _ _ `]-oo, b]) => //=.
     rewrite opp_itv_bndy opprK/=.
     by apply: subset_itvl; rewrite bnd_simp.
   apply/measurable_fun_itv_bndo_bndcP; apply: measurable_funM => //.
@@ -1695,7 +1691,7 @@ rewrite -[RHS]integral_itv_obnd_cbnd; last first.
   - apply: open_continuous_measurable_fun; first by [].
     by move=> x/=; rewrite inE => /cdF.
 rewrite -[LHS]integral_itv_obnd_cbnd; last first.
-  apply: measurable_funM.
+  apply/measurable_EFinP/measurable_funM.
     apply: (@measurable_comp _ _ _ _ _ _ `](- F b)%R, +oo[) => //=.
     - move=> x/= [r]; rewrite in_itv/= andbT => br <-{x}.
       by rewrite in_itv/= andbT ltrN2 ndF ?in_itv//= 1?ltrNl// lerNl ltW.
@@ -1765,7 +1761,8 @@ rewrite -{2}setC0 -(set_itvoc0 0%R) setCitv/= ge0_integral_setU//=; first last.
   + by move=> ? ? _ _; exact: ndF.
   + by rewrite interiorT.
 - by apply/measurable_EFinP; rewrite -setCitvr setvU; exact: mGFF'.
-rewrite integral_itv_obnd_cbnd; last by apply: measurable_funTS; apply: mGFF'.
+rewrite integral_itv_obnd_cbnd; last first.
+  by apply/measurable_EFinP/measurable_funTS; exact: mGFF'.
 rewrite -(increasing_ge0_integration_by_substitutiony _ _ _ cvgFy); first last.
 - by move=> x; rewrite in_itv/= andbT => F0x; exact: G0.
 - exact: continuous_subspaceT.
@@ -1786,7 +1783,7 @@ rewrite -(increasing_ge0_integration_by_substitutionNy _ _ cvgFNy); first last.
 - by move=> x _; exact: cdF.
 - by move=> x y _ _; exact: ndF.
 rewrite -integral_itv_obnd_cbnd; last first.
-  by apply: measurable_funTS; exact: continuous_measurable_fun.
+  by apply/measurable_EFinP/measurable_funTS; exact: continuous_measurable_fun.
 rewrite -ge0_integral_setU//=; first last.
 - rewrite disj_set2E; apply/eqP; rewrite -subset0 => x/=.
   by rewrite !in_itv/= andbT ltNge => -[? /negP].
@@ -1858,7 +1855,7 @@ rewrite -(setUv [set x : R | 0 <= x]%R) ge0_integral_setU//= ; last 4 first.
   exact/disj_setPCl.
 rewrite mule_natl mule2n; congr +%E.
 rewrite -set_itvcy// setCitvr.
-rewrite integral_itv_bndo_bndc; last exact: measurable_funTS.
+rewrite integral_itv_bndo_bndc; last exact/measurable_EFinP/measurable_funTS.
 rewrite -{1}oppr0 ge0_integration_by_substitutionNy//.
 - apply: eq_integral => /= x; rewrite inE/= in_itv/= andbT => x0.
   by rewrite (evenf x).
diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
index 5f0fe74e9e..4da1e92903 100644
--- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
+++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
@@ -206,7 +206,7 @@ Lemma Rintegral_itv_bndo_bndc (a : itv_bound R) (r : R) f :
    \int[mu]_(x in [set` Interval a (BRight r)]) (f x).
 Proof.
 move=> mf; rewrite /Rintegral integral_itv_bndo_bndc//.
-by apply/measurable_EFinP; exact: (measurable_int mu).
+exact: (measurable_int mu).
 Qed.
 
 Lemma Rintegral_itv_obnd_cbnd (r : R) (b : itv_bound R) f :
@@ -215,7 +215,7 @@ Lemma Rintegral_itv_obnd_cbnd (r : R) (b : itv_bound R) f :
   \int[mu]_(x in [set` Interval (BLeft r) b]) (f x).
 Proof.
 move=> mf; rewrite /Rintegral integral_itv_obnd_cbnd//.
-by apply/measurable_EFinP; exact: (measurable_int mu).
+exact: (measurable_int mu).
 Qed.
 
 Lemma Rintegral_set1 f (r : R) : \int[mu]_(x in [set r]) f x = 0.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
index a6ad41e9fb..1df878888c 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
@@ -568,6 +568,33 @@ Qed.
 
 End ge0_transfer.
 
+Section change_of_variable.
+Open Scope ereal_scope.
+Context {R : realType}.
+
+Local Notation mu := lebesgue_measure.
+
+Lemma lebesgue_measureN (A : set R) : measurable A ->
+  pushforward mu (-%R : _ -> measurableTypeR R) A = mu A.
+Proof.
+move=> mA; apply/esym/lebesgue_measure_unique => //= _ [[a b]] _ <-.
+rewrite /pushforward opp_preimage_itvbndbnd/= !lebesgue_measure_itv/=.
+by rewrite !lte_fin ltrN2 opprK addrC.
+Qed.
+
+Lemma ge0_integration_by_substitution0 (f : R -> \bar R) :
+  measurable_fun [set: R] f -> (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.
+move=> mf f0; rewrite (_ : `]-oo, 0%R]%classic =
+    (-%R : _ -> measurableTypeR R) @^-1` `[0%R, +oo[); last first.
+  by rewrite opp_preimage_itvbndy oppr0.
+rewrite -ge0_integral_pushforward//=; last exact: measurable_funS mf.
+by apply: eq_measure_integral => //= A mA AS; exact/esym/lebesgue_measureN.
+Qed.
+
+End change_of_variable.
+
 Section integral_dirac.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (a : T) (R : realType).
@@ -907,25 +934,23 @@ by apply: ge0_subset_integral => //; exact: measurableT_comp.
 Qed.
 
 End subset_integral.
-#[deprecated(since="mathcomp-analysis 1.0.1", note="use `ge0_integral_setU` instead")]
-Notation integral_setU := ge0_integral_setU (only parsing).
 
 Section integral_setU_EFin.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType)
         (mu : {measure set T -> \bar R}).
 
-Lemma integral_setU_EFin (A B : set T) (f : T -> R) :
+Lemma integral_setU (A B : set T) (f : T -> \bar R) :
   measurable A -> measurable B ->
   measurable_fun (A `|` B) f ->
   [disjoint A & B] ->
-  \int[mu]_(x in (A `|` B)) (f x)%:E = \int[mu]_(x in A) (f x)%:E +
-                                       \int[mu]_(x in B) (f x)%:E.
+  \int[mu]_(x in (A `|` B)) f x = \int[mu]_(x in A) f x +
+                                  \int[mu]_(x in B) f x.
 Proof.
 move=> mA mB ABf AB.
 rewrite integralE/=.
-rewrite ge0_integral_setU//; last exact/measurable_funepos/measurable_EFinP.
-rewrite ge0_integral_setU//; last exact/measurable_funeneg/measurable_EFinP.
+rewrite ge0_integral_setU//; last exact/measurable_funepos.
+rewrite ge0_integral_setU//; last exact/measurable_funeneg.
 rewrite [X in _ = X + _]integralE/=.
 rewrite [X in _ = _ + X]integralE/=.
 set ap : \bar R := \int[mu]_(x in A) _; set an : \bar R := \int[mu]_(x in A) _.
@@ -934,6 +959,16 @@ rewrite oppeD 1?addeACA//.
 by rewrite ge0_adde_def// inE integral_ge0.
 Qed.
 
+Lemma __deprecated__integral_setU_EFin (A B : set T) (f : T -> R) :
+  measurable A -> measurable B ->
+  measurable_fun (A `|` B) f ->
+  [disjoint A & B] ->
+  \int[mu]_(x in (A `|` B)) (f x)%:E = \int[mu]_(x in A) (f x)%:E +
+                                       \int[mu]_(x in B) (f x)%:E.
+Proof.
+by move=> mA mB ABf AB; apply: integral_setU => //; exact/measurable_EFinP.
+Qed.
+
 Lemma integral_bigsetU_EFin (I : eqType) (F : I -> set T) (f : T -> R)
     (s : seq I) :
   (forall i, d.-measurable (F i)) ->
@@ -944,7 +979,7 @@ Lemma integral_bigsetU_EFin (I : eqType) (F : I -> set T) (f : T -> R)
 Proof.
 move=> mF; elim: s => [|h t ih] us tF D mf.
   by rewrite /D 2!big_nil integral_set0.
-rewrite /D big_cons integral_setU_EFin//.
+rewrite /D big_cons __deprecated__integral_setU_EFin//.
 - rewrite big_cons ih//.
   + by move: us => /= /andP[].
   + by apply: sub_trivIset tF => /= i /= it; rewrite inE it orbT.
@@ -959,6 +994,8 @@ rewrite /D big_cons integral_setU_EFin//.
 Qed.
 
 End integral_setU_EFin.
+#[deprecated(since="mathcomp-analysis 1.16.0", note="use `integral_setU instead`")]
+Notation integral_setU_EFin := __deprecated__integral_setU_EFin (only parsing).
 
 Section ge0_integral_bigcup.
 Local Open Scope ereal_scope.
@@ -1351,11 +1388,11 @@ Proof.
 move=> mD mf mg f0 g0 [N [mN N0 subN]].
 rewrite integralEpatch// [RHS]integralEpatch//.
 rewrite (ge0_negligible_integral mN)//; last 2 first.
-  - by apply/measurable_restrict => //; rewrite setIidr.
-  - by move=> x Dx; rewrite /= patchE (mem_set Dx) f0.
+- by apply/measurable_restrict => //; rewrite setIidr.
+- by move=> x Dx; rewrite /= patchE (mem_set Dx) f0.
 rewrite [RHS](ge0_negligible_integral mN)//; last 2 first.
-  - by apply/measurable_restrict => //; rewrite setIidr.
-  - by move=> x Dx; rewrite /= patchE (mem_set Dx) g0.
+- by apply/measurable_restrict => //; rewrite setIidr.
+- by move=> x Dx; rewrite /= patchE (mem_set Dx) g0.
 apply: eq_integral => x;rewrite in_setD => /andP[_ xN].
 apply: contrapT; rewrite !patchE; case: ifPn => xD //.
 move: xN; rewrite notin_setE; apply: contra_not => fxgx; apply: subN => /=.
@@ -1368,10 +1405,10 @@ Lemma ae_eq_integral (D : set T) (g f : T -> \bar R) :
 Proof.
 move=> mD mf mg /ae_eq_funeposneg[Dfgp Dfgn].
 rewrite integralE// [in RHS]integralE//; congr (_ - _).
-  by apply: ge0_ae_eq_integral => //; [exact: measurable_funepos|
+- by apply: ge0_ae_eq_integral => //; [exact: measurable_funepos|
                                        exact: measurable_funepos].
-by apply: ge0_ae_eq_integral => //; [exact: measurable_funeneg|
-                                     exact: measurable_funeneg].
+- by apply: ge0_ae_eq_integral => //; [exact: measurable_funeneg|
+                                       exact: measurable_funeneg].
 Qed.
 
 End ae_eq_integral.
@@ -1493,41 +1530,41 @@ rewrite ge0_integral_setU//=.
 - by apply/disj_setPRL => x /[swap] ->; rewrite /ball/= subKr gtr0_norm// ltxx.
 Qed.
 
-Lemma integral_setD1_EFin (f : R -> R) r (D : set R) :
+Lemma integral_setD1 (f : R -> \bar R) r (D : set R) :
   measurable (D `\ r) -> measurable_fun (D `\ r) f ->
-  \int[mu]_(x in D `\ r) (f x)%:E = \int[mu]_(x in D) (f x)%:E.
+  \int[mu]_(x in D `\ r) f x = \int[mu]_(x in D) f x.
 Proof.
 move=> mD mfl; have [Dr|NDr] := pselect (D r); last by rewrite not_setD1.
-rewrite -[in RHS](@setD1K _ r D)// integral_setU_EFin//=.
+rewrite -[in RHS](@setD1K _ r D)// integral_setU//=.
 - by rewrite integral_set1// add0e.
 - by apply/measurable_funU => //; split => //; exact: measurable_fun_set1.
 - by rewrite disj_set2E setDIK.
 Qed.
 
-Lemma integral_itv_bndo_bndc (a : itv_bound R) (r : R) (f : R -> R) :
+Lemma integral_itv_bndo_bndc (a : itv_bound R) (r : R) (f : R -> \bar R) :
   measurable_fun [set` Interval a (BLeft r)] f ->
-   \int[mu]_(x in [set` Interval a (BLeft r)]) (f x)%:E =
-   \int[mu]_(x in [set` Interval a (BRight r)]) (f x)%:E.
+   \int[mu]_(x in [set` Interval a (BLeft r)]) f x =
+   \int[mu]_(x in [set` Interval a (BRight r)]) f x.
 Proof.
 move=> mf; have [ar|ar] := leP a (BLeft r).
-- by rewrite -[RHS](@integral_setD1_EFin _ r) ?setDitv1r.
+- by rewrite -[RHS](@integral_setD1 _ r) ?setDitv1r.
 - by rewrite !set_itv_ge// -leNgt// ltW.
 Qed.
 
-Lemma integral_itv_obnd_cbnd (r : R) (b : itv_bound R) (f : R -> R) :
+Lemma integral_itv_obnd_cbnd (r : R) (b : itv_bound R) (f : R -> \bar R) :
   measurable_fun [set` Interval (BRight r) b] f ->
-   \int[mu]_(x in [set` Interval (BRight r) b]) (f x)%:E =
-   \int[mu]_(x in [set` Interval (BLeft r) b]) (f x)%:E.
+   \int[mu]_(x in [set` Interval (BRight r) b]) f x =
+   \int[mu]_(x in [set` Interval (BLeft r) b]) f x.
 Proof.
 move=> mf; have [rb|rb] := leP (BRight r) b.
-- by rewrite -[RHS](@integral_setD1_EFin _ r) ?setDitv1l.
+- by rewrite -[RHS](@integral_setD1 _ r) ?setDitv1l.
 - by rewrite !set_itv_ge// -leNgt -?ltBRight_leBLeft// ltW.
 Qed.
 
-Lemma integral_itv_bndoo (x y : R) (f : R -> R) (b0 b1 : bool) :
+Lemma integral_itv_bndoo (x y : R) (f : R -> \bar R) (b0 b1 : bool) :
   measurable_fun `]x, y[ f ->
-  \int[mu]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (f z)%:E =
-  \int[mu]_(z in `]x, y[) (f z)%:E.
+  \int[mu]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) f z =
+  \int[mu]_(z in `]x, y[) f z.
 Proof.
 have [xy|yx _|-> _] := ltgtP x y; last 2 first.
 - rewrite !set_itv_ge ?integral_set0//=.
@@ -1535,9 +1572,9 @@ have [xy|yx _|-> _] := ltgtP x y; last 2 first.
   + by move: b0 b1 => [|] [|]; rewrite bnd_simp ?lt_geF// le_gtF// ltW.
 - by move: b0 b1 => [|] [|]; rewrite !set_itvE ?integral_set0 ?integral_set1.
 move=> mf.
-transitivity (\int[mu]_(z in [set` Interval (BSide b0 x) (BLeft y)]) (f z)%:E).
+transitivity (\int[mu]_(z in [set` Interval (BSide b0 x) (BLeft y)]) f z).
   case: b1 => //; rewrite -integral_itv_bndo_bndc//.
-  by case: b0 => //; exact/measurable_fun_itv_obnd_cbndP.
+  by case: b0 => //; exact/emeasurable_fun_itv_obnd_cbndP.
 by case: b0 => //; rewrite -integral_itv_obnd_cbnd.
 Qed.
 
@@ -1548,12 +1585,15 @@ Lemma eq_integral_itv_bounded (x y : R) (g f : R -> R) (b0 b1 : bool) :
   \int[mu]_(z in [set` Interval (BSide b0 x) (BSide b1 y)]) (g z)%:E.
 Proof.
 move=> mf mg fg.
-rewrite integral_itv_bndoo// (@integral_itv_bndoo _ _ g)//.
+rewrite integral_itv_bndoo//; last exact/measurable_EFinP.
+rewrite (@integral_itv_bndoo _ _ (EFin \o g))//; last exact/measurable_EFinP.
 by apply: eq_integral => z; rewrite inE/= => zxy; congr EFin; exact: fg.
 Qed.
 
 End lebesgue_measure_integral.
 Arguments integral_Sset1 {R f A} r.
+#[deprecated(since="mathcomp-analysis 1.16.0", note="renamed_to `integral_setD1`")]
+Notation integral_setD1_EFin := integral_setD1 (only parsing).
 
 Section ge0_nondecreasing_set_cvg_integral.
 Context {d : measure_display} {T : measurableType d} {R : realType}.
diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v
index 4b9e20fe1f..e51f5f88f3 100644
--- a/theories/lebesgue_integral_theory/simple_functions.v
+++ b/theories/lebesgue_integral_theory/simple_functions.v
@@ -33,7 +33,6 @@ From mathcomp Require Import function_spaces.
 (*       {nnsfun T >-> R} == type of non-negative simple functions            *)
 (*          indic_sfun mD := mindic _ mD                                      *)
 (*             cst_sfun r == constant simple function                         *)
-(*           max_sfun f g := f \max f                                         *)
 (*           cst_nnsfun r == constant simple function                         *)
 (*                nnsfun0 := cst_nnsfun 0                                     *)
 (*         add_nnsfun f g := f \+ g                                           *)
@@ -210,10 +209,6 @@ Definition indic_sfun (D : set aT) (mD : measurable D) : {sfun aT >-> rT} :=
 HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_sfun k).
 Definition scale_sfun k f : {sfun aT >-> rT} := k \o* f.
 
-(* NB: already in `measurable_realfun.v` *)
-HB.instance Definition _ f g := max_mfun_subproof f g.
-Definition max_sfun f g : {sfun aT >-> _} := f \max g.
-
 End ring.
 Arguments indic_sfun {d aT rT} _.
 
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 1bdafa94af..50b5ccad1a 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -343,6 +343,12 @@ HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R).
 HB.instance Definition _ (R : realType) :=
   SigmaFiniteMeasure.on (@lebesgue_measure R).
 
+Lemma lebesgue_measure_unique {R : realType}
+    (mu : {measure set (measurableTypeR R) -> \bar R}) :
+    (forall X, ocitv X -> lebesgue_measure X = mu X) ->
+  forall A, measurable A -> lebesgue_measure A = mu A.
+Proof. exact: lebesgue_stieltjes_measure_unique. Qed.
+
 Definition completed_lebesgue_measure {R : realType} : set _ -> \bar R :=
   completed_lebesgue_stieltjes_measure idfun.
 HB.instance Definition _ (R : realType) :=
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
index 4d3ca1d3a9..d9ae2019c0 100644
--- a/theories/lebesgue_stieltjes_measure.v
+++ b/theories/lebesgue_stieltjes_measure.v
@@ -510,16 +510,17 @@ Definition measurableTypeR (R : realType) :=
   g_sigma_algebraType R.-ocitv.-measurable.
 
 Section lebesgue_stieltjes_measure.
-Variable R : realType.
+Context {R : realType}.
+Variable f : cumulative R R.
 
-Lemma lebesgue_stieltjes_measure_unique (f : cumulative R R)
+Lemma lebesgue_stieltjes_measure_unique
     (mu : {measure set (measurableTypeR R) -> \bar R}) :
     (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) ->
-  forall X, measurable X -> lebesgue_stieltjes_measure f X = mu X.
+  forall A, measurable A -> lebesgue_stieltjes_measure f A = mu A.
 Proof.
-move=> muE X mX; apply: measure_extension_unique => //=.
+move=> muE A mA; apply: measure_extension_unique => //=.
   exact: wlength_sigma_finite.
-by move=> A mA; rewrite -muE// -measurable_mu_extE.
+by move=> X mX; rewrite -muE// -measurable_mu_extE.
 Qed.
 
 End lebesgue_stieltjes_measure.
diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v
index 7f0d773d3b..2ce14c69ee 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                                         *)
 (* ```                                                                        *)
 (******************************************************************************)
 
@@ -189,70 +190,6 @@ End puncture_ereal_itv.
 Section salgebra_R_ssets.
 Variable R : realType.
 
-Lemma measurable_fun_itv_bndo_bndcP (a : itv_bound R) (b : R) (f : R -> R) :
-  measurable_fun [set` Interval a (BLeft b)] f <->
-  measurable_fun [set` Interval a (BRight b)] f.
-Proof.
-split; [have [ab ?|ab _] := leP a (BLeft b) |have [ab _|ab] := leP (BLeft b) a].
-- rewrite -setUitv1//; apply/measurable_funU => //; split => //.
-  exact: measurable_fun_set1.
-- by rewrite set_itv_ge -?leNgt//; exact: measurable_fun_set0.
-- by rewrite set_itv_ge -?leNgt//; exact: measurable_fun_set0.
-- by rewrite -setUitv1 ?ltW// => /measurable_funU[].
-Qed.
-
-Lemma measurable_fun_itv_obnd_cbndP (a : R) (b : itv_bound R) (f : R -> R) :
-  measurable_fun [set` Interval (BRight a) b] f <->
-  measurable_fun [set` Interval (BLeft a) b] f.
-Proof.
-split; [have [ab mf|ab _] := leP (BRight a) b|
-        have [ab _|ab] := leP b (BRight a)].
-- rewrite -setU1itv//; apply/measurable_funU => //; split => //.
-  exact: measurable_fun_set1.
-- rewrite set_itv_ge; first exact: measurable_fun_set0.
-  by rewrite -leNgt; case: b ab => -[].
-- by rewrite set_itv_ge// -?leNgt//; exact: measurable_fun_set0.
-- by rewrite -setU1itv ?ltW// => /measurable_funU[].
-Qed.
-
-#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_obnd_cbnd` instead")]
-Lemma measurable_fun_itv_co (x y : R) b0 b1 (f : R -> R) :
-  measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
-  measurable_fun `[x, y[ f.
-Proof.
-move: b0 b1 => [|] [|]//.
-- by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp.
-- by move/measurable_fun_itv_obnd_cbndP.
-- move=> mf.
-  have : measurable_fun `[x, y] f by exact/measurable_fun_itv_obnd_cbndP.
-  by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp.
-Qed.
-
-#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_bndo_bndc` instead")]
-Lemma measurable_fun_itv_oc (x y : R) b0 b1 (f : R -> R) :
-  measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
-  measurable_fun `]x, y] f.
-Proof.
-move: b0 b1 => [|] [|]//.
-- move=> mf.
-  have : measurable_fun `[x, y] f by exact/measurable_fun_itv_bndo_bndcP.
-  by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp.
-- by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp.
-- by move/measurable_fun_itv_bndo_bndcP.
-Qed.
-
-Lemma measurable_fun_itv_cc (x y : R) b0 b1 (f : R -> R) :
-  measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
-  measurable_fun `[x, y] f.
-Proof.
-move: b0 b1 => [|] [|]//.
-- by move/measurable_fun_itv_bndo_bndcP.
-- move=> mf.
-  have : measurable_fun `[x, y[ f by exact/measurable_fun_itv_obnd_cbndP.
-  by move/measurable_fun_itv_bndo_bndcP.
-- by move/measurable_fun_itv_obnd_cbndP.
-Qed.
-
 HB.instance Definition _ := (ereal_isMeasurable (R.-ocitv.-measurable)).
 (* NB: Until we dropped support for Coq 8.12, we were using
 HB.instance (\bar (Real.sort R))
@@ -1175,13 +1112,20 @@ Definition indic_mfun (D : set aT) (mD : measurable D) : {mfun aT >-> rT} :=
 HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst k).
 Definition scale_mfun k f : {mfun aT >-> rT} := k \o* f.
 
-Lemma max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g).
+Let max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g).
 Proof. by split; apply: measurable_maxr. Qed.
 
 HB.instance Definition _ f g := max_mfun_subproof f g.
 
 Definition max_mfun f g : {mfun aT >-> _} := f \max g.
 
+Let 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?*)
@@ -1454,6 +1398,96 @@ congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]].
 by move=> ? ?; exact: preimage_image.
 Qed.
 
+Section measurable_fun_itvW.
+Context {R : realType}.
+
+Lemma emeasurable_fun_itv_obnd_cbndP (a : R) (b : itv_bound R) (f : R -> \bar R) :
+  measurable_fun [set` Interval (BRight a) b] f <->
+  measurable_fun [set` Interval (BLeft a) b] f.
+Proof.
+split; [have [ab mf|ab _] := leP (BRight a) b|
+        have [ab _|ab] := leP b (BRight a)].
+- rewrite -setU1itv//; apply/measurable_funU => //; split => //.
+  exact: measurable_fun_set1.
+- rewrite set_itv_ge; first exact: measurable_fun_set0.
+  by rewrite -leNgt; case: b ab => -[].
+- by rewrite set_itv_ge// -?leNgt//; exact: measurable_fun_set0.
+- by rewrite -setU1itv ?ltW// => /measurable_funU[].
+Qed.
+
+Lemma measurable_fun_itv_obnd_cbndP (a : R) (b : itv_bound R) (f : R -> R) :
+  measurable_fun [set` Interval (BRight a) b] f <->
+  measurable_fun [set` Interval (BLeft a) b] f.
+Proof.
+by split => /measurable_EFinP/emeasurable_fun_itv_obnd_cbndP/measurable_EFinP.
+Qed.
+
+Lemma emeasurable_fun_itv_bndo_bndcP (a : itv_bound R) (b : R) (f : R -> \bar R) :
+  measurable_fun [set` Interval a (BLeft b)] f <->
+  measurable_fun [set` Interval a (BRight b)] f.
+Proof.
+split; [have [ab ?|ab _] := leP a (BLeft b) |have [ab _|ab] := leP (BLeft b) a].
+- rewrite -setUitv1//; apply/measurable_funU => //; split => //.
+  exact: measurable_fun_set1.
+- by rewrite set_itv_ge -?leNgt//; exact: measurable_fun_set0.
+- by rewrite set_itv_ge -?leNgt//; exact: measurable_fun_set0.
+- by rewrite -setUitv1 ?ltW// => /measurable_funU[].
+Qed.
+
+Lemma measurable_fun_itv_bndo_bndcP (a : itv_bound R) (b : R) (f : R -> R) :
+  measurable_fun [set` Interval a (BLeft b)] f <->
+  measurable_fun [set` Interval a (BRight b)] f.
+Proof.
+by split => /measurable_EFinP/emeasurable_fun_itv_bndo_bndcP/measurable_EFinP.
+Qed.
+
+#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_obnd_cbnd` instead")]
+Lemma measurable_fun_itv_co (x y : R) b0 b1 (f : R -> R) :
+  measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
+  measurable_fun `[x, y[ f.
+Proof.
+move: b0 b1 => [|] [|]//.
+- by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp.
+- by move/measurable_fun_itv_obnd_cbndP.
+- move=> mf.
+  have : measurable_fun `[x, y] f by exact/measurable_fun_itv_obnd_cbndP.
+  by apply: measurable_funS => //; apply: subset_itvl; rewrite bnd_simp.
+Qed.
+
+#[deprecated(since="mathcomp-analysis 1.9.0", note="use `measurable_fun_itv_bndo_bndc` instead")]
+Lemma measurable_fun_itv_oc (x y : R) b0 b1 (f : R -> R) :
+  measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
+  measurable_fun `]x, y] f.
+Proof.
+move: b0 b1 => [|] [|]//.
+- move=> mf.
+  have : measurable_fun `[x, y] f by exact/measurable_fun_itv_bndo_bndcP.
+  by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp.
+- by apply: measurable_funS => //; apply: subset_itvr; rewrite bnd_simp.
+- by move/measurable_fun_itv_bndo_bndcP.
+Qed.
+
+Lemma emeasurable_fun_itv_cc (x y : R) b0 b1 (f : R -> \bar R) :
+  measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
+  measurable_fun `[x, y] f.
+Proof.
+move: b0 b1 => [|] [|]//.
+- by move/emeasurable_fun_itv_bndo_bndcP.
+- move=> mf.
+  have : measurable_fun `[x, y[ f by exact/emeasurable_fun_itv_obnd_cbndP.
+  by move/emeasurable_fun_itv_bndo_bndcP.
+- by move/emeasurable_fun_itv_obnd_cbndP.
+Qed.
+
+Lemma measurable_fun_itv_cc (x y : R) b0 b1 (f : R -> R) :
+  measurable_fun [set` Interval (BSide b0 x) (BSide b1 y)] f ->
+  measurable_fun `[x, y] f.
+Proof.
+by move=> /measurable_EFinP/emeasurable_fun_itv_cc/measurable_EFinP.
+Qed.
+
+End measurable_fun_itvW.
+
 Lemma measurable_fun_dirac
     d {T : measurableType d} {R : realType} D (U : set T) :
   measurable U -> measurable_fun D (fun x => \d_x U : \bar R).
@@ -1554,6 +1588,7 @@ apply: (eq_measurable_fun (fun x => limn_esup (f_ ^~ x))) => //.
   by move=> x; rewrite inE => Dx; rewrite fE.
 exact: measurable_fun_limn_esup.
 Qed.
+
 End emeasurable_fun.
 Arguments emeasurable_fun_cvg {d T R D} f_.
 
diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v
index 992f0e1272..c8131df2a6 100644
--- a/theories/probability_theory/random_variable.v
+++ b/theories/probability_theory/random_variable.v
@@ -136,6 +136,104 @@ Proof. by move=> mf intf; rewrite integral_pushforward. Qed.
 
 End transfer_probability.
 
+Section pmf_definition.
+Context {d} {T : measurableType d} {R : realType} (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.
+Local Open Scope ereal_scope.
+Context d (T : measurableType d) (R : realType)
+  (P : probability T R) (X : {RV P >-> R}).
+
+Local Notation mu := lebesgue_measure.
+
+Lemma lebesgue_integral_pmf : \int[mu]_r (pmf X r)%:E = 0.
+Proof.
+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 lt_neqAle pmf_ge0 andbT negbK => /eqP.
+have cpmfP : countable pmfP := pmf_gt0_countable X.
+have mpmfP : measurable pmfP by exact: countable_measurable.
+have mpmf : measurable_fun setT (fun r => (pmf X r)%:E).
+  by apply/measurable_EFinP; exact: pmf_measurable.
+rewrite -Upmf ge0_integral_setU ?Upmf//=; last 2 first.
+  by rewrite pmf0NP; exact: measurableC.
+  by move=> x _; rewrite lee_fin pmf_ge0.
+rewrite [X in _ + X]integral0_eq ?addr0; last by move=> r <-.
+apply: null_set_integral => //=; first exact: measurable_funTS.
+exact: countable_lebesgue_measure0.
+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 +249,14 @@ 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 [set: R] (cdf X).
+Proof.
+suff: measurable_fun setT (fine \o cdf X) => [/measurable_EFinP |].
+  by apply: eq_measurable_fun => r _/=; rewrite fineK// fin_num_measure.
+apply: nondecreasing_measurable => //= r s rs.
+by rewrite fine_le ?fin_num_measure// cdf_nondecreasing.
+Qed.
+
 Lemma cvg_cdfy1 : cdf X @ +oo%R --> 1.
 Proof.
 pose s : \bar R := ereal_sup (range (cdf X)).
@@ -341,6 +447,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 [set: R] (ccdf X).
+Proof.
+apply: (eq_measurable_fun (fun r => 1 - cdf X r)) => [r _|].
+  by rewrite ccdf_1_cdf.
+by apply: emeasurable_funB => //; exact: cdf_measurable.
+Qed.
+
 Lemma cvg_ccdfy0 : ccdf X @ +oo%R --> 0.
 Proof.
 have : 1 - cdf X r @[r --> +oo%R] --> 1 - 1.
@@ -512,13 +625,70 @@ 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]).
+have : measurable_fun setT (<%R s) by exact: measurable_fun_ltr.
+rewrite [X in measurable X](_ : _ = (<%R s) @^-1` [set true]).
   by move=> /(_ measurableT [set true]); rewrite setTI; exact.
 by apply: eq_set => r; rewrite in_itv/= s_ge0.
 Qed.
 
+Let ge0_expectation_preimage (X : {RV P >-> R}) : (forall x, 0 <= X x)%R ->
+  'E_P[X] = \int[mu]_(r in `[0%R, +oo[) P (X @^-1` `[r, +oo[).
+Proof.
+have mPeqr : measurable_fun setT (fun r => P (X @^-1` [set r])).
+  apply: (eq_measurable_fun (EFin \o pmf X)) => [r/= _|].
+    by rewrite fineK// fin_num_measure.
+  by apply/measurable_EFinP; exact: pmf_measurable.
+have mPgtr : measurable_fun setT (fun r : R => P (X @^-1` `]r, +oo[)).
+  exact: ccdf_measurable.
+move=> X_ge0; rewrite ge0_expectation_ccdf//.
+transitivity
+    (\int[mu]_(r in `[0%R, +oo[) (P (X @^-1` [set r]) + P (X @^-1` `]r, +oo[))).
+  rewrite ge0_integralD//; [|exact: measurable_funTS..].
+  rewrite [X in _ = X + _](_ : _ = 0) ?add0e; first exact: eq_integral.
+  rewrite -(lebesgue_integral_pmf X) integral_mkcond.
+  apply: eq_integral => /= r _.
+  rewrite patchE; have [r_ge0 | r_lt0] := boolP (r \in `[0%R, +oo[).
+  - by rewrite ifT ?inE// fineK ?fin_num_measure.
+  - rewrite mem_setE (negbTE r_lt0) fineK ?fin_num_measure//.
+    rewrite (_ : _ @^-1` _ = set0) ?measure0//.
+    rewrite -nonemptyPn; apply: contraNnot r_lt0.
+    by case=> x <-; rewrite in_itv/= andbT.
+apply: eq_integral =>/= r _; rewrite -measureU//.
+- by rewrite -preimage_setU setU1itv.
+- exact: measurable_funPTI.
+- by rewrite -preimage_setI -subset0 => x/= [->]; rewrite in_itv/= 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 (Y @^-1` `[r, +oo[)).
+have mgeY r : d.-measurable (Y @^-1` `[r, +oo[) by exact: measurable_funPTI.
+have mfPleY : measurable_fun setT fPleY.
+  apply: nonincreasing_measurable => // r s rs.
+  rewrite fine_le ?fin_num_measure ?le_measure ?inE//.
+  by apply: preimage_subset; apply: subset_itvr; rewrite bnd_simp.
+move=> X_le0.
+have Y_ge0 x : (0 <= Y x)%R by rewrite oppr_ge0/=.
+transitivity (- 'E_P[Y]).
+  rewrite !expectation_def /Y -integral_ge0N/= => [|x _].
+    by apply: eq_integral => x _; rewrite opprK.
+  by rewrite lee_fin/= oppr_ge0.
+transitivity (- \int[mu]_(s in `]-oo, 0%R]) P (Y @^-1` `[(- s)%R, +oo[)).
+  rewrite ge0_expectation_preimage ?ge0_integration_by_substitution0//.
+  by apply: (eq_measurable_fun (fun r:R => (fine (P (Y @^-1` `[r, +oo[ )))%:E))
+     => [r _|]; [rewrite fineK ?fin_num_measure | apply/measurable_EFinP].
+transitivity (- \int[mu]_(s in `]-oo, 0%R] `\ 0%R) P (Y @^-1` `[(- s)%R, +oo[)).
+  congr -%E; rewrite setDitv1r integral_itv_bndo_bndc//=.
+  apply/measurable_funTS => /=.
+  under eq_fun => s
+    do rewrite -(@fineK _ (P (Y @^-1` `[(- s)%R, +oo[))) ?fin_num_measure//.
+  exact/measurableT_comp/(measurableT_comp mfPleY).
+rewrite setDitv1r; congr -%E; apply: eq_integral => r _.
+by rewrite (@comp_preimage _ _ _ _ _ -%R)/= opp_preimage_itvbndy/= opprK.
+Qed.
+
 End tail_expectation_formula.
 
 HB.lock Definition covariance {d} {T : measurableType d} {R : realType}
@@ -1039,71 +1209,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).