From e8ee334c6b447fd6e436f297a95032b5c05ec4d1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 5 May 2024 18:38:09 +0900 Subject: [PATCH] shorter measurability proofs --- theories/kernel.v | 4 +- theories/lebesgue_integral.v | 34 +++++++--- theories/prob_lang.v | 127 ++++++++++++++--------------------- 3 files changed, 78 insertions(+), 87 deletions(-) diff --git a/theories/kernel.v b/theories/kernel.v index 84c3c7f94c..8a07ef9194 100644 --- a/theories/kernel.v +++ b/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. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 451e8a3146..ed262f459e 100644 --- a/theories/lebesgue_integral.v +++ b/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 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 h0 mh. +move=> mD; move: (mD). +apply/(@measurable_restrict _ _ _ _ _ setT) => //. +rewrite [X in measurable_fun _ X](_ : _ = + (fun x => \sum_(0 <= i 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 \sum_(n 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 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 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 ->