improvements

theories/kernel.v

@@ -132,7 +132,7 @@ Lemma measurable_fun_kseries (U : set Y) :
   measurable U -> measurable_fun [set: X] (kseries ^~ U).
 Proof.
 move=> mU.
-by apply: ge0_emeasurable_fun_sum => // n; exact/measurable_kernel.
+by apply: ge0_emeasurable_fun_sum => // n _; exact/measurable_kernel.
 Qed.
 
 HB.instance Definition _ :=
@@ -506,7 +506,7 @@ Variable k : X * Y -> \bar R.
 
 Lemma measurable_fun_xsection_integral
     (l : X -> {measure set Y -> \bar R})
-    (k_ : ({nnsfun [the measurableType _ of X * Y] >-> R})^nat)
+    (k_ : {nnsfun (X * Y) >-> R}^nat)
     (ndk_ : nondecreasing_seq (k_ : (X * Y -> R)^nat))
     (k_k : forall z, (k_ n z)%:E @[n --> \oo] --> k z) :
   (forall n r,
@@ -585,7 +585,7 @@ have [l_ hl_] := sfinite_kernel l.
 rewrite (_ : (fun x => _) = (fun x =>
     mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first.
   by apply/funext => x; rewrite hl_//; exact/measurable_xsection.
-apply: ge0_emeasurable_fun_sum => // m.
+apply: ge0_emeasurable_fun_sum => // m _.
 by apply: measurable_fun_xsection_finite_kernel => // /[!inE].
 Qed.
 
@@ -614,7 +614,7 @@ Qed.
 HB.instance Definition _ := isKernel.Build _ _ _ _ _ (kdirac mf)
   measurable_fun_kdirac.
 
-Let kdirac_prob x : kdirac mf x setT = 1.
+Let kdirac_prob x : kdirac mf x [set: Y] = 1.
 Proof. by rewrite /kdirac/= diracT. Qed.
 
 HB.instance Definition _ := Kernel_isProbability.Build _ _ _ _ _
@@ -717,46 +717,14 @@ HB.instance Definition _ t :=
   Kernel_isFinite.Build _ _ _ _ R (kadd k1 k2) kadd_finite_uub.
 End fkadd.
 
-Lemma measurable_fun_mnormalize d d' (X : measurableType d)
-    (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) :
-  measurable_fun [set: X] (fun x =>
-    [the probability _ _ of mnormalize (k x) point] : pprobability Y R).
-Proof.
-apply: (@measurability _ _ _ _ _ _
-  (@pset _ _ _ : set (set (pprobability Y R)))) => //.
-move=> _ -[_ [r r01] [Ys mYs <-]] <-.
-rewrite /mnormalize /mset /preimage/=.
-apply: emeasurable_fun_infty_o => //.
-rewrite /mnormalize/=.
-rewrite (_ : (fun x => _) = (fun x => if (k x setT == 0) || (k x setT == +oo)
-    then \d_point Ys else k x Ys * ((fine (k x setT))^-1)%:E)); last first.
-  by apply/funext => x/=; case: ifPn.
-apply: measurable_fun_if => //.
-- apply: (measurable_fun_bool true) => //.
-  rewrite (_ : _ @^-1` _ = [set t | k t setT == 0] `|`
-                           [set t | k t setT == +oo]); last first.
-    by apply/seteqP; split=> x /= /orP//.
-  by apply: measurableU; exact: kernel_measurable_eq_cst.
-- apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel.
-  apply/EFin_measurable_fun; rewrite setTI.
-  apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]).
-  + exact: open_measurable.
-  + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey.
-  + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0.
-    exact: inv_continuous.
-  + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel.
-Qed.
-
 Section knormalize.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variable f : R.-ker X ~> Y.
 
 Definition knormalize (P : probability Y R) : X -> {measure set Y -> \bar R} :=
-  fun x => [the measure _ _ of mnormalize (f x) P].
-
-Variable P : probability Y R.
+  fun x => mnormalize (f x) P.
 
-Let measurable_fun_knormalize U :
+Let measurable_knormalize (P : probability Y R) U :
   measurable U -> measurable_fun [set: X] (knormalize P ^~ U).
 Proof.
 move=> mU; rewrite /knormalize/= /mnormalize /=.
@@ -773,7 +741,7 @@ apply: measurable_fun_if => //.
 - apply: (@measurable_funS _ _ _ _ setT) => //.
   exact: kernel_measurable_fun_eq_cst.
 - apply: emeasurable_funM.
-    by have := measurable_kernel f U mU; exact: measurable_funS.
+    exact: measurable_funS (measurable_kernel f U mU).
   apply/EFin_measurable_fun.
   apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]) => //.
   + exact: open_measurable.
@@ -786,17 +754,48 @@ apply: measurable_fun_if => //.
     by have := measurable_kernel f _ measurableT; exact: measurable_funS.
 Qed.
 
-HB.instance Definition _ := isKernel.Build _ _ _ _ R (knormalize P)
-  measurable_fun_knormalize.
+HB.instance Definition _ (P : probability Y R) :=
+  isKernel.Build _ _ _ _ R (knormalize P) (measurable_knormalize P).
 
-Let knormalize1 x : knormalize P x [set: Y] = 1.
+Let knormalize1 (P : probability Y R) x : knormalize P x [set: Y] = 1.
 Proof. by rewrite /knormalize/= probability_setT. Qed.
 
-HB.instance Definition _ :=
-  @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) knormalize1.
+HB.instance Definition _ (P : probability Y R):=
+  @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) (knormalize1 P).
 
 End knormalize.
 
+(* TODO: useful? *)
+Lemma measurable_fun_mnormalize d d' (X : measurableType d)
+    (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) :
+  measurable_fun [set: X] (fun x =>
+    [the probability _ _ of mnormalize (k x) point] : pprobability Y R).
+Proof.
+apply: (@measurability _ _ _ _ _ _
+  (@pset _ _ _ : set (set (pprobability Y R)))) => //.
+move=> _ -[_ [r r01] [Ys mYs <-]] <-.
+rewrite /mnormalize /mset /preimage/=.
+apply: emeasurable_fun_infty_o => //.
+rewrite /mnormalize/=.
+rewrite (_ : (fun x => _) = (fun x => if (k x setT == 0) || (k x setT == +oo)
+    then \d_point Ys else k x Ys * ((fine (k x setT))^-1)%:E)); last first.
+  by apply/funext => x/=; case: ifPn.
+apply: measurable_fun_if => //.
+- apply: (measurable_fun_bool true) => //.
+  rewrite (_ : _ @^-1` _ = [set t | k t setT == 0] `|`
+                           [set t | k t setT == +oo]); last first.
+    by apply/seteqP; split=> x /= /orP//.
+  by apply: measurableU; exact: kernel_measurable_eq_cst.
+- apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel.
+  apply/EFin_measurable_fun; rewrite setTI.
+  apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]).
+  + exact: open_measurable.
+  + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey.
+  + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0.
+    exact: inv_continuous.
+  + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel.
+Qed.
+
 Section kcomp_def.
 Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2)
   (Z : measurableType d3) (R : realType).

