diff --git a/theories/probability.v b/theories/probability.v index 72ddd04ba..e07651a05 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -161,6 +161,95 @@ move=> cg; apply: (card_le_finite _ (range g))=> //. exact/subset_card_le/image_subset. Qed. +(* compatible generalization of lebesgue_integral.measurable_sfunP *) +Lemma measurable_sfunP d1 d2 (aT : measurableType d1) + (rT : measurableType d2) (f : {mfun aT >-> rT}) (Y : set rT) : + measurable Y -> measurable (f @^-1` Y). +Proof. by move=> mY; rewrite -[f @^-1` _]setTI; exact: measurable_funP. Qed. + +(* compatible generalizations of two lemmas from sequences.v *) +Lemma ereal_nondecreasing_series (R : realDomainType) (u_ : sequence \bar R) + N (P : pred nat) : + (forall n : nat, P n -> (0%R <= u_ n)%E) -> + {homo (fun n : nat => \sum_(N <= i < n | P i) u_ i) : + n m / (n <= m)%N >-> (n <= m)%E}. +Proof. by move=> u_ge0 n m nm; rewrite lee_sum_nneg_natr// => k _ /u_ge0. Qed. + +Lemma nneseries_lim_ge (R : realType) (u_ : sequence \bar R) m (P : pred nat) + (k : nat) : + (forall n : nat, P n -> (0%R <= u_ n)%E) -> + ((\sum_(m <= i < k | P i) u_ i)%R <= \big[+%R/0%R]_(m <= i -> //. +by apply: ereal_sup_ubound; exists k. +Qed. + +(* generalizations with an additional predicate (m <= i)%N as in big_geq_mkord *) +Lemma lee_sum_fset_nat_geq (R : realDomainType) (f : sequence \bar R) + (F : {fset nat}) (m n : nat) (P : pred nat) : + (forall i : nat, P i -> (0%R <= f i)%E) -> + [set` F] `<=` `I_n -> + ((\sum_(i <- F | P i && (m <= i)%N) f i)%R + <= (\sum_(m <= i < n | P i) f i)%R)%E. +Proof. +move=> f0 Fn. +rewrite big_geq_mkord/= -(big_mkord (fun i => P i && (m <= i)%N)). +apply: lee_sum_fset_nat=> //. +by move=> ? /andP [] *; exact: f0. +Qed. +Arguments lee_sum_fset_nat_geq {R f} F m n P. + +Lemma lee_sum_fset_lim_geq (R : realType) (f : sequence \bar R) + (F : {fset nat}) m (P : pred nat) : + (forall i : nat, P i -> (0%R <= f i)%E) -> + ((\sum_(i <- F | P i && (m <= i)%N) f i)%R + <= \big[+%R/0%R]_(m <= i f0; pose n := (\max_(k <- F) k).+1. +rewrite (le_trans (lee_sum_fset_nat_geq F m n _ _ _))//; last exact: nneseries_lim_ge. +move=> k /= kF; rewrite /n big_seq_fsetE/=. +by rewrite -[k]/(val [`kF]%fset) ltnS leq_bigmax. +Qed. +Arguments lee_sum_fset_lim_geq {R f} F m P. + +Lemma nneseries_esum_geq (R : realType) (a : nat -> \bar R) m (P : pred nat) : + (forall n : nat, P n -> (0%R <= a n)%E) -> + \big[+%R/0]_(m <= i a0; apply/eqP; rewrite eq_le; apply/andP; split. + apply: (lime_le (is_cvg_nneseries_cond a0)); apply: nearW => n. + apply: ereal_sup_ubound; exists [set` [fset val i | i in 'I_n & P i && (m <= i)%N]%fset]. + split; first exact: finite_fset. + by move=> /= k /imfsetP[/= i]; rewrite inE => + ->. + rewrite fsbig_finite//= set_fsetK big_imfset/=; last first. + by move=> ? ? ? ? /val_inj. + by rewrite big_filter big_enum_cond/= big_geq_mkord. +apply: ub_ereal_sup => _ [/= F [finF PF] <-]. +rewrite fsbig_finite//= -(big_rmcond_in (fun i=> P i && (m <= i)%N))/=. + exact: lee_sum_fset_lim_geq. +by move=> k; rewrite in_fset_set// inE => /PF ->. +Qed. + +Lemma nneseriesID (R : realType) m (a P : pred nat) (f : nat -> \bar R): + (forall k : nat, P k -> (0%R <= f k)%E) -> + \big[+%R/0]_(m <= k nn. +rewrite nneseries_esum_geq//. +rewrite (esumID a)/=; last by move=> ? /andP [] *; exact: nn. +have->: [set x | P x && (m <= x)%N] `&` (fun x : nat => a x) = + [set x | (P x && a x) && (m <= x)%N]. + by apply: funext=> x /=; rewrite (propext (rwP andP)) andbAC. +have->: [set x | P x && (m <= x)%N] `&` ~` (fun x : nat => a x) = + [set x | (P x && ~~ a x) && (m <= x)%N]. + apply: funext=> x /=. + by rewrite (propext (rwP negP)) (propext (rwP andP)) andbAC. +by rewrite -!nneseries_esum_geq//; move=> ? /andP [] *; exact: nn. +Qed. + End move_to_somewhere. Arguments countable_range_comp [T0 T1 T2]. Arguments finite_range_comp [T0 T1 T2]. @@ -2819,7 +2908,7 @@ Definition bernoulli_RV (X : {dRV P >-> bool}) := distribution P X = bernoulli p. Lemma bernoulli_RV1 (X : {dRV P >-> bool}) : bernoulli_RV X -> - P [set i | X i == 1%R] == p%:E. + P [set i | X i == 1%R] = p%:E. Proof. move=> [[/(congr1 (fun f => f [set 1%:R]))]]. rewrite bernoulliE//. @@ -2833,7 +2922,7 @@ by apply/seteqP; split => [x /eqP H//|x /eqP]. Qed. Lemma bernoulli_RV2 (X : {dRV P >-> bool}) : bernoulli_RV X -> - P [set i | X i == 0%R] == (`1-p)%:E. + P [set i | X i == 0%R] = (`1-p)%:E. Proof. move=> [[/(congr1 (fun f => f [set 0%:R]))]]. rewrite bernoulliE//. @@ -3027,36 +3116,35 @@ Lemma bernoulli_mmt_gen_fun (X : {dRV P >-> bool}) (t : R) : Proof. move=> bX. rewrite/mmt_gen_fun. pose mmtX : {RV P >-> R} := expR \o t \o* (btr P X). -transitivity ((expR (t * 1))%:E * P [set x | X x == true] + (expR (t * 0))%:E * P [set x | X x == false]). - set Y := expR \o _. - have cntY: countable (range Y). - rewrite /Y mulr_funEcomp /btr /bool_to_real. - apply: countable_range_comp; left. - apply: countable_range_comp; left. - apply: countable_range_comp; left. - apply: countable_range_comp; left. - apply: (sub_countable _ [set: bool])=> //. - exact: subset_card_le. - pose dY:= discreteMeasurableFun.Pack (discreteMeasurableFun.Class (MeasurableFun_isDiscrete.Build _ _ _ _ _ cntY)). - have->: Y = dY by []. - rewrite dRV_expectation; last first. - rewrite /dY /=. - apply: measurable_bounded_integrable=> //. - by rewrite /= probability_setT ltry. - rewrite bounded_image. - apply: finite_bounded. - rewrite mulr_funEcomp. - apply: (finite_range_comp _ expR); left. - apply: finite_range_comp; left. - apply: finite_range_comp; left. - apply: finite_range_comp; left. - apply: (card_le_finite _ [set: bool])=> //. - exact: subset_card_le. - admit. -rewrite mulr1 mulr0 expR0 mul1e. -rewrite (eqP (bernoulli_RV1 bX)) (eqP (bernoulli_RV2 bX)). -by rewrite -EFinM -EFinD mulrC. -Admitted. +set A := X @^-1` [set true]. +set B := X @^-1` [set false]. +have mA: measurable A by exact: measurable_sfunP. +have mB: measurable B by exact: measurable_sfunP. +have dAB: [disjoint A & B] + by rewrite /disj_set /A /B preimage_true preimage_false setICr. +have TAB: setT = A `|` B by rewrite -preimage_setU -setT_bool preimage_setT. +rewrite unlock. +rewrite TAB integral_setU_EFin -?TAB//. +under eq_integral. + move=> x /=. + rewrite /A inE /bool_to_real /= => ->. + rewrite mul1r. + over. +rewrite integral_cst//. +under eq_integral. + move=> x /=. + rewrite /B inE /bool_to_real /= => ->. + rewrite mul0r. + over. +rewrite integral_cst//. +rewrite /A /B /preimage /=. +under eq_set do rewrite (propext (rwP eqP)). +rewrite (bernoulli_RV1 bX). +under eq_set do rewrite (propext (rwP eqP)). +rewrite (bernoulli_RV2 bX). +rewrite -EFinD; congr (_ + _)%:E; rewrite mulrC//. +by rewrite expR0 mulr1. +Qed. Lemma iter_mule (n : nat) (x y : \bar R) : iter n ( *%E x) y = (x ^+ n * y)%E. Proof. by elim: n => [|n ih]; rewrite ?mul1e// [LHS]/= ih expeS muleA. Qed.