Skip to content

Commit

Permalink
use bool instead of I_2
Browse files Browse the repository at this point in the history
  • Loading branch information
affeldt-aist committed Dec 3, 2024
1 parent da1f343 commit 72dd499
Showing 1 changed file with 29 additions and 31 deletions.
60 changes: 29 additions & 31 deletions theories/probability.v
Original file line number Diff line number Diff line change
Expand Up @@ -899,13 +899,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.

Expand Down Expand Up @@ -940,54 +939,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).
Expand All @@ -997,11 +996,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).
Expand Down Expand Up @@ -1140,15 +1139,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).
Expand Down

0 comments on commit 72dd499

Please sign in to comment.