From 486cd4688bde6ec6b1b5c22c6787f10c96f82f11 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 1 Sep 2022 20:31:03 +0900 Subject: [PATCH] mscore using mscale and dirac --- theories/kernel.v | 159 ++----------------------------------------- theories/prob_lang.v | 95 ++++++++++---------------- 2 files changed, 41 insertions(+), 213 deletions(-) diff --git a/theories/kernel.v b/theories/kernel.v index 6decb7a906..5f0d7c2e9f 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -74,121 +74,6 @@ Qed. End integralM_0ifneg. Arguments integralM_0ifneg {d T R} m {D} mD f. -Section integralM_indic. -Local Open Scope ereal_scope. -Variables (d : measure_display) (T : measurableType d) (R : realType). -Variables (m : {measure set T -> \bar R}) (D : set T) (mD : measurable D). - -Let integralM_indic (f : R -> set T) (k : R) : - ((k < 0)%R -> f k = set0) -> measurable (f k) -> - \int[m]_(x in D) (k * \1_(f k) x)%:E = k%:E * \int[m]_(x in D) (\1_(f k) x)%:E. -Proof. -move=> fk0 mfk. -under eq_integral do rewrite EFinM. -apply: (integralM_0ifneg _ _ (fun k x => (\1_(f k) x)%:E)) => //=. -- by move=> r t Dt; rewrite lee_fin. -- by move/fk0 => -> /=; apply/funext => x; rewrite indicE in_set0. -- apply/EFin_measurable_fun. - by rewrite (_ : \1_(f k) = mindic R mfk). -Qed. - -End integralM_indic. -Arguments integralM_indic {d T R} m {D} mD f. - -(* NB: PR in progress *) -Section integral_mscale. -Variables (R : realType) (k : {nonneg R}). -Variables (d : measure_display) (T : measurableType d). -Variable (m : {measure set T -> \bar R}) (D : set T) (f : T -> \bar R). -Hypotheses (mD : measurable D). - -Let integral_mscale_indic (E : set T) (mE : measurable E) : - \int[mscale k m]_(x in D) (\1_E x)%:E = - k%:num%:E * \int[m]_(x in D) (\1_E x)%:E. -Proof. by rewrite !integral_indic. Qed. - -Let integral_mscale_nnsfun (h : {nnsfun T >-> R}) : - \int[mscale k m]_(x in D) (h x)%:E = k%:num%:E * \int[m]_(x in D) (h x)%:E. -Proof. -rewrite -ge0_integralM//; last 2 first. -apply/EFin_measurable_fun. - exact: measurable_funS (@measurable_funP _ _ _ h). - by move=> x _; rewrite lee_fin. -under eq_integral do rewrite fimfunE -sumEFin. -under [LHS]eq_integral do rewrite fimfunE -sumEFin. -rewrite /=. -rewrite ge0_integral_sum//; last 2 first. - move=> r. - apply/EFin_measurable_fun/measurable_funrM. - apply: (@measurable_funS _ _ _ _ setT) => //. - have fr : measurable (h @^-1` [set r]) by exact/measurable_sfunP. - by rewrite (_ : \1__ = mindic R fr). - by move=> n x Dx; rewrite EFinM muleindic_ge0. -under eq_integral. - move=> x xD. - rewrite ge0_sume_distrr//; last first. - by move=> r _; rewrite EFinM muleindic_ge0. - over. -rewrite /=. -rewrite ge0_integral_sum//; last 2 first. - move=> r. - apply/EFin_measurable_fun/measurable_funrM/measurable_funrM. - apply: (@measurable_funS _ _ _ _ setT) => //. - have fr : measurable (h @^-1` [set r]) by exact/measurable_sfunP. - by rewrite (_ : \1__ = mindic R fr). - move=> n x Dx. - by rewrite EFinM mule_ge0// muleindic_ge0. -apply eq_bigr => r _. -rewrite ge0_integralM//; last 2 first. - apply/EFin_measurable_fun/measurable_funrM. - apply: (@measurable_funS _ _ _ _ setT) => //. - have fr : measurable (h @^-1` [set r]) by exact/measurable_sfunP. - by rewrite (_ : \1__ = mindic R fr). - by move=> t Dt; rewrite muleindic_ge0. -by rewrite !integralM_indic_nnsfun//= integral_mscale_indic// muleCA. -Qed. - -Lemma ge0_integral_mscale (mf : measurable_fun D f) : - (forall x, D x -> 0 <= f x) -> - \int[mscale k m]_(x in D) f x = k%:num%:E * \int[m]_(x in D) f x. -Proof. -move=> f0; have [f_ [ndf_ f_f]] := approximation mD mf f0. -transitivity (lim (fun n => \int[mscale k m]_(x in D) (f_ n x)%:E)). - rewrite -monotone_convergence//=; last 3 first. - move=> n; apply/EFin_measurable_fun. - by apply: (@measurable_funS _ _ _ _ setT). - by move=> n x Dx; rewrite lee_fin. - by move=> x Dx a b /ndf_ /lefP; rewrite lee_fin. - apply eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //=. - exact: f_f. -rewrite (_ : \int[m]_(x in D) _ = lim (fun n => \int[m]_(x in D) (f_ n x)%:E)); last first. - rewrite -monotone_convergence//. - apply: eq_integral => x /[!inE] xD. - apply/esym/cvg_lim => //. - exact: f_f. - move=> n. - apply/EFin_measurable_fun. - by apply: (@measurable_funS _ _ _ _ setT). - by move=> n x Dx; rewrite lee_fin. - by move=> x Dx a b /ndf_ /lefP; rewrite lee_fin. -rewrite -ereal_limrM//; last first. - apply/ereal_nondecreasing_is_cvg => a b ab. - apply ge0_le_integral => //. - by move=> x Dx; rewrite lee_fin. - apply/EFin_measurable_fun. - by apply: (@measurable_funS _ _ _ _ setT). - by move=> x Dx; rewrite lee_fin. - apply/EFin_measurable_fun. - by apply: (@measurable_funS _ _ _ _ setT). - move=> x Dx. - rewrite lee_fin. - by move/ndf_ : ab => /lefP. -congr (lim _); apply/funext => n /=. -by rewrite integral_mscale_nnsfun. -Qed. - -End integral_mscale. - (* TODO: PR *) Canonical unit_pointedType := PointedType unit tt. @@ -232,23 +117,6 @@ HB.instance Definition _ := @isMeasurable.Build default_measure_display bool (Po End discrete_measurable_bool. -(* NB: PR in progress *) -Lemma measurable_fun_fine (R : realType) (D : set (\bar R)) : measurable D -> - measurable_fun D fine. -Proof. -move=> mD _ /= B mB; rewrite [X in measurable X](_ : _ `&` _ = if 0%R \in B then - D `&` ((EFin @` B) `|` [set -oo; +oo]) else D `&` EFin @` B); last first. - apply/seteqP; split=> [[r [Dr Br]|[Doo B0]|[Doo B0]]|[r| |]]. - - by case: ifPn => _; split => //; left; exists r. - - by rewrite mem_set//; split => //; right; right. - - by rewrite mem_set//; split => //; right; left. - - by case: ifPn => [_ [Dr [[s + [sr]]|[]//]]|_ [Dr [s + [sr]]]]; rewrite sr. - - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []]. - - by case: ifPn => [/[!inE] B0 [Doo [[]//|]] [//|_]|B0 [Doo//] []]. -case: ifPn => B0; apply/measurableI => //; last exact: measurable_EFin. -by apply: measurableU; [exact: measurable_EFin|exact: measurableU]. -Qed. - (* TODO: PR *) Lemma measurable_fun_fst (d1 d2 : _) (T1 : measurableType d1) (T2 : measurableType d2) : measurable_fun setT (@fst T1 T2). @@ -293,25 +161,6 @@ Qed. End measurable_fun_comp. -Lemma open_continuousP (S T : topologicalType) (f : S -> T) (D : set S) : - open D -> - {in D, continuous f} <-> (forall A, open A -> open (D `&` f @^-1` A)). -Proof. -move=> oD; split=> [fcont|fcont s /[!inE] sD A]. - rewrite !openE => A Aop s [Ds] /Aop /fcont; rewrite inE => /(_ Ds) fsA. - by rewrite interiorI; split => //; move: oD; rewrite openE; exact. -rewrite nbhs_simpl /= !nbhsE => - [B [[oB Bfs] BA]]. -by exists (D `&` f @^-1` B); split=> [|t [Dt] /BA//]; split => //; exact/fcont. -Qed. - -Lemma open_continuous_measurable_fun (R : realType) (f : R -> R) D : - open D -> {in D, continuous f} -> measurable_fun D f. -Proof. -move=> oD /(open_continuousP _ oD) cf. -apply: (measurability (RGenOpens.measurableE R)) => _ [_ [a [b ->] <-]]. -by apply: open_measurable; exact/cf/interval_open. -Qed. - Lemma set_boolE (B : set bool) : [\/ B == [set true], B == [set false], B == set0 | B == setT]. Proof. have [Bt|Bt] := boolP (true \in B). @@ -771,7 +620,7 @@ rewrite [X in measurable_fun _ X](_ : _ = (fun x => apply/EFin_measurable_fun/measurable_funrM/measurable_fun_prod1 => /=. rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) r))//. exact/measurable_funP. - - by move=> m y _; rewrite muleindic_ge0. + - by move=> m y _; rewrite nnfun_muleindic_ge0. apply emeasurable_fun_sum => r. rewrite [X in measurable_fun _ X](_ : _ = (fun x => r%:E * \int[l x]_y (\1_(k_ n @^-1` [set r]) (x, y))%:E)); last first. @@ -1103,7 +952,7 @@ rewrite ge0_integral_sum//; last 2 first. move=> r; apply/EFin_measurable_fun/measurable_funrM. have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. by rewrite (_ : \1__ = mindic R fr). - by move=> r z _; rewrite EFinM muleindic_ge0. + by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. under [in RHS]eq_integral. move=> y _. under eq_integral. @@ -1114,7 +963,7 @@ under [in RHS]eq_integral. move=> r; apply/EFin_measurable_fun/measurable_funrM. have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. by rewrite (_ : \1__ = mindic R fr). - by move=> r z _; rewrite EFinM muleindic_ge0. + by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. under eq_bigr. move=> r _. rewrite (@integralM_indic _ _ _ _ _ _ (fun r => f @^-1` [set r]))//; last first. @@ -1127,7 +976,7 @@ rewrite /= ge0_integral_sum//; last 2 first. have := measurable_kernel k (f @^-1` [set r]) (measurable_sfunP f r). by move=> /measurable_fun_prod1; exact. - move=> n y _. - have := @mulem_ge0 _ _ _ (k (x, y)) n (fun n => f @^-1` [set n]). + have := @mulemu_ge0 _ _ _ (k (x, y)) n (fun n => f @^-1` [set n]). by apply; exact: preimage_nnfun0. apply eq_bigr => r _. rewrite (@integralM_indic _ _ _ _ _ _ (fun r => f @^-1` [set r]))//; last first. diff --git a/theories/prob_lang.v b/theories/prob_lang.v index e644a49fd2..12a615e58a 100644 --- a/theories/prob_lang.v +++ b/theories/prob_lang.v @@ -42,7 +42,7 @@ apply/prod_measurable_funP => /=; split. exact: measurable_fun_fst. Qed. -Lemma onem1 (R : numDomainType) (p : R) : (p + `1- p = 1)%R. +Lemma onem1' (R : numDomainType) (p : R) : (p + `1- p = 1)%R. Proof. by rewrite /onem addrCA subrr addr0. Qed. Lemma onem_nonneg_proof (R : numDomainType) (p : {nonneg R}) (p1 : (p%:num <= 1)%R) : @@ -68,7 +68,7 @@ Local Close Scope ring_scope. Let mbernoulli_setT : mbernoulli [set: _] = 1. Proof. rewrite /mbernoulli/= /measure_add/= /msum 2!big_ord_recr/= big_ord0 add0e/=. -by rewrite /mscale/= !diracE !in_setT !mule1 -EFinD onem1. +by rewrite /mscale/= !diracE !in_setT !mule1 -EFinD onem1'. Qed. HB.instance Definition _ := @isProbability.Build _ _ R mbernoulli mbernoulli_setT. @@ -81,35 +81,25 @@ Section mscore. Variables (d : _) (T : measurableType d). Variables (R : realType) (f : T -> R). -Definition mscore t (U : set unit) : \bar R := - if U == set0 then 0 else `| (f t)%:E |. +Definition mscore t : {measure set _ -> \bar R} := + let p := NngNum (@normr_ge0 _ _ (`| f t |)%R) in + [the measure _ _ of mscale p [the measure _ _ of dirac tt]]. -Let mscore0 t : mscore t (set0 : set unit) = 0 :> \bar R. -Proof. by rewrite /mscore eqxx. Qed. - -Let mscore_ge0 t U : 0 <= mscore t U. -Proof. by rewrite /mscore; case: ifP. Qed. - -Let mscore_sigma_additive t : semi_sigma_additive (mscore t). +Lemma mscoreE t U : mscore t U = if U == set0 then 0 else `| (f t)%:E |. Proof. -move=> /= F mF tF mUF; rewrite /mscore; case: ifPn => [/eqP/bigcup0P F0|]. - rewrite (_ : (fun _ => _) = cst 0); first exact: cvg_cst. - apply/funext => k. - under eq_bigr do rewrite F0// eqxx. - by rewrite big1. -move=> /eqP/bigcup0P/existsNP[k /not_implyP[_ /eqP Fk0]]. -rewrite -(cvg_shiftn k.+1)/=. -rewrite (_ : (fun _ => _) = cst `|(f t)%:E|); first exact: cvg_cst. -apply/funext => n. -rewrite big_mkord (bigD1 (widen_ord (leq_addl n _) (Ordinal (ltnSn k))))//=. -rewrite (negbTE Fk0) big1 ?adde0// => i/= ik; rewrite ifT//. -have [/eqP//|Fitt] := set_unit (F i). -move/trivIsetP : tF => /(_ i k Logic.I Logic.I ik). -by rewrite Fitt setTI => /eqP; rewrite (negbTE Fk0). +rewrite /mscore/= /mscale/=; have [->|->] := set_unit U. + by rewrite eqxx diracE in_set0 mule0. +rewrite diracE in_setT mule1 ifF// ?normr_id//. +by apply/negbTE/set0P; exists tt. Qed. -HB.instance Definition _ (t : T) := isMeasure.Build _ _ _ - (mscore t) (mscore0 t) (mscore_ge0 t) (@mscore_sigma_additive t). +Lemma measurable_fun_mscore U : measurable_fun setT f -> + measurable_fun setT (mscore ^~ U). +Proof. +move=> mr; under eq_fun do rewrite mscoreE/=. +have [U0|U0] := eqVneq U set0; first exact: measurable_fun_cst. +by apply: measurable_fun_comp => //; exact: measurable_fun_comp. +Qed. End mscore. @@ -138,39 +128,34 @@ Lemma k_sigma_additive i t : semi_sigma_additive (k mr i t). Proof. move=> /= F mF tF mUF; rewrite /k /=. have [F0|] := eqVneq (\bigcup_n F n) set0. - rewrite [in X in _ --> X]/mscore F0 eqxx. - rewrite (_ : (fun _ => _) = cst 0). + rewrite F0 measure0 (_ : (fun _ => _) = cst 0). by case: ifPn => _; exact: cvg_cst. apply/funext => k; rewrite big1// => n _. - move : F0 => /bigcup0P F0. - by rewrite /mscore F0// eqxx; case: ifP. + by move: F0 => /bigcup0P -> //; rewrite measure0; case: ifPn. move=> UF0; move: (UF0). move=> /eqP/bigcup0P/existsNP[m /not_implyP[_ /eqP Fm0]]. -rewrite [in X in _ --> X]/mscore (negbTE UF0). +rewrite [in X in _ --> X]mscoreE (negbTE UF0). rewrite -(cvg_shiftn m.+1)/=. case: ifPn => ir. rewrite (_ : (fun _ => _) = cst `|(r t)%:E|); first exact: cvg_cst. apply/funext => n. rewrite big_mkord (bigD1 (widen_ord (leq_addl n _) (Ordinal (ltnSn m))))//=. - rewrite [in X in X + _]/mscore (negbTE Fm0) ir big1 ?adde0// => /= j jk. - rewrite /mscore. - have /eqP Fj0 : F j == set0. + rewrite [in X in X + _]mscoreE (negbTE Fm0) ir big1 ?adde0// => /= j jk. + rewrite mscoreE; have /eqP -> : F j == set0. have [/eqP//|Fjtt] := set_unit (F j). move/trivIsetP : tF => /(_ j m Logic.I Logic.I jk). by rewrite Fjtt setTI => /eqP; rewrite (negbTE Fm0). - rewrite Fj0 eqxx. - by case: ifP. + by rewrite eqxx; case: ifP. rewrite (_ : (fun _ => _) = cst 0); first exact: cvg_cst. apply/funext => n. rewrite big_mkord (bigD1 (widen_ord (leq_addl n _) (Ordinal (ltnSn m))))//=. -rewrite [in X in if X then _ else _]/mscore (negbTE Fm0) (negbTE ir) add0e. +rewrite [in X in if X then _ else _]mscoreE (negbTE Fm0) (negbTE ir) add0e. rewrite big1//= => j jm. -rewrite /mscore. -have /eqP Fj0 : F j == set0. +rewrite mscoreE; have /eqP -> : F j == set0. have [/eqP//|Fjtt] := set_unit (F j). move/trivIsetP : tF => /(_ j m Logic.I Logic.I jm). by rewrite Fjtt setTI => /eqP; rewrite (negbTE Fm0). -by rewrite Fj0 eqxx; case: ifP. +by rewrite eqxx; case: ifP. Qed. HB.instance Definition _ i t := isMeasure.Build _ _ _ @@ -181,16 +166,12 @@ Proof. move=> /= mU; rewrite /k /=. rewrite (_ : (fun x : T => _) = (fun x => if (i%:R)%:E <= x < (i.+1%:R)%:E then x else 0) \o (mscore r ^~ U)) //. -apply: measurable_fun_comp => /=; last first. - rewrite /mscore. - have [U0|U0] := eqVneq U set0; first exact: measurable_fun_cst. - by apply: measurable_fun_comp => //; exact/EFin_measurable_fun. +apply: measurable_fun_comp => /=; last exact/measurable_fun_mscore. pose A : _ -> \bar R := (fun x => x * (\1_(`[i%:R%:E, i.+1%:R%:E [%classic : set (\bar R)) x)%:E). rewrite (_ : (fun x => _) = A); last first. apply/funext => x; rewrite /A; case: ifPn => ix. by rewrite indicE/= mem_set ?mule1//. - rewrite indicE/= memNset ?mule0//. - by rewrite /= in_itv/=; exact/negP. + by rewrite indicE/= memNset ?mule0// /= in_itv/=; exact/negP. rewrite {}/A. apply emeasurable_funM => /=; first exact: measurable_fun_id. apply/EFin_measurable_fun. @@ -206,8 +187,7 @@ HB.instance Definition _ i := Lemma mk_uub (i : nat) : measure_fam_uub (mk i). Proof. -exists i.+1%:R => /= t. -rewrite /k /mscore setT_unit. +exists i.+1%:R => /= t; rewrite /k mscoreE setT_unit. rewrite (_ : [set tt] == set0 = false); last first. by apply/eqP => /seteqP[] /(_ tt) /(_ erefl). by case: ifPn => // /andP[]. @@ -228,11 +208,7 @@ Definition kscore (mr : measurable_fun setT r) Variable (mr : measurable_fun setT r). Let measurable_fun_kscore U : measurable U -> measurable_fun setT (kscore mr ^~ U). -Proof. -move=> /= mU; rewrite /mscore. -have [U0|U0] := eqVneq U set0; first exact: measurable_fun_cst. -by apply: measurable_fun_comp => //; exact/EFin_measurable_fun. -Qed. +Proof. by move=> /= _; exact: measurable_fun_mscore. Qed. HB.instance Definition _ := isKernel.Build _ _ T _ (*Datatypes_unit__canonical__measure_Measurable*) R (kscore mr) measurable_fun_kscore. @@ -245,9 +221,9 @@ Let sfinite_kscore : exists k : (R.-fker T ~> _)^nat, Proof. rewrite /=. exists (fun i => [the R.-fker _ ~> _ of mk mr i]) => /= t U mU. -rewrite /mseries /mscore; case: ifPn => [/eqP U0|U0]. +rewrite /mseries /kscore/= mscoreE; case: ifPn => [/eqP U0|U0]. by apply/esym/nneseries0 => i _; rewrite U0 measure0. -rewrite /mk /= /k /= /mscore (negbTE U0). +rewrite /mk /= /k /= mscoreE (negbTE U0). apply/esym/cvg_lim => //. rewrite -(cvg_shiftn `|floor (fine `|(r t)%:E|)|%N.+1)/=. rewrite (_ : (fun _ => _) = cst `|(r t)%:E|); first exact: cvg_cst. @@ -438,10 +414,11 @@ Lemma scoreE (t : T) (U : set bool) (n : nat) (b : bool) (f0 : forall r, (0 <= r)%R -> (0 <= f r)%R) (mf : measurable_fun setT f) : score (measurable_fun_comp mf (@measurable_fun_snd _ _ _ _)) - (t, b, n%:R) ((fun _ => (snd \o fst) (t, b, tt)) @^-1` U) = + (t, b, n%:R) (curry (snd \o fst) (t, b) @^-1` U) = (f n%:R)%:E * \d_b U. Proof. -rewrite /score/= /mscore/= diracE. +set x := score _. +rewrite /score/= /kscore/= mscoreE diracE. have [U0|U0] := set_unit ((fun=> b) @^-1` U). - rewrite U0 eqxx memNset ?mule0// => Ub. by move: U0 => /seteqP[/(_ tt)] /(_ Ub). @@ -827,7 +804,9 @@ Section letinC. Variables (d d' d3 d4 : _) (R : realType) (X : measurableType d) (Y : measurableType d') (Z : measurableType d3) (U : measurableType d4). + Let f (xyz : unit * X * X) := (xyz.1.2, xyz.2). + Lemma mf : measurable_fun setT f. Proof. rewrite /=.