diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 7a1ad23f2..15ecdee55 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -53,55 +53,6 @@ ### Changed -- 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` @@ -129,13 +80,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/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.