shorter measurability proofs

Author: affeldt-aist

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 _ :=
@@ -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.
 

theories/lebesgue_integral.v

@@ -1968,15 +1968,29 @@ 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.
+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 :
@@ -5702,8 +5716,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 _; apply: 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/prob_lang.v

@@ -115,6 +115,14 @@ Definition dep_uncurry (A : Type) (B : A -> Type) (C : Type) :
     (forall a : A, B a -> C) -> {a : A & B a} -> C :=
   fun f p => let (a, Ba) := p in f a Ba.
 
+(* TODO: move *)
+Lemma measurable_natmul {R : realType} D n :
+  measurable_fun D ((@GRing.natmul R)^~ n).
+Proof.
+under eq_fun do rewrite -mulr_natr.
+by do 2 apply: measurable_funM => //.
+Qed.
+
 Section bernoulli_pmf.
 Context {R : realType} (p : R).
 Local Open Scope ring_scope.
@@ -136,6 +144,12 @@ Qed.
 
 End bernoulli_pmf.
 
+Lemma measurable_bernoulli_pmf {R : realType} D n :
+  measurable_fun D (@bernoulli_pmf R ^~ n).
+Proof.
+by apply/measurable_funTS/measurable_fun_if => //=; exact: measurable_funB.
+Qed.
+
 Definition bernoulli {R : realType} (p : R) : set bool -> \bar R := fun A =>
   if (0 <= p <= 1)%R then \sum_(b \in A) (bernoulli_pmf p b)%:E else \d_false A.
 
@@ -243,33 +257,18 @@ Proof.
 apply: (@measurability _ _ _ _ _ _
   (@pset _ _ _ : set (set (pprobability _ R)))) => //.
 move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=.
