diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 344dcb5ba..7a3b00364 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -72,6 +72,15 @@
            `derivable_Nyo_continuousWoo`,
            `derivable_Nyo_continuousW`
 
+- in `realfun.v`:
+  + lemma `derivable_oy_continuous_bndN`
+
+- in `ftc.v`:
+  + lemmas `integration_by_partsy_ge0_ge0`,
+           `integration_by_partsy_le0_ge0`,
+           `integration_by_partsy_le0_le0`,
+           `integration_by_partsy_ge0_le0`
+
 ### Changed
 
 - in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
@@ -324,6 +333,9 @@
   + definition `poisson_pmf`, lemmas `poisson_pmf_ge0`, `measurable_poisson_pmf`,
   + definition `poisson_prob`
 
+- in `measurable_function.v`:
+  + lemma `measurable_funS`: implicits changed
+
 ### Renamed
 
 - in `reals.v`:
diff --git a/theories/charge.v b/theories/charge.v
index 8e80aee8c..63046f360 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -1845,7 +1845,7 @@ have int_f_E j S : measurable S -> \int[mu]_(x in S) f_ j x = nu (S `&` E j).
   have mSIEj := measurableI _ _ mS (mE j).
   have mSDEj := measurableD mS (mE j).
   rewrite -{1}(setUIDK S (E j)) (ge0_integral_setU _ mSIEj mSDEj)//; last 2 first.
-    - by rewrite setUIDK; exact: (measurable_funS measurableT).
+    - by rewrite setUIDK; exact: measurable_funTS.
     - by apply/disj_set2P; rewrite setDE setIACA setICr setI0.
   rewrite /f_ -(eq_integral _ (g_ j)); last first.
     by move=> x /[!inE] SIEjx; rewrite /f_ ifT// inE; exact: (@subIsetr _ S).
@@ -1957,7 +1957,7 @@ have -> : \int[nu]_(x in E) f x =
   under eq_integral => x /[!inE] /fE -> //.
   apply: monotone_convergence => //.
   - move=> n; apply/measurable_EFinP.
-    by apply: (measurable_funS measurableT) => //; exact/measurable_funP.
+    by apply: measurable_funTS => //; exact/measurable_funP.
   - by move=> n x Ex //=; rewrite lee_fin.
   - by move=> x Ex a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 have -> : \int[mu]_(x in E) (f \* g) x =
diff --git a/theories/ftc.v b/theories/ftc.v
index 157a707d5..b5ed70d5a 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -836,6 +836,286 @@ Qed.
 
 End integration_by_parts.
 
