Generalize lemma null_set_integral

CHANGELOG_UNRELEASED.md

@@ -44,6 +44,9 @@
   + definition `product_subprobability`
   + lemma `product_subprobability_setC`
 
+- in `lebesgue_integral_theory/lebesgue_integrable.v`
+  + lemma `null_set_integrable`
+
 - new file `lebesgue_integral_theory/giry.v`
   + definition `measure_eq`
   + definition `giry`
@@ -72,6 +75,9 @@
 - in `subspace_topology.v`:
   + definition `from_subspace`
 
+- in `lebesgue_integrable.v`:
+  + lemma `integrable_set0`
+
 ### Changed
 
 - in `charge.v`:
@@ -118,6 +124,8 @@
     `integration_by_substitution_onem`,
     `Rintegration_by_substitution_onem`
 
+- in `lebesgue_integral_theory/lebesgue_integrable.v`
+  + lemma `null_set_integral`
 
 ### Deprecated
 

theories/charge.v

@@ -1260,7 +1260,8 @@ rewrite (le_trans (le_abse_integral _ _ _))//=.
   by case/integrableP : intnf => /= + _; exact: measurable_funTS.
 rewrite le_eqVlt; apply/orP; left; apply/eqP.
 under eq_integral do rewrite abse_id.
-by apply: null_set_integral => //=; exact: integrableS intnf.
+apply: null_set_integral => //=.
+by apply: measurable_funTS; apply: measurable_int intnf.
 Qed.
 
 End dominates_induced.

theories/lebesgue_integral_theory/lebesgue_integrable.v

@@ -135,6 +135,12 @@ apply/integrableP; split=> //; under eq_integral do rewrite (gee0_abs (lexx 0)).
 by rewrite integral0.
 Qed.
 
+Lemma integrable_set0 f : mu.-integrable set0 f.
+Proof.
+apply/integrableP; split; first exact: measurable_fun_set0.
+by rewrite integral_set0.
+Qed.
+
 Lemma eq_integrable f g : {in D, f =1 g} -> mu_int f -> mu_int g.
 Proof.
 move=> fg /integrableP[mf fi]; apply/integrableP; split.
@@ -811,11 +817,19 @@ congr (_ - _); apply: ge0_negligible_integral => //; apply: (measurable_int mu).
 exact: integrable_funeneg.
 Qed.
 
+Lemma null_set_integrable (N : set T) (f : T -> \bar R) :
+  measurable N -> measurable_fun N f -> mu N = 0 -> mu.-integrable N f.
+Proof.
+move=> mN mf muN0.
+by rewrite (negligible_integrable mN) ?setDv//; exact: integrable_set0.
+Qed.
+
 Lemma null_set_integral (N : set T) (f : T -> \bar R) :
-  measurable N -> mu.-integrable N f ->
-  mu N = 0 -> \int[mu]_(x in N) f x = 0.
+  measurable N -> measurable_fun N f -> mu N = 0 -> \int[mu]_(x in N) f x = 0.
 Proof.
-by move=> mN intf ?; rewrite (negligible_integral mN mN)// setDv integral_set0.
+move=> mN mf N0.
+rewrite (negligible_integral mN mN) ?setDv ?integral_set0//.
+exact: null_set_integrable.
 Qed.
 
 End negligible_integral.

theories/probability.v

@@ -1876,8 +1876,8 @@ Lemma normal_prob_dominates : normal_prob `<< mu.
 Proof.
 apply/null_content_dominatesP=> A mA muA0; rewrite /normal_prob /normal_pdf.
 have [s0|s0] := eqVneq sigma 0.
-  apply: null_set_integral => //=; apply: (integrableS measurableT) => //=.
-  exact: integrable_indic_itv.
+  apply: null_set_integral => //=; apply: measurable_funTS => /=.
+  exact/measurable_EFinP/measurable_indic.
 apply/eqP; rewrite eq_le; apply/andP; split; last first.
   apply: integral_ge0 => x _.
   by rewrite lee_fin mulr_ge0 ?normal_peak_ge0 ?normal_fun_ge0.