-rewrite /bernoulli; have := @subsetT _ Ys; rewrite setT_bool => UT.
-have [->|->|->|->] /= := subset_set2 UT.
-- rewrite [X in measurable_fun _ X](_ : _ = cst 0%E)//.
-  by apply/funext => x/=; case: ifPn => // _; rewrite fsbig_set0.
-- rewrite [X in measurable_fun _ X](_ : _ =
-    (fun x => if 0 <= x <= 1 then x%:E else 0%E))//.
-    apply: measurable_fun_ifT => //=; apply: measurable_and => //;
-    apply: (measurable_fun_bool true) => //=.
-      rewrite (_ : _ @^-1` _ = `[0, +oo[%classic)//.
-      by apply/seteqP; split => [x|x] /=; rewrite in_itv/= andbT.
-    by rewrite (_ : _ @^-1` _ = `]-oo, 1]%classic).
-  apply/funext => x/=; case: ifPn => /= x01.
-    by rewrite fsbig_set1//= lee_fin; case/andP : x01.
-  by rewrite diracE memNset//.
-- rewrite [X in measurable_fun _ X](_ : _ =
-    (fun x => if 0 <= x <= 1 then (`1-x)%:E else 1%E))//.
-    apply: measurable_fun_ifT => //=.
-      apply: measurable_and => //; apply: (measurable_fun_bool true) => //=.
-        rewrite (_ : _ @^-1` _ = `[0, +oo[%classic)//.
-        by apply/seteqP; split => [x|x] /=; rewrite in_itv/= andbT.
-      by rewrite (_ : _ @^-1` _ = `]-oo, 1]%classic).
-    exact/EFin_measurable_fun/measurable_funB.
-  apply/funext => x/=; case: ifPn => /= x01.
-    by rewrite fsbig_set1//= lee_fin subr_ge0; case/andP : x01.
-  by rewrite diracE mem_set.
-- rewrite [X in measurable_fun _ X](_ : _ = cst 1%E)//; apply/funext => x/=.
-  by rewrite -setT_bool diracT; case: ifPn => // x01; rewrite bernoulli_pmf1.
+apply: measurable_fun_if => //=.
+  apply: measurable_and => //; apply: (measurable_fun_bool true) => //=.
+    rewrite (_ : _ @^-1` _ = `[0, +oo[%classic)//.
+    by apply/seteqP; split => [x|x] /=; rewrite in_itv/= andbT.
+  by rewrite (_ : _ @^-1` _ = `]-oo, 1]%classic).
+apply: (eq_measurable_fun (fun t =>
+    \sum_(b <- fset_set Ys) (bernoulli_pmf t b)%:E)).
+  move=> x /set_mem[_/= x01].
+  by rewrite fsbig_finite//=.
+apply: emeasurable_fun_sum => n.
+move=> k Ysk; apply/measurableT_comp => //.
+exact: measurable_bernoulli_pmf.
 Qed.
 
 Lemma measurable_bernoulli2 U : measurable U ->
@@ -296,6 +295,15 @@ Qed.
 
 End binomial_pmf.
 
+Lemma measurable_binomial_pmf {R : realType} D n k :
+  measurable_fun D (@binomial_pmf R n ^~ k).
+Proof.
+apply: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x *+ 'C(n, k))%R) => /=.
+  exact: measurable_natmul.
+apply: measurable_funM => //=; apply: measurable_fun_pow.
+exact: measurable_funB.
+Qed.
+
 Definition binomial_prob {R : realType} (n : nat) (p : R) : set nat -> \bar R :=
   fun U => if (0 <= p <= 1)%R then
     \esum_(k in U) (binomial_pmf n p k)%:E else \d_O U.
@@ -432,9 +440,6 @@ rewrite addeC -ge0_sume_distrl.
   by apply/mulrn_wge0/mulr_ge0; apply/exprn_ge0 => //; exact/onem_ge0.
 Qed.
 
-Lemma sumbool_ler {R : realDomainType} (x y : R) : (x <= y)%R + (x > y)%R.
-Proof. by have [_|_] := leP x y; [exact: inl|exact: inr]. Qed.
-
 Section binomial_total.
 Local Open Scope ring_scope.
 Variables (R : realType) (n : nat).
@@ -448,48 +453,20 @@ apply: (@measurability _ _ _ _ _ _
 move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=.
 rewrite /binomial_prob/=.
 set f := (X in measurable_fun _ X).
-rewrite (_ : f = fun x => if 0 <= x <= 1 then (\sum_(m < n.+1)
-      if sumbool_ler 0 x is inl l0p then
-        if sumbool_ler x 1 is inl lp1 then
-           mscale (@bin_prob _ n _ l0p lp1 m) (\d_(nat_of_ord m)) Ys
-         else
-          (x ^+ m * `1-x ^+ (n - m) *+ 'C(n, m))%:E * \d_(nat_of_ord m) Ys
-      else (x ^+ m * `1-x ^+ (n - m) *+ 'C(n, m))%:E * \d_(nat_of_ord m) Ys)%E
-   else \d_0%N Ys)//.
-  apply: measurable_fun_ifT => //=.
-    apply: measurable_and => //; apply: (measurable_fun_bool true) => //=.
-      rewrite (_ : _ @^-1` _ = `[0, +oo[%classic)//.
-      by apply/seteqP; split => [x|x] /=; rewrite in_itv/= andbT.
-    by rewrite (_ : _ @^-1` _ = `]-oo, 1]%classic).
-  apply: emeasurable_fun_sum => m /=.
-  rewrite /mscale/= [X in measurable_fun _ X](_ : _ = (fun x =>
-    (x ^+ m * `1-x ^+ (n - m) *+ 'C(n, m))%:E * \d_(nat_of_ord m) Ys)%E); last first.
-    by apply:funext => x; case: sumbool_ler => // x0; case: sumbool_ler.
-  apply: emeasurable_funM => //; apply/EFin_measurable_fun => //.
-  under eq_fun do rewrite -mulr_natr.
-  do 2 apply: measurable_funM => //.
-  exact/measurable_fun_pow/measurable_funB.
-rewrite {}/f; apply/funext => x.
-case: ifPn => // /andP[x0 x1].
-rewrite (esumID `I_n.+1)//; last first.
-  by move=> k _; rewrite lee_fin// binomial_pmf_ge0// x0.
-rewrite [X in (_ + X)%E]esum1 ?adde0; last first.
-  by move=> k [_ /= /negP]; rewrite -leqNgt => nk; rewrite /binomial_pmf bin_small.
-rewrite esum_mkcondl esum_fset//=; last first.
-  move=> k; rewrite inE/= ltnS => kn.
-  by case: ifPn => // _; rewrite lee_fin binomial_pmf_ge0// x0.
-rewrite -fsbig_ord//=; apply: eq_bigr => i _.
-case: ifPn => iYs.
-  case: sumbool_ler => //= x0'.
-    case: sumbool_ler => //= x1'.
-      by rewrite /mscale/= /binomial_pmf diracE iYs mule1.
-    by move: x1'; rewrite ltNge x1.
-  by move: x0'; rewrite ltNge x0.
-case: sumbool_ler => //= x0'.
-  case: sumbool_ler => //= x1'.
-    by rewrite /mscale/= /binomial_pmf diracE (negbTE iYs) mule0.
-  by move: x1'; rewrite ltNge x1.
-by move: x0'; rewrite ltNge x0.
+apply: measurable_fun_if => //=.
+  apply: measurable_and => //; apply: (measurable_fun_bool true) => //=.
+    rewrite (_ : _ @^-1` _ = `[0, +oo[%classic)//.
+    by apply/seteqP; split => [x|x] /=; rewrite in_itv/= andbT.
+  by rewrite (_ : _ @^-1` _ = `]-oo, 1]%classic).
+apply: (eq_measurable_fun (fun t =>
+    \sum_(k <oo | k \in Ys) (binomial_pmf n t k)%:E)).
+  move=> x /set_mem[_/= x01].
+  rewrite nneseries_esum// -1?[in RHS](set_mem_set Ys)// => k kYs.
+  by rewrite lee_fin binomial_pmf_ge0.
+apply: ge0_emeasurable_fun_sum.
+  by move=> k x/= [_ x01] _; rewrite lee_fin binomial_pmf_ge0.
+move=> k Ysk; apply/measurableT_comp => //.
+exact: measurable_binomial_pmf.
 Qed.
 
 End binomial_total.
@@ -1998,9 +1975,9 @@ Context d d' d1 d2 d3 (X : measurableType d) (Y : measurableType d')
   (R : realType).
 Import Notations.
 Variables (t : R.-sfker X ~> T1)
-          (u : R.-sfker [the measurableType _ of (X * T1)%type] ~> T2)
-          (v : R.-sfker [the measurableType _ of (X * T2)%type] ~> Y)
-          (v' : R.-sfker [the measurableType _ of (X * T1 * T2)%type] ~> Y)
+          (u : R.-sfker (X * T1) ~> T2)
+          (v : R.-sfker (X * T2) ~> Y)
+          (v' : R.-sfker (X * T1 * T2) ~> Y)
           (vv' : forall y, v =1 fun xz => v' (xz.1, y, xz.2)).
 
 Lemma letinA x A : measurable A ->