Generalize integration_by_parts

CHANGELOG_UNRELEASED.md

@@ -72,6 +72,18 @@
            `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`
+
+- in `real_interval.v`:
+  + lemma `subset_itvoSo_cSc`
+
 ### Changed
 
 - in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
@@ -324,6 +336,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`:

reals/real_interval.v

@@ -251,6 +251,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.

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 =