theories/lebesgue_integral.v

@@ -1968,15 +1968,30 @@ move=> fs mh; under eq_fun do rewrite fsbig_finite//.
 exact: emeasurable_fun_sum.
 Qed.
 
-Lemma ge0_emeasurable_fun_sum D (h : nat -> (T -> \bar R)) :
-  (forall k x, 0 <= h k x) -> (forall k, measurable_fun D (h k)) ->
-  measurable_fun D (fun x => \sum_(i <oo) h i x).
-Proof.
-move=> h0 mh; rewrite [X in measurable_fun _ X](_ : _ =
-    (fun x => limn_esup (fun n => \sum_(0 <= i < n) h i x))); last first.
+Lemma ge0_emeasurable_fun_sum D (h : nat -> (T -> \bar R)) (P : pred nat) :
+  (forall k x, D x -> P k -> 0 <= h k x) -> (forall k, P k -> measurable_fun D (h k)) ->
+  measurable_fun D (fun x => \sum_(i <oo | i \in P) h i x).
+Proof.
+Proof.
+move=> h0 mh.
+move=> mD; move: (mD).
+apply/(@measurable_restrict _ _ _ _ _ setT) => //.
+rewrite [X in measurable_fun _ X](_ : _ =
+  (fun x => \sum_(0 <= i <oo | i \in P) (h i \_ D) x)); last first.
+  apply/funext => x/=; rewrite /patch; case: ifPn => // xD.
+  by rewrite eseries0.
+rewrite [X in measurable_fun _ X](_ : _ =
+    (fun x => limn_esup (fun n => \sum_(0 <= i < n | P i) (h i) \_ D x))); last first.
   apply/funext=> x; rewrite is_cvg_limn_esupE//.
-  exact: is_cvg_ereal_nneg_natsum.
-by apply: measurable_fun_limn_esup => k; exact: emeasurable_fun_sum.
+  apply: is_cvg_nneseries_cond => n Pn; rewrite patchE.
+  by case: ifPn => // xD; rewrite h0//; exact/set_mem.
+apply: measurable_fun_limn_esup => k.
+under eq_fun do rewrite big_mkcond.
+apply: emeasurable_fun_sum => n.
+have [|] := boolP (n \in P).
+  rewrite /in_mem/= => Pn; rewrite Pn.
+  by apply/(measurable_restrict (h n)) => //; exact: mh.
+by rewrite /in_mem/= => /negbTE ->.
 Qed.
 
 Lemma emeasurable_funB D f g :
