generalize integral_setD_EFin (math-comp#1327)

* generalize integral_itv_obnd_cbnd, integral_itv_bndo_bndc

---------

Co-authored-by: Reynald Affeldt <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -18,6 +18,11 @@
 
 - in `topology.v`:
   + lemmas `in_nearW`, `open_in_nearW`
+- in `classical_sets.v`:
+  + lemma `not_setD1`
+
+- in `measure.v`:
+  + lemma `measurable_fun_set1`
 
 ### Changed
 
@@ -38,6 +43,10 @@
 - in `constructive_ereal.v`:
   + lemmas `maxeMr`, `maxeMl`, `mineMr`, `mineMr`:
     hypothesis weakened from strict inequality to large inequality
+- in `lebesgue_integral.v`:
+  + lemma `integral_setD1_EFin`
+  + lemmas `integral_itv_bndo_bndc`, `integral_itv_obnd_cbnd`
+  + lemmas `Rintegral_itv_bndo_bndc`, `Rintegral_itv_obnd_cbnd`
 
 ### Deprecated
 

classical/classical_sets.v

@@ -1192,6 +1192,9 @@ Proof. by rewrite /setY setDE setCK setIid setDE setIid setUv. Qed.
 Lemma setCYT A : ~` A `+` A = [set: T].
 Proof. by rewrite setYC setYCT. Qed.
 
+Lemma not_setD1 a A : ~ A a -> A `\ a = A.
+Proof. by move=> NDr; apply/setDidPl/disjoints_subset/subsetCr => _ ->. Qed.
+
 End basic_lemmas.
 #[global]
 Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core.

theories/ftc.v

@@ -456,15 +456,13 @@ have [xz|xz|->] := ltgtP x z; last by rewrite subrr normr0 ltW.
     exists `|b - z|; first by rewrite /= gtr0_norm ?subr_gt0.
     move=> y /= + yz.
     by rewrite ltr0_norm ?subr_lt0// gtr0_norm ?subr_gt0// opprB ltrBlDr subrK.
-  rewrite -opprB normrN Rintegral_itvB ?bnd_simp; last 3 first.
+  rewrite -opprB normrN Rintegral_itvB ?bnd_simp; [| |exact/ltW..]; last first.
     by apply: integrableS intf => //; apply: subset_itvl; exact: ltW.
-    exact/ltW.
-    exact/ltW.
+  have zxab : `[z, x] `<=` `[a, b] by apply: subset_itvScc; exact/ltW.
+  have intzxf : mu.-integrable `[z, x] (EFin \o f) by exact: integrableS intf.
   rewrite Rintegral_itv_obnd_cbnd//; last first.
-    by apply: integrableS intf => //; apply: subset_itvScc => //; exact/ltW.
-  have zxab : `[z, x] `<=` `[a, b].
-    by apply: subset_itvScc; rewrite bnd_simp; exact/ltW.
-  apply: (le_trans (le_normr_integral _ _)) => //; first exact: integrableS intf.
+    by apply: (@integrableS _ _ _ mu `[z, x]) => //; exact: subset_itv_oc_cc.
+  apply: (le_trans (le_normr_integral _ _)) => //.
   rewrite -(setIidl zxab) Rintegral_mkcondr/=.
   under eq_Rintegral do rewrite restrict_normr.
   apply/ltW/int_normr_cont => //.

theories/lebesgue_integral.v

@@ -6450,35 +6450,33 @@ rewrite ge0_integral_setU//=.
 Qed.
 
 Lemma integral_setD1_EFin (f : R -> R) r (D : set R) :
-  measurable D -> measurable_fun D f -> D 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.
 Proof.
-move=> mD mf Dr; rewrite -[in RHS](@setD1K _ r D)// integral_setU_EFin//.
-- by rewrite integral_set1// ?add0e.
-- exact: measurableD.
-- by rewrite setD1K.
-- by rewrite disj_set2E; apply/eqP/seteqP; split => // x [? []].
+move=> mD mfl; have [Dr|NDr] := pselect (D r); last by rewrite not_setD1.
+rewrite -[in RHS](@setD1K _ r D)// integral_setU_EFin//=.
+- 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) :
-  measurable_fun [set` Interval a (BRight r)] f ->
+  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.
 Proof.
 move=> mf; have [ar|ar] := leP a (BLeft r).
-- rewrite -[RHS](@integral_setD1_EFin _ r) ?setDitv1r//.
-  by rewrite /= in_itv /= lexx andbT {mf}; case: a ar => -[].
+- by rewrite -[RHS](@integral_setD1_EFin _ r) ?setDitv1r.
 - by rewrite !set_itv_ge// -leNgt// ltW.
 Qed.
 
 Lemma integral_itv_obnd_cbnd (r : R) (b : itv_bound R) (f : R -> R) :
-  measurable_fun [set` Interval (BLeft r) b] f ->
+  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.
 Proof.
 move=> mf; have [rb|rb] := leP (BRight r) b.
-- rewrite -[RHS](@integral_setD1_EFin _ r) ?setDitv1l//.
-  by rewrite /= in_itv /= lexx/= {mf}; case: b rb => -[].
+- by rewrite -[RHS](@integral_setD1_EFin _ r) ?setDitv1l.
 - by rewrite !set_itv_ge// -leNgt -?ltBRight_leBLeft// ltW.
 Qed.
 
@@ -6491,7 +6489,7 @@ Notation mu := (@lebesgue_measure R).
 Implicit Type f : R -> R.
 
 Lemma Rintegral_itv_bndo_bndc (a : itv_bound R) (r : R) f :
-  mu.-integrable [set` Interval a (BRight r)] (EFin \o f) ->
+  mu.-integrable [set` Interval a (BLeft r)] (EFin \o f) ->
    \int[mu]_(x in [set` Interval a (BLeft r)]) (f x) =
    \int[mu]_(x in [set` Interval a (BRight r)]) (f x).
 Proof.
@@ -6500,7 +6498,7 @@ by apply/EFin_measurable_fun; exact: (measurable_int mu).
 Qed.
 
 Lemma Rintegral_itv_obnd_cbnd (r : R) (b : itv_bound R) f :
-  mu.-integrable [set` Interval (BLeft r) b] (EFin \o f) ->
+  mu.-integrable [set` Interval (BRight r) b] (EFin \o f) ->
   \int[mu]_(x in [set` Interval (BRight r) b]) (f x) =
   \int[mu]_(x in [set` Interval (BLeft r) b]) (f x).
 Proof.
@@ -6522,18 +6520,16 @@ move=> itf; rewrite le_eqVlt => /predU1P[ax|ax xb].
   rewrite ax => _; rewrite [in X in _ - X]set_itv_ge ?bnd_simp//.
   by rewrite Rintegral_set0 subr0.
 rewrite (@itv_bndbnd_setU _ _ _ (BLeft x)); last 2 first.
-  by case: a ax {itf} => -[]//.
+  by case: a ax {itf} => -[].
   by rewrite (le_trans _ xb)// bnd_simp.
 rewrite Rintegral_setU_EFin//=.
 - rewrite addrAC Rintegral_itv_bndo_bndc//; last first.
-    by apply: integrableS itf => //; exact: subset_itvl.
+    apply: integrableS itf => //; apply: subset_itvl.
+    by rewrite (le_trans _ xb)// bnd_simp.
   rewrite subrr add0r Rintegral_itv_obnd_cbnd//.
-  apply: integrableS itf => //; apply: subset_itvr.
-  by case: a ax => -[].
-- rewrite -itv_bndbnd_setU//.
-    by case: a ax {itf} => -[]//.
-  by rewrite (le_trans _ xb)// bnd_simp.
-- apply/disj_setPS => y; rewrite /= !in_itv/= => -[/andP[_ yx] /andP[]].
+  by apply: integrableS itf => //; exact/subset_itvr/ltW.
+- by rewrite -itv_bndbnd_setU -?ltBRight_leBLeft// ltW.
+- apply/disj_setPS => y [/=]; rewrite 2!in_itv/= => /andP[_ yx] /andP[].
   by rewrite leNgt yx.
 Qed.
 

theories/measure.v

@@ -1582,6 +1582,10 @@ apply/seteqP; split=> [t /=| t /= [] [] ->//].
 by case: ifPn => ft; [left|right].
 Qed.
 
+Lemma measurable_fun_set1 a (f : T1 -> T2) :
+measurable_fun (set1 a) f.
+Proof. by move=> ? ? ?; rewrite set1I; case: ifP. Qed.
+
 End measurable_fun.
 #[global] Hint Extern 0 (measurable_fun _ (fun=> _)) =>
   solve [apply: measurable_cst] : core.