+Section integration_by_partsy_ge0.
+Context {R : realType}.
+Notation mu := lebesgue_measure.
+Local Open Scope ereal_scope.
+Local Open Scope classical_set_scope.
+
+Variables (F G f g : R -> R) (a FGoo : R).
+Hypothesis cf : {within `[a, +oo[, continuous f}.
+Hypothesis Foy : derivable_oy_continuous_bnd F a.
+Hypothesis Ff : {in `]a, +oo[%R, F^`() =1 f}.
+Hypothesis cg : {within `[a, +oo[, continuous g}.
+Hypothesis Goy : derivable_oy_continuous_bnd G a.
+Hypothesis Gg : {in `]a, +oo[%R, G^`() =1 g}.
+Hypothesis cvgFG : (F * G)%R x @[x --> +oo%R] --> FGoo.
+
+Let mFg :  measurable_fun `]a, +oo[ (F * g)%R.
+Proof.
+apply: (measurable_funS `[a, +oo[) => //.
+  by apply: subset_itvr; rewrite bnd_simp.
+apply: measurable_funM; apply: subspace_continuous_measurable_fun => //.
+exact: derivable_oy_continuous_within_itvcy.
+Qed.
+
+Let cfG : {within `[a, +oo[, continuous (f * G)%R}.
+Proof.
+have /continuous_within_itvcyP[aycf cfa] := cf.
+have /derivable_oy_continuous_within_itvcy/continuous_within_itvcyP[] := Goy.
+move=> aycG cGa; apply/continuous_within_itvcyP; split; last exact: cvgM.
+by move=> x ax; apply: continuousM; [exact: aycf|exact: aycG].
+Qed.
+
+Let mfG : measurable_fun `]a, +oo[ (f * G)%R.
+Proof.
+apply/measurable_fun_itv_obnd_cbndP.
+exact: subspace_continuous_measurable_fun.
+Qed.
+
+Let Ffai i : {in `]a + i%:R, a + i.+1%:R[%R, F^`() =1 f}.
+Proof.
+by apply/(in1_subset_itv _ Ff)/subset_itv => //; rewrite bnd_simp lerDl.
+Qed.
+
+Let Ggai i : {in `]a + i%:R, a + i.+1%:R[%R, G^`() =1 g}.
+Proof.
+by apply/(in1_subset_itv _ Gg)/subset_itv => //; rewrite bnd_simp lerDl.
+Qed.
+
+Let FGaoo :
+  (F (a + x.-1%:R) * G (a + x.-1%:R) - F a * G a)%:E @[x --> \oo] -->
+  (FGoo - F a * G a)%:E.
+Proof.
+apply: cvg_EFin; first exact: nearW; apply: cvgB; last exact: cvg_cst.
+rewrite -cvg_shiftS/=.
+apply: (@cvg_comp _ _ _ _ (F \* G)%R _ +oo%R); last exact: cvgFG; apply/cvgeryP.
+apply: (@cvge_pinftyP R (fun x => (a + x)%:E) +oo).1; last exact: cvgr_idn.
+by apply/cvgeryP; exact: cvg_addrl.
+Qed.
+
+Let sumN_Nsum_fG n :
+  \sum_(0 <= i < n)
+    (- (\int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i)
+         (f x * G x)%:E))%E =
+  - (\sum_(0 <= i < n)
+      (\int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i)
+        (f x * G x)%:E)%E).
+Proof.
+rewrite big_nat_cond fin_num_sumeN; rewrite -?big_nat_cond//; move=> m _.
+rewrite seqDUE integral_itv_obnd_cbnd; last first.
+  apply: measurable_funS mfG => //.
+  by apply/subset_itv => //; rewrite bnd_simp// lerDl.
+apply: integrable_fin_num => //=.
+apply: continuous_compact_integrable; first exact: segment_compact.
+apply: continuous_subspaceW cfG.
+by apply/subset_itv => //; rewrite bnd_simp// lerDl.
+Qed.
+
+Let sumNint_sumintN_fG n :
+  \sum_(0 <= i < n)
+    (- (\int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i)
+         (f x * G x)%:E))%E =
+  \sum_(0 <= i < n)
+    (\int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i)
+         (- (f x * G x))%:E)%E.
+Proof.
+rewrite big_nat_cond [RHS]big_nat_cond.
+apply: eq_bigr => i.
+rewrite seqDUE andbT => i0n.
+rewrite 2?integral_itv_obnd_cbnd; last 2 first.
+  apply: measurableT_comp => //.
+  apply: measurable_funS mfG => //.
+  by apply/subset_itv; rewrite bnd_simp// lerDl.
+  apply: measurable_funS mfG => //.
+  by apply/subset_itv; rewrite bnd_simp// lerDl.
+rewrite -integralN ?integrable_add_def ?continuous_compact_integrable//.
+  exact: segment_compact.
+apply: continuous_subspaceW cfG.
+by apply/subset_itv; rewrite bnd_simp// lerDl.
+Qed.
+
+Let sum_integral_limn :
+  \sum_(0 <= i <oo)
+    \int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i) (F x * g x)%:E
+  = limn (fun n => (F (a + n.-1%:R) * G (a + n.-1%:R) - F a * G a)%:E
+                    + \sum_(0 <= i < n)
+                      - \int[mu]_(x in seqDU (fun k => `]a, (a + k%:R)]) i)
+                          (f x * G x)%:E).
+Proof.
+apply: congr_lim; apply/funext => n.
+case: n.
+  by rewrite big_nat_cond [in RHS]big_nat_cond 2?big_pred0//= 2!addr0 subrr.
+case => [|n].
+  rewrite 2!big_nat1 seqDUE -pred_Sn addr0 subrr add0r.
+  by rewrite set_itvoc0 2!integral_set0 oppe0.
+rewrite big_nat_recl// [in RHS]big_nat_recl//=.
+rewrite seqDUE/= addr0 set_itvoc0 2!integral_set0 oppe0 2!add0r.
+under eq_bigr => i _.
+  rewrite seqDUE/= integral_itv_obnd_cbnd; last first.
+    apply: (measurable_funS `]a, +oo[) => //.
+    by apply/subset_itv => //; rewrite bnd_simp lerDl.
+  rewrite (integration_by_parts _ _ _ (@Ffai i) _ _ (@Ggai i)); last 5 first.
+  - by rewrite ltrD2l ltr_nat.
+  - apply: continuous_subspaceW cf.
+    by apply/subset_itv => //; rewrite bnd_simp lerDl.
+  - apply: derivable_oy_continuousWoo Foy.
+    + by rewrite ltrD2l ltr_nat.
+    + by rewrite lerDl.
+  - apply: continuous_subspaceW cg.
+    by apply/subset_itv => //; rewrite bnd_simp lerDl.
+  - apply: derivable_oy_continuousWoo Goy.
+    + by rewrite ltrD2l ltr_nat.
+    + by rewrite lerDl.
+  over.
+rewrite big_split/=.
+under eq_bigr do rewrite EFinB.
+rewrite telescope_sume// addr0; congr +%E.
+apply: eq_bigr => k _; rewrite seqDUE/= integral_itv_obnd_cbnd//.
+apply: measurable_funS mfG => //.
+by apply/subset_itv => //; rewrite bnd_simp lerDl.
+Qed.
+
+Lemma integration_by_partsy_ge0_ge0 :
+  {in `]a, +oo[, forall x, 0 <= (f x * G x)%:E} ->
+  {in `]a, +oo[, forall x, 0 <= (F x * g x)%:E} ->
+  \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E -
+  \int[mu]_(x in `[a, +oo[) (f x * G x)%:E.
+Proof.
+move=> fG0 Fg0.
+rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//.
+rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq.
+rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight.
+- rewrite sum_integral_limn; apply/cvg_lim => //.
+  apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo.
+  under eq_cvg do rewrite sumN_Nsum_fG; apply: cvgeN.
+  apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x.
+  rewrite seqDUE => anx; apply: fG0; rewrite inE/=.
+  by apply: subset_itv anx; rewrite bnd_simp// lerDl.
+- by move=> k; apply: measurableD => //; apply: bigsetU_measurable.
+- exact/measurable_EFinP.
+- by move=> ? ?; rewrite fG0// inE.
+- by move=> k; apply: measurableD => //; apply: bigsetU_measurable.
+- exact/measurable_EFinP.
+- by move=> ? ?; rewrite Fg0// inE.
+Qed.
+
+Lemma integration_by_partsy_le0_ge0 :
+  {in `]a, +oo[, forall x, (f x * G x)%:E <= 0} ->
+  {in `]a, +oo[, forall x, 0 <= (F x * g x)%:E} ->
+  \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E +
+  \int[mu]_(x in `[a, +oo[) (- (f x * G x)%:E).
+Proof.
+move=> fG0 Fg0.
+have mMfG : measurable_fun `]a, +oo[ (fun x => (- (f x * G x))%R).
+  exact: measurableT_comp.
+rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//.
+rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq.
+rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight.
+- rewrite sum_integral_limn; apply/cvg_lim => //.
+  apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo.
+  under eq_cvg do rewrite sumNint_sumintN_fG.
+  apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x.
+  rewrite seqDUE => anx; rewrite EFinN oppe_ge0.
+  apply: fG0; rewrite inE/=.
+  by apply: subset_itv anx; rewrite bnd_simp// lerDl.
+- by move=> k; apply: measurableD => //; apply: bigsetU_measurable.
+- by apply/measurable_EFinP; exact: measurableT_comp.
+- by move=> ? ?; rewrite EFinN oppe_ge0 fG0// inE.
+- by move=> k; apply: measurableD => //; apply: bigsetU_measurable.
+- exact/measurable_EFinP.
+- by move=> ? ?; rewrite Fg0// inE.
+Qed.
+
+End integration_by_partsy_ge0.
+
+Section integration_by_partsy_le0.
+Context {R: realType}.
+Notation mu := lebesgue_measure.
+Local Open Scope ereal_scope.
+Local Open Scope classical_set_scope.
+
+Variables (F G f g : R -> R) (a FGoo : R).
+Hypothesis cf : {within `[a, +oo[, continuous f}.
+Hypothesis Foy : derivable_oy_continuous_bnd F a.
+Hypothesis Ff : {in `]a, +oo[%R, F^`() =1 f}.
+Hypothesis cg : {within `[a, +oo[, continuous g}.
+Hypothesis Goy : derivable_oy_continuous_bnd G a.
+Hypothesis Gg : {in `]a, +oo[%R, G^`() =1 g}.
+Hypothesis cvgFG : (F \* G)%R x @[x --> +oo%R] --> FGoo.
+
+Let mFg : measurable_fun `]a, +oo[ (F * g)%R.
+Proof.
+apply: subspace_continuous_measurable_fun => //.
+rewrite continuous_open_subspace// => x ax.
+apply: cvgM.
+  have [+ _]:= Foy; move/derivable_within_continuous.
+  by rewrite continuous_open_subspace//; apply.
+have /continuous_within_itvcyP[+ _] := cg.
+by apply; rewrite inE/= in ax.
+Qed.
+
+Let NintNFg : {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} ->
+  \int[mu]_(x in `[a, +oo[) (F x * g x)%:E =
+  - \int[mu]_(x in `[a, +oo[) (- F x * g x)%:E.
+Proof.
+move=> Fg0.
+rewrite -integral_itv_obnd_cbnd//.
+under eq_integral => x do rewrite -(opprK (F x)) mulNr EFinN.
+rewrite integralN/=; last first.
+  apply: fin_num_adde_defl.
+  apply/EFin_fin_numP; exists 0%R.
+  apply/eqe_oppLRP; rewrite oppe0.
+  apply: integral0_eq => /= x ax.
+  apply: (@ge0_funenegE _ _ `]a, +oo[); last by rewrite inE/=.
+  move=> ?/= ?; rewrite mulNr EFinN oppe_ge0 Fg0//=.
+  by rewrite inE.
+rewrite integral_itv_obnd_cbnd//.
+under [X in _ _ X]eq_fun do rewrite mulNr; exact: measurableT_comp.
+Qed.
+
+Lemma integration_by_partsy_le0_le0 :
+  {in `]a, +oo[, forall x, (f x * G x)%:E <= 0} ->
+  {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} ->
+  \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E +
+  \int[mu]_(x in `[a, +oo[) (- (f x * G x)%:E).
+Proof.
+move=> fG0 Fg0.
+rewrite NintNFg//.
+rewrite (@integration_by_partsy_ge0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//.
+- rewrite oppeB; last exact: fin_num_adde_defr.
+  rewrite -EFinN opprD 2!opprK mulNr.
+  by under eq_integral do rewrite mulNr EFinN.
+- by move=> ?; apply: cvgN; exact: cf.
+- exact: derivable_oy_continuous_bndN.
+- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.
+- by under eq_cvg do rewrite fctE/= mulNr; apply: cvgN.
+- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: fG0.
+- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: Fg0.
+Qed.
+
+Lemma integration_by_partsy_ge0_le0 :
+  {in `]a, +oo[, forall x, 0 <= (f x * G x)%:E} ->
+  {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} ->
+  \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E -
+  \int[mu]_(x in `[a, +oo[) (f x * G x)%:E.
+Proof.
+move=> fG0 Fg0.
+rewrite NintNFg//.
+rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//.
+- rewrite oppeD; last exact: fin_num_adde_defr.
+  rewrite -EFinN opprD 2!opprK mulNr.
+  by under eq_integral do rewrite mulNr EFinN oppeK.
+- by move=> ?; apply: cvgN; exact: cf.
+- exact: derivable_oy_continuous_bndN.
+- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.
+- by under eq_cvg do rewrite fctE/= mulNr; apply: cvgN.
+- by move=> ? ?; rewrite mulNr EFinN oppe_le0; exact: fG0.
+- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; exact: Fg0.
+Qed.
+
+End integration_by_partsy_le0.
+
 Section Rintegration_by_parts.
 Context {R : realType}.
 Notation mu := lebesgue_measure.
@@ -1293,8 +1573,7 @@ have mGFNF' i : measurable_fun `[a, (a + i.+1%:R)[ ((G \o F) * - F^`())%R.
   apply: open_continuous_measurable_fun; first exact: interval_open.
   move=> x; rewrite inE/= in_itv/= => /andP[ax _].
   apply: continuousM; last first.
-    apply: continuousN.
-    by apply: cdF; rewrite in_itv/= andbT.
+    by apply: continuousN; apply: cdF; rewrite in_itv/= andbT.
   apply: continuous_comp.
     have := derivable_within_continuous dF.
     rewrite continuous_open_subspace; last exact: interval_open.
@@ -1321,7 +1600,7 @@ transitivity (limn (fun n => \int[mu]_(x in `[F (a + n%:R)%R, F a[) (G x)%:E)).
     exact: (@sub_trivIset _ _ _ [set: nat]).
     apply/measurable_EFinP.
     rewrite big_mkord -bigsetU_seqDU.
-    apply: (measurable_funS _
+    apply: (measurable_funS _ _
         (@bigsetU_bigcup _ (fun k =>`]F (a + k.+1%:R)%R, _[%classic) _)).
       exact: bigcup_measurable.
     apply/measurable_fun_bigcup => //.
@@ -1374,7 +1653,7 @@ transitivity (limn (fun n =>
   - exact: iota_uniq.
   - exact: (@sub_trivIset _ _ _ [set: nat]).
   - apply/measurable_EFinP.
-    apply: (measurable_funS (measurable_itv `]a, (a + n.+1%:R)[)).
+    apply: (measurable_funS `]a, (a + n.+1%:R)[) => //.
       rewrite big_mkord -bigsetU_seqDU.
       rewrite -(bigcup_mkord _ (fun k => `]a, (a + k.+1%:R)[%classic)).
       apply: bigcup_sub => k/= kn.
diff --git a/theories/kernel.v b/theories/kernel.v
index d5df49fa3..9094cff8e 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -899,8 +899,7 @@ apply: measurable_fun_if => //.
 - rewrite setTI [X in measurable X](_ : _ = [set t | f t setT != 0]).
     exact: kernel_measurable_neq_cst.
   by apply/seteqP; split => [x /negbT//|x /negbTE].
-- apply: (@measurable_funS _ _ _ _ setT) => //.
-  exact: kernel_measurable_fun_eq_cst.
+- by apply: measurable_funTS => //; exact: kernel_measurable_fun_eq_cst.
 - apply: emeasurable_funM.
     exact: measurable_funS (measurable_kernel f U mU).
   apply/measurable_EFinP.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
index d83e7c0d7..694ff7777 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
@@ -142,11 +142,11 @@ have intg : mu.-integrable E (EFin \o h).
 exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans.
   pose fgh x := `|(f x - g x)%:E| + `|(g x - h x)%:E|.
   apply: (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //.
-  - apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //.
+  - apply: (measurable_funS E) => //; do 2 apply: measurableT_comp => //.
     exact: measurable_funB.
   - by move=> z _; rewrite adde_ge0.
   - apply: measurableT_comp => //; apply: measurable_funD;
-      apply: (measurable_funS mE (@subset_refl _ E));
+      apply: (measurable_funS _ mE (@subset_refl _ E));
       (apply: measurableT_comp => //);
       exact: measurable_funB.
   - move=> x _; rewrite -(subrK (g x) (f x)) -(addrA (_ + _)%R) lee_fin.
@@ -161,12 +161,12 @@ rewrite EFinD lteD// -(setDKU AE) ge0_integral_setU => //; first last.
 - exact: measurableD.
 rewrite (@ae_eq_integral _ _ _ mu A (cst 0)) //; first last.
 - by apply: aeW => z Az; rewrite (gh z) ?inE// subrr abse0.
-- apply: (measurable_funS mE) => //; do 2 apply: measurableT_comp => //.
+- apply: (measurable_funS E) => //; do 2 apply: measurableT_comp => //.
   exact: measurable_funB.
 rewrite integral0 adde0.
 apply: (le_lt_trans (integral_le_bound (M *+ 2)%:E _ _ _ _)) => //.
 - exact: measurableD.
-- apply: (measurable_funS mE) => //; apply: measurableT_comp => //.
+- apply: (measurable_funS E) => //; apply: measurableT_comp => //.
   exact: measurable_funB.
 - by rewrite lee_fin mulrn_wge0// ltW.
 - apply: aeW => z [Ez _]; rewrite /= lee_fin mulr2n.
@@ -331,7 +331,8 @@ Lemma locally_integrableS (A B : set R) f :
 Proof.
 move=> mA mB AB [mfB oT ifB].
 have ? : measurable_fun [set: R] (f \_ A).
-  apply/(measurable_restrictT _ _).1 => //; apply: (measurable_funS _ AB) => //.
+  apply/(measurable_restrictT _ _).1 => //.
+  apply: (measurable_funS _ _ AB) => //.
   exact/(measurable_restrictT _ _).2.
 split => // K KT cK; apply: le_lt_trans (ifB _ KT cK).
 apply: ge0_le_integral => //=; first exact: compact_measurable.
@@ -1043,7 +1044,7 @@ rewrite -invfM lef_pV2 ?posrE ?divr_gt0// -(@natr1 _ n) -lerBlDr.
 by near: n; exact: nbhs_infty_ger.
 Unshelve. all: by end_near. Qed.
 
-Lemma lebesgue_differentiation f : locally_integrable setT f ->
+Lemma lebesgue_differentiation f : locally_integrable [set: R] f ->
   {ae mu, forall x, lebesgue_pt f x}.
 Proof.
 move=> locf.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
index 4efad18f7..2aa43358e 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
@@ -229,7 +229,7 @@ split.
   apply/funext => n; apply: ae_eq_integral => //.
   + apply: measurableT_comp => //; apply: emeasurable_funB => //.
     apply/measurable_restrict => //; first exact: measurableD.
-    exact: (measurable_funS mD).
+    exact: (measurable_funS D).
   + by rewrite /g_; apply: measurableT_comp => //; exact: emeasurable_funB.
   + exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx.
     by rewrite /f_' /f' /restrict mem_set.
@@ -242,7 +242,7 @@ split.
   set Y := (X in _ -> _ --> X); rewrite [X in _ --> X -> _](_ : _ = Y) //.
   apply: ae_eq_integral => //.
     apply/measurable_restrict => //; first exact: measurableD.
-    exact: (measurable_funS mD).
+    exact: (measurable_funS D).
   exists N; split => //; rewrite -(setCK N); apply: subsetC => x /= Nx Dx.
   by rewrite /f' /restrict mem_set.
 Qed.
diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v
index 2cf18dca4..84b9c2872 100644
--- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v
+++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v
@@ -456,8 +456,8 @@ have-> : D `&` (f \+ g) @^-1` A =
   by case: (f x) (g x) Afgx => [rf||] [rg||].
 have Dfg : D `&` [set x | f x +? g x] `<=` D by apply: subIset; left.
 apply: hwlogD => //.
-- by apply: (measurable_funS mD) => //; do ?exact: measurableI.
-- by apply: (measurable_funS mD) => //; do ?exact: measurableI.
+- by apply: (measurable_funS _ mD) => //; do ?exact: measurableI.
+- by apply: (measurable_funS _ mD) => //; do ?exact: measurableI.
 - by rewrite -setIA setIid.
 - by move=> ? [].
 Qed.
@@ -552,8 +552,8 @@ have-> : D `&` (fun x => f x * g x) @^-1` A =
   by apply: contra_notT NA0; rewrite negbK => /eqP <-.
 have Dfg : D `&` [set x | f x *? g x] `<=` D by apply: subIset; left.
 apply: hwlogM => //.
-- by apply: (measurable_funS mD) => //; do ?exact: measurableI.
-- by apply: (measurable_funS mD) => //; do ?exact: measurableI.
+- by apply: (measurable_funS _ mD) => //; do ?exact: measurableI.
+- by apply: (measurable_funS _ mD) => //; do ?exact: measurableI.
 - by rewrite -setIA setIid.
 - by move=> ? [].
 Qed.
diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v
index fb680408d..f305e2527 100644
--- a/theories/measurable_realfun.v
+++ b/theories/measurable_realfun.v
@@ -1708,7 +1708,7 @@ move=> mf mg mA Afin [C [mC C0 nC] epspos].
 have [B [mB Beps Bunif]] : exists B, [/\ d.-measurable B, mu B < eps%:E &
     {uniform (A `\` C) `\` B,  f @\oo --> g}].
   apply: pointwise_almost_uniform => //.
-  - by move=> n; apply : (measurable_funS mA _ (mf n)) => ? [].
+  - by move=> n; apply : (measurable_funS _ mA _ (mf n)) => ? [].
   - by apply: measurableI => //; exact: measurableC.
   - by rewrite (le_lt_trans _ Afin)// le_measure// inE//; exact: measurableD.
   - by move=> x; rewrite setDE; case => Ax /(subsetC nC); rewrite setCK; exact.
diff --git a/theories/measure_theory/measurable_function.v b/theories/measure_theory/measurable_function.v
index c43a271cb..54e7060f3 100644
--- a/theories/measure_theory/measurable_function.v
+++ b/theories/measure_theory/measurable_function.v
@@ -174,6 +174,7 @@ End measurable_fun.
   solve [apply: measurable_id] : core.
 Arguments eq_measurable_fun {d1 d2 T1 T2 D} f {g}.
 Arguments measurable_fun_eqP {d1 d2 T1 T2 D} f {g}.
+Arguments measurable_funS {d1 d2 T1 T2} E {D f}.
 
 Section mfun.
 Context {d d'} {aT : sigmaRingType d} {rT : sigmaRingType d'}.
diff --git a/theories/realfun.v b/theories/realfun.v
index 8d430961b..ed2af1071 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -1192,6 +1192,13 @@ Definition derivable_Nyo_continuous_bnd (f : R -> V) (x : R) :=
 Definition derivable_oy_continuous_bnd (f : R -> V) (x : R) :=
   {in `]x, +oo[, forall x, derivable f x 1} /\ f @ x^'+ --> f x.
 
+Lemma derivable_oy_continuous_bndN (f : R -> V) (x : R) :
+  derivable_oy_continuous_bnd f x -> derivable_oy_continuous_bnd (- f) x.
+Proof.
+move=> [/= derF Fa]; split; last exact: cvgN.
+by move=> /= ? ?; exact/derivableN/derF.
+Qed.
+
 Lemma derivable_oy_continuous_within_itvcy (f : R -> V) (x : R) :
   derivable_oy_continuous_bnd f x -> {within `[x, +oo[, continuous f}.
 Proof.