From 538b914cbca5cb4ad1de7dac913df023c0076090 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 19 Nov 2024 10:45:03 +0900 Subject: [PATCH] complete thm 2.13 --- CHANGELOG_UNRELEASED.md | 56 -- _CoqProject | 1 + classical/mathcomp_extra.v | 35 + theories/Make | 1 + theories/independence.v | 1340 ++++++++++++++++++++++++++++++++++++ theories/probability.v | 458 +----------- 6 files changed, 1390 insertions(+), 501 deletions(-) create mode 100644 theories/independence.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c7669fc3d..1e27a7684 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -58,55 +58,6 @@ + change implicits of `measurable_funP` -- in file `normedtype.v`, - changed `completely_regular_space` to depend on uniform separators - which removes the dependency on `R`. The old formulation can be - recovered easily with `uniform_separatorP`. - -- moved from `Rstruct.v` to `Rstruct_topology.v` - + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`, - `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs` - and `nbhs_pt_comp` - -- moved from `real_interval.v` to `normedtype.v` - + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`, - `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`, - `disj_itv_Rhull` -- in `topology.v`: - + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, - `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned - into local `Let`'s - -- in `lebesgue_integral.v`: - + structure `SimpleFun` now inside a module `HBSimple` - + structure `NonNegSimpleFun` now inside a module `HBNNSimple` - + lemma `cst_nnfun_subproof` has now a different statement - + lemma `indic_nnfun_subproof` has now a different statement -- in `mathcomp_extra.v`: - + definition `idempotent_fun` - -- in `topology_structure.v`: - + definitions `regopen`, `regclosed` - + lemmas `closure_setC`, `interiorC`, `closureU`, `interiorU`, - `closureEbigcap`, `interiorEbigcup`, - `closure_open_regclosed`, `interior_closed_regopen`, - `closure_interior_idem`, `interior_closure_idem` - -- in file `topology_structure.v`, - + mixin `isContinuous`, type `continuousType`, structure `Continuous` - + new lemma `continuousEP`. - + new definition `mkcts`. - -- in file `subspace_topology.v`, - + new lemmas `continuous_subspace_setT`, `nbhs_prodX_subspace_inE`, and - `continuous_subspace_prodP`. - + type `continuousFunType`, HB structure `ContinuousFun` - -- in file `subtype_topology.v`, - + new lemmas `subspace_subtypeP`, `subspace_sigL_continuousP`, - `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`, - `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`. - - in `lebesgue_integrale.v` + change implicits of `measurable_funP` @@ -137,13 +88,6 @@ ### Removed -- in `lebesgue_integral.v`: - + definition `cst_mfun` - + lemma `mfun_cst` - -- in `cardinality.v`: - + lemma `cst_fimfun_subproof` - - in `lebesgue_integral.v`: + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead) + lemma `cst_nnfun_subproof` (turned into a `Let`) diff --git a/_CoqProject b/_CoqProject index 882574185..fd675df69 100644 --- a/_CoqProject +++ b/_CoqProject @@ -86,6 +86,7 @@ theories/lebesgue_integral.v theories/ftc.v theories/hoelder.v theories/probability.v +theories/independence.v theories/convex.v theories/charge.v theories/kernel.v diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index f2c287308..f7c05dd23 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -538,3 +538,38 @@ Qed. Definition sigT_fun {I : Type} {X : I -> Type} {T : Type} (f : forall i, X i -> T) (x : {i & X i}) : T := (f (projT1 x) (projT2 x)). + +(* PR 114 to finmap in progress *) +Section FsetPartitions. +Variables T I : choiceType. +Implicit Types (x y z : T) (A B D X : {fset T}) (P Q : {fset {fset T}}). +Implicit Types (J : pred I) (F : I -> {fset T}). + +Variables (R : Type) (idx : R) (op : Monoid.com_law idx). +Let rhs_cond P K E := + (\big[op/idx]_(A <- P) \big[op/idx]_(x <- A | K x) E x)%fset. +Let rhs P E := (\big[op/idx]_(A <- P) \big[op/idx]_(x <- A) E x)%fset. + +Lemma partition_disjoint_bigfcup (f : T -> R) (F : I -> {fset T}) + (K : {fset I}) : + (forall i j, i \in K -> j \in K -> i != j -> [disjoint F i & F j])%fset -> + \big[op/idx]_(i <- \big[fsetU/fset0]_(x <- K) (F x)) f i = + \big[op/idx]_(k <- K) (\big[op/idx]_(i <- F k) f i). +Proof. +move=> disjF; pose P := [fset F i | i in K & F i != fset0]%fset. +have trivP : trivIfset P. + apply/trivIfsetP => _ _ /imfsetP[i iK ->] /imfsetP[j jK ->] neqFij. + move: iK; rewrite !inE/= => /andP[iK Fi0]. + move: jK; rewrite !inE/= => /andP[jK Fj0]. + by apply: (disjF _ _ iK jK); apply: contraNneq neqFij => ->. +have -> : (\bigcup_(i <- K) F i)%fset = fcover P. + apply/esym; rewrite /P fcover_imfset big_mkcond /=; apply eq_bigr => i _. + by case: ifPn => // /negPn/eqP. +rewrite big_trivIfset // /rhs big_imfset => [|i j iK /andP[jK notFj0] eqFij] /=. + rewrite big_filter big_mkcond; apply eq_bigr => i _. + by case: ifPn => // /negPn /eqP ->; rewrite big_seq_fset0. +move: iK; rewrite !inE/= => /andP[iK Fi0]. +by apply: contraNeq (disjF _ _ iK jK) _; rewrite -fsetI_eq0 eqFij fsetIid. +Qed. + +End FsetPartitions. diff --git a/theories/Make b/theories/Make index d82042d37..dacb6a9d7 100644 --- a/theories/Make +++ b/theories/Make @@ -52,6 +52,7 @@ lebesgue_integral.v ftc.v hoelder.v probability.v +independence.v lebesgue_stieltjes_measure.v convex.v charge.v diff --git a/theories/independence.v b/theories/independence.v new file mode 100644 index 000000000..2fb365ae1 --- /dev/null +++ b/theories/independence.v @@ -0,0 +1,1340 @@ +(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import all_ssreflect. +From mathcomp Require Import ssralg poly ssrnum ssrint interval finmap. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop. +From HB Require Import structures. +From mathcomp Require Import exp numfun lebesgue_measure lebesgue_integral. +From mathcomp Require Import reals ereal signed topology normedtype sequences. +From mathcomp Require Import esum measure exp numfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral kernel probability. + +(**md**************************************************************************) +(* # Independence *) +(* *) +(* ``` *) +(* independent_events I F == the events F indexed by I are independent *) +(* mutual_independence I F == the classes F indexed by I are independent *) +(* independent_RVs I X == the random variables X indexed by I are independent *) +(* independent_RVs2 X Y == the random variables X and Y are independent *) +(* ``` *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Section independent_events. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Definition independent_events (I0 : choiceType) (I : set I0) (A : I0 -> set T) + := (forall i, I i -> measurable (A i)) /\ + forall J : {fset I0}, [set` J] `<=` I -> + P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i). + +End independent_events. + +Section independent_events_lemmas. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Lemma independent_event_cplt (I0 : choiceType) (I : set I0) (A : I0 -> set T) : + independent_events P I A -> + independent_events P I (fun i => ~` A i). +Proof. +move=> [mA PIA]; split=> [i Ii|]. + exact/measurableC/mA. +move=> J. +move: J I A mA PIA. +apply: finSet_rect => J ih I A mA PIA JI. +have [J0|/fset0Pn[j jJ]] := eqVneq J fset0. + by rewrite J0 big_seq_fset0 bigcap_fset big_seq_fset0 probability_setT. +rewrite bigcap_fset. +rewrite [in LHS](big_fsetD1 _ jJ)/=. +rewrite [RHS](big_fsetD1 _ jJ)/=. +rewrite -(@ih _ _ I); last 4 first. + by apply: fproperD1. + move=> i Ii. + by apply: mA. + move=> K KI. + by apply: PIA. + move=> x/=; rewrite !inE => /andP[xj xJ]. + by apply: JI. +Abort. + +End independent_events_lemmas. + +Section mutual_independence. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Definition g_sigma_family (I0 : choiceType) (I : set I0) + (F : I0 -> set (set T)) : set (set T) := + <>. + +Definition mutual_independence (I0 : choiceType) (I : set I0) + (F : I0 -> set (set T)) := + (forall i, I i -> F i `<=` @measurable _ T) /\ + forall J : {fset I0}, + [set` J] `<=` I -> + forall E : I0 -> set T, + (forall i, i \in J -> E i \in F i) -> + P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j). + +Lemma eq_mutual_independence (I0 : choiceType) (I : set I0) + (F F' : I0 -> set (set T)) : + (forall i, I i -> F i = F' i) -> + mutual_independence I F -> mutual_independence I F'. +Proof. +move=> FF' IF; split => [i Ii|J JI E EF']. + by rewrite -FF'//; apply IF. +apply IF => // i iJ. +by rewrite FF' ?EF'//; exact: JI. +Qed. + +Definition independence (F G : set (set T)) := + [/\ F `<=` @measurable _ T, + G `<=` @measurable _ T & + forall A B, A \in F -> B \in G -> P (A `&` B) = P A * P B]. + +Lemma independence2P (I0 : choiceType) (F G : set (set T)) : + independence F G <-> + mutual_independence [set: bool] (fun b => if b then F else G). +Proof. +split=> [[mF mG FG]|/= indeF]. + split=> [/= [|]//|/= J Jbool E EF]. + have [/eqP Jtrue|/eqP Jfalse| |] := set_bool [set` J]. + - rewrite -bigcap_fset Jtrue bigcap_set1. + by rewrite fsbig_seq ?Jtrue ?fsbig_set1//. + - rewrite -bigcap_fset Jfalse bigcap_set1. + by rewrite fsbig_seq// ?Jfalse fsbig_set1. + - rewrite set_seq_eq0 => /eqP ->. + by rewrite !big_nil probability_setT. + - rewrite setT_bool => /eqP {}Jbool. + rewrite -bigcap_fset Jbool bigcap_setU1 bigcap_set1. + rewrite FG//; last 2 first. + rewrite EF//. + rewrite -(set_fsetK J) Jbool. + by rewrite in_fset_set// !inE/=; left. + rewrite EF//. + rewrite -(set_fsetK J) Jbool. + by rewrite in_fset_set// !inE/=; right. + rewrite -(set_fsetK J) Jbool. + rewrite fset_setU1//= fset_set1. + rewrite big_fsetU1 ?inE//=. + by rewrite big_seq_fset1. +split. +- case: indeF => /= [+ _] => /(_ true). + exact. +- case: indeF => /= [+ _] => /(_ false). + exact. +move=> A B AF BG. +case: indeF => _ /= /(_ [fset true; false]%fset _ (fun b => if b then A else B)). +do 2 rewrite big_fsetU1/= ?inE//= big_seq_fset1. +by apply => // -[]. +Qed. + +End mutual_independence. + +Lemma setT_setI_bigsetI (I0 : choiceType) (J : seq I0) T G (F : I0 -> set T) : + G [set: T] -> setI_closed G -> (forall i, i \in J -> G (F i)) -> + G (\big[setI/setT]_(i <- J) F i). +Proof. +move=> GT GI; rewrite big_seq; elim/big_rec : _ => //. +by move=> i A iJ ih GF; apply: GI => //; [exact: GF|exact: ih]. +Qed. + +Lemma setI_closed_setT T (F : set (set T)) : + setI_closed F -> setI_closed (F `|` [set setT]). +Proof. +move=> IF. +move=> C D [FC|/= ->{C}]. + move=> [FD|/= ->{D}]. + left. + exact: IF. + rewrite setIT. + by left. +- move=> [FD|->{D}]. + rewrite setTI. + by left. + rewrite !setTI. + by right. +Qed. + +Lemma setI_closed_set0 T (F : set (set T)) : + setI_closed F -> setI_closed (F `|` [set set0]). +Proof. +move=> IF. +move=> C D [FC|/= ->{C}]. + move=> [FD|/= ->{D}]. + left. + exact: IF. + rewrite setI0. + by right. +- move=> [FD|->{D}]. + rewrite set0I. + by right. + rewrite !set0I. + by right. +Qed. + +Lemma setI_closed_set0' T (F : set (set T)) : + F set0 -> + setI_closed (F `|` [set set0]) -> setI_closed F. +Proof. +move=> F0 IF. +move=> C D FC FD. +have [//|/= ->] : (F `|` [set set0]) (C `&` D). + by apply: IF; left. +by []. +Qed. + +Lemma g_sigma_setU d {T : measurableType d} (F : set (set T)) A : + <> A -> + <> = @measurable _ T -> + <> = <>. +Proof. +move=> FA sFT. +apply/seteqP; split=> [B|B]. + apply: sub_sigma_algebra2. + exact: subsetUl. +apply: smallest_sub => //. +move=> C [FC|/= ->//]. +exact: sub_gen_smallest. +Qed. + +Lemma g_sigma_algebra_measure_unique142b : +forall {d : measure_display} {R : realType} {T : measurableType d} (G : set (set T)), +G `<=` d.-measurable -> +forall m1 m2 : {finite_measure set T -> \bar R}, +(m1 [set: T] = m2 [set: T]) -> +setI_closed G -> +(forall A : set T, G A -> m1 A = m2 A) -> +forall E : set T, <> E -> m1 E = m2 E. +Proof. +move=> d R T G Gm m1 m2 m1m2T IG m1m2 E sGE. +apply: (@g_sigma_algebra_measure_unique _ _ _ (G `|` [set setT]) _ (fun=> setT)) => //. +- by move=> A [/Gm//|/= ->//]. +- by right. +- by rewrite bigcup_const. +- exact: setI_closed_setT. +- by move=> B [/m1m2 //|/= ->]. +- move=> n. + apply: fin_num_fun_lty. + exact: fin_num_measure. +- move: E sGE. + apply: smallest_sub => //. + move=> C GC. + apply: sub_gen_smallest. + by left. +Qed. + +Section lem142b. +Context d {T : measurableType d} {R : realType}. +Variable mu : {finite_measure set T -> \bar R}. +Variable F : set (set T). +Hypothesis setI_closed_F : setI_closed F. (* pi-system *) +Hypothesis FT : F `<=` @measurable _ T. +Hypothesis sFT : <> = @measurable _ T. + +Lemma lem142b : forall nu : {finite_measure set T -> \bar R}, + (mu setT = nu setT) -> + (forall E, F E -> nu E = mu E) -> + forall A, measurable A -> mu A = nu A. +Proof. +move=> nu munu numu A mA. +apply: (measure_unique (F `|` [set setT]) (fun=> setT)) => //. +- rewrite -sFT; apply: g_sigma_setU => //. + by rewrite sFT. +- exact: setI_closed_setT. +- by move=> n /=; right. +- by rewrite bigcup_const. +- move=> E [/numu //|/= ->]. + by rewrite munu. +- move=> n. + apply: fin_num_fun_lty. + exact: fin_num_measure. +Qed. + +End lem142b. + +Section mrestr_finite. +Context d (T : measurableType(*NB: why not sigmaRing?*) d) (R : realType). +Variables (mu : {finite_measure set T -> \bar R}) (D : set T) (mD : measurable D). + +Local Notation restr := (mrestr mu mD). + +Let fin_num_restr : fin_num_fun restr. +Proof. +move=> A mA; have := fin_num_measure mu A mA. +rewrite !ge0_fin_numE//=; apply: le_lt_trans. +by apply: le_measure => //; rewrite inE//=; exact: measurableI. +Qed. + +HB.instance Definition _ := @Measure_isFinite.Build _ T _ restr fin_num_restr. + +End mrestr_finite. + +Section mscale_finite. +Context d (T : measurableType(*NB: why not sigmaRing?*) d) (R : realType). +Variables (mu : {finite_measure set T -> \bar R}) (r : {nonneg R}). + +Local Notation scale := (mscale r mu). + +Let fin_num_scale : fin_num_fun scale. +Proof. +by move=> A mA; have muA := fin_num_measure mu A mA; rewrite fin_numM. +Qed. + +HB.instance Definition _ := @Measure_isFinite.Build _ T _ scale fin_num_scale. + +End mscale_finite. + +Section prode_ge0. + +Lemma prode_ge0: + forall [R : numDomainType] [I : Type] (r : seq I) [P : pred I] [E : I -> \bar R], + (forall i : I, P i -> (0 <= E i)%E) -> (0 <= \prod_(i <- r | P i) E i)%E. +Proof. +move=> R I r P E E0. +by elim/big_ind : _ => // x y x0 y0; rewrite mule_ge0//. +Qed. + +Lemma prode_fin_num : + forall [R : numDomainType] [I : Type] (r : seq I) [P : pred I] [E : I -> \bar R], + (forall i : I, P i -> (E i \is a fin_num)%E) -> + (\prod_(i <- r | P i) E i \is a fin_num)%E. +Proof. +move=> R I r P E E_fin_num. +by elim/big_ind : _ => // x y x0 y0; rewrite fin_numM. +Qed. + +End prode_ge0. + +Section mutual_independence_properties. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Lemma mutual_independence_finite (I0 : choiceType) (I : {fset I0}%fset) + (F : I0 -> set (set T)) : + (forall i, i \in I -> F i `<=` @measurable _ T /\ (F i) [set: T]) -> + mutual_independence P [set` I] F <-> + forall E : I0 -> set T, + (forall i : I0, i \in I -> E i \in F i) -> + P (\big[setI/setT]_(j <- I) E j) = \prod_(j <- I) P (E j). +Proof. +move=> mF; split=> [indeF E EF|indeF]; first by apply indeF. +split=> [i /mF[]//|J JI E EF]. +pose E' i := if i \in J then E i else [set: T]. +have /indeF : forall i, i \in I -> E' i \in F i. + move=> i iI; rewrite /E'; case: ifPn => [|iJ]; first exact: EF. + by rewrite inE; apply mF. +move/fsubsetP : (JI) => /(big_fset_incl _) <- /=; last first. + by move=> j jI jJ; rewrite /E' (negbTE jJ). +move/fsubsetP : (JI) => /(big_fset_incl _) <- /=; last first. + by move=> j jI jJ; rewrite /E' (negbTE jJ); rewrite probability_setT. +rewrite big_seq [in X in X = _ -> _](eq_bigr E); last first. + by move=> i iJ; rewrite /E' iJ. +rewrite -big_seq => ->. +by rewrite !big_seq; apply: eq_bigr => i iJ; rewrite /E' iJ. +Qed. + +Lemma mutual_independence_finiteS (I0 : choiceType) (I : set I0) + (F : I0 -> set (set T)) : + mutual_independence P I F <-> + (forall J : {fset I0}%fset, [set` J] `<=` I -> mutual_independence P [set` J] F). +Proof. +split=> [indeF J JI|indeF]. + split=> [i /JI Ii|K KJ E EF]. + by apply indeF. + by apply indeF => // i /KJ /JI. +split=> [i Ii|J JI E EF]. + have : [set` [fset i]%fset] `<=` I. + by move=> j; rewrite /= inE => /eqP ->. + by move/indeF => [+ _]; apply; rewrite /= inE. +by have [_] := indeF _ JI; exact. +Qed. + +Lemma mutual_independence_finite_g_sigma (I0 : choiceType) (I : set I0) + (F : I0 -> set (set T)) : + (forall i, i \in I -> setI_closed (F i `|` [set set0])) -> + mutual_independence P I F <-> mutual_independence P I (fun i => <>). +Proof. +split=> indeF; last first. + split=> [i Ii|J JI E EF]. + case: indeF => /(_ _ Ii) + _. + by apply: subset_trans; exact: sub_gen_smallest. + apply indeF => // i iJ; rewrite inE. + by apply: sub_gen_smallest; exact/set_mem/EF. +split=> [i Ii|K KI E EF]. + case: indeF => + _ => /(_ _ Ii). + by apply: smallest_sub; exact: sigma_algebra_measurable. +suff: forall J J' : {fset I0}%fset, + (J `<=` J')%fset -> [set` J'] `<=` I -> + forall E : I0 -> set T, + (forall i, i \in J -> E i \in <>) -> + (forall i, i \in [set` J'] `\` [set` J] -> E i \in F i) -> + P (\big[setI/setT]_(j <- J') E j) = \prod_(j <- J') P (E j). + move=> /(_ K K (@fsubset_refl _ _) KI E); apply. + - by move=> i iK; exact: EF. + - by move=> i; rewrite setDv inE. +move=> {E EF K KI}. +apply: finSet_rect => K ih J' KJ' J'I E EsF EF. +have [K0|/fset0Pn[j jK]] := eqVneq K fset0. + apply indeF => // i iJ'. + by apply: EF; rewrite !inE; split => //=; rewrite K0 inE. +pose J := (K `\ j)%fset. +have jI : j \in I by apply/mem_set/J'I => /=; move/fsubsetP : KJ'; exact. +have JK : (J `<` K)%fset by rewrite fproperD1. +have JjJ' : (j |` J `<=` J')%fset. + by apply: fsubset_trans KJ'; rewrite fsetD1K. +have JJ' : (J `<=` J')%fset. + by apply: fsubset_trans JjJ'; apply: fsubsetU1. +pose T' := (*g_sigma_algebraType (F j)*)T. +have L i : i \in J' -> d.-measurable (E i). + move=> iJ'. + have Ii : I i. + by apply/J'I => /=. + case: indeF => + _ => /(_ i Ii) Fim. + suff: <> (E i). + apply: smallest_sub => //. + exact: sigma_algebra_measurable. + apply/set_mem. + have [iK|iK] := boolP (i \in K). + by rewrite EsF//. + have : E i \in F i. + rewrite EF// !inE/=; split => //. + exact/negP. + move/set_mem. + by move/sub_sigma_algebra => /(_ setT)/mem_set. +have mmu : measurable (\big[setI/[set: T]]_(j0 <- (J' `\ j)%fset) (E j0)). + rewrite big_seq. + apply: bigsetI_measurable => i. + rewrite !inE => /andP[ij iJ']. + exact: L. +pose mu0 (A : set T) := P (A `&` \big[setI/[set: T]]_(j0 <- (J' `\ j)%fset) (E j0)). +pose mu := [the {finite_measure set _ -> \bar _} of mrestr P mmu]. +have muEj : forall A, (*(F j `|` [set setT]) A ->*) + mu A = P (A `&` \big[setI/[set: T]]_(j0 <- (J' `\ j)%fset) (E j0)). + by move=> A. +pose nu0 (A : set T) := P A * \prod_(j0 <- (J' `\ j)%fset) P (E j0). +have K1 : 0 <= \prod_(j0 <- (J' `\ j)%fset) P (E j0). + by apply: prode_ge0 => //. +have K2 : \prod_(j0 <- (J' `\ j)%fset) P (E j0) \is a fin_num. + rewrite big_seq prode_fin_num// => i. + rewrite !inE/= => /andP[ij iJ']. + rewrite fin_num_measure//. + by apply: L. +have K3 : (0 <= fine (\prod_(j0 <- (J' `\ j)%fset) P (E j0)))%R. + by rewrite fine_ge0//. +pose nu := [the measure _ _ of mscale (NngNum K3) P]. +have nuEj : forall A, (*(F j `|` [set setT]) A ->*) + nu A = P A * \prod_(j0 <- (J' `\ j)%fset) P (E j0). + move=> A. + rewrite /nu/= /mscale muleC/=. + by rewrite fineK//. +have JJ'j : (J `<=` J' `\ j)%fset by exact: fsetSD. +have J'jI : [set` (J' `\ j)%fset] `<=` I. + by apply: subset_trans J'I; apply/fsubsetP; exact: fsubsetDl. +have jJ' : j \in J'. + move/fsubsetP : JjJ'; apply. + by rewrite !inE eqxx. +have H1 : forall A, (F j `|` [set set0; setT]) A -> mu A = nu A. + move=> A [FjA|[->|->]]. + - rewrite muEj//(*; last by left*). + rewrite nuEj//(*; last by left*). + pose E' i := if i == j then A else E i. + transitivity (P (\big[setI/[set: T]]_(j0 <- (J')%fset) E' j0)). + rewrite [in RHS](big_fsetD1 j)//= {1}/E' eqxx//. + congr (P (_ `&` _)). + rewrite !big_seq; apply: eq_bigr => i. + rewrite !inE => /andP[ij _]. + by rewrite /E' (negbTE ij). + transitivity (\prod_(j0 <- (J')%fset) P (E' j0)); last first. + rewrite [in LHS](big_fsetD1 j)//= {1}/E' eqxx//. + congr (P _ * _). + rewrite !big_seq; apply: eq_bigr => i. + rewrite !inE => /andP[ij _]. + by rewrite /E' (negbTE ij). + apply: (ih _ JK _ JJ' J'I). + + move=> i iJ. + rewrite /E'. + case: ifPn => [/eqP ->|ij]. + rewrite inE. + by apply: sub_sigma_algebra. + rewrite EsF//. + by move/fproper_sub : JK => /fsubsetP; apply. + + move=> i. + rewrite ![in X in X -> _]inE /= ![in X in X -> _]inE => -[]. + move=> iJ' /negP. + rewrite negb_and negbK => /predU1P[ij|]. + rewrite /E' ij eqxx. + by rewrite inE. + move=> iK. + rewrite /E'. + rewrite ifF//; last first. + apply/negP => /eqP ?; subst j. + by rewrite jK in iK. + rewrite EF// !inE/=. + split => //. + exact/negP. + - by rewrite !measure0. + - rewrite muEj(*; last by right*). + rewrite nuEj(*; last by right*). + rewrite setTI. + rewrite probability_setT mul1e. + apply: (ih _ JK _ JJ'j J'jI). + + move=> i iJ. + rewrite EsF//. + by move/fproper_sub : JK => /fsubsetP; apply. + + move=> i. + rewrite ![in X in X -> _]inE /= ![in X in X -> _]inE => -[]. + move=> /andP[ij iJ']. + rewrite ij/= => iK. + by rewrite EF// !inE/=. +have H2 : forall A, <> A -> mu A = nu A. + move=> A sFjA. + have H3 : setI_closed (F j `|` [set set0]) by exact: H. + apply: (@g_sigma_algebra_measure_unique142b _ _ _ (F j `|` [set set0] : set (set T'))) => //. +(* apply: (g_sigma_algebra_measure_unique )).*) +(* apply: (@lem142b _ _ _ _ (F j `|` [set set0] : set (set T'))) => //.*) + move=> B /= [|]. + move: B. + case: indeF => + _. + apply. + by apply/set_mem. + by move=> ->. + - rewrite muEj(*; last by right*). + rewrite nuEj(*; last by right*). + rewrite setTI. + rewrite probability_setT mul1e. + apply: (ih _ JK _ JJ'j J'jI). + + move=> i iJ. + rewrite EsF//. + by move/fproper_sub : JK => /fsubsetP; apply. + + move=> i. + rewrite ![in X in X -> _]inE /= ![in X in X -> _]inE => -[]. + move=> /andP[ij iJ']. + rewrite ij/= => iK. + by rewrite EF// !inE/=. + move=> B FjB. + apply: H1. + case: FjB => [|->//]; first by left. + by right; left. + move: sFjA. + by apply: sub_smallest2r. +red in indeF. +have H3 : <> (E j). + apply/set_mem. + by rewrite EsF//. +rewrite [in LHS](big_fsetD1 j)//=. +rewrite [in RHS](big_fsetD1 j)//=. +have := H2 _ H3. +rewrite muEj. +by rewrite nuEj. +Qed. + +Lemma mutual_independence_bigcup (K0 : pointedType) (I0 : pointedType) (K : {fset K0}) + (I_ : K0 -> set I0) (I : set I0) (F : I0 -> set (set T)) : + trivIset [set` K] (fun i => I_ i) -> + (forall k, k \in K -> I_ k `<=` I) -> + mutual_independence P I F -> + mutual_independence P [set` K] (fun k => \bigcup_(i in I_ k) F i). +Proof. +move=> KI I_I PIF. +split=> [i Ki A [j ij FjA]|K' K'K E EF]. + case: PIF => + _ => /(_ j); apply => //. + by apply: (I_I _ Ki). +case: PIF => Fm PIF. +have @f : K0 -> I0. + (* pick on i from I_ k s.t. E k \in F (f k) *) + move=> k. + destruct (pselect (k \in K')). + generalize (EF _ i). + move/set_mem. + rewrite /bigcup/=. + move=> /cid2[i' _ _]. + exact: i'. + exact: point. +have H : forall k, k \in K' -> E k \in F (f k). + move=> k kK'. + rewrite /f/=. + case: pselect => [a|//]. + case: cid2 => //. + by move=> i iIk /mem_set. +have @g : I0 -> K0. + move=> i. + destruct (pselect (exists2 k, k \in K & i \in I_ k)). + case: (cid2 e). + move=> x _ _. + exact: x. + exact: point. +have gf i : i \in K' -> g (f i) = i. + move=> iK'. + rewrite /f. + case: pselect => // iK'_. + case: cid2 => //. + move=> j jIi FjEi. + rewrite /g. + case: pselect => // k'. + case: cid2 => //= k'' k''K. + move=> jIk'. + apply/eqP/negP => /negP k'i. + move/trivIsetP : KI => /(_ k'' i) /=. + move=> /(_ k''K (K'K _ iK') k'i)/= /eqP. + apply/negP. + apply/set0P. + exists j; split => //. + exact/set_mem. + exfalso. + apply: k'. + exists i => //. + by apply: K'K. + by apply/mem_set. +pose J' : {fset I0} := (\bigcup_(k <- K') [fset f k])%fset. +pose E' (i : I0) : set T := E (g i). +have H1 : P (\big[setI/[set: T]]_(j <- J') E' j) = \prod_(j <- J') P (E' j). + apply: PIF. + move=> i/=. + rewrite /J'. + move/bigfcupP => [k]. + rewrite andbT => kK'. + rewrite inE => /eqP ->. + apply: (I_I k) => /=. + by apply: K'K. + rewrite /f. + case: pselect => // kK'_. + by case: cid2 => //. + move=> i. + move=> /bigfcupP[k']. + rewrite andbT => k'K. + rewrite inE => /eqP ?; subst i. + rewrite /E'. + rewrite gf//. + by apply: H. +transitivity (P (\big[setI/[set: T]]_(j <- J') E' j)). + congr (P _). + apply/seteqP; split=> [t|]. + rewrite -bigcap_fset => L. + rewrite -bigcap_fset => j/=. + rewrite /J' => /bigfcupP[k]. + rewrite andbT => kK'. + rewrite !inE => /eqP ?; subst j. + rewrite /E'. + apply: L => //=. + by rewrite gf//. + move=> t. + rewrite -bigcap_fset => L. + rewrite -bigcap_fset => j/= jK'. + have /= := L (f j). + rewrite /E'. + rewrite gf//. + apply. + apply/bigfcupP. + exists j. + by rewrite jK'. + by rewrite inE. +rewrite H1. +rewrite /J' /E'. +rewrite partition_disjoint_bigfcup//=. + rewrite big_seq. + rewrite [in RHS]big_seq. + apply: eq_big => // k kK'. + by rewrite big_seq_fset1 gf//. +move=> k1 k2 k1K' k2K' k1k2 /=. +rewrite -fsetI_eq0 -fsubset0. +apply/fsubsetP => i. +rewrite !inE => /andP[]. +rewrite /f. +case: pselect. +move=> k1K'_. +case: cid2 => // i' i'k1 Fi' /eqP ?. +subst i'. +case: pselect. +move=> k2K'_. +case: cid2 => // j ik2 FjEk2 /eqP ?. +subst j. +move/trivIsetP : KI => /(_ k1 k2 (K'K _ k1K') (K'K _ k2K') k1k2). +move/seteqP => [+ _]. +move=> /(_ i)/=. +rewrite -falseE; apply. +by []. +done. +done. +Qed. + +End mutual_independence_properties. + +Section g_sigma_algebra_mapping_lemmas. +Context d {T : measurableType d} {R : realType}. + +Lemma g_sigma_algebra_mapping_comp (X : {mfun T >-> R}) (f : R -> R) : + measurable_fun setT f -> + g_sigma_algebra_mapping (f \o X)%R `<=` g_sigma_algebra_mapping X. +Proof. exact: preimage_class_comp. Qed. + +Lemma g_sigma_algebra_mapping_funrpos (X : {mfun T >-> R}) : + g_sigma_algebra_mapping X^\+%R `<=` d.-measurable. +Proof. +by move=> A/= -[B mB] <-; have := measurable_funrpos (measurable_funP X); exact. +Qed. + +Lemma g_sigma_algebra_mapping_funrneg (X : {mfun T >-> R}) : + g_sigma_algebra_mapping X^\-%R `<=` d.-measurable. +Proof. +by move=> A/= -[B mB] <-; have := measurable_funrneg (measurable_funP X); exact. +Qed. + +End g_sigma_algebra_mapping_lemmas. +Arguments g_sigma_algebra_mapping_comp {d T R X} f. + +Section independent_RVs. +Context {R : realType} d (T : measurableType d). +Context {I0 : choiceType}. +Context {d' : I0 -> _} (T' : forall i : I0, measurableType (d' i)). +Variable P : probability T R. + +Definition independent_RVs (I : set I0) + (X : forall i : I0, {mfun T >-> T' i}) : Prop := + mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). + +End independent_RVs. + +Section independent_RVs2. +Context {R : realType} d (T : measurableType d). +Variable P : probability T R. + +Definition independent_RVs2 d'' (T'' : measurableType d'') + (X Y : {mfun T >-> T''}) := + independent_RVs P [set: bool] [eta (fun=> cst point) with false |-> X, true |-> Y]. + +End independent_RVs2. + +Section thm216. +Context {R : realType} d (T : measurableType d). +Context {I0 : choiceType}. +Context {d' : I0 -> _} (T' : forall i : I0, measurableType (d' i)). +Variable P : probability T R. + +Lemma thm216 (I : set I0) (F : forall i : I0, set (set (T' i))) + (X : forall i : I0, {RV P >-> T' i}) : + (forall i, i \in I -> setI_closed (F i)) -> + (forall i, i \in I -> F i `<=` @measurable _ (T' i)) -> + (forall i, i \in I -> @measurable _ (T' i) = <>) -> + mutual_independence P I (fun i => preimage_class setT (X i) (F i)) -> + independent_RVs P I X. +Proof. +move=> IF FA AsF indeX1. +have H1 i : I i -> setI_closed (preimage_class setT (X i) (F i)). + move=> Ii A B [A' FiA']. + rewrite setTI => <-{A}. + move=> [B' FiB']. + rewrite setTI => <-{B}. + rewrite /preimage_class/=. + exists (A' `&` B'). + apply: IF => //. + exact/mem_set. + by rewrite setTI. + (* NB: lemma 2.16 *) +have H2 i : I i -> <> = g_sigma_algebra_mapping (X i). + move=> Ii. + rewrite /g_sigma_algebra_mapping. + rewrite AsF; last exact/mem_set. + by rewrite -sigma_algebra_preimage_classE. + (* NB: lemma 2.16 *) +rewrite /independent_RVs. +suff: mutual_independence P I (fun i : I0 => <>). + by apply: eq_mutual_independence. +apply: (mutual_independence_finite_g_sigma _ _).1. +- move=> i Ii. + apply: setI_closed_set0. + apply:H1. + exact/set_mem. +- split. + move=> i Ii. + move=> A [A' mA'] <-{A}. + apply/measurable_funP => //. + apply: FA => //. + exact/mem_set. + move=> J JI E EF. + by apply indeX1 => //. +Qed. + +End thm216. + +Section independent_RVs_lemmas. +Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). +Variable P : probability T R. +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 => /=. +- 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=> [[|]/= _|J J2 E JE]. +- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrpos. +- apply indeXY => //= i iJ; have := JE _ iJ. + 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=> [/= [|]// _ |J J2 E JE]. +- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrneg. +- apply indeXY => //= i iJ; have := JE _ iJ. + 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=> [/= [|]// _ |J J2 E JE]. +- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrneg. +- apply indeXY => //= i iJ; have := JE _ iJ. + 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_funrneg. +Qed. + +Lemma independent_RVs2_funrpospos (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+. +Proof. +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/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_funrpos. +Qed. + +End independent_RVs_lemmas. + +Definition preimage_classes I (d : I -> measure_display) + (Tn : forall k, semiRingOfSetsType (d k)) (T : Type) (fn : forall k, T -> Tn k) := + <>. +Arguments preimage_classes {I} d Tn {T} fn. + +Lemma measurable_fun_prod d [T : measurableType d] [R : realType] [D : set T] [I : eqType] + (s : seq I) [h : I -> T -> R] : + (forall n : I, n \in s -> measurable_fun D (h n)) -> + measurable_fun D (fun x => (\prod_(i <- s) h i x)%R). +Proof. +elim: s. + move=> mh. + under eq_fun do rewrite big_nil//=. + exact: measurable_cst. +move=> x y ih mh. +under eq_fun do rewrite big_cons//=. +apply: measurable_funM => //. + apply: mh. + by rewrite mem_head. +apply: ih => n ny. +apply: mh. +by rewrite inE orbC ny. +Qed. + +Section pairRV. +Context d d' {T : measurableType d} {T' : measurableType d'} {R : realType} + (P : probability T R). + +Definition pairRV (X Y : {RV P >-> T'}) : T * T -> T' * T' := + (fun x => (X x.1, Y x.2)). + +Lemma pairM (X Y : {RV P >-> T'}) : measurable_fun setT (pairRV X Y). +Proof. +rewrite /pairRV. +apply/prod_measurable_funP; split => //=. + rewrite (_ : (fst \o (fun x : T * T => (X x.1, Y x.2))) = (fun x => X x.1))//. + by apply/measurableT_comp => //=. +rewrite (_ : (snd \o (fun x : T * T => (X x.1, Y x.2))) = (fun x => Y x.2))//. +by apply/measurableT_comp => //=. +Qed. + +HB.instance Definition _ (X Y : {RV P >-> T'}) := + @isMeasurableFun.Build _ _ _ _ (pairRV X Y) (pairM X Y). + +End pairRV. + +Section product_expectation. +Context {R : realType} d (T : measurableType d). +Variable P : probability T R. +Local Open Scope ereal_scope. + +Let mu := @lebesgue_measure R. + +Let mprod_m (X Y : {RV P >-> R}) (A1 : set R) (A2 : set R) : + measurable A1 -> measurable A2 -> + (distribution P X \x distribution P Y) (A1 `*` A2) = + ((distribution P X) A1 * (distribution P Y) A2)%E. +Proof. +move=> mA1 mA2. +etransitivity. + by apply: product_measure1E. +rewrite /=. +done. +Qed. + +Lemma tmp0 (X Y : {RV P >-> R}) (B1 B2 : set R) : + measurable B1 -> measurable B2 -> + independent_RVs2 P X Y -> + P (X @^-1` B1 `&` Y @^-1` B2) = P (X @^-1` B1) * P (Y @^-1` B2). +Proof. +move=> mB1 mB2. +rewrite /independent_RVs2 /independent_RVs /mutual_independence /= => -[_]. +move/(_ [fset false; true]%fset (@subsetT _ _) + (fun b => if b then Y @^-1` B2 else X @^-1` B1)). +rewrite !big_fsetU1 ?inE//= !big_seq_fset1/=. +apply => -[|] /= _; rewrite !inE; rewrite /g_sigma_algebra_mapping. +by exists B2 => //; rewrite setTI. +by exists B1 => //; rewrite setTI. +Qed. + +Lemma tmp1 (X Y : {RV P >-> R}) (B1 B2 : set R) : + measurable B1 -> measurable B2 -> + independent_RVs2 P X Y -> + P (X @^-1` B1 `&` Y @^-1` B2) = (P \x P) (pairRV X Y @^-1` (B1 `*` B2)). +Proof. +move=> mB1 mB2 XY. +rewrite (_ : ((fun x : T * T => (X x.1, Y x.2)) @^-1` (B1 `*` B2)) = + (X @^-1` B1) `*` (Y @^-1` B2)); last first. + by apply/seteqP; split => [[x1 x2]|[x1 x2]]//. +rewrite product_measure1E; last 2 first. + rewrite -[_ @^-1` _]setTI. + by apply: (measurable_funP X). + rewrite -[_ @^-1` _]setTI. + by apply: (measurable_funP Y). +by rewrite tmp0//. +Qed. + +Let phi (x : R * R) := (x.1 * x.2)%R. +Let mphi : measurable_fun setT phi. +Proof. +rewrite /= /phi. +by apply: measurable_funM. +Qed. + +Lemma PP : (P \x P) setT = 1. +Proof. +rewrite /product_measure1 /=. +rewrite /xsection/=. +under eq_integral. + move=> t _. + rewrite (_ : [set y | (t, y) \in [set: T * T]] = setT); last first. + apply/seteqP; split => [x|x]// _ /=. + by rewrite in_setT. + rewrite probability_setT. + over. +rewrite integral_cst // mul1e. +apply: probability_setT. +Qed. + +HB.instance Definition _ := @Measure_isProbability.Build _ _ R (P \x P) PP. + +Lemma integrable_expectationM (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + 'E_(P \x P) [(fun x => `|X x.1 * Y x.2|)%R] < +oo +(* `|'E_(P) [(fun x => X x * Y x)%R]| < +oo *) . +Proof. +move=> indeXY iX iY. +(*apply: (@le_lt_trans _ _ 'E_(P \x P)[(fun x => `|(X x.1 * Y x.2)|%R)] + (* 'E_(P)[(fun x => `|(X x * Y x)|%R)] *) ). + rewrite unlock/=. + rewrite (le_trans (le_abse_integral _ _ _))//. + apply/measurable_EFinP/measurable_funM. + by apply/measurableT_comp => //. + by apply/measurableT_comp => //.*) +rewrite unlock. +rewrite [ltLHS](_ : _ = + \int[distribution (P \x P) (pairRV X Y)%R]_x `|x.1 * x.2|%:E); last first. + rewrite integral_distribution//=; last first. + apply/measurable_EFinP => //=. + by apply/measurableT_comp => //=. +(* admit. (* NG *)*) +rewrite [ltLHS](_ : _ = + \int[distribution P X \x distribution P Y]_x `|x.1 * x.2|%:E); last first. + apply: eq_measure_integral => //= A mA _. + apply/esym. + apply: product_measure_unique => //= A1 A2 mA1 mA2. + rewrite /pushforward/=. + rewrite -tmp1//. + by rewrite tmp0//. +rewrite fubini_tonelli1//=; last first. + by apply/measurable_EFinP => /=; apply/measurableT_comp => //=. +rewrite /fubini_F/= -/mu. +rewrite [ltLHS](_ : _ = \int[distribution P X]_x `|x|%:E * + \int[distribution P Y]_y `|y|%:E); last first. + rewrite -ge0_integralZr//=; last 2 first. + exact/measurable_EFinP. + by apply: integral_ge0 => //. + apply: eq_integral => x _. + rewrite -ge0_integralZl//=. + by under eq_integral do rewrite normrM. + exact/measurable_EFinP. +rewrite integral_distribution//=; last exact/measurable_EFinP. +rewrite integral_distribution//=; last exact/measurable_EFinP. +rewrite lte_mul_pinfty//. + by apply: integral_ge0 => //. + apply: integral_fune_fin_num => //=. + by move/integrable_abse : iX => //. +apply: integral_fune_lt_pinfty => //. +by move/integrable_abse : iY => //. +Qed. + +End product_expectation. + +Section product_expectation. +Context {R : realType} d (T : measurableType d). +Variable P : probability T R. +Local Open Scope ereal_scope. + +Import HBNNSimple. + +Let expectationM_nnsfun (f g : {nnsfun T >-> R}) : + (forall y y', y \in range f -> y' \in range g -> + P (f @^-1` [set y] `&` g @^-1` [set y']) = + P (f @^-1` [set y]) * P (g @^-1` [set y'])) -> + 'E_P [f \* g] = 'E_P [f] * 'E_P [g]. +Proof. +move=> fg; transitivity + ('E_P [(fun x => (\sum_(y \in range f) y * \1_(f @^-1` [set y]) x)%R) + \* (fun x => (\sum_(y \in range g) y * \1_(g @^-1` [set y]) x)%R)]). + by congr ('E_P [_]); apply/funext => t/=; rewrite (fimfunE f) (fimfunE g). +transitivity ('E_P [(fun x => (\sum_(y \in range f) \sum_(y' \in range g) y * y' + * \1_(f @^-1` [set y] `&` g @^-1` [set y']) x)%R)]). + congr ('E_P [_]); apply/funext => t/=. + rewrite mulrC; rewrite fsbig_distrr//=. (* TODO: lemma fsbig_distrl *) + apply: eq_fsbigr => y yf; rewrite mulrC; rewrite fsbig_distrr//=. + by apply: eq_fsbigr => y' y'g; rewrite indicI mulrCA !mulrA (mulrC y'). +rewrite unlock. +under eq_integral do rewrite -fsumEFin//. +transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + ((y * y')%:E * \int[P]_w (\1_(f @^-1` [set y] `&` g @^-1` [set y']) w)%:E))). + rewrite ge0_integral_fsum//=; last 2 first. + - move=> r; under eq_fun do rewrite -fsumEFin//. + apply: emeasurable_fun_fsum => // s. + apply/measurable_EFinP/measurable_funM => //. + exact/measurable_indic/measurableI. + - move=> r t _; rewrite lee_fin sumr_ge0 // => s _; rewrite -lee_fin. + by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. + apply: eq_fsbigr => y yf. + under eq_integral do rewrite -fsumEFin//. + rewrite ge0_integral_fsum//=; last 2 first. + - move=> r; apply/measurable_EFinP; apply: measurable_funM => //. + exact/measurable_indic/measurableI. + - move=> r t _. + by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. + apply: eq_fsbigr => y' y'g. + under eq_integral do rewrite EFinM. + by rewrite integralZl//; exact/integrable_indic/measurableI. +transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + ((y * y')%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E * + \int[P]_w (\1_(g @^-1` [set y']) w)%:E)))). + apply: eq_fsbigr => y fy; apply: eq_fsbigr => y' gy'; congr *%E. + transitivity ('E_P[\1_(f @^-1` [set y] `&` g @^-1` [set y'])]). + by rewrite unlock. + transitivity ('E_P[\1_(f @^-1` [set y])] * 'E_P[\1_(g @^-1` [set y'])]); + last by rewrite unlock. + rewrite expectation_indic//; last exact: measurableI. + by rewrite !expectation_indic// fg. +transitivity ( + (\sum_(y \in range f) (y%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E))) * + (\sum_(y' \in range g) (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E))). + transitivity (\sum_(y \in range f) (\sum_(y' \in range g) + (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E)%E)%R * + (y%:E * \int[P]_w (\1_(f @^-1` [set y]) w)%:E)%E%R); last first. + rewrite !fsbig_finite//= ge0_sume_distrl//; last first. + move=> r _; rewrite -integralZl//; last exact: integrable_indic. + by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. + by apply: eq_bigr => r _; rewrite muleC. + apply: eq_fsbigr => y fy. + rewrite !fsbig_finite//= ge0_sume_distrl//; last first. + move=> r _; rewrite -integralZl//; last exact: integrable_indic. + by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. + apply: eq_bigr => r _; rewrite (mulrC y) EFinM. + by rewrite [X in _ * X]muleC muleACA. +suff: forall h : {nnsfun T >-> R}, + (\sum_(y \in range h) (y%:E * \int[P]_w (\1_(h @^-1` [set y]) w)%:E)%E)%R + = \int[P]_w (h w)%:E. + by move=> suf; congr *%E; rewrite suf. +move=> h. +apply/esym. +under eq_integral do rewrite (fimfunE h). +under eq_integral do rewrite -fsumEFin//. +rewrite ge0_integral_fsum//; last 2 first. +- by move=> r; exact/measurable_EFinP/measurable_funM. +- by move=> r t _; rewrite lee_fin -lee_fin nnfun_muleindic_ge0. +by apply: eq_fsbigr => y fy; rewrite -integralZl//; exact/integrable_indic. +Qed. + +Lemma expectationM_ge0 (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + 'E_P[X] *? 'E_P[Y] -> + (forall t, 0 <= X t)%R -> (forall t, 0 <= Y t)%R -> + 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. +Proof. +move=> indeXY defXY X0 Y0. +have mX : measurable_fun setT (EFin \o X) by exact/measurable_EFinP. +have mY : measurable_fun setT (EFin \o Y) by exact/measurable_EFinP. +pose X_ := nnsfun_approx measurableT mX. +pose Y_ := nnsfun_approx measurableT mY. +have EXY : 'E_P[X_ n \* Y_ n] @[n --> \oo] --> 'E_P [X * Y]. + rewrite unlock; have -> : \int[P]_w ((X * Y) w)%:E = + \int[P]_x limn (fun n => (EFin \o (X_ n \* Y_ n)%R) x). + apply: eq_integral => t _; apply/esym/cvg_lim => //=. + rewrite fctE EFinM; under eq_fun do rewrite EFinM. + by apply: cvgeM; [rewrite mule_def_fin//| + apply: cvg_nnsfun_approx => //= x _; rewrite lee_fin..]. + apply: cvg_monotone_convergence => //. + - by move=> n; apply/measurable_EFinP; exact: measurable_funM. + - by move=> n t _; rewrite lee_fin. + - move=> t _ m n mn. + by rewrite lee_fin/= ler_pM//; exact/lefP/nd_nnsfun_approx. +have EX : 'E_P[X_ n] @[n --> \oo] --> 'E_P [X]. + rewrite unlock. + have -> : \int[P]_w (X w)%:E = \int[P]_x limn (fun n => (EFin \o X_ n) x). + by apply: eq_integral => t _; apply/esym/cvg_lim => //=; + apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. + apply: cvg_monotone_convergence => //. + - by move=> n; exact/measurable_EFinP. + - by move=> n t _; rewrite lee_fin. + - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. +have EY : 'E_P[Y_ n] @[n --> \oo] --> 'E_P [Y]. + rewrite unlock. + have -> : \int[P]_w (Y w)%:E = \int[P]_x limn (fun n => (EFin \o Y_ n) x). + by apply: eq_integral => t _; apply/esym/cvg_lim => //=; + apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. + apply: cvg_monotone_convergence => //. + - by move=> n; exact/measurable_EFinP. + - by move=> n t _; rewrite lee_fin. + - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. +have {EX EY}EXY' : 'E_P[X_ n] * 'E_P[Y_ n] @[n --> \oo] --> 'E_P[X] * 'E_P[Y]. + apply: cvgeM => //. +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 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 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. +pose AX := approx_A setT (EFin \o X). +pose AY := approx_A setT (EFin \o Y). +pose BX := approx_B setT (EFin \o X). +pose BY := approx_B setT (EFin \o Y). +have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> + g_sigma_algebra_mapping Z (approx_A setT (EFin \o Z) m k). + move=> mk; rewrite /g_sigma_algebra_mapping /approx_A mk setTI. + rewrite /preimage_class/=; exists [set` dyadic_itv R m k] => //. + rewrite setTI/=; apply/seteqP; split => z/=. + by rewrite inE/= => Zz; exists (Z z). + by rewrite inE/= => -[r rmk] [<-]. +have mB (Z : {RV P >-> R}) k : + g_sigma_algebra_mapping Z (approx_B setT (EFin \o Z) k). + rewrite /g_sigma_algebra_mapping /approx_B setTI /preimage_class/=. + by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itv_c_infty. +have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> + measurable_fun setT + (\1_(approx_A setT (EFin \o Z) n k) : g_sigma_algebra_mappingType Z -> R). + move=> k kn. + exact/(@measurable_indicP _ (g_sigma_algebra_mappingType Z))/mA. +rewrite !inE => /orP[|]/eqP->{i} //=. + have : @measurable_fun _ _ (g_sigma_algebra_mappingType X) _ setT (X_ n). + rewrite nnsfun_approxE//. + apply: measurable_funD => //=. + apply: measurable_fun_sum => //= k'; apply: measurable_funM => //. + by apply: measurable_indic; exact: mA. + apply: measurable_funM => //. + by apply: measurable_indic; exact: mB. + rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)). + by rewrite setTI. +have : @measurable_fun _ _ (g_sigma_algebra_mappingType Y) _ setT (Y_ n). + rewrite nnsfun_approxE//. + apply: measurable_funD => //=. + apply: measurable_fun_sum => //= k'; apply: measurable_funM => //. + by apply: measurable_indic; exact: mA. + apply: measurable_funM => //. + by apply: measurable_indic; exact: mB. +move=> /(_ measurableT [set y] (measurable_set1 y)). +by rewrite setTI. +Qed. + +Lemma integrable_expectationM000 (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + `|'E_P [X * Y]| < +oo. +Proof. +move=> indeXY iX iY. +apply: (@le_lt_trans _ _ 'E_P[(@normr _ _ \o X) * (@normr _ _ \o Y)]). + rewrite unlock/=. + rewrite (le_trans (le_abse_integral _ _ _))//. + apply/measurable_EFinP/measurable_funM. + by have /measurable_EFinP := measurable_int _ iX. + by have /measurable_EFinP := measurable_int _ iY. + apply: ge0_le_integral => //=. + - by apply/measurable_EFinP; exact/measurableT_comp. + - by move=> x _; rewrite lee_fin/= mulr_ge0/=. + - by apply/measurable_EFinP; apply/measurable_funM; exact/measurableT_comp. + - by move=> t _; rewrite lee_fin/= normrM. +rewrite expectationM_ge0//=. +- rewrite lte_mul_pinfty//. + + by rewrite expectation_ge0/=. + + rewrite expectation_fin_num//= compA//. + exact: (integrable_abse iX). + + by move/integrableP : iY => [_ iY]; rewrite unlock. +- exact: independent_RVs2_comp. +- apply: mule_def_fin; rewrite unlock integral_fune_fin_num//. + + exact: (integrable_abse iX). + + exact: (integrable_abse iY). +Qed. + +Lemma independent_integrableM (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + P.-integrable setT (EFin \o (X \* Y)%R). +Proof. +move=> indeXY iX iY. +apply/integrableP; split; first exact/measurable_EFinP/measurable_funM. +have := integrable_expectationM000 indeXY iX iY. +rewrite unlock => /abse_integralP; apply => //. +exact/measurable_EFinP/measurable_funM. +Qed. + +(* TODO: rename to expectationM when deprecation is removed *) +Lemma expectation_prod (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. +Proof. +move=> XY iX iY. +transitivity ('E_P[(X^\+ - X^\-) * (Y^\+ - Y^\-)]). + congr ('E_P[_]). + apply/funext => /=t. + by rewrite [in LHS](funrposneg X)/= [in LHS](funrposneg Y). +have ? : P.-integrable [set: T] (EFin \o X^\-%R). + by rewrite -funerneg; exact/integrable_funeneg. +have ? : P.-integrable [set: T] (EFin \o X^\+%R). + by rewrite -funerpos; exact/integrable_funepos. +have ? : P.-integrable [set: T] (EFin \o Y^\+%R). + by rewrite -funerpos; exact/integrable_funepos. +have ? : P.-integrable [set: T] (EFin \o Y^\-%R). + by rewrite -funerneg; exact/integrable_funeneg. +have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\+)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrpospos. +have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\+)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrnegpos. +have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\-)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrposneg. +have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\-)%R). + by apply: independent_integrableM => //=; exact: independent_RVs2_funrnegneg. +transitivity ('E_P[X^\+ * Y^\+] - 'E_P[X^\- * Y^\+] + - 'E_P[X^\+ * Y^\-] + 'E_P[X^\- * Y^\-]). + rewrite mulrDr !mulrDl -expectationB//= -expectationB//=; last first. + rewrite (_ : _ \o _ = EFin \o (X^\+ \* Y^\+)%R \- + (EFin \o (X^\- \* Y^\+)%R))//. + exact: integrableB. + rewrite -expectationD//=; last first. + rewrite (_ : _ \o _ = (EFin \o (X^\+ \* Y^\+)%R) + \- (EFin \o (X^\- \* Y^\+)%R) \- (EFin \o (X^\+ \* Y^\-)%R))//. + by apply: integrableB => //; exact: integrableB. + congr ('E_P[_]); apply/funext => t/=. + by rewrite !fctE !(mulNr,mulrN,opprK,addrA)/=. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrpospos. + by rewrite mule_def_fin// expectation_fin_num. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrnegpos. + by rewrite mule_def_fin// expectation_fin_num. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrposneg. + by rewrite mule_def_fin// expectation_fin_num. +rewrite [in LHS]expectationM_ge0//=; last 2 first. + exact: independent_RVs2_funrnegneg. + by rewrite mule_def_fin// expectation_fin_num//=. +transitivity ('E_P[X^\+ - X^\-] * 'E_P[Y^\+ - Y^\-]). + rewrite -addeA -addeACA -muleBr; last 2 first. + by rewrite expectation_fin_num. + by rewrite fin_num_adde_defr// expectation_fin_num. + rewrite -oppeB; last first. + by rewrite fin_num_adde_defr// fin_numM// expectation_fin_num. + rewrite -muleBr; last 2 first. + by rewrite expectation_fin_num. + by rewrite fin_num_adde_defr// expectation_fin_num. + rewrite -muleBl; last 2 first. + by rewrite fin_numB// !expectation_fin_num//. + by rewrite fin_num_adde_defr// expectation_fin_num. + by rewrite -expectationB//= -expectationB. +by congr *%E; congr ('E_P[_]); rewrite [RHS]funrposneg. +Qed. + +Lemma prodE (s : seq nat) (X : {RV P >-> R}^nat) (t : T) : + (\prod_(i <- s) X i t)%R = ((\prod_(j <- s) X j)%R t). +Proof. +by elim/big_ind2 : _ => //= {}X x {}Y y -> ->. +Qed. + +Lemma set_cons2 (I : eqType) (x y : I) : [set` [:: x; y]] = [set x ; y]. +Proof. +apply/seteqP; split => z /=; rewrite !inE. + move=> /orP[|] /eqP ->; auto. +by move=> [|] ->; rewrite eqxx// orbT. +Qed. + +Lemma independent_RVsD1 (I : {fset nat}) i0 (X : {RV P >-> R}^nat) : + independent_RVs P [set` I] X -> independent_RVs P [set` (I `\ i0)%fset] X. +Proof. +move=> H. +split => [/= i|/= J JIi0 E EK]. + rewrite !inE => /andP[ii0 iI]. + by apply H. +apply H => //. +by move=> /= x /JIi0 /=; rewrite !inE => /andP[]. +Qed. + +End product_expectation. diff --git a/theories/probability.v b/theories/probability.v index 66f39ef44..ad51df5cc 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -34,10 +34,6 @@ From mathcomp Require Import lebesgue_integral kernel. (* dRV_enum X == bijection between the domain and the range of X *) (* pmf X r := fine (P (X @^-1` [set r])) *) (* enum_prob X k == probability of the kth value in the range of X *) -(* independent_events I F == the events F indexed by I are independent *) -(* mutual_independence I F == the classes F indexed by I are independent *) -(* independent_RVs I X == the random variables X indexed by I are independent *) -(* independent_RVs2 X Y == the random variables X and Y are independent *) (* ``` *) (* *) (* ``` *) @@ -76,22 +72,23 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Definition random_variable (d : _) (T : measurableType d) (R : realType) - (P : probability T R) := {mfun T >-> R}. +Definition random_variable (d d' : _) (T : measurableType d) + (T' : measurableType d') (R : realType) (P : probability T R) := {mfun T >-> T'}. -Notation "{ 'RV' P >-> R }" := (@random_variable _ _ R P) : form_scope. +Notation "{ 'RV' P >-> T }" := (@random_variable _ _ _ T _ P) : form_scope. Lemma notin_range_measure d (T : measurableType d) (R : realType) (P : {measure set T -> \bar R}) (X : T -> R) r : r \notin range X -> P (X @^-1` [set r]) = 0%E. Proof. by rewrite notin_setE => hr; rewrite preimage10. Qed. -Lemma probability_range d (T : measurableType d) (R : realType) - (P : probability T R) (X : {RV P >-> R}) : P (X @^-1` range X) = 1%E. +Lemma probability_range d d' (T : measurableType d) (T' : measurableType d') + (R : realType) (P : probability T R) (X : {RV P >-> T'}) : + P (X @^-1` range X) = 1%E. Proof. by rewrite preimage_range probability_setT. Qed. -Definition distribution d (T : measurableType d) (R : realType) - (P : probability T R) (X : {mfun T >-> R}) := +Definition distribution d d' (T : measurableType d) (T' : measurableType d') + (R : realType) (P : probability T R) (X : {mfun T >-> T'}) := pushforward P (@measurable_funP _ _ _ _ X). Section distribution_is_probability. @@ -122,14 +119,15 @@ End distribution_is_probability. Section transfer_probability. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) (P : probability T R). +Context d d' (T : measurableType d) (T' : measurableType d') (R : realType). +Variable (P : probability T R). -Lemma probability_distribution (X : {RV P >-> R}) r : +Lemma probability_distribution (X : {RV P >-> T'}) r : P [set x | X x = r] = distribution P X [set r]. Proof. by []. Qed. -Lemma integral_distribution (X : {RV P >-> R}) (f : R -> \bar R) : - measurable_fun [set: R] f -> (forall y, 0 <= f y) -> +Lemma integral_distribution (X : {RV P >-> T'}) (f : T' -> \bar R) : + measurable_fun [set: T'] f -> (forall y, 0 <= f y) -> \int[distribution P X]_y f y = \int[P]_x (f \o X) x. Proof. by move=> mf f0; rewrite ge0_integral_pushforward. Qed. @@ -868,436 +866,6 @@ Qed. End discrete_distribution. -Section independent_events. -Context {R : realType} d {T : measurableType d}. -Variable P : probability T R. -Local Open Scope ereal_scope. - -Definition independent_events (I0 : choiceType) (I : set I0) (A : I0 -> set T) := - forall J : {fset I0}, [set` J] `<=` I -> - P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i). - -End independent_events. - -Section mutual_independence. -Context {R : realType} d {T : measurableType d}. -Variable P : probability T R. -Local Open Scope ereal_scope. - -Definition mutual_independence (I0 : choiceType) (I : set I0) - (F : I0 -> set (set T)) := - (forall i : I0, I i -> F i `<=` @measurable _ T) /\ - forall J : {fset I0}, - [set` J] `<=` I -> - forall E : I0 -> set T, - (forall i : I0, i \in J -> E i \in F i) -> - P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j). - -End mutual_independence. - -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 := - mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). - -Definition independent_RVs2 (X Y : {mfun T >-> T'}) := - independent_RVs [set: bool] [eta (fun=> cst point) with false |-> X, true |-> Y]. - -End independent_RVs. - -Section g_sigma_algebra_mapping_lemmas. -Context d {T : measurableType d} {R : realType}. - -Lemma g_sigma_algebra_mapping_comp (X : {mfun T >-> R}) (f : R -> R) : - measurable_fun setT f -> - g_sigma_algebra_mapping (f \o X)%R `<=` g_sigma_algebra_mapping X. -Proof. exact: preimage_class_comp. Qed. - -Lemma g_sigma_algebra_mapping_funrpos (X : {mfun T >-> R}) : - g_sigma_algebra_mapping X^\+%R `<=` d.-measurable. -Proof. -by move=> A/= -[B mB] <-; have := measurable_funrpos (measurable_funP X); exact. -Qed. - -Lemma g_sigma_algebra_mapping_funrneg (X : {mfun T >-> R}) : - g_sigma_algebra_mapping X^\-%R `<=` d.-measurable. -Proof. -by move=> A/= -[B mB] <-; have := measurable_funrneg (measurable_funP X); exact. -Qed. - -End g_sigma_algebra_mapping_lemmas. -Arguments g_sigma_algebra_mapping_comp {d T R X} f. - -Section independent_RVs_lemmas. -Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). -Variable P : probability T R. -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 => /=. -- 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=> [[|]/= _|J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrneg. -- exact: g_sigma_algebra_mapping_funrpos. -- apply indeXY => //= i iJ; have := JE _ iJ. - 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=> [/= [|]// _ |J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrpos. -- exact: g_sigma_algebra_mapping_funrneg. -- apply indeXY => //= i iJ; have := JE _ iJ. - 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=> [/= [|]// _ |J J2 E JE]. -- exact: g_sigma_algebra_mapping_funrneg. -- exact: g_sigma_algebra_mapping_funrneg. -- apply indeXY => //= i iJ; have := JE _ iJ. - 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_funrneg. -Qed. - -Lemma independent_RVs2_funrpospos (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+. -Proof. -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/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_funrpos. -Qed. - -End independent_RVs_lemmas. - -Section product_expectation. -Context {R : realType} d (T : measurableType d). -Variable P : probability T R. -Local Open Scope ereal_scope. - -Import HBNNSimple. - -Let expectationM_nnsfun (f g : {nnsfun T >-> R}) : - (forall y y', y \in range f -> y' \in range g -> - P (f @^-1` [set y] `&` g @^-1` [set y']) = - P (f @^-1` [set y]) * P (g @^-1` [set y'])) -> - 'E_P [f \* g] = 'E_P [f] * 'E_P [g]. -Proof. -move=> fg; transitivity - ('E_P [(fun x => (\sum_(y \in range f) y * \1_(f @^-1` [set y]) x)%R) - \* (fun x => (\sum_(y \in range g) y * \1_(g @^-1` [set y]) x)%R)]). - by congr ('E_P [_]); apply/funext => t/=; rewrite (fimfunE f) (fimfunE g). -transitivity ('E_P [(fun x => (\sum_(y \in range f) \sum_(y' \in range g) y * y' - * \1_(f @^-1` [set y] `&` g @^-1` [set y']) x)%R)]). - congr ('E_P [_]); apply/funext => t/=. - rewrite mulrC; rewrite fsbig_distrr//=. (* TODO: lemma fsbig_distrl *) - apply: eq_fsbigr => y yf; rewrite mulrC; rewrite fsbig_distrr//=. - by apply: eq_fsbigr => y' y'g; rewrite indicI mulrCA !mulrA (mulrC y'). -rewrite unlock. -under eq_integral do rewrite -fsumEFin//. -transitivity (\sum_(y \in range f) (\sum_(y' \in range g) - ((y * y')%:E * \int[P]_w (\1_(f @^-1` [set y] `&` g @^-1` [set y']) w)%:E))). - rewrite ge0_integral_fsum//=; last 2 first. - - move=> r; under eq_fun do rewrite -fsumEFin//. - apply: emeasurable_fun_fsum => // s. - apply/measurable_EFinP/measurable_funM => //. - exact/measurable_indic/measurableI. - - move=> r t _; rewrite lee_fin sumr_ge0 // => s _; rewrite -lee_fin. - by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. - apply: eq_fsbigr => y yf. - under eq_integral do rewrite -fsumEFin//. - rewrite ge0_integral_fsum//=; last 2 first. - - move=> r; apply/measurable_EFinP; apply: measurable_funM => //. - exact/measurable_indic/measurableI. - - move=> r t _. - by rewrite indicI/= indicE -mulrACA EFinM mule_ge0// nnfun_muleindic_ge0. - apply: eq_fsbigr => y' y'g. - under eq_integral do rewrite EFinM. - by rewrite integralZl//; exact/integrable_indic/measurableI. -transitivity (\sum_(y \in range f) (\sum_(y' \in range g) - ((y * y')%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E * - \int[P]_w (\1_(g @^-1` [set y']) w)%:E)))). - apply: eq_fsbigr => y fy; apply: eq_fsbigr => y' gy'; congr *%E. - transitivity ('E_P[\1_(f @^-1` [set y] `&` g @^-1` [set y'])]). - by rewrite unlock. - transitivity ('E_P[\1_(f @^-1` [set y])] * 'E_P[\1_(g @^-1` [set y'])]); - last by rewrite unlock. - rewrite expectation_indic//; last exact: measurableI. - by rewrite !expectation_indic// fg. -transitivity ( - (\sum_(y \in range f) (y%:E * (\int[P]_w (\1_(f @^-1` [set y]) w)%:E))) * - (\sum_(y' \in range g) (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E))). - transitivity (\sum_(y \in range f) (\sum_(y' \in range g) - (y'%:E * \int[P]_w (\1_(g @^-1` [set y']) w)%:E)%E)%R * - (y%:E * \int[P]_w (\1_(f @^-1` [set y]) w)%:E)%E%R); last first. - rewrite !fsbig_finite//= ge0_sume_distrl//; last first. - move=> r _; rewrite -integralZl//; last exact: integrable_indic. - by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. - by apply: eq_bigr => r _; rewrite muleC. - apply: eq_fsbigr => y fy. - rewrite !fsbig_finite//= ge0_sume_distrl//; last first. - move=> r _; rewrite -integralZl//; last exact: integrable_indic. - by apply: integral_ge0 => t _; rewrite nnfun_muleindic_ge0. - apply: eq_bigr => r _; rewrite (mulrC y) EFinM. - by rewrite [X in _ * X]muleC muleACA. -suff: forall h : {nnsfun T >-> R}, - (\sum_(y \in range h) (y%:E * \int[P]_w (\1_(h @^-1` [set y]) w)%:E)%E)%R - = \int[P]_w (h w)%:E. - by move=> suf; congr *%E; rewrite suf. -move=> h. -apply/esym. -under eq_integral do rewrite (fimfunE h). -under eq_integral do rewrite -fsumEFin//. -rewrite ge0_integral_fsum//; last 2 first. -- by move=> r; exact/measurable_EFinP/measurable_funM. -- by move=> r t _; rewrite lee_fin -lee_fin nnfun_muleindic_ge0. -by apply: eq_fsbigr => y fy; rewrite -integralZl//; exact/integrable_indic. -Qed. - -Lemma expectationM_ge0 (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> - 'E_P[X] *? 'E_P[Y] -> - (forall t, 0 <= X t)%R -> (forall t, 0 <= Y t)%R -> - 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. -Proof. -move=> indeXY defXY X0 Y0. -have mX : measurable_fun setT (EFin \o X) by exact/measurable_EFinP. -have mY : measurable_fun setT (EFin \o Y) by exact/measurable_EFinP. -pose X_ := nnsfun_approx measurableT mX. -pose Y_ := nnsfun_approx measurableT mY. -have EXY : 'E_P[X_ n \* Y_ n] @[n --> \oo] --> 'E_P [X * Y]. - rewrite unlock; have -> : \int[P]_w ((X * Y) w)%:E = - \int[P]_x limn (fun n => (EFin \o (X_ n \* Y_ n)%R) x). - apply: eq_integral => t _; apply/esym/cvg_lim => //=. - rewrite fctE EFinM; under eq_fun do rewrite EFinM. - by apply: cvgeM; [rewrite mule_def_fin//| - apply: cvg_nnsfun_approx => //= x _; rewrite lee_fin..]. - apply: cvg_monotone_convergence => //. - - by move=> n; apply/measurable_EFinP; exact: measurable_funM. - - by move=> n t _; rewrite lee_fin. - - move=> t _ m n mn. - by rewrite lee_fin/= ler_pM//; exact/lefP/nd_nnsfun_approx. -have EX : 'E_P[X_ n] @[n --> \oo] --> 'E_P [X]. - rewrite unlock. - have -> : \int[P]_w (X w)%:E = \int[P]_x limn (fun n => (EFin \o X_ n) x). - by apply: eq_integral => t _; apply/esym/cvg_lim => //=; - apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. - apply: cvg_monotone_convergence => //. - - by move=> n; exact/measurable_EFinP. - - by move=> n t _; rewrite lee_fin. - - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. -have EY : 'E_P[Y_ n] @[n --> \oo] --> 'E_P [Y]. - rewrite unlock. - have -> : \int[P]_w (Y w)%:E = \int[P]_x limn (fun n => (EFin \o Y_ n) x). - by apply: eq_integral => t _; apply/esym/cvg_lim => //=; - apply: cvg_nnsfun_approx => // x _; rewrite lee_fin. - apply: cvg_monotone_convergence => //. - - by move=> n; exact/measurable_EFinP. - - by move=> n t _; rewrite lee_fin. - - by move=> t _ m n mn; rewrite lee_fin/=; exact/lefP/nd_nnsfun_approx. -have {EX EY}EXY' : 'E_P[X_ n] * 'E_P[Y_ n] @[n --> \oo] --> 'E_P[X] * 'E_P[Y]. - apply: cvgeM => //. -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 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 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. -pose AX := approx_A setT (EFin \o X). -pose AY := approx_A setT (EFin \o Y). -pose BX := approx_B setT (EFin \o X). -pose BY := approx_B setT (EFin \o Y). -have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> - g_sigma_algebra_mapping Z (approx_A setT (EFin \o Z) m k). - move=> mk; rewrite /g_sigma_algebra_mapping /approx_A mk setTI. - rewrite /preimage_class/=; exists [set` dyadic_itv R m k] => //. - rewrite setTI/=; apply/seteqP; split => z/=. - by rewrite inE/= => Zz; exists (Z z). - by rewrite inE/= => -[r rmk] [<-]. -have mB (Z : {RV P >-> R}) k : - g_sigma_algebra_mapping Z (approx_B setT (EFin \o Z) k). - rewrite /g_sigma_algebra_mapping /approx_B setTI /preimage_class/=. - by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itv_c_infty. -have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> - measurable_fun setT - (\1_(approx_A setT (EFin \o Z) n k) : g_sigma_algebra_mappingType Z -> R). - move=> k kn. - exact/(@measurable_indicP _ (g_sigma_algebra_mappingType Z))/mA. -rewrite !inE => /orP[|]/eqP->{i} //=. - have : @measurable_fun _ _ (g_sigma_algebra_mappingType X) _ setT (X_ n). - rewrite nnsfun_approxE//. - apply: measurable_funD => //=. - apply: measurable_fun_sum => //= k'; apply: measurable_funM => //. - by apply: measurable_indic; exact: mA. - apply: measurable_funM => //. - by apply: measurable_indic; exact: mB. - rewrite /measurable_fun => /(_ measurableT _ (measurable_set1 x)). - by rewrite setTI. -have : @measurable_fun _ _ (g_sigma_algebra_mappingType Y) _ setT (Y_ n). - rewrite nnsfun_approxE//. - apply: measurable_funD => //=. - apply: measurable_fun_sum => //= k'; apply: measurable_funM => //. - by apply: measurable_indic; exact: mA. - apply: measurable_funM => //. - by apply: measurable_indic; exact: mB. -move=> /(_ measurableT [set y] (measurable_set1 y)). -by rewrite setTI. -Qed. - -Lemma integrable_expectationM (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> - `|'E_P [X * Y]| < +oo. -Proof. -move=> indeXY iX iY. -apply: (@le_lt_trans _ _ 'E_P[(@normr _ _ \o X) * (@normr _ _ \o Y)]). - rewrite unlock/=. - rewrite (le_trans (le_abse_integral _ _ _))//. - apply/measurable_EFinP/measurable_funM. - by have /measurable_EFinP := measurable_int _ iX. - by have /measurable_EFinP := measurable_int _ iY. - apply: ge0_le_integral => //=. - - by apply/measurable_EFinP; exact/measurableT_comp. - - by move=> x _; rewrite lee_fin/= mulr_ge0/=. - - by apply/measurable_EFinP; apply/measurable_funM; exact/measurableT_comp. - - by move=> t _; rewrite lee_fin/= normrM. -rewrite expectationM_ge0//=. -- rewrite lte_mul_pinfty//. - + by rewrite expectation_ge0/=. - + rewrite expectation_fin_num//= compA//. - exact: (integrable_abse iX). - + by move/integrableP : iY => [_ iY]; rewrite unlock. -- exact: independent_RVs2_comp. -- apply: mule_def_fin; rewrite unlock integral_fune_fin_num//. - + exact: (integrable_abse iX). - + exact: (integrable_abse iY). -Qed. - -Lemma independent_integrableM (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> - P.-integrable setT (EFin \o (X \* Y)%R). -Proof. -move=> indeXY iX iY. -apply/integrableP; split; first exact/measurable_EFinP/measurable_funM. -have := integrable_expectationM indeXY iX iY. -rewrite unlock => /abse_integralP; apply => //. -exact/measurable_EFinP/measurable_funM. -Qed. - -(* TODO: rename to expectationM when deprecation is removed *) -Lemma expectation_prod (X Y : {RV P >-> R}) : - independent_RVs2 P X Y -> - P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> - 'E_P [X * Y] = 'E_P [X] * 'E_P [Y]. -Proof. -move=> XY iX iY. -transitivity ('E_P[(X^\+ - X^\-) * (Y^\+ - Y^\-)]). - congr ('E_P[_]). - apply/funext => /=t. - by rewrite [in LHS](funrposneg X)/= [in LHS](funrposneg Y). -have ? : P.-integrable [set: T] (EFin \o X^\-%R). - by rewrite -funerneg; exact/integrable_funeneg. -have ? : P.-integrable [set: T] (EFin \o X^\+%R). - by rewrite -funerpos; exact/integrable_funepos. -have ? : P.-integrable [set: T] (EFin \o Y^\+%R). - by rewrite -funerpos; exact/integrable_funepos. -have ? : P.-integrable [set: T] (EFin \o Y^\-%R). - by rewrite -funerneg; exact/integrable_funeneg. -have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\+)%R). - by apply: independent_integrableM => //=; exact: independent_RVs2_funrpospos. -have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\+)%R). - by apply: independent_integrableM => //=; exact: independent_RVs2_funrnegpos. -have ? : P.-integrable [set: T] (EFin \o (X^\+ \* Y^\-)%R). - by apply: independent_integrableM => //=; exact: independent_RVs2_funrposneg. -have ? : P.-integrable [set: T] (EFin \o (X^\- \* Y^\-)%R). - by apply: independent_integrableM => //=; exact: independent_RVs2_funrnegneg. -transitivity ('E_P[X^\+ * Y^\+] - 'E_P[X^\- * Y^\+] - - 'E_P[X^\+ * Y^\-] + 'E_P[X^\- * Y^\-]). - rewrite mulrDr !mulrDl -expectationB//= -expectationB//=; last first. - rewrite (_ : _ \o _ = EFin \o (X^\+ \* Y^\+)%R \- - (EFin \o (X^\- \* Y^\+)%R))//. - exact: integrableB. - rewrite -expectationD//=; last first. - rewrite (_ : _ \o _ = (EFin \o (X^\+ \* Y^\+)%R) - \- (EFin \o (X^\- \* Y^\+)%R) \- (EFin \o (X^\+ \* Y^\-)%R))//. - by apply: integrableB => //; exact: integrableB. - congr ('E_P[_]); apply/funext => t/=. - by rewrite !fctE !(mulNr,mulrN,opprK,addrA)/=. -rewrite [in LHS]expectationM_ge0//=; last 2 first. - exact: independent_RVs2_funrpospos. - by rewrite mule_def_fin// expectation_fin_num. -rewrite [in LHS]expectationM_ge0//=; last 2 first. - exact: independent_RVs2_funrnegpos. - by rewrite mule_def_fin// expectation_fin_num. -rewrite [in LHS]expectationM_ge0//=; last 2 first. - exact: independent_RVs2_funrposneg. - by rewrite mule_def_fin// expectation_fin_num. -rewrite [in LHS]expectationM_ge0//=; last 2 first. - exact: independent_RVs2_funrnegneg. - by rewrite mule_def_fin// expectation_fin_num//=. -transitivity ('E_P[X^\+ - X^\-] * 'E_P[Y^\+ - Y^\-]). - rewrite -addeA -addeACA -muleBr; last 2 first. - by rewrite expectation_fin_num. - by rewrite fin_num_adde_defr// expectation_fin_num. - rewrite -oppeB; last first. - by rewrite fin_num_adde_defr// fin_numM// expectation_fin_num. - rewrite -muleBr; last 2 first. - by rewrite expectation_fin_num. - by rewrite fin_num_adde_defr// expectation_fin_num. - rewrite -muleBl; last 2 first. - by rewrite fin_numB// !expectation_fin_num//. - by rewrite fin_num_adde_defr// expectation_fin_num. - by rewrite -expectationB//= -expectationB. -by congr *%E; congr ('E_P[_]); rewrite [RHS]funrposneg. -Qed. - -End product_expectation. - Section bernoulli_pmf. Context {R : realType} (p : R). Local Open Scope ring_scope.