@@ -5261,7 +5276,7 @@ rewrite ge0_integralZl//; last by rewrite lee_fin.
 - by move=> y _; rewrite lee_fin.
 Qed.
 
-Lemma sfun_measurable_fun_fubini_tonelli_F : measurable_fun setT F.
+Lemma sfun_measurable_fun_fubini_tonelli_F : measurable_fun [set: T1] F.
 Proof.
 rewrite sfun_fubini_tonelli_FE//; apply: emeasurable_fun_fsum => // r.
 exact/measurable_funeM/measurable_fun_xsection.
@@ -5702,8 +5717,8 @@ transitivity (\sum_(n <oo) \int[s1 n]_x \sum_(m <oo) \int[s2 m]_y f (x, y)).
         fun x => \sum_(n <oo) \int[s2 n]_y f (x, y)); last first.
       apply/funext => x.
       by rewrite ge0_integral_measure_series//; exact/measurableT_comp.
-    apply: ge0_emeasurable_fun_sum; first by move=> k x; exact: integral_ge0.
-    by move=> k; apply: measurable_fun_fubini_tonelli_F.
+    apply: ge0_emeasurable_fun_sum; first by move=> k x *; exact: integral_ge0.
+    by move=> k _; exact: measurable_fun_fubini_tonelli_F.
   apply: eq_eseriesr => n _; apply: eq_integral => x _.
   by rewrite ge0_integral_measure_series//; exact/measurableT_comp.
 transitivity (\sum_(n <oo) \sum_(m <oo) \int[s1 n]_x \int[s2 m]_y f (x, y)).

theories/lebesgue_measure.v

@@ -1577,6 +1577,20 @@ move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->.
 - by rewrite preimage_setT setIT.
 Qed.
 
+Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g ->
+  measurable_fun D (fun x => f x <= g x).
+Proof.
+move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->.
+- under eq_fun do rewrite -subr_ge0.
+  rewrite preimage_true -preimage_itv_c_infty.
+  by apply: (measurable_funB mg mf) => //; exact: measurable_itv.
+- under eq_fun do rewrite leNgt -subr_gt0.
+  rewrite preimage_false set_predC setCK -preimage_itv_o_infty.
+  by apply: (measurable_funB mf mg) => //; exact: measurable_itv.
+- by rewrite preimage_set0 setI0.
+- by rewrite preimage_setT setIT.
+Qed.
+
 Lemma measurable_maxr D f g :
   measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \max g).
 Proof.

theories/measure.v

@@ -1177,6 +1177,36 @@ have [-> _|-> _|-> _ |-> _] := subset_set2 YT.
 - by rewrite -setT_bool preimage_setT setIT.
 Qed.
 
+Lemma measurable_fun_TF D (f : T1 -> bool) :
+  measurable (D `&` f @^-1` [set true]) ->
+  measurable (D `&` f @^-1` [set false]) ->
+  measurable_fun D f.
+Proof.
+move=> mT mF mD /= Y mY.
+have := @subsetT _ Y; rewrite setT_bool => YT.
+move: mY; have [-> _|-> _|-> _ |-> _] := subset_set2 YT.
+- by rewrite preimage0 ?setI0.
+- exact: mT.
+- exact: mF.
+- by rewrite -setT_bool preimage_setT setIT.
+Qed.
+
+Lemma measurable_and D (f : T1 -> bool) (g : T1 -> bool) :
+  measurable_fun D f -> measurable_fun D g ->
+  measurable_fun D (fun x => f x && g x).
+Proof.
+move=> mf mg mD; apply: measurable_fun_TF => //.
+- rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `&`
+                                      (D `&` g @^-1` [set true])); last first.
+    by rewrite setIACA setIid; congr (_ `&` _); apply/seteqP; split => x /andP.
+  by apply: measurableI; [exact: mf|exact: mg].
+- rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set false] `|`
+                                      (D `&` g @^-1` [set false])); last first.
+  rewrite -setIUr; congr (_ `&` _).
+  by apply/seteqP; split => x /=; case: (f x); case: (g x); tauto.
+- by apply: measurableU; [exact: mf|exact: mg].
+Qed.
+
 End measurable_fun.
 #[global] Hint Extern 0 (measurable_fun _ (fun=> _)) =>
   solve [apply: measurable_cst] : core.