diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 318217cd5..b0212288f 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -20,6 +20,88 @@
 - in probability.v
   + lemma `pmf_ge0`
   + lemmas `pmf_gt0_countable`, `pmf_measurable`
+- in set_interval.v
+  + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`
+
+- in `set_interval.v`:
+  + lemmas `itv_setU_setT`, `disjoint_rays`
+
+- in `constructive_ereal.v`:
+  + lemma `ltgte_fin_num`
+
+- in `probability.v`:
+  + definition `ccdf`
+  + lemmas `lebesgue_stieltjes_cdf_id`, `cdf_ccdf_1`, `ccdf_nonincreasing`, `cvg_ccdfy0`, `cvg_ccdfNy1`, `ccdf_right_continuous`, `ge0_expectation_ccdf`
+  + corollaries `ccdf_cdf_1`, `ccdf_1_cdf`, `cdf_1_ccdf`
+
+- in `num_normedtype.v`:
+  + lemma `nbhs_infty_gtr`
+- in `function_spaces.v`:
+  + lemmas `cvg_big`, `continuous_big`
+
+- in `realfun.v`:
+  + lemma `cvg_addrl_Ny`
+
+- in `constructive_ereal.v`:
+  + lemmas `mule_natr`, `dmule_natr`
+  + lemmas `inve_eqy`, `inve_eqNy`
+
+- in `uniform_structure.v`:
+  + lemma `continuous_injective_withinNx`
+
+- in `constructive_ereal.v`:
+  + variants `Ione`, `Idummy_placeholder`
+  + inductives `Inatmul`, `IEFin`
+  + definition `parse`, `print`
+  + number notations in scopes `ereal_dual_scope` and `ereal_scope`
+  + notation `- 1` in scopes `ereal_dual_scope` and `ereal_scope`
+- in `pseudometric_normed_Zmodule.v`:
+  + lemma `le0_ball0`
+- in `theories/landau.v`:
+  + lemma `littleoE0`
+
+- in `constructive_ereal.v`:
+  + lemma `lt0_adde`
+
+- in `unstable.v`
+  + lemmas `coprime_prodr`, `Gauss_dvd_prod`, `expn_prod`, `mono_leq_infl`,
+    `card_big_setU`
+
+- file `pnt.v`
+  + definitions `next_prime`, `prime_seq`
+  + lemmas `leq_prime_seq`, `mem_prime_seq`
+  + theorem `dvg_sum_inv_prime_seq`
+- new directory `theories/measure_theory` with new files:
+  + `measurable_structure.v`
+  + `measure_function.v`
+  + `counting_measure.v`
+  + `dirac_measure.v`
+  + `probability_measure.v`
+  + `measure_negligible.v`
+  + `measure_extension.v`
+  + `measurable_function.v`
+  + `measure.v`
+
+- in `realfun.v`:
+  + lemmas `derivable_oy_continuous_within_itvcy`,
+           `derivable_oy_continuous_within_itvNyc`
+  + lemmas `derivable_oo_continuousW`,
+           `derivable_oy_continuousWoo`,
+           `derivable_oy_continuousW`,
+           `derivable_Nyo_continuousWoo`,
+           `derivable_Nyo_continuousW`
+
+- in `realfun.v`:
+  + lemma `derivable_oy_RcontinuousN`
+
+- in `ftc.v`:
+  + lemmas `integration_by_partsy_ge0_ge0`,
+           `integration_by_partsy_le0_ge0`,
+           `integration_by_partsy_le0_le0`,
+           `integration_by_partsy_ge0_le0`
+
+- in `real_interval.v`:
+  + lemma `subset_itvoSo_cSc`
 
 ### Changed
 - in set_interval.v
@@ -135,6 +217,261 @@
     * definition `pmf`
     * lemmas `pmf_ge0`, `pmf_gt0_countable`, `pmf_measurable`, `dRV_expectation`,
       `expectation_pmf`
+- in set_interval.v
+  + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool)
+
+- in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
+  + lemma `nondecreasing_right_continuousP` 
+  + definition `CumulativeBounded`
+
+- in `lebesgue_stieltjes_measure.v`, according to generalization of `Cumulative`, modified:
+  + lemmas `wlength_ge0`, `cumulative_content_sub_fsum`, `wlength_sigma_subadditive`, `lebesgue_stieltjes_measure_unique`
+  + definitions `lebesgue_stieltjes_measure`, `completed_lebesgue_stieltjes_measure`
+
+- moved from `vitali_lemma.v` to `pseudometric_normed_Zmodule.v` and renamed:
+  + `closure_ball` -> `closure_ballE`
+
+- moved from `theories/measure.v` (now removed)
+  + to `sequences.v`:
+    * lemmas `epsilon_trick`, `epsilon_trick0`
+  + to `measure_theory/measurable_structure.v`:
+    * definitions `setC_closed`, `setI_closed`, `setU_closed`, `setSD_closed`,
+      `setD_closed`, `setY_closed`, `fin_bigcap_closed`, `finN0_bigcap_closed`,
+      `fin_bigcup_closed`, `semi_setD_closed`
+    * lemma `setD_semi_setD_closed`
+    * definitions `ndseq_closed`, `niseq_closed`, `trivIset_closed`, `fin_trivIset_closed`,
+      `setring`, `sigma_ring`, `sigma_algebra`, `dynkin`, `lambda_system`,
+      `monotone`
+    * lemmas `powerset_sigma_ring`, `powerset_lambda_system`
+    * notations `<<l _, >>`, `<<l _ >>`, `<<d _ >>`, `<<s _, _>>`, `<<s _ >>`,
+      `<<r _ >>`, `<<sr _ >>`, `<<M _ >>`
+    * lemmas `lambda_system_smallest`, `fin_bigcup_closedP`, `finN0_bigcap_closedP`,
+      `setD_closedP`, `sigma_algebra_bigcap`, `sigma_algebraP`, `smallest_sigma_algebra`,
+      `sub_sigma_algebra2`, `sigma_algebra_id`, `sub_sigma_algebra`,
+      `sigma_algebra0`, `sigma_algebraCD`, `sigma_algebra_bigcup`,
+      `smallest_setring`, `sub_setring2`, `setring_id`, `sub_setring`,
+      `setring0`, `setringD`, `setringU`, `setring_fin_bigcup`, `g_sigma_algebra_lambda_system`,
+      `smallest_sigma_ring`, `sigma_ring_monotone`, `g_sigma_ring_monotone`,
+      `sub_g_sigma_ring`, `setring_monotone_sigma_ring`, `g_monotone_monotone`,
+      `g_monotone_setring`, `g_monotone_g_sigma_ring`, `monotone_setring_sub_g_sigma_ring`,
+      `smallest_lambda_system`, `lambda_system_subset`, `dynkinT`, `dynkinC`,
+      `dynkinU`, `dynkin_lambda_system`, `g_dynkin_dynkin`, `sigma_algebra_dynkin`,
+      `dynkin_setI_sigma_algebra`, `setI_closed_g_dynkin_g_sigma_algebra`
+    * definition `strace`
+    * lemmas `subset_strace`, `g_sigma_ring_strace`, `strace_sigma_ring`,
+      `setI_g_sigma_ring`, `sigma_algebra_strace`
+    * mixin `isSemiRingOfSets`, structure `SemiRingOfSets`,
+      notation `semiRingOfSetsType`
+    * lemma `measurable_curry`
+    * notations `.-measurable`, `'measurable`
+    * mixin `SemiRingOfSets_isRingOfSets`, structure `RingOfSets`,
+      notation `ringOfSetsType`
+    * mixin `RingOfSets_isAlgebraOfSets`, structure `AlgebraOfSets`,
+      notation `algebraOfSetsType`
+    * mixin `hasMeasurableCountableUnion`
+    * structure `SigmaRing`, structure `SigmaRing`, notation `sigmaRingType`
+    * factory `isSigmaRing`
+    * structure `Measurable`, notation `measurableType`
+    * factories `isRingOfSets`, `isRingOfSets_setY`, `isAlgebraOfSets`,
+      `isAlgebraOfSets_setD`, `isMeasurable`
+    * lemmas `bigsetU_measurable`, `fin_bigcup_measurable`, `measurableD`,
+      `seqDU_measurable`, ` measurableC`, `bigsetI_measurable`, `fin_bigcap_measurable`,
+      `measurableID`, `bigcup_measurable`, `bigcap_measurable`, `bigcapT_measurable`,
+      `countable_measurable`, `sigmaRingType_lambda_system`, `countable_bigcupT_measurable`,
+      `bigcupT_measurable_rat`, `sigma_algebra_measurable`, `bigcap_measurableType`
+    * definition `discrete_measurable`
+    * lemmas `discrete_measurable0`, `discrete_measurableC`, `discrete_measurableU`
+    * definitions `sigma_display`, `g_sigma_algebraType`
+    * lemmas `sigma_algebraC`
+    * notations `.-sigma`, `.-sigma.-measurable`
+    * lemma `measurable_g_measurableTypeE`
+    * definition `preimage_set_system`
+    * lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`,
+      `preimage_set_system_id`, `sigma_algebra_preimage`
+    * definition `image_set_system`
+    * lemmas `sigma_algebra_image`, `g_sigma_preimageE`
+    * definition `subset_sigma_subadditive`
+    * lemmas `big_trivIset`
+    * definition `covered_by`
+    * lemmas `covered_bySr`, `covered_byP`, `covered_by_finite`, `covered_by_countable`,
+      `measurable_uncurry`
+    * definition `g_sigma_preimageU`
+    * lemmas `g_sigma_preimageU_comp`
+    * definition `measure_prod_display`
+    * notation `.-prod`, `.-prod.-measurable`
+    * lemmas `measurableX`, `measurable_prod_measurableType`,
+      `measurable_prod_g_measurableTypeR`, `measurable_prod_g_measurableType`
+    * definition `g_sigma_preimage`
+    * lemma `g_sigma_preimage_comp`
+    * definition `measure_tuple_display`
+    * definition `measure_dominates`, notation ``` `<< ```
+    * lemma `measure_dominates_trans`
+  + to `measure_theory/measure_function.v`:
+    * definitions `semi_additive2`, `semi_additive`, `semi_sigma_additive`,
+      `additive2`, `additive`, `sigma_additive`, `subadditive`,
+      `measurable_subset_sigma_subadditive`
+    * lemma `semi_additiveW`
+    * lemmas `semi_additiveE`, `semi_additive2E`, `additive2P`
+    * lemmas `semi_sigma_additive_is_additive`, `semi_sigma_additiveE`,
+      `sigma_additive_is_additive`
+    * mixin `isContent`, structure `Content`, notation `{content set _ -> \bar _}`
+    * lemma `content_inum_subproof`
+    * lemmas `measure0`, `measure_gt0`, `measure_semi_additive_ord`,
+      `measure_semi_additive_ord_I`, `content_fin_bigcup`, `measure_semi_additive2`
+    * lemmas `measureU`, `measure_bigsetU`, `measure_fin_bigcup`,
+      `measure_bigsetU_ord_cond`, `measure_bigsetU_ord`, `measure_fbigsetU`
+    * mixin `Content_isMeasure`
+    * structure `Measure`, notations `measure`,
+      `{measure set _ -> \bar _}`
+    * lemma `measure_inum_subproof`
+    * factory `isMeasure`, lemma `eq_measure`
+    * lemmma `measure_semi_bigcup`
+    * lemmas `measure_sigma_additive`, `measure_bigcup`
+    * definition `msum`
+    * definition `mzero`, lemma `msum_mzero`
+    * definition `measure_add`, `measure_addE`
+    * definition `mscale`
+    * definition `mseries`
+    * definition `pushforward`
+    * module `SetRing`
+    * notations `.-ring`, `.-ring.-measurable`
+    * lemmas `le_measure`, `measure_le0`
+    * lemmas `content_subadditive`, `content_sub_fsum`
+    * lemmas `content_ring_sup_sigma_additive`, `content_ring_sigma_additive`
+    * lemmas `ring_sigma_subadditive`, `ring_semi_sigma_additive`,
+      `semiring_sigma_additive`
+    * factory `Content_SigmaSubAdditive_isMeasure`
+    * lemma `measure_sigma_subadditive`
+    * lemma `measure_sigma_subadditive_tail`
+    * definition `fin_num_fun`
+    * lemmas `fin_num_fun_lty`, `lty_fin_num_fun`
+    * definitions `sfinite_measure`, `sigma_finite`
+    * lemma `fin_num_fun_sigma_finite`
+    * definition `mrestr`
+    * lemma `sfinite_measure_sigma_finite`
+    * mixin `isSFinite`, structure `SFiniteMeasure`,
+      notation `{sfinite_measure set _ -> \bar _}`
+    * mixin `isSigmaFinite`, structure `SigmaFiniteContent`,
+      notation `sigma_finite_content`, `{sigma_finite_content set _ -> \bar _}`
+    * structure `SigmaFiniteMeasure`, notations `sigma_finite_measure`,
+      `{sigma_finite_measure set _ -> \bar _}`
+    * factory `Measure_isSigmaFinite`
+    * lemmas `sigma_finite_mzero`, `sfinite_mzero`
+    * mixin `isFinite`, structures `FinNumFun`, `FiniteMeasure`,
+      notation `{finite_measure set _ -> \bar _}`
+    * factories `Measure_isFinite`, `Measure_isSFinite`
+    * definition `sfinite_measure_seq`
+    * lemma `sfinite_measure_seqP`
+    * definition `mfrestr`
+    * lemmas `measureIl`, `measureIr`, `subset_measure0`
+    * lemmas `measureDI`, `measureD`, `measureU2`
+    * lemmas `measureUfinr`, `measureUfinl`, `null_set_setU`, `measureU0`
+    * lemma `eq_measureU`
+    * lemma `g_sigma_algebra_measure_unique_trace`
+    * lemmas `nondecreasing_cvg_mu`, `nonincreasing_cvg_mu`
+    * definition `lim_sup_set`
+    * lemmas `lim_sup_set_ub`, `lim_sup_set_cvg`
+    * lemma `lim_sup_set_cvg0`
+    * theorem `Boole_inequality`
+    * lemma `sigma_finiteP`
+    * theorem `generalized_Boole_inequality`
+    * lemmas `g_sigma_algebra_measure_unique_cover`, `g_sigma_algebra_measure_unique`
+    * lemma `measure_unique`
+  + to `measure_theory/counting_measure.v`:
+    * definition `counting`
+    * lemma `sigma_finite_counting`
+  + to `measure_theory/dirac_measure.v`:
+    * definition `dirac`, notation `\d_`
+    * lemmas `finite_card_sum`, `finite_card_dirac`, `infinite_card_dirac `
+  + to `measure_theory/probability_measure.v`:
+    * mixin `isSubProbability`, structure `SubProbability`, notation `subprobability`
+    * factory `Measure_isSubProbability`
+    * mixin `isProbability`, structure `Probability`, notation `probability`
+    * lemmas `probability_le1`, `probability_setC`
+    * factory `Measure_isProbability`
+    * definition `mnormalize`
+    * lemmas `mnormalize_id`
+    * definitions `mset`, `pset`, `pprobability`
+    * lemmas `lt0_mset`, `gt1_mset`
+  + to `measure_theory/measure_negligible.v`:
+    * definition `negligible`, notation `.-negligible`
+    * lemmas `negligibleP`, `negligible_set0`, `measure_negligible`, `negligibleS`,
+      `negligibleI`
+    * definition `measure_is_complete`
+    * lemmas `negligibleU`, `negligible_bigsetU`, `negligible_bigcup`
+    * definition `almost_everywhere`, `ae_filter_ringOfSetsType`,
+      `ae_properfilter_algebraOfSetsType`
+    * definition `ae_eq`, notations `{ae _, _}`, `\forall _ \ae _, _`,
+      `_ = _ [%ae _ in _]`, `_ = _ %[ae _]`
+    * lemmas `measure0_ae`, `aeW`
+    * instance `ae_eq_equiv`
+    * instances `comp_ae_eq`, `comp_ae_eq2`, `comp_ae_eq2'`, `sub_ae_eq2`
+    * lemmas `ae_eq0`, `ae_eq_refl`, `ae_eq_comp`, `ae_eq_comp2`,
+      `ae_eq_funeposneg`, `ae_eq_sym`, `ae_eq_trans`, `ae_eq_sub`,
+      `ae_eq_mul2r`, `ae_eq_mul2l`, `ae_eq_mul1l`, `ae_eq_abse`, `ae_foralln`
+    * lemmas `ae_eq_subset`, `ae_eqe_mul2l`
+    * lemma `measure_dominates_ae_eq`
+  + to `measure_theory/measure_extension.v`:
+    * definitions `sigma_subadditive`, `subset_sigma_subadditive`
+    * mixin `isOuterMeasure`, structure `OuterMeasure`
+    * notation `{outer_measure set _ -> \bar _}`
+    * factory `isSubsetOuterMeasure`
+    * lemmas `outer_measure_sigma_subadditive_tail`, `outer_measure_subadditive`,
+      `outer_measureU2`, `le_outer_measureIC`
+    * definition `caratheodory_measurable`, notation `.-caratheodory`
+    * lemma `le_caratheodory_measurable`
+    * lemmas `outer_measure_bigcup_lim`, `caratheodory_measurable_set0`,
+      `caratheodory_measurable_setC`, `caratheodory_measurable_setU_le`,
+      `caratheodory_measurable_setU`, `caratheodory_measurable_bigsetU`,
+      `caratheodory_measurable_setI`, `caratheodory_measurable_setD`,
+      `disjoint_caratheodoryIU`, `caratheodory_additive`, `caratheodory_lime_le`,
+      `caratheodory_measurable_trivIset_bigcup`, `caratheodory_measurable_bigcup`
+    * definition `caratheodory_type`, notation `.-cara.-measurable`
+    * definition `caratheodory_display`, notation `.-cara`
+    * lemmas `caratheodory_measure0`, `caratheodory_measure_ge0`,
+      `caratheodory_measure_sigma_additive`, `measure_is_complete_caratheodory`
+    * definition `measurable_cover`, lemmas `cover_measurable`, `cover_subset`
+    * definition `mu_ext`, notation `^*`
+    * lemmas `le_mu_ext`, `mu_ext_ge0`, `mu_ext0`, `mu_ext_sigma_subadditive`
+    * lemmas `Rmu_ext`, `measurable_mu_extE`, `measurable_Rmu_extE`
+    * lemma `sub_caratheodory`
+    * definition `measure_extension`
+    * lemmas `measure_extension_sigma_finite`, `measure_extension_unique`
+    * lemma `caratheodory_measurable_mu_ext`
+    * definition `completed_measure_extension`
+    * lemma `completed_measure_extension_sigma_finite`
+  + to `measure_theory/measurable_function.v`:
+    * mixin `isMeasurableFun`, structure `MeasurableFun`, notations `{mfun _ >-> _}`,
+      `[mfun of _]`
+    * lemmas `measurable_funP`, `measurable_funPTI`
+    * definitions `mfun`, `mfun_key`, canonical `mfun_keyed`
+    * lemmas `measurable_id`, `measurable_comp`, `eq_measurable_fun`,
+      `measurable_fun_eqP`, `measurable_cst`, `measurable_fun_bigcup`,
+      `measurable_funU`, `measurable_funS`, `measurable_fun_if`,
+      `measurable_fun_set0`, `measurable_fun_set1`
+    * definitions `mfun_Sub_subproof`, `mfun_Sub`
+    * lemmas `mfun_rect`, `mfun_val`, `mfuneqP`
+    * lemmas `measurableT_comp`, `measurable_funTS`, `measurable_restrict`,
+      `measurable_restrictT`, `measurable_fun_ifT`, `measurable_fun_bool`,
+      `measurable_and`, `measurable_neg`, `measurable_or`
+    * lemmas `preimage_set_system_measurable_fun`, `measurability`
+    * lemmas `measurable_fun_pairP`, `measurable_fun_pair`
+    * lemmas `measurable_fst`, `measurable_snd`, `measurable_swap`
+    * lemmas `measurable_tnth`, `measurable_fun_tnthP`, `measurable_cons`
+    * lemmas `measurable_behead`, `measurable_fun_if_pair`
+    * lemmas `pair1_measurable`, `pair2_measurable`
+    * lemmas `measurable_xsection`, `measurable_ysection`,
+      `measurable_fun_pair1`, `measurable_fun_pair2`
+
+- in `constructive_ereal.v`:
+  + instance of `Monoid.isLaw` for `mine`
+
+- in `probability.v`:
+  + definition `poisson_pmf`, lemmas `poisson_pmf_ge0`, `measurable_poisson_pmf`,
+  + definition `poisson_prob`
+
+- in `measurable_function.v`:
+  + lemma `measurable_funS`: implicits changed
 
 ### Renamed
 - in `set_interval.v`:
@@ -162,6 +499,9 @@
   + `weak_sep_nbhsE` -> `initial_sep_nbhsE`
   + `weak_sep_openE` -> `initial_sep_openE`
   + `join_product_weak` -> `join_product_initial`
+- in set_interval.v
+  + `itv_is_ray` -> `itv_is_open_unbounded`
+  + `itv_is_bd_open` -> `itv_is_oo`
 
 ### Generalized
 
diff --git a/reals/real_interval.v b/reals/real_interval.v
index 4beab5562..3aa9ddb3a 100644
--- a/reals/real_interval.v
+++ b/reals/real_interval.v
@@ -249,6 +249,40 @@ Qed.
 
 End itv_realDomainType.
 
+(* generalization of
+  a < b -> `]a, b] `<=` `]r, +oo[ -> `[a, b] `<=` `[r, +oo[. *)
+Lemma subset_itvoSo_cSc {R : realFieldType} (r a : R) (b x : itv_bound R) :
+  (BRight a < b)%O ->
+  (b <= x)%O ->
+  [set` Interval (BRight a)(*open*) b]
+    `<=` [set` Interval (BRight r)(*open*) x] ->
+  [set` Interval (BLeft a)(*closed*) b]
+    `<=` [set` Interval (BLeft r)(*closed*) x].
+Proof.
+move: b => [[|]b ab bx abrx|[//|/= _]]; rewrite ?bnd_simp.
+- apply: subset_itv => //=; rewrite bnd_simp leNgt; apply/negP => ar.
+  have rb : (r <= b)%O.
+    rewrite leNgt; apply/negP => br; have /= := abrx ((a + b) / 2).
+    rewrite !in_itv/= !midf_lt//= => /(_ isT).
+    by rewrite ltNge (le_trans _ (ltW br))//= midf_le// ltW.
+  have /abrx /= : (a + r) / 2 \in `]a, b[.
+    by rewrite in_itv/= midf_lt//= (lt_le_trans _ rb)// midf_lt.
+  by rewrite in_itv/= ltNge midf_le// ltW.
+- apply: subset_itv => //=; rewrite bnd_simp leNgt; apply/negP => ar.
+  have rb : r <= b.
+    rewrite leNgt; apply/negP => br; have /= := abrx ((a + b) / 2).
+    rewrite !in_itv/= midf_lt// (midf_le (ltW _))// => /(_ isT).
+    by rewrite ltNge (le_trans _ (ltW br))//= midf_le// ltW.
+  have /abrx /= : (a + r) / 2 \in `]a, b].
+    by rewrite in_itv/= midf_lt//= (le_trans _ rb)// (midf_le (ltW _)).
+  by rewrite in_itv/= ltNge midf_le// ltW.
+- move/eqP => ->{x} ar.
+  apply/subset_itvr; rewrite bnd_simp leNgt; apply/negP => ra.
+  have /= := ar ((a + r) / 2).
+  rewrite !in_itv/= !andbT midf_lt// => /(_ isT).
+  by rewrite ltNge  midf_le// ltW.
+Qed.
+
 Section set_ereal.
 Context (R : realType) T (f g : T -> \bar R).
 Local Open Scope ereal_scope.
diff --git a/theories/charge.v b/theories/charge.v
index 7f1a4f6b1..698584f58 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -1890,7 +1890,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).
@@ -2002,7 +2002,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 b83b6a397..4cf211786 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -839,6 +839,298 @@ 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.
+by apply: cvg_comp; [apply: cvgr_idn|apply: cvg_addrl].
+Qed.
+
+Let fin_num_intfG (c d : R) : `]c, d] `<=` `]a, +oo[ ->
+  \int[mu]_(x in `]c, d]) (f x * G x)%:E \is a fin_num.
+Proof.
+have [dc _|cd cday] := leP d c.
+  by rewrite set_itv_ge ?bnd_simp -?leNgt// integral_set0.
+rewrite integral_itv_obnd_cbnd; last exact: measurable_funS mfG.
+apply: integrable_fin_num => //=.
+apply: continuous_compact_integrable; first exact: segment_compact.
+by apply: continuous_subspaceW cfG; exact: subset_itvoSo_cSc.
+Qed.
+
+Let sum_integral_limn :
+  \sum_(0 <= i <oo)
+    \int[mu]_(x in `](a + i.-1%:R), (a + i%:R)]) (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 `](a + i.-1%:R), (a + i%:R)])
+                          (f x * G x)%:E).
+Proof.
+apply/congr_lim/funext => -[|[|n]].
+  by rewrite !big_nil/= oppr0 !addr0 subrr.
+  by rewrite 2!big_nat1/= addr0 subrr add0r set_itvoc0 2!integral_set0 oppe0.
+rewrite big_nat_recl// [in RHS]big_nat_recl//=.
+rewrite addr0 set_itvoc0 2!integral_set0 2!add0r.
+have mFg' i : measurable_fun `](a + i%:R), (a + i.+1%:R)]
+    (fun x => F x * g x)%R.
+  apply: measurable_funS mFg => //.
+  by apply/subset_itv => //; rewrite bnd_simp lerDl.
+have mfG' i : measurable_fun `](a + i%:R), (a + i.+1%:R)]
+    (fun x => f x * G x)%R.
+  apply: measurable_funS mfG => //.
+  by apply/subset_itv => //; rewrite bnd_simp lerDl.
+under eq_bigr => i _.
+  rewrite integral_itv_obnd_cbnd//.
+  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; last by rewrite lerDl.
+    by rewrite ltrD2l ltr_nat.
+  - apply: continuous_subspaceW cg.
+    by apply/subset_itv => //; rewrite bnd_simp lerDl.
+  - apply: derivable_oy_continuousWoo Goy; last by rewrite lerDl.
+    by rewrite ltrD2l ltr_nat.
+  over.
+rewrite big_split/=.
+under eq_bigr do rewrite EFinB.
+rewrite telescope_sume => [|//|//]; rewrite addr0; congr +%E.
+rewrite sumeN//.
+- congr (- _).
+  by apply: eq_bigr => k _; rewrite integral_itv_obnd_cbnd.
+- move=> x y _ _; rewrite fin_num_adde_defl//.
+  rewrite -integral_itv_obnd_cbnd//= fin_num_intfG//.
+  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.
+rewrite seqDU_bigcup_eq.
+rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight.
+- under eq_eseriesr do rewrite seqDUE.
+  under [in RHS]eq_eseriesr do rewrite seqDUE.
+  rewrite [LHS]sum_integral_limn; apply: cvg_lim => //.
+  apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo.
+  apply: cvgeN.
+  apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x.
+  move=> 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 -integralN/=; last first.
+  rewrite fin_num_adde_defr//.
+  under eq_integral do rewrite (le0_funeposE fG0) 1?inE//.
+  by rewrite integral_cst// mul0e.
+rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq.
+rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight.
+- under eq_eseriesr do rewrite seqDUE.
+  under [in RHS]eq_eseriesr do rewrite seqDUE.
+  rewrite [LHS]sum_integral_limn; apply: cvg_lim => //.
+  apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo.
+  rewrite [X in X x @[x --> _] --> _](_ : _ = fun x => \sum_(0 <= i < x)
+      \int[mu]_(x in `](a + i.-1%:R), (a + i%:R)]) (- (f x * G x))%:E);
+      last first.
+    apply: funext => n; rewrite -sumeN; last first.
+      move=> x y _ _; rewrite fin_num_adde_defl//.
+      apply: fin_num_intfG => //.
+      by apply/subset_itv; rewrite bnd_simp//= lerDl.
+    apply: eq_bigr => -[_|m _].
+      by rewrite addr0 set_itvxx 2!integral_set0 oppe0.
+    have ? :
+      measurable_fun `](a + m%:R), (a + m.+1%:R)] (fun x => (f x * G x)%R).
+      apply: measurable_funS mfG => //.
+      by apply: subset_itv => //; rewrite bnd_simp lerDl.
+    under [RHS]eq_integral do rewrite EFinN.
+    rewrite [in RHS]integralN//.
+    apply: fin_num_adde_defr => /=; apply: integrable_pos_fin_num => //=.
+    apply/integrableP; split; first exact/measurable_EFinP.
+    rewrite integral_fin_num_abs// fin_num_intfG//.
+    by apply: subset_itv => //; rewrite bnd_simp lerDl.
+  apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x.
+  move=> anx; rewrite EFinN oppe_ge0.
+  apply: fG0; rewrite inE/=.
+  by apply: subset_itv anx; rewrite bnd_simp// lerDl.
+- by move=> k; apply: measurableD => //; exact: bigsetU_measurable.
+- exact/measurable_EFinP/measurableT_comp.
+- by move=> ? ?; rewrite EFinN oppe_ge0 fG0// inE.
+- by move=> k; apply: measurableD => //; exact: 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 [/derivable_within_continuous + _] := Foy.
+  by rewrite continuous_open_subspace => [|//]; apply.
+have /continuous_within_itvcyP[+ _] := cg.
+by apply; rewrite inE/= in ax.
+Qed.
+
+Let mfG : measurable_fun `]a, +oo[ (f * G)%R.
+Proof.
+apply: subspace_continuous_measurable_fun => //.
+rewrite continuous_open_subspace// => x ax.
+apply: cvgM.
+  have /continuous_within_itvcyP[+ _] := cf.
+  by apply; rewrite inE/= in ax.
+have [/derivable_within_continuous + _] := Goy.
+by rewrite continuous_open_subspace => [|//]; apply.
+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/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/=.
+  by move=> ?/= ?; rewrite mulNr EFinN oppe_ge0 Fg0//= 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_RcontinuousN.
+- by move=> ? ?; rewrite fctE derive1N ?Ff => [//|//|]; apply: Foy.1.
+- by [].
+- by [].
+- by [].
+- 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 oppeK.
+  by under eq_integral do rewrite mulNr EFinN.
+- by move=> ?; apply: cvgN; exact: cf.
+- exact: derivable_oy_RcontinuousN.
+- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.
+- by [].
+- by [].
+- by [].
+- 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.
@@ -1028,24 +1320,6 @@ Unshelve. all: end_near. Qed.
 
 End integration_by_substitution_preliminaries.
 
-(* PR in progress *)
-Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
-    (l : set_system T) :
-  f x @[x --> -oo] --> l <-> (f \o -%R) x @[x --> +oo] --> l.
-Proof.
-have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
-by rewrite (eq_cvg -oo _ f_opp) [in X in X <-> _]fmap_comp ninftyN.
-Qed.
-
-(* PR in progress *)
-Lemma cvgy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
-    (l : set_system T) :
-  f x @[x --> +oo] --> l <-> (f \o -%R) x @[x --> -oo] --> l.
-Proof.
-have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
-by rewrite (eq_cvg +oo _ f_opp) [in X in X <-> _]fmap_comp ninfty.
-Qed.
-
 Section integration_by_substitution.
 Local Open Scope ereal_scope.
 Context {R : realType}.
@@ -1298,8 +1572,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.
@@ -1326,7 +1599,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 => //.
@@ -1379,7 +1652,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 2eaa9643c..12c84bf58 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -898,8 +898,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 a7a232c7e..a72be77ab 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
@@ -142,10 +142,10 @@ 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.
   - 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.
@@ -160,12 +160,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.
@@ -328,7 +328,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.
@@ -1036,7 +1037,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 3622ce6a1..faae353ad 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 14da12b36..6fbe6fc19 100644
--- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v
+++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v
@@ -458,8 +458,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.
@@ -554,8 +554,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 422a97b53..4696383d3 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 56c294b87..b5291dbe4 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 1acb9d7af..2978e5397 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -1124,6 +1124,13 @@ Definition derivable_Nyo_Lcontinuous (f : R -> V) (x : R) :=
 Definition derivable_oy_Rcontinuous (f : R -> V) (x : R) :=
   {in `]x, +oo[, forall x, derivable f x 1} /\ f @ x^'+ --> f x.
 
+Lemma derivable_oy_RcontinuousN (f : R -> V) (x : R) :
+  derivable_oy_Rcontinuous f x -> derivable_oy_Rcontinuous (- f) x.
+Proof.
+case=> /= derF Fa; split; last exact: cvgN.
+by move=> /= ? ?; exact/derivableN/derF.
+Qed.
+
 Lemma derivable_oy_Rcontinuous_within_itvcy (f : R -> V) (x : R) :
   derivable_oy_Rcontinuous f x -> {within `[x, +oo[, continuous f}.
 Proof.