From 7be5887a2757558a0a9a7a500870092dc076b58e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 19 Nov 2024 10:35:23 +0900 Subject: [PATCH] use bool instead of I_2 --- theories/probability.v | 60 ++++++++++++++++++++---------------------- 1 file changed, 29 insertions(+), 31 deletions(-) diff --git a/theories/probability.v b/theories/probability.v index 14e61d0e4..983fbfa00 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -927,13 +927,12 @@ Section independent_RVs. Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). Variable P : probability T R. -Definition independent_RVs (I0 : choiceType) (I : set I0) - (X : I0 -> {mfun T >-> T'}) : Prop := +Definition independent_RVs (I0 : choiceType) + (I : set I0) (X : I0 -> {mfun T >-> T'}) : Prop := mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). Definition independent_RVs2 (X Y : {mfun T >-> T'}) := - independent_RVs [set 0%N; 1%N] - [eta (fun=> cst point) with 0%N |-> X, 1%N |-> Y]. + independent_RVs [set: bool] [eta (fun=> cst point) with false |-> X, true |-> Y]. End independent_RVs. @@ -968,54 +967,54 @@ Local Open Scope ring_scope. Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P (f \o X) (g \o Y). Proof. -move=> indeXY; split => [i [|]->{i}/= Z/=|J J01 E JE]. -- by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; - exact/measurableT_comp. -- by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; - exact/measurableT_comp. -- apply indeXY => //= i iJ; have := JE _ iJ. - have : i \in [set 0%N; 1%N] by rewrite inE; apply: J01. - rewrite inE/= => -[|] /eqP ->/=; rewrite !inE. - + exact: g_sigma_algebra_mapping_comp. - + by case: ifPn => [/eqP ->|i0]; exact: g_sigma_algebra_mapping_comp. +move=> indeXY; split => /=. +- move=> [] _ /= A. + + by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; + exact/measurableT_comp. + + by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; + exact/measurableT_comp. +- move=> J _ E JE. + apply indeXY => //= i iJ; have := JE _ iJ. + by move: i {iJ} =>[|]//=; rewrite !inE => Eg; + exact: g_sigma_algebra_mapping_comp Eg. Qed. Lemma independent_RVs2_funrposneg (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\-. Proof. -move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. -- exact: g_sigma_algebra_mapping_funrpos. +move=> indeXY; split=> [[|]/= _|J J2 E JE]. - exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrpos. - apply indeXY => //= i iJ; have := JE _ iJ. - move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). - exact: measurable_funrpos. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R) => //. + exact: measurable_funrpos. Qed. Lemma independent_RVs2_funrnegpos (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\+. Proof. -move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. -- exact: g_sigma_algebra_mapping_funrneg. +move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. - exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrneg. - apply indeXY => //= i iJ; have := JE _ iJ. - move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). - exact: measurable_funrneg. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). exact: measurable_funrpos. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. Qed. Lemma independent_RVs2_funrnegneg (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\-. Proof. -move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. - exact: g_sigma_algebra_mapping_funrneg. - exact: g_sigma_algebra_mapping_funrneg. - apply indeXY => //= i iJ; have := JE _ iJ. - move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). @@ -1025,11 +1024,11 @@ Qed. Lemma independent_RVs2_funrpospos (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+. Proof. -move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +move=> indeXY; split=> [/= [|]//= _ |J J2 E JE]. - exact: g_sigma_algebra_mapping_funrpos. - exact: g_sigma_algebra_mapping_funrpos. - apply indeXY => //= i iJ; have := JE _ iJ. - move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). exact: measurable_funrpos. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). @@ -1168,15 +1167,14 @@ have {EX EY}EXY' : 'E_P[X_ n] * 'E_P[Y_ n] @[n --> \oo] --> 'E_P[X] * 'E_P[Y]. suff : forall n, 'E_P[X_ n \* Y_ n] = 'E_P[X_ n] * 'E_P[Y_ n]. by move=> suf; apply: (cvg_unique _ EXY) => //=; under eq_fun do rewrite suf. move=> n; apply: expectationM_nnsfun => x y xX_ yY_. -suff : P (\big[setI/setT]_(j <- [fset 0%N; 1%N]%fset) +suff : P (\big[setI/setT]_(j <- [fset false; true]%fset) [eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], 1%N |-> Y_ n @^-1` [set y]] j) = - \prod_(j <- [fset 0%N; 1%N]%fset) + \prod_(j <- [fset false; true]%fset) P ([eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], 1%N |-> Y_ n @^-1` [set y]] j). by rewrite !big_fsetU1/= ?inE//= !big_seq_fset1/=. move: indeXY => [/= _]; apply => // i. - by rewrite /= !inE => /orP[|]/eqP ->; auto. pose AX := approx_A setT (EFin \o X). pose AY := approx_A setT (EFin \o Y). pose BX := approx_B setT (EFin \o X).