From 9bda506071296300428c1b23f7809467804fcfbc Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 5 Nov 2024 11:35:42 +0900 Subject: [PATCH 1/4] expectation of product --- CHANGELOG_UNRELEASED.md | 108 ++++++++ theories/lebesgue_integral.v | 4 + theories/lebesgue_measure.v | 6 + theories/measure.v | 70 +++++ theories/numfun.v | 165 +++++++++++- theories/probability.v | 478 +++++++++++++++++++++++++++++++++++ 6 files changed, 827 insertions(+), 4 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 7a5228a1c..a49e2050b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -14,6 +14,25 @@ + lemma `partition_disjoint_bigfcup` - in `lebesgue_measure.v`: + lemma `measurable_indicP` +- in `constructive_ereal.v`: + + notation `\prod_( i <- r | P ) F` for extended real numbers and its variants + +- in `numfun.v`: + + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-` + + lemmas `funrpos_ge0`, `funrneg_ge0`, `funrposN`, `funrnegN`, `ge0_funrposE`, + `ge0_funrnegE`, `le0_funrposE`, `le0_funrnegE`, `ge0_funrposM`, `ge0_funrnegM`, + `le0_funrposM`, `le0_funrnegM`, `funr_normr`, `funrposneg`, `funrD_Dpos`, + `funrD_posD`, `funrpos_le`, `funrneg_le` + + lemmas `funerpos`, `funerneg` + +- in `measure.v`: + + lemma `preimage_class_comp` + + defintions `mapping_display`, `g_sigma_algebra_mappingType`, `g_sigma_algebra_mapping`, + notations `.-mapping`, `.-mapping.-measurable` + +- in `lebesgue_measure.v`: + + lemma `measurable_indicP` + + lemmas `measurable_funrpos`, `measurable_funrneg` - in `lebesgue_integral.v`: + definition `dyadic_approx` (was `Let A`) @@ -27,6 +46,19 @@ - in `probability.v`: + lemma `expectation_def` + notation `'M_` +- in `probability.v`: + + lemma `expectationM_ge0` + + definition `independent_events` + + definition `mutual_independence` + + definition `independent_RVs` + + definition `independent_RVs2` + + lemmas `g_sigma_algebra_mapping_comp`, `g_sigma_algebra_mapping_funrpos`, + `g_sigma_algebra_mapping_funrneg` + + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`, + `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`, + `independent_RVs2_funrpospos` + + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`, + ` expectation_prod` - in `lebesgue_integral.v`: + lemmas `integrable_pushforward`, `integral_pushforward` @@ -40,6 +72,61 @@ - in `lebesgue_integrale.v` + 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` + +### Changed + ### Renamed - in `lebesgue_measure.v`: @@ -64,6 +151,7 @@ - in `probability.v`: + `integral_distribution` -> `ge0_integral_distribution` + + `expectationM` -> `expectationMl` ### Generalized @@ -89,6 +177,26 @@ ### Removed +- in `topology_structure.v`: + + lemma `closureC` + +- in file `lebesgue_integral.v`: + + lemma `approximation` + +### 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`) + + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead) + - in `lebesgue_integral.v`: + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`) + notation `measurable_fun_indic` (deprecation since 0.6.3) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 5553c2ad2..c34879a56 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1608,7 +1608,11 @@ move=> m n mn; rewrite (nnsfun_approxE n) (nnsfun_approxE m). exact: nd_approx. Qed. +<<<<<<< HEAD #[deprecated(since="mathcomp-analysis 1.8.0", note="use `nnsfun_approx`, `cvg_nnsfun_approx`, and `nd_nnsfun_approx` instead")] +======= +#[deprecated(since="mathcomp-analysis 1.7.0", note="use `nnsfun_approx`, `cvg_nnsfun_approx`, and `nd_nnsfun_approx` instead")] +>>>>>>> da1f3437 (expectation of product) Lemma approximation : (forall t, D t -> (0 <= f t)%E) -> exists g : {nnsfun T >-> R}^nat, nondecreasing_seq (g : (T -> R)^nat) /\ (forall x, D x -> EFin \o g^~ x @ \oo --> f x). diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index c0abfbdd3..268d9e07e 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1053,6 +1053,12 @@ by move=> mf mg mD; move: (mD); apply: measurable_fun_if => //; [exact: measurable_fun_ltr|exact: measurable_funS mg|exact: measurable_funS mf]. Qed. +Lemma measurable_funrpos D f : measurable_fun D f -> measurable_fun D f^\+. +Proof. by move=> mf; exact: measurable_maxr. Qed. + +Lemma measurable_funrneg D f : measurable_fun D f -> measurable_fun D f^\-. +Proof. by move=> mf; apply: measurable_maxr => //; exact: measurableT_comp. Qed. + Lemma measurable_minr D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \min g). Proof. diff --git a/theories/measure.v b/theories/measure.v index b26b412db..f3fcb1177 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -70,6 +70,11 @@ From HB Require Import structures. (* G.-sigma.-measurable A == A is measurable for the sigma-algebra <> *) (* g_sigma_algebraType G == the measurableType corresponding to <> *) (* This is an HB alias. *) +(* g_sigma_algebra_mapping f == sigma-algebra generated by the mapping f *) +(* g_sigma_algebra_mappingType f == the measurableType corresponding to *) +(* g_sigma_algebra_mapping f *) +(* This is an HB alias. *) +(* f.-mapping.-measurable A == A is measurable for g_sigma_algebra_mapping f *) (* mu .-cara.-measurable == sigma-algebra of Caratheodory measurable sets *) (* ``` *) (* *) @@ -296,6 +301,9 @@ Reserved Notation "'\d_' a" (at level 8, a at level 2, format "'\d_' a"). Reserved Notation "G .-sigma" (at level 1, format "G .-sigma"). Reserved Notation "G .-sigma.-measurable" (at level 2, format "G .-sigma.-measurable"). +Reserved Notation "f .-mapping" (at level 1, format "f .-mapping"). +Reserved Notation "f .-mapping.-measurable" + (at level 2, format "f .-mapping.-measurable"). Reserved Notation "d .-ring" (at level 1, format "d .-ring"). Reserved Notation "d .-ring.-measurable" (at level 2, format "d .-ring.-measurable"). @@ -1729,6 +1737,16 @@ Definition preimage_class (aT rT : Type) (D : set aT) (f : aT -> rT) (G : set (set rT)) : set (set aT) := [set D `&` f @^-1` B | B in G]. +Lemma preimage_class_comp (aT : Type) + d (rT : measurableType d) d' (T : sigmaRingType d') + (g : rT -> T) (f : aT -> rT) (D : set aT) : + measurable_fun setT g -> + preimage_class D (g \o f) measurable `<=` preimage_class D f measurable. +Proof. +move=> mg A; rewrite /preimage_class/= => -[B GB]; exists (g @^-1` B) => //. +by rewrite -[X in measurable X]setTI; exact: mg. +Qed. + (* f is measurable on the sigma-algebra generated by itself *) Lemma preimage_class_measurable_fun d (aT : pointedType) (rT : measurableType d) (D : set aT) (f : aT -> rT) : @@ -1813,6 +1831,58 @@ Qed. End measurability. +Definition mapping_display {T T'} : (T -> T') -> measure_display. +Proof. exact. Qed. + +Definition g_sigma_algebra_mappingType d' (T : pointedType) + (T' : measurableType d') (f : T -> T') : Type := T. + +Definition g_sigma_algebra_mapping d' (T : pointedType) + (T' : measurableType d') (f : T -> T') := + preimage_class setT f (@measurable _ T'). + +Section mapping_generated_sigma_algebra. +Context {d'} (T : pointedType) (T' : measurableType d'). +Variable f : T -> T'. + +Let mapping_set0 : g_sigma_algebra_mapping f set0. +Proof. +rewrite /g_sigma_algebra_mapping /preimage_class/=. +by exists set0 => //; rewrite preimage_set0 setI0. +Qed. + +Let mapping_setC A : + g_sigma_algebra_mapping f A -> g_sigma_algebra_mapping f (~` A). +Proof. +rewrite /g_sigma_algebra_mapping /preimage_class/= => -[B mB] <-{A}. +by exists (~` B); [exact: measurableC|rewrite !setTI preimage_setC]. +Qed. + +Let mapping_bigcup (F : (set T)^nat) : + (forall i, g_sigma_algebra_mapping f (F i)) -> + g_sigma_algebra_mapping f (\bigcup_i (F i)). +Proof. +move=> mF; rewrite /g_sigma_algebra_mapping /preimage_class/=. +pose g := fun i => sval (cid2 (mF i)). +pose mg := fun i => svalP (cid2 (mF i)). +exists (\bigcup_i g i). + by apply: bigcup_measurable => k; case: (mg k). +rewrite setTI /g preimage_bigcup; apply: eq_bigcupr => k _. +by case: (mg k) => _; rewrite setTI. +Qed. + +HB.instance Definition _ := Pointed.on (g_sigma_algebra_mappingType f). + +HB.instance Definition _ := @isMeasurable.Build (mapping_display f) + (g_sigma_algebra_mappingType f) (g_sigma_algebra_mapping f) + mapping_set0 mapping_setC mapping_bigcup. + +End mapping_generated_sigma_algebra. + +Notation "f .-mapping" := (mapping_display f) : measure_display_scope. +Notation "f .-mapping.-measurable" := + (measurable : set (set (g_sigma_algebra_mappingType f))) : classical_set_scope. + Local Open Scope ereal_scope. Definition subset_sigma_subadditive {T} {R : numFieldType} diff --git a/theories/numfun.v b/theories/numfun.v index 3a892df55..159626c8f 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -14,12 +14,15 @@ From mathcomp Require Import function_spaces. (* ``` *) (* {nnfun T >-> R} == type of non-negative functions *) (* f ^\+ == the function formed by the non-negative outputs *) -(* of f (from a type to the type of extended real *) -(* numbers) and 0 otherwise *) -(* rendered as f ⁺ with company-coq (U+207A) *) +(* of f and 0 otherwise *) +(* The codomain of f is the real numbers in scope *) +(* ring_scope and the extended real numbers in scope *) +(* ereal_scope. *) +(* It is rendered as f ⁺ with company-coq (U+207A). *) (* f ^\- == the function formed by the non-positive outputs *) (* of f and 0 o.w. *) -(* rendered as f ⁻ with company-coq (U+207B) *) +(* Similar to ^\+. *) +(* It is rendered as f ⁻ with company-coq (U+207B). *) (* \1_ A == indicator function 1_A *) (* ``` *) (* *) @@ -127,6 +130,149 @@ Proof. by apply/funext=> x; rewrite /patch/=; case: ifP; rewrite ?mule0. Qed. End erestrict_lemmas. +Section funrposneg. +Local Open Scope ring_scope. + +Definition funrpos T (R : realDomainType) (f : T -> R) := + fun x => maxr (f x) 0. +Definition funrneg T (R : realDomainType) (f : T -> R) := + fun x => maxr (- f x) 0. + +End funrposneg. + +Notation "f ^\+" := (funrpos f) : ring_scope. +Notation "f ^\-" := (funrneg f) : ring_scope. + +Section funrposneg_lemmas. +Local Open Scope ring_scope. +Variables (T : Type) (R : realDomainType) (D : set T). +Implicit Types (f g : T -> R) (r : R). + +Lemma funrpos_ge0 f x : 0 <= f^\+ x. +Proof. by rewrite /funrpos /= le_max lexx orbT. Qed. + +Lemma funrneg_ge0 f x : 0 <= f^\- x. +Proof. by rewrite /funrneg le_max lexx orbT. Qed. + +Lemma funrposN f : (\- f)^\+ = f^\-. Proof. exact/funext. Qed. + +Lemma funrnegN f : (\- f)^\- = f^\+. +Proof. by apply/funext => x; rewrite /funrneg opprK. Qed. + +(* TODO: the following lemmas require a pointed type and realDomainType does +not seem to be at this point + +Lemma funrpos_restrict f : (f \_ D)^\+ = (f^\+) \_ D. +Proof. +by apply/funext => x; rewrite /patch/_^\+; case: ifP; rewrite //= maxxx. +Qed. + +Lemma funrneg_restrict f : (f \_ D)^\- = (f^\-) \_ D. +Proof. +by apply/funext => x; rewrite /patch/_^\-; case: ifP; rewrite //= oppr0 maxxx. +Qed.*) + +Lemma ge0_funrposE f : (forall x, D x -> 0 <= f x) -> {in D, f^\+ =1 f}. +Proof. by move=> f0 x; rewrite inE => Dx; apply/max_idPl/f0. Qed. + +Lemma ge0_funrnegE f : (forall x, D x -> 0 <= f x) -> {in D, f^\- =1 cst 0}. +Proof. +by move=> f0 x; rewrite inE => Dx; apply/max_idPr; rewrite lerNl oppr0 f0. +Qed. + +Lemma le0_funrposE f : (forall x, D x -> f x <= 0) -> {in D, f^\+ =1 cst 0}. +Proof. by move=> f0 x; rewrite inE => Dx; exact/max_idPr/f0. Qed. + +Lemma le0_funrnegE f : (forall x, D x -> f x <= 0) -> {in D, f^\- =1 \- f}. +Proof. +by move=> f0 x; rewrite inE => Dx; apply/max_idPl; rewrite lerNr oppr0 f0. +Qed. + +Lemma ge0_funrposM r f : (0 <= r)%R -> + (fun x => r * f x)^\+ = (fun x => r * (f^\+ x)). +Proof. by move=> ?; rewrite funeqE => x; rewrite /funrpos maxr_pMr// mulr0. Qed. + +Lemma ge0_funrnegM r f : (0 <= r)%R -> + (fun x => r * f x)^\- = (fun x => r * (f^\- x)). +Proof. +by move=> r0; rewrite funeqE => x; rewrite /funrneg -mulrN maxr_pMr// mulr0. +Qed. + +Lemma le0_funrposM r f : (r <= 0)%R -> + (fun x => r * f x)^\+ = (fun x => - r * (f^\- x)). +Proof. +move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr. +by rewrite funrposN ge0_funrnegM ?oppr_ge0. +Qed. + +Lemma le0_funrnegM r f : (r <= 0)%R -> + (fun x => r * f x)^\- = (fun x => - r * (f^\+ x)). +Proof. +move=> r0; rewrite -[in LHS](opprK r); under eq_fun do rewrite mulNr. +by rewrite funrnegN ge0_funrposM ?oppr_ge0. +Qed. + +Lemma funr_normr f : normr \o f = f^\+ \+ f^\-. +Proof. +rewrite funeqE => x /=; have [fx0|/ltW fx0] := leP (f x) 0. +- rewrite ler0_norm// /funrpos /funrneg. + move/max_idPr : (fx0) => ->; rewrite add0r. + by move: fx0; rewrite -{1}oppr0 lerNr => /max_idPl ->. +- rewrite ger0_norm// /funrpos /funrneg; move/max_idPl : (fx0) => ->. + by move: fx0; rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0. +Qed. + +Lemma funrposneg f : f = (fun x => f^\+ x - f^\- x). +Proof. +rewrite funeqE => x; rewrite /funrpos /funrneg; have [|/ltW] := leP (f x) 0. + by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r. +by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0. +Qed. + +Lemma funrD_Dpos f g : f \+ g = (f \+ g)^\+ \- (f \+ g)^\-. +Proof. +apply/funext => x; rewrite /funrpos /funrneg/=; have [|/ltW] := lerP 0 (f x + g x). +- by rewrite -{1}oppr0 -lerNl => /max_idPr ->; rewrite subr0. +- by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite opprK add0r. +Qed. + +Lemma funrD_posD f g : f \+ g = (f^\+ \+ g^\+) \- (f^\- \+ g^\-). +Proof. +apply/funext => x; rewrite /funrpos /funrneg/=. +have [|fx0] := lerP 0 (f x); last rewrite add0r. +- rewrite -{1}oppr0 lerNl => /max_idPr ->; have [|/ltW] := lerP 0 (g x). + by rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0 subr0. + by rewrite -{1}oppr0 -lerNr => /max_idPl ->; rewrite addr0 sub0r opprK. +- move/ltW : (fx0); rewrite -{1}oppr0 lerNr => /max_idPl ->. + have [|]/= := lerP 0 (g x); last rewrite add0r. + by rewrite -{1}oppr0 lerNl => /max_idPr ->; rewrite addr0 opprK addrC. + by rewrite -oppr0 ltrNr -{1}oppr0 => /ltW/max_idPl ->; rewrite opprD !opprK. +Qed. + +Lemma funrpos_le f g : + {in D, forall x, f x <= g x} -> {in D, forall x, f^\+ x <= g^\+ x}. +Proof. +move=> fg x Dx; rewrite /funrpos /maxr; case: ifPn => fx; case: ifPn => gx //. +- by rewrite leNgt. +- by move: fx; rewrite -leNgt => /(lt_le_trans gx); rewrite ltNge fg. +- exact: fg. +Qed. + +Lemma funrneg_le f g : + {in D, forall x, f x <= g x} -> {in D, forall x, g^\- x <= f^\- x}. +Proof. +move=> fg x Dx; rewrite /funrneg /maxr; case: ifPn => gx; case: ifPn => fx //. +- by rewrite leNgt. +- by move: gx; rewrite -leNgt => /(lt_le_trans fx); rewrite ltrN2 ltNge fg. +- by rewrite lerN2; exact: fg. +Qed. + +End funrposneg_lemmas. +#[global] +Hint Extern 0 (is_true (0%R <= _ ^\+ _)%R) => solve [apply: funrpos_ge0] : core. +#[global] +Hint Extern 0 (is_true (0%R <= _ ^\- _)%R) => solve [apply: funrneg_ge0] : core. + Section funposneg. Local Open Scope ereal_scope. @@ -276,6 +422,17 @@ Hint Extern 0 (is_true (0%R <= _ ^\+ _)%E) => solve [apply: funepos_ge0] : core. #[global] Hint Extern 0 (is_true (0%R <= _ ^\- _)%E) => solve [apply: funeneg_ge0] : core. +Section funrpos_funepos_lemmas. +Context {T : Type} {R : realDomainType}. + +Lemma funerpos (f : T -> R) : (EFin \o f)^\+%E = (EFin \o f^\+). +Proof. by apply/funext => x; rewrite /funepos /funrpos/= EFin_max. Qed. + +Lemma funerneg (f : T -> R) : (EFin \o f)^\-%E = (EFin \o f^\-). +Proof. by apply/funext => x; rewrite /funeneg /funrneg/= EFin_max. Qed. + +End funrpos_funepos_lemmas. + Definition indic {T} {R : ringType} (A : set T) (x : T) : R := (x \in A)%:R. Reserved Notation "'\1_' A" (at level 8, A at level 2, format "'\1_' A") . Notation "'\1_' A" := (indic A) : ring_scope. diff --git a/theories/probability.v b/theories/probability.v index c958e511f..14e61d0e4 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -35,6 +35,10 @@ 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 *) (* ``` *) (* *) (* ``` *) @@ -222,8 +226,13 @@ by apply/funext => t/=; rewrite big_map sumEFin mfun_sum. Qed. End expectation_lemmas. +<<<<<<< HEAD #[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to `expectationZl`")] Notation expectationM := expectationZl (only parsing). +======= +#[deprecated(since="mathcomp-analysis 1.7.0", note="use `expectationMl` instead")] +Notation expectationM := expectationMl (only parsing). +>>>>>>> e2b06243 (expectation of product) HB.lock Definition covariance {d} {T : measurableType d} {R : realType} (P : probability T R) (X Y : T -> R) := @@ -254,7 +263,11 @@ rewrite expectationD/=; last 2 first. - by rewrite compreBr// integrableB// compre_scale ?integrableZl. - by rewrite compre_scale// integrableZl// finite_measure_integrable_cst. rewrite 2?expectationB//= ?compre_scale// ?integrableZl//. +<<<<<<< HEAD rewrite 3?expectationZl//= ?finite_measure_integrable_cst//. +======= +rewrite 3?expectationMl//= ?finite_measure_integrable_cst//. +>>>>>>> e2b06243 (expectation of product) by rewrite expectation_cst mule1 fineM// EFinM !fineK// muleC subeK ?fin_numM. Qed. @@ -294,7 +307,11 @@ have aXY : (a \o* X * Y = a \o* (X * Y))%R. rewrite [LHS]covarianceE => [||//|] /=; last 2 first. - by rewrite compre_scale ?integrableZl. - by rewrite aXY compre_scale ?integrableZl. +<<<<<<< HEAD rewrite covarianceE// aXY !expectationZl//. +======= +rewrite covarianceE// aXY !expectationMl//. +>>>>>>> e2b06243 (expectation of product) by rewrite -muleA -muleBr// fin_num_adde_defr// expectation_fin_num. Qed. @@ -541,6 +558,24 @@ Qed. End variance. Notation "'V_ P [ X ]" := (variance P X). +(* TODO: move earlier *) +Section mfun_measurable_realType. +Context {d} {aT : measurableType d} {rT : realType}. + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ f^\+ + (measurable_funrpos (@measurable_funP _ _ _ _ f)). + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ f^\- + (measurable_funrneg (@measurable_funP _ _ _ _ f)). + +HB.instance Definition _ (f : {mfun aT >-> rT}) := + @isMeasurableFun.Build d _ _ _ (@normr _ _ \o f) + (measurableT_comp (@normr_measurable _ _) (@measurable_funP _ _ _ _ f)). + +End mfun_measurable_realType. + Section markov_chebyshev_cantelli. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). @@ -861,6 +896,438 @@ 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 0%N; 1%N] + [eta (fun=> cst point) with 0%N |-> X, 1%N |-> 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 => [i [|]->{i}/= Z/=|J J01 E JE]. +- by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; + exact/measurableT_comp. +- by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; + exact/measurableT_comp. +- apply indeXY => //= i iJ; have := JE _ iJ. + have : i \in [set 0%N; 1%N] by rewrite inE; apply: J01. + rewrite inE/= => -[|] /eqP ->/=; rewrite !inE. + + exact: g_sigma_algebra_mapping_comp. + + by case: ifPn => [/eqP ->|i0]; exact: g_sigma_algebra_mapping_comp. +Qed. + +Lemma independent_RVs2_funrposneg (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\-. +Proof. +move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrneg. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. +Qed. + +Lemma independent_RVs2_funrnegpos (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\+. +Proof. +move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrpos. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). + exact: measurable_funrpos. +Qed. + +Lemma independent_RVs2_funrnegneg (X Y : {RV P >-> R}) : + independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\-. +Proof. +move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +- exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrneg. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. + + 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=> [/= i [|] -> /=|J J01 E JE]. +- exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrpos. +- apply indeXY => //= i iJ; have := JE _ iJ. + move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + + 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 0%N; 1%N]%fset) + [eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], + 1%N |-> Y_ n @^-1` [set y]] j) = + \prod_(j <- [fset 0%N; 1%N]%fset) + P ([eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], + 1%N |-> Y_ n @^-1` [set y]] j). + by rewrite !big_fsetU1/= ?inE//= !big_seq_fset1/=. +move: indeXY => [/= _]; apply => // i. + by rewrite /= !inE => /orP[|]/eqP ->; auto. +pose AX := approx_A setT (EFin \o X). +pose AY := approx_A setT (EFin \o Y). +pose BX := approx_B setT (EFin \o X). +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. @@ -1346,18 +1813,29 @@ pose f_ := nnsfun_approx measurableT mf. transitivity (lim (\int[uniform_prob ab]_x (f_ n x)%:E @[n --> \oo])%E). rewrite -monotone_convergence//=. - apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //=. +<<<<<<< HEAD exact: cvg_nnsfun_approx. +======= + exact/cvg_nnsfun_approx. +>>>>>>> e2b06243 (expectation of product) - by move=> n; exact/measurable_EFinP/measurable_funTS. - by move=> n ? _; rewrite lee_fin. - by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. rewrite [X in _ = (_ * X)%E](_ : _ = lim (\int[mu]_(x in `[a, b]) (f_ n x)%:E @[n --> \oo])%E); last first. rewrite -monotone_convergence//=. +<<<<<<< HEAD - apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //. exact: cvg_nnsfun_approx. - by move=> n; exact/measurable_EFinP/measurable_funTS. - by move=> n ? _; rewrite lee_fin. - by move=> ? _ ? ? ?; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. +======= + - by apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. + - by move=> n; exact/measurable_EFinP/measurable_funTS. + - by move=> n ? _; rewrite lee_fin. + - by move=> ? _ u v uv; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. +>>>>>>> e2b06243 (expectation of product) rewrite -limeMl//. by apply: congr_lim; apply/funext => n /=; exact: integral_uniform_nnsfun. apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=. From 7be5887a2757558a0a9a7a500870092dc076b58e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 19 Nov 2024 10:35:23 +0900 Subject: [PATCH 2/4] use bool instead of I_2 --- theories/probability.v | 60 ++++++++++++++++++++---------------------- 1 file changed, 29 insertions(+), 31 deletions(-) diff --git a/theories/probability.v b/theories/probability.v index 14e61d0e4..983fbfa00 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -927,13 +927,12 @@ Section independent_RVs. Context {R : realType} d d' (T : measurableType d) (T' : measurableType d'). Variable P : probability T R. -Definition independent_RVs (I0 : choiceType) (I : set I0) - (X : I0 -> {mfun T >-> T'}) : Prop := +Definition independent_RVs (I0 : choiceType) + (I : set I0) (X : I0 -> {mfun T >-> T'}) : Prop := mutual_independence P I (fun i => g_sigma_algebra_mapping (X i)). Definition independent_RVs2 (X Y : {mfun T >-> T'}) := - independent_RVs [set 0%N; 1%N] - [eta (fun=> cst point) with 0%N |-> X, 1%N |-> Y]. + independent_RVs [set: bool] [eta (fun=> cst point) with false |-> X, true |-> Y]. End independent_RVs. @@ -968,54 +967,54 @@ Local Open Scope ring_scope. Lemma independent_RVs2_comp (X Y : {RV P >-> R}) (f g : {mfun R >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P (f \o X) (g \o Y). Proof. -move=> indeXY; split => [i [|]->{i}/= Z/=|J J01 E JE]. -- by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; - exact/measurableT_comp. -- by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; - exact/measurableT_comp. -- apply indeXY => //= i iJ; have := JE _ iJ. - have : i \in [set 0%N; 1%N] by rewrite inE; apply: J01. - rewrite inE/= => -[|] /eqP ->/=; rewrite !inE. - + exact: g_sigma_algebra_mapping_comp. - + by case: ifPn => [/eqP ->|i0]; exact: g_sigma_algebra_mapping_comp. +move=> indeXY; split => /=. +- move=> [] _ /= A. + + by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; + exact/measurableT_comp. + + by rewrite /g_sigma_algebra_mapping/= /preimage_class/= => -[B mB <-]; + exact/measurableT_comp. +- move=> J _ E JE. + apply indeXY => //= i iJ; have := JE _ iJ. + by move: i {iJ} =>[|]//=; rewrite !inE => Eg; + exact: g_sigma_algebra_mapping_comp Eg. Qed. Lemma independent_RVs2_funrposneg (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\-. Proof. -move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. -- exact: g_sigma_algebra_mapping_funrpos. +move=> indeXY; split=> [[|]/= _|J J2 E JE]. - exact: g_sigma_algebra_mapping_funrneg. +- exact: g_sigma_algebra_mapping_funrpos. - apply indeXY => //= i iJ; have := JE _ iJ. - move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). - exact: measurable_funrpos. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R) => //. + exact: measurable_funrpos. Qed. Lemma independent_RVs2_funrnegpos (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\+. Proof. -move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. -- exact: g_sigma_algebra_mapping_funrneg. +move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. - exact: g_sigma_algebra_mapping_funrpos. +- exact: g_sigma_algebra_mapping_funrneg. - apply indeXY => //= i iJ; have := JE _ iJ. - move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. - + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). - exact: measurable_funrneg. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). exact: measurable_funrpos. + + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). + exact: measurable_funrneg. Qed. Lemma independent_RVs2_funrnegneg (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\- Y^\-. Proof. -move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +move=> indeXY; split=> [/= [|]// _ |J J2 E JE]. - exact: g_sigma_algebra_mapping_funrneg. - exact: g_sigma_algebra_mapping_funrneg. - apply indeXY => //= i iJ; have := JE _ iJ. - move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). exact: measurable_funrneg. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr (- x) 0)%R). @@ -1025,11 +1024,11 @@ Qed. Lemma independent_RVs2_funrpospos (X Y : {RV P >-> R}) : independent_RVs2 P X Y -> independent_RVs2 P X^\+ Y^\+. Proof. -move=> indeXY; split=> [/= i [|] -> /=|J J01 E JE]. +move=> indeXY; split=> [/= [|]//= _ |J J2 E JE]. - exact: g_sigma_algebra_mapping_funrpos. - exact: g_sigma_algebra_mapping_funrpos. - apply indeXY => //= i iJ; have := JE _ iJ. - move/J01 : (iJ) => /= -[|] ->//=; rewrite !inE. + move/J2 : iJ; move: i => [|]// _; rewrite !inE. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). exact: measurable_funrpos. + apply: (g_sigma_algebra_mapping_comp (fun x => maxr x 0)%R). @@ -1168,15 +1167,14 @@ have {EX EY}EXY' : 'E_P[X_ n] * 'E_P[Y_ n] @[n --> \oo] --> 'E_P[X] * 'E_P[Y]. suff : forall n, 'E_P[X_ n \* Y_ n] = 'E_P[X_ n] * 'E_P[Y_ n]. by move=> suf; apply: (cvg_unique _ EXY) => //=; under eq_fun do rewrite suf. move=> n; apply: expectationM_nnsfun => x y xX_ yY_. -suff : P (\big[setI/setT]_(j <- [fset 0%N; 1%N]%fset) +suff : P (\big[setI/setT]_(j <- [fset false; true]%fset) [eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], 1%N |-> Y_ n @^-1` [set y]] j) = - \prod_(j <- [fset 0%N; 1%N]%fset) + \prod_(j <- [fset false; true]%fset) P ([eta fun=> set0 with 0%N |-> X_ n @^-1` [set x], 1%N |-> Y_ n @^-1` [set y]] j). by rewrite !big_fsetU1/= ?inE//= !big_seq_fset1/=. move: indeXY => [/= _]; apply => // i. - by rewrite /= !inE => /orP[|]/eqP ->; auto. pose AX := approx_A setT (EFin \o X). pose AY := approx_A setT (EFin \o Y). pose BX := approx_B setT (EFin \o X). From a1eb371cbe18b7c7bdc4086e28de870d482acdd3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 19 Nov 2024 10:45:03 +0900 Subject: [PATCH 3/4] complete thm 2.13 --- CHANGELOG_UNRELEASED.md | 82 +-- _CoqProject | 1 + theories/Make | 1 + theories/independence.v | 1130 ++++++++++++++++++++++++++++++++++ theories/lebesgue_integral.v | 4 - theories/probability.v | 458 -------------- 6 files changed, 1134 insertions(+), 542 deletions(-) create mode 100644 theories/independence.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a49e2050b..172ae0368 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -14,8 +14,6 @@ + lemma `partition_disjoint_bigfcup` - in `lebesgue_measure.v`: + lemma `measurable_indicP` -- in `constructive_ereal.v`: - + notation `\prod_( i <- r | P ) F` for extended real numbers and its variants - in `numfun.v`: + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-` @@ -31,7 +29,6 @@ notations `.-mapping`, `.-mapping.-measurable` - in `lebesgue_measure.v`: - + lemma `measurable_indicP` + lemmas `measurable_funrpos`, `measurable_funrneg` - in `lebesgue_integral.v`: @@ -46,7 +43,8 @@ - in `probability.v`: + lemma `expectation_def` + notation `'M_` -- in `probability.v`: + +- new file `independence.v`: + lemma `expectationM_ge0` + definition `independent_events` + definition `mutual_independence` @@ -72,61 +70,6 @@ - in `lebesgue_integrale.v` + 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` - -### Changed - ### Renamed - in `lebesgue_measure.v`: @@ -151,7 +94,6 @@ - in `probability.v`: + `integral_distribution` -> `ge0_integral_distribution` - + `expectationM` -> `expectationMl` ### Generalized @@ -177,26 +119,6 @@ ### Removed -- in `topology_structure.v`: - + lemma `closureC` - -- in file `lebesgue_integral.v`: - + lemma `approximation` - -### 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`) - + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead) - - in `lebesgue_integral.v`: + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`) + notation `measurable_fun_indic` (deprecation since 0.6.3) 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/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..6e8bd8d78 --- /dev/null +++ b/theories/independence.v @@ -0,0 +1,1130 @@ +(* 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 set systems 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} (P : probability T R) + {I0 : choiceType}. +Local Open Scope ereal_scope. + +Definition independent_events (I : set I0) (E : I0 -> set T) := + (forall i, I i -> measurable (E i)) /\ + forall J : {fset I0}, [set` J] `<=` I -> + P (\bigcap_(i in [set` J]) E i) = \prod_(i <- J) P (E i). + +End independent_events. + +Section mutual_independence. +Context {R : realType} d {T : measurableType d} (P : probability T R) + {I0 : choiceType}. +Local Open Scope ereal_scope. + +Definition g_sigma_family (I : set I0) (F : I0 -> set_system T) + : set_system T := + <>. + +Definition mutual_independence (I : set I0) (F : I0 -> set_system T) := + (forall i, I i -> F i `<=` measurable) /\ + forall J : {fset I0}, [set` J] `<=` I -> + forall E, (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 (I : set I0) (F F' : I0 -> set_system 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. + +End mutual_independence. + +Section independence. +Context {R : realType} d {T : measurableType d} (P : probability T R). +Local Open Scope ereal_scope. + +Definition independence (F G : set_system T) := + [/\ F `<=` measurable , G `<=` measurable & + forall A B, A \in F -> B \in G -> P (A `&` B) = P A * P B]. + +Lemma independenceP (F G : set_system T) : independence F G <-> + mutual_independence P [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//. + + rewrite -(set_fsetK J) Jbool. + rewrite fset_setU1//= fset_set1. + rewrite big_fsetU1 ?inE//=. + by rewrite big_seq_fset1. + + 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. +split. +- by case: indeF => /= [+ _] => /(_ true); exact. +- by 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 independence. + +Lemma setI_closed_setT T (F : set_system T) : + setI_closed F -> setI_closed (F `|` [set setT]). +Proof. +move=> IF=> C D [FC|/= ->{C}]. +- move=> [FD|/= ->{D}]. + by left; exact: IF. + by rewrite setIT; left. +- move=> [FD|->{D}]. + by rewrite setTI; left. + by rewrite !setTI; right. +Qed. + +Lemma setI_closed_set0 T (F : set_system T) : + setI_closed F -> setI_closed (F `|` [set set0]). +Proof. +move=> IF=> C D [FC|/= ->{C}]. +- move=> [FD|/= ->{D}]. + by left; exact: IF. + by rewrite setI0; right. +- move=> [FD|->{D}]. + by rewrite set0I; right. + by rewrite !set0I; right. +Qed. + +Lemma setI_closed_set0' T (F : set_system T) : + F set0 -> + setI_closed (F `|` [set set0]) -> setI_closed F. +Proof. +move=> F0 IF C D FC FD. +have [//|/= ->//] : (F `|` [set set0]) (C `&` D). +by apply: IF; left. +Qed. + +Lemma g_sigma_setU d {T : measurableType d} (F : set_system T) A : + <> A -> + <> = @measurable _ T -> + <> = <>. +Proof. +move=> FA sFT; apply/seteqP; split=> [B|B]. + by apply: sub_sigma_algebra2; exact: subsetUl. +apply: smallest_sub => // C [FC|/= ->//]. +exact: sub_gen_smallest. +Qed. + +Lemma g_sigma_algebra_finite_measure_unique {d} {T : measurableType d} + {R : realType} (G : set_system T) : + G `<=` d.-measurable -> + setI_closed G -> + forall m1 m2 : {finite_measure set T -> \bar R}, + m1 [set: T] = m2 [set: T] -> + (forall A : set T, G A -> m1 A = m2 A) -> + forall E : set T, <> E -> m1 E = m2 E. +Proof. +move=> Gm IG m1 m2 m1m2T 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 //|/= ->]. +- by move=> n; apply: fin_num_fun_lty; exact: fin_num_measure. +- move: E sGE; apply: smallest_sub => // C GC. + by apply: sub_gen_smallest; left. +Qed. + +(*Section lem142b. +Context d {T : measurableType d} {R : realType}. +Variable mu : {finite_measure set T -> \bar R}. +Variable F : set_system 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 mutual_independence_properties. +Context {R : realType} d {T : measurableType d} (P : probability T R). +Local Open Scope ereal_scope. + +(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(i) *) +Lemma mutual_independence_fset {I0 : choiceType} (I : {fset I0}) + (F : I0 -> set_system T) : + (forall i, i \in I -> F i `<=` measurable /\ (F i) [set: T]) -> + mutual_independence P [set` I] F <-> + forall E, (forall i, 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. + +(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(ii) *) +Lemma mutual_independence_finiteS {I0 : choiceType} (I : set I0) + (F : I0 -> set_system 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. + +(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(iii) *) +Theorem mutual_independence_finite_g_sigma {I0 : choiceType} (I : set I0) + (F : I0 -> set_system 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, (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'; exact: fsubsetU1. +have J'mE i : i \in J' -> d.-measurable (E i). + move=> iJ'. + case: indeF => + _ => /(_ i (J'I _ iJ')) Fim. + suff: <> (E i). + by apply: smallest_sub => //; exact: sigma_algebra_measurable. + apply/set_mem. + have [iK|iK] := boolP (i \in K); first by rewrite EsF. + have /set_mem : E i \in F i. + by rewrite EF// !inE/=; split => //; exact/negP. + 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 /[!inE] /andP[_ iJ']. + exact: J'mE. +pose mu0 A := P (A `&` \big[setI/[set: T]]_(j0 <- (J' `\ j)%fset) (E j0)). +pose mu := [the {finite_measure set _ -> \bar _} of mrestr P mmu]. +pose nu0 A := P A * \prod_(j0 <- (J' `\ j)%fset) P (E j0). +have nuk : (0 <= fine (\prod_(j0 <- (J' `\ j)%fset) P (E j0)))%R. + by rewrite fine_ge0// prode_ge0. +pose nu := [the measure _ _ of mscale (NngNum nuk) P]. +have nuEj A : nu A = P A * \prod_(j0 <- (J' `\ j)%fset) P (E j0). + rewrite /nu/= /mscale muleC/= fineK// big_seq. + rewrite prode_fin_num// => i /[!inE]/= /andP[ij iJ']. + by rewrite fin_num_measure//; exact: J'mE. +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' by move/fsubsetP : JjJ'; apply; rewrite !inE eqxx. +have Fjmunu A : (F j `|` [set set0; setT]) A -> mu A = nu A. + move=> [FjA|[->|->]]. + - rewrite nuEj. + pose E' i := if i == j then A else E i. + transitivity (P (\big[setI/[set: T]]_(j <- J') E' j)). + rewrite [in RHS](big_fsetD1 j)//= {1}/E' eqxx//; congr (P (_ `&` _)). + rewrite !big_seq; apply: eq_bigr => i /[!inE] /andP[ij _]. + by rewrite /E' (negbTE ij). + transitivity (\prod_(j <- J') P (E' j)); last first. + rewrite [in LHS](big_fsetD1 j)//= {1}/E' eqxx//; congr (P _ * _). + rewrite !big_seq; apply: eq_bigr => i /[!inE] /andP[ij _]. + by rewrite /E' (negbTE ij). + apply: (ih _ JK _ JJ' J'I). + + move=> i iJ. + rewrite /E'; case: ifPn => [/eqP ->|ij]. + by rewrite inE; exact: 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 => -[] iJ' /negP. + rewrite negb_and negbK => /predU1P[ij|iK]. + by rewrite /E' ij eqxx inE. + rewrite /E' ifF//; last first. + apply/negP => /eqP ij. + by rewrite ij jK in iK. + by rewrite EF// !inE/=; split => //; exact/negP. + - by rewrite !measure0. + - rewrite /mu /= /mrestr /= nuEj setTI 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'] iK. + by rewrite EF// !inE. +have sFjmunu A : <> A -> mu A = nu A. + move=> sFjA. + apply: (@g_sigma_algebra_finite_measure_unique _ _ _ (F j `|` [set set0])). + - move=> B /= [|->//]. + move: B. + case: indeF => + _. + by apply; exact/set_mem. + - exact: H. + - rewrite /mu/= /mrestr/= nuEj setTI 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: Fjmunu. + case: FjB => [|->//]; first by left. + by right; left. + - by move: sFjA; exact: sub_smallest2r. +rewrite [in LHS](big_fsetD1 j)//= [in RHS](big_fsetD1 j)//=. +have /sFjmunu : <> (E j) by apply/set_mem; rewrite EsF. +by rewrite /mu/= /mrestr/= nuEj. +Qed. + +(* pick an i from I_ k s.t. E k \in F (f k) *) +Local Definition f (K0 : choiceType) (K : {fset K0}) + (I0 : pointedType) (F : I0 -> set_system T) E I_ + (EF : forall k, k \in K -> E k \in \bigcup_(i in I_ k) F i) k := + if pselect (k \in K) is left kK then + sval (cid2 (set_mem (EF _ kK))) + else + point. + +Local Lemma f_prop (K0 : choiceType) (K : {fset K0}) + (I0 : pointedType) (F : I0 -> set_system T) E I_ + (EF : forall k, k \in K -> E k \in \bigcup_(i in I_ k) F i) k : + k \in K -> E k \in F (f EF k). +Proof. +move=> kK; rewrite /f; case: pselect => [kK_/=|//]. +by case: cid2 => // i/= ? /mem_set. +Qed. + +Local Lemma f_inj (K0 : choiceType) (K K' : {fset K0}) + (K'K : [set` K'] `<=` [set` K]) (I0 : pointedType) (F : I0 -> set_system T) + E I_ (EF : forall k, k \in K' -> E k \in \bigcup_(i in I_ k) F i) + (KI : trivIset [set` K] I_) k1 k2 : + k1 \in K' -> k2 \in K'-> k1 != k2 -> + ([fset f EF k1] `&` [fset f EF k2] = fset0)%fset. +Proof. +move=> k1K' k2K' k1k2; apply/eqP; rewrite -fsubset0. +apply/fsubsetP => i /[!inE] /andP[]. +rewrite /f; case: pselect => // k1K'_. +case: cid2 => // i' i'k1 Fi' /eqP ->{i}. +case: pselect => // k2K'_. +case: cid2 => // j ik2 FjEk2 /eqP/= i'j. +rewrite -{j}i'j in ik2 FjEk2 *. +move/trivIsetP : KI => /(_ _ _ (K'K _ k1K') (K'K _ k2K') k1k2). +by move/seteqP => [+ _] => /(_ i')/=; rewrite -falseE; exact. +Qed. + +Local Definition g (K0 : pointedType) (K' : {fset K0}) + (I0 : Type) (I_ : K0 -> set I0) (i : I0) : K0 := + if pselect (exists2 k, k \in K' & i \in I_ k) is left e then + sval (cid2 e) + else + point. + +Local Lemma gf (K0 I0 : pointedType) (F : I0 -> set_system T) + (K K' : {fset K0}) (K'K : [set` K'] `<=` [set` K]) + E I_ (EF : forall k, k \in K' -> E k \in \bigcup_(i in I_ k) F i) + (KI : trivIset [set` K] (fun i => I_ i)) i : i \in K' -> g K I_ (f EF i) = i. +Proof. +move=> iK'; rewrite /f; case: pselect => // iK'_. +case: cid2 => // j jIi FjEi. +rewrite /g; case: pselect => // k'; last first. + exfalso; apply: k'. + by exists i => //; [exact: K'K|exact/mem_set]. +case: cid2 => //= k'' k''K jIk'. +apply/eqP/negP => /negP k'i. +move/trivIsetP : KI => /(_ k'' i) /= /(_ k''K (K'K _ iK') k'i)/= /eqP. +apply/negP/set0P; exists j; split => //. +exact/set_mem. +Qed. + +(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.13(iv) *) +Lemma mutual_independence_bigcup (K0 I0 : pointedType) (K : {fset K0}) + (I_ : K0 -> set I0) (I : set I0) (F : I0 -> set_system 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]. + by case: PIF => + _ => /(_ j); apply => //; exact: (I_I _ Ki). +case: PIF => Fm PIF. +pose f' := f EF. +pose g' := g K I_. +pose J' := (\bigcup_(k <- K') [fset f' k])%fset. +pose E' := E \o g'. +suff: P (\big[setI/[set: T]]_(j <- J') E' j) = \prod_(j <- J') P (E' j). + move=> suf. + transitivity (P (\big[setI/[set: T]]_(j <- J') E' j)). + congr (P _). + apply/seteqP; split=> [t|]. + rewrite -!bigcap_fset => L j => /bigfcupP[k] /[!andbT] kK'. + rewrite !inE => /eqP ->{j}. + apply: L => //=. + by rewrite /g' /f' gf. + move=> t. + rewrite -!bigcap_fset => L j/= jK'. + have /= := L (f' j). + rewrite /E' /g' /f'/= gf//. + by apply; apply/bigfcupP; exists j;[rewrite jK'|rewrite inE]. + rewrite suf partition_disjoint_bigfcup//=. + rewrite [LHS]big_seq [RHS]big_seq; apply: eq_big => // k kK'. + by rewrite big_seq_fset1 /E' /g' /f' /= gf. + move=> k1 k2 k1K' k2K' k1k2 /=. + by rewrite -fsetI_eq0 -fsubset0 (f_inj K'K). +apply: PIF. +- move=> i/= /bigfcupP[k] /[!andbT] kK' /[!inE] /eqP ->. + apply: (I_I k) => /=; first exact: K'K. + by rewrite /f' /f; case: pselect => // kK'_; case: cid2. +- move=> i /bigfcupP[k'] /[!andbT] k'K /[!inE] /eqP ->{i}. + by rewrite /E' /g' /f'/= gf//; exact/set_mem/f_prop. +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 d' (T : measurableType d) (T' : measurableType d'). +Variable P : probability T R. + +Definition independent_RVs2 (X Y : {mfun T >-> T'}) := + independent_RVs P [set: bool] (fun b => if b then Y else X). + +End independent_RVs2. + +Section independent_generators. +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. + +(**md see Achim Klenke's Probability Thery, Ch.2, sec.2.1, thm.2.16 *) +Theorem independent_generators (I : set I0) (F : forall i : I0, set_system (T' i)) + (X : forall i, {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 closed_preimage 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. +have gen_preimage i : I i -> + <> = g_sigma_algebra_mapping (X i). + move=> Ii. + rewrite /g_sigma_algebra_mapping AsF; last exact/mem_set. + by rewrite -sigma_algebra_preimage_classE. +rewrite /independent_RVs. +suff: mutual_independence P I (fun i => <>). + exact: eq_mutual_independence. +apply: (mutual_independence_finite_g_sigma _ _).1. +- by move=> i Ii; apply: setI_closed_set0; exact/closed_preimage/set_mem. +- split => [i Ii A [A' mA'] <-{A}|J JI E EF]. + by apply/measurable_funP => //; apply: FA => //; exact/mem_set. + by apply indeX1. +Qed. + +End independent_generators. + +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_prod d [T : measurableType d] [R : realType] [D : set T] [I : eqType] + (s : seq I) [h : I -> T -> R] : + (forall i, i \in s -> measurable_fun D (h i)) -> + measurable_fun D (fun x => (\prod_(i <- s) h i x)%R). +Proof. +elim: s => [mh|x y ih mh]. + under eq_fun do rewrite big_nil//=. + exact: measurable_cst. +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_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 := dyadic_approx setT (EFin \o X). +pose AY := dyadic_approx setT (EFin \o Y). +pose BX := integer_approx setT (EFin \o X). +pose BY := integer_approx setT (EFin \o Y). +have mA (Z : {RV P >-> R}) m k : (k < m * 2 ^ m)%N -> + g_sigma_algebra_mapping Z (dyadic_approx setT (EFin \o Z) m k). + move=> mk; rewrite /g_sigma_algebra_mapping /dyadic_approx 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 (integer_approx setT (EFin \o Z) k). + rewrite /g_sigma_algebra_mapping /integer_approx setTI /preimage_class/=. + by exists `[k%:R, +oo[%classic => //; rewrite setTI preimage_itvcy. +have m1A (Z : {RV P >-> R}) : forall k, (k < n * 2 ^ n)%N -> + measurable_fun setT + (\1_(dyadic_approx 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_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_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/lebesgue_integral.v b/theories/lebesgue_integral.v index c34879a56..5553c2ad2 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1608,11 +1608,7 @@ move=> m n mn; rewrite (nnsfun_approxE n) (nnsfun_approxE m). exact: nd_approx. Qed. -<<<<<<< HEAD #[deprecated(since="mathcomp-analysis 1.8.0", note="use `nnsfun_approx`, `cvg_nnsfun_approx`, and `nd_nnsfun_approx` instead")] -======= -#[deprecated(since="mathcomp-analysis 1.7.0", note="use `nnsfun_approx`, `cvg_nnsfun_approx`, and `nd_nnsfun_approx` instead")] ->>>>>>> da1f3437 (expectation of product) Lemma approximation : (forall t, D t -> (0 <= f t)%E) -> exists g : {nnsfun T >-> R}^nat, nondecreasing_seq (g : (T -> R)^nat) /\ (forall x, D x -> EFin \o g^~ x @ \oo --> f x). diff --git a/theories/probability.v b/theories/probability.v index 983fbfa00..6468b6fd8 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -35,10 +35,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 *) (* ``` *) (* *) (* ``` *) @@ -226,13 +222,8 @@ by apply/funext => t/=; rewrite big_map sumEFin mfun_sum. Qed. End expectation_lemmas. -<<<<<<< HEAD #[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to `expectationZl`")] Notation expectationM := expectationZl (only parsing). -======= -#[deprecated(since="mathcomp-analysis 1.7.0", note="use `expectationMl` instead")] -Notation expectationM := expectationMl (only parsing). ->>>>>>> e2b06243 (expectation of product) HB.lock Definition covariance {d} {T : measurableType d} {R : realType} (P : probability T R) (X Y : T -> R) := @@ -263,11 +254,7 @@ rewrite expectationD/=; last 2 first. - by rewrite compreBr// integrableB// compre_scale ?integrableZl. - by rewrite compre_scale// integrableZl// finite_measure_integrable_cst. rewrite 2?expectationB//= ?compre_scale// ?integrableZl//. -<<<<<<< HEAD rewrite 3?expectationZl//= ?finite_measure_integrable_cst//. -======= -rewrite 3?expectationMl//= ?finite_measure_integrable_cst//. ->>>>>>> e2b06243 (expectation of product) by rewrite expectation_cst mule1 fineM// EFinM !fineK// muleC subeK ?fin_numM. Qed. @@ -307,11 +294,7 @@ have aXY : (a \o* X * Y = a \o* (X * Y))%R. rewrite [LHS]covarianceE => [||//|] /=; last 2 first. - by rewrite compre_scale ?integrableZl. - by rewrite aXY compre_scale ?integrableZl. -<<<<<<< HEAD rewrite covarianceE// aXY !expectationZl//. -======= -rewrite covarianceE// aXY !expectationMl//. ->>>>>>> e2b06243 (expectation of product) by rewrite -muleA -muleBr// fin_num_adde_defr// expectation_fin_num. Qed. @@ -896,436 +879,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. @@ -1811,29 +1364,18 @@ pose f_ := nnsfun_approx measurableT mf. transitivity (lim (\int[uniform_prob ab]_x (f_ n x)%:E @[n --> \oo])%E). rewrite -monotone_convergence//=. - apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //=. -<<<<<<< HEAD exact: cvg_nnsfun_approx. -======= - exact/cvg_nnsfun_approx. ->>>>>>> e2b06243 (expectation of product) - by move=> n; exact/measurable_EFinP/measurable_funTS. - by move=> n ? _; rewrite lee_fin. - by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. rewrite [X in _ = (_ * X)%E](_ : _ = lim (\int[mu]_(x in `[a, b]) (f_ n x)%:E @[n --> \oo])%E); last first. rewrite -monotone_convergence//=. -<<<<<<< HEAD - apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //. exact: cvg_nnsfun_approx. - by move=> n; exact/measurable_EFinP/measurable_funTS. - by move=> n ? _; rewrite lee_fin. - by move=> ? _ ? ? ?; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. -======= - - by apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx. - - by move=> n; exact/measurable_EFinP/measurable_funTS. - - by move=> n ? _; rewrite lee_fin. - - by move=> ? _ u v uv; rewrite lee_fin; exact/lefP/nd_nnsfun_approx. ->>>>>>> e2b06243 (expectation of product) rewrite -limeMl//. by apply: congr_lim; apply/funext => n /=; exact: integral_uniform_nnsfun. apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=. From add35c81aa89fd4ad00e53f20fb89db39ce717f5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 5 Nov 2024 11:35:42 +0900 Subject: [PATCH 4/4] a sampling theorem Co-authored-by: @affeldt-aist Co-authored-by: @t6s --- CHANGELOG_UNRELEASED.md | 47 ++ _CoqProject | 1 + reals/itv.v | 5 +- reals/signed.v | 1 + theories/Make | 1 + theories/independence.v | 29 +- theories/probability.v | 450 ++++++++++++++++- theories/sampling.v | 1043 +++++++++++++++++++++++++++++++++++++++ 8 files changed, 1541 insertions(+), 36 deletions(-) create mode 100644 theories/sampling.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 172ae0368..3851b9362 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -31,6 +31,22 @@ - in `lebesgue_measure.v`: + lemmas `measurable_funrpos`, `measurable_funrneg` +- in `numfun.v`: + + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-` + + lemmas `funrpos_ge0`, `funrneg_ge0`, `funrposN`, `funrnegN`, `ge0_funrposE`, + `ge0_funrnegE`, `le0_funrposE`, `le0_funrnegE`, `ge0_funrposM`, `ge0_funrnegM`, + `le0_funrposM`, `le0_funrnegM`, `funr_normr`, `funrposneg`, `funrD_Dpos`, + `funrD_posD`, `funrpos_le`, `funrneg_le` + + lemmas `funerpos`, `funerneg` + +- in `measure.v`: + + lemma `preimage_class_comp` + + defintions `mapping_display`, `g_sigma_algebra_mappingType`, `g_sigma_algebra_mapping`, + notations `.-mapping`, `.-mapping.-measurable` + +- in `lebesgue_measure.v`: + + lemmas `measurable_funrpos`, `measurable_funrneg` + - in `lebesgue_integral.v`: + definition `dyadic_approx` (was `Let A`) + definition `integer_approx` (was `Let B`) @@ -44,6 +60,28 @@ + lemma `expectation_def` + notation `'M_` +- new file `independence.v`: + + lemma `expectationM_ge0` + + definition `independent_events` + + definition `mutual_independence` + + definition `independent_RVs` + + definition `independent_RVs2` + + lemmas `g_sigma_algebra_mapping_comp`, `g_sigma_algebra_mapping_funrpos`, + `g_sigma_algebra_mapping_funrneg` + + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`, + `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`, + `independent_RVs2_funrpospos` + + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`, + ` expectation_prod` +- in `lebesgue_integral.v`: + + lemma `abse_integralP` +- in `signed.v`: + + definition `onem_NngNum` +- in `measure.v`: + + definition `bernoulli`, declared as a probability measure instance +- in `itv.v`: + + canonical `onem_itv01` + - new file `independence.v`: + lemma `expectationM_ge0` + definition `independent_events` @@ -94,6 +132,7 @@ - in `probability.v`: + `integral_distribution` -> `ge0_integral_distribution` + + `expectationM` -> `expectationMl` ### Generalized @@ -119,6 +158,14 @@ ### Removed +- in `topology_structure.v`: + + lemma `closureC` + +- in file `lebesgue_integral.v`: + + lemma `approximation` + +### Removed + - in `lebesgue_integral.v`: + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`) + notation `measurable_fun_indic` (deprecation since 0.6.3) diff --git a/_CoqProject b/_CoqProject index fd675df69..1dd1a187f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -87,6 +87,7 @@ theories/ftc.v theories/hoelder.v theories/probability.v theories/independence.v +theories/sampling.v theories/convex.v theories/charge.v theories/kernel.v diff --git a/reals/itv.v b/reals/itv.v index 7ac9e597b..4a2a1dee1 100644 --- a/reals/itv.v +++ b/reals/itv.v @@ -850,6 +850,9 @@ Lemma inum_lt : {mono inum : x y / (x < y)%O}. Proof. by []. Qed. End Morph. +Canonical onem_itv01 {R : realDomainType} (p : {i01 R}) : {i01 R} := + @Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum]. + Section Test1. Variable R : numDomainType. @@ -890,8 +893,6 @@ Definition s_of_pq (p q : {i01 R}) : {i01 R} := Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p. Proof. by apply/val_inj; rewrite /= subr0 mulr1 subKr. Qed. -Canonical onem_itv01 (p : {i01 R}) : {i01 R} := - @Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum]. Definition s_of_pq' (p q : {i01 R}) : {i01 R} := (`1- (`1-(p%:inum) * `1-(q%:inum)))%:i01. diff --git a/reals/signed.v b/reals/signed.v index 84fc0d8db..00ccfc44b 100644 --- a/reals/signed.v +++ b/reals/signed.v @@ -123,6 +123,7 @@ From mathcomp Require Import mathcomp_extra. (* Canonical instances are also provided according to types, as a *) (* fallback when no known operator appears in the expression. Look to *) (* nat_snum below for an example on how to add your favorite type. *) +(* *) (******************************************************************************) Reserved Notation "{ 'compare' x0 & nz & cond }" diff --git a/theories/Make b/theories/Make index dacb6a9d7..80918ce21 100644 --- a/theories/Make +++ b/theories/Make @@ -53,6 +53,7 @@ ftc.v hoelder.v probability.v independence.v +sampling.v lebesgue_stieltjes_measure.v convex.v charge.v diff --git a/theories/independence.v b/theories/independence.v index 6e8bd8d78..26ecb9962 100644 --- a/theories/independence.v +++ b/theories/independence.v @@ -766,24 +766,15 @@ 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 *) . + 'E_(P \x P) [(fun x => `|X x.1 * Y x.2|)%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. + rewrite ge0_integral_distribution//=; last first. apply/measurable_EFinP => //=. - by apply/measurableT_comp => //=. -(* admit. (* NG *)*) + exact/measurableT_comp. rewrite [ltLHS](_ : _ = \int[distribution P X \x distribution P Y]_x `|x.1 * x.2|%:E); last first. apply: eq_measure_integral => // A mA _. @@ -804,14 +795,14 @@ rewrite [ltLHS](_ : _ = \int[distribution P X]_x `|x|%:E * 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 ge0_integral_distribution//=; last exact/measurable_EFinP. +rewrite ge0_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 => //. +- exact: 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. diff --git a/theories/probability.v b/theories/probability.v index 6468b6fd8..a59d37ce4 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -7,7 +7,7 @@ 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. +From mathcomp Require Import lebesgue_integral kernel hoelder derive. (**md**************************************************************************) (* # Probability *) @@ -80,6 +80,225 @@ Definition random_variable d d' (T : measurableType d) (T' : measurableType d') Notation "{ 'RV' P >-> T' }" := (@random_variable _ _ _ T' _ P) : form_scope. +Section move_to_somewhere. + +Lemma mulr_funEcomp (R : semiRingType) (T : Type) (x : R) (f : T -> R) : + x \o* f = *%R^~ x \o f. +Proof. by []. Qed. + +Lemma bounded_image (T : Type) (K : numFieldType) + (V : pseudoMetricNormedZmodType K) (E : T -> V) (A : set T) : + [bounded y | y in E @` A] = [bounded E x | x in A]. +Proof. +rewrite /bounded_near !nearE. +congr (+oo _); apply: funext=> M. +apply: propext; split => /=. + by move=> + x Ax => /(_ (E x)); apply; exists x. +by move=> H x [] y Ay <-; exact: H. +Qed. + +Lemma finite_bounded (K : realFieldType) (V : pseudoMetricNormedZmodType K) + (A : set V) : finite_set A -> bounded_set A. +Proof. +move=> fA. +exists (\big[Order.max/0]_(y <- fset_set A) normr y). +split=> //. + apply: (big_ind (fun x => x \is Num.real))=> //. + by move=> *; exact: max_real. +move=> x ltx v Av /=. +apply/ltW/(le_lt_trans _ ltx)/le_bigmax_seq=> //. +by rewrite in_fset_set// inE. +Qed. + +Arguments sub_countable [T U]. +Arguments card_le_finite [T U]. +(* naming inconsistency: there is also `sub_finite_set`: + sub_finite_set : + forall [T : Type] [A B : set T], A `<=` B -> finite_set B -> finite_set A *) + +Lemma countable_range_comp (T0 T1 T2 : Type) (f : T0 -> T1) (g : T1 -> T2) : + countable (range f) \/ countable (range g) -> countable (range (g \o f)). +Proof. +rewrite -(image_comp f g). +case. + move=> cf; apply: (sub_countable _ (range f))=> //. + exact: card_image_le. +move=> cg; apply: (sub_countable _ (range g))=> //. +exact/subset_card_le/image_subset. +Qed. + +Lemma finite_range_comp (T0 T1 T2 : Type) (f : T0 -> T1) (g : T1 -> T2) : + finite_set (range f) \/ finite_set (range g) -> finite_set (range (g \o f)). +Proof. +rewrite -(image_comp f g). +case. + move=> cf; apply: (card_le_finite _ (range f))=> //. + exact: card_image_le. +move=> cg; apply: (card_le_finite _ (range g))=> //. +exact/subset_card_le/image_subset. +Qed. + +(* compatible generalization of lebesgue_integral.measurable_sfunP *) +Lemma measurable_sfunP d1 d2 (aT : measurableType d1) + (rT : measurableType d2) (f : {mfun aT >-> rT}) (Y : set rT) : + measurable Y -> measurable (f @^-1` Y). +Proof. by move=> mY; rewrite -[f @^-1` _]setTI; exact: measurable_funP. Qed. + +(* compatible generalizations of two lemmas from sequences.v *) +Lemma ereal_nondecreasing_series (R : realDomainType) (u_ : sequence \bar R) + N (P : pred nat) : + (forall n : nat, P n -> (0%R <= u_ n)%E) -> + {homo (fun n : nat => \sum_(N <= i < n | P i) u_ i) : + n m / (n <= m)%N >-> (n <= m)%E}. +Proof. by move=> u_ge0 n m nm; rewrite lee_sum_nneg_natr// => k _ /u_ge0. Qed. + +Lemma nneseries_lim_ge (R : realType) (u_ : sequence \bar R) m (P : pred nat) + (k : nat) : + (forall n : nat, P n -> (0%R <= u_ n)%E) -> + ((\sum_(m <= i < k | P i) u_ i)%R <= \big[+%R/0%R]_(m <= i -> //. +by apply: ereal_sup_ubound; exists k. +Qed. + +(* generalizations with an additional predicate (m <= i)%N as in big_geq_mkord *) +Lemma lee_sum_fset_nat_geq (R : realDomainType) (f : sequence \bar R) + (F : {fset nat}) (m n : nat) (P : pred nat) : + (forall i : nat, P i -> (0%R <= f i)%E) -> + [set` F] `<=` `I_n -> + ((\sum_(i <- F | P i && (m <= i)%N) f i)%R + <= (\sum_(m <= i < n | P i) f i)%R)%E. +Proof. +move=> f0 Fn. +rewrite big_geq_mkord/= -(big_mkord (fun i => P i && (m <= i)%N)). +apply: lee_sum_fset_nat=> //. +by move=> ? /andP [] *; exact: f0. +Qed. +Arguments lee_sum_fset_nat_geq {R f} F m n P. + +Lemma lee_sum_fset_lim_geq (R : realType) (f : sequence \bar R) + (F : {fset nat}) m (P : pred nat) : + (forall i : nat, P i -> (0%R <= f i)%E) -> + ((\sum_(i <- F | P i && (m <= i)%N) f i)%R + <= \big[+%R/0%R]_(m <= i f0; pose n := (\max_(k <- F) k).+1. +rewrite (le_trans (lee_sum_fset_nat_geq F m n _ _ _))//; last exact: nneseries_lim_ge. +move=> k /= kF; rewrite /n big_seq_fsetE/=. +by rewrite -[k]/(val [`kF]%fset) ltnS leq_bigmax. +Qed. +Arguments lee_sum_fset_lim_geq {R f} F m P. + +Lemma nneseries_esum_geq (R : realType) (a : nat -> \bar R) m (P : pred nat) : + (forall n : nat, P n -> (0%R <= a n)%E) -> + \big[+%R/0]_(m <= i a0; apply/eqP; rewrite eq_le; apply/andP; split. + apply: (lime_le (is_cvg_nneseries_cond a0)); apply: nearW => n. + apply: ereal_sup_ubound; exists [set` [fset val i | i in 'I_n & P i && (m <= i)%N]%fset]. + split; first exact: finite_fset. + by move=> /= k /imfsetP[/= i]; rewrite inE => + ->. + rewrite fsbig_finite//= set_fsetK big_imfset/=; last first. + by move=> ? ? ? ? /val_inj. + by rewrite big_filter big_enum_cond/= big_geq_mkord. +apply: ub_ereal_sup => _ [/= F [finF PF] <-]. +rewrite fsbig_finite//= -(big_rmcond_in (fun i=> P i && (m <= i)%N))/=. + exact: lee_sum_fset_lim_geq. +by move=> k; rewrite in_fset_set// inE => /PF ->. +Qed. + +Lemma nneseriesID (R : realType) m (a P : pred nat) (f : nat -> \bar R): + (forall k : nat, P k -> (0%R <= f k)%E) -> + \big[+%R/0]_(m <= k nn. +rewrite nneseries_esum_geq//. +rewrite (esumID a)/=; last by move=> ? /andP [] *; exact: nn. +have->: [set x | P x && (m <= x)%N] `&` (fun x : nat => a x) = + [set x | (P x && a x) && (m <= x)%N]. + by apply: funext=> x /=; rewrite (propext (rwP andP)) andbAC. +have->: [set x | P x && (m <= x)%N] `&` ~` (fun x : nat => a x) = + [set x | (P x && ~~ a x) && (m <= x)%N]. + apply: funext=> x /=. + by rewrite (propext (rwP negP)) (propext (rwP andP)) andbAC. +by rewrite -!nneseries_esum_geq//; move=> ? /andP [] *; exact: nn. +Qed. + +Lemma subset_itvW_bound (d : Order.disp_t) (T : porderType d) + (x y z u : itv_bound T) : + (x <= y)%O -> (z <= u)%O -> [set` Interval y z] `<=` [set` Interval x u]. +Proof. +move=> xy zu. +by apply: (@subset_trans _ [set` Interval x z]); + [exact: subset_itvr | exact: subset_itvl]. +Qed. + +Lemma gtr0_derive1_homo (R : realType) (f : R^o -> R^o) (a b : R) (sa sb : bool) : + (forall x : R, x \in `]a, b[ -> derivable f x 1) -> + (forall x : R, x \in `]a, b[ -> 0 < 'D_1 f x) -> + {within [set` (Interval (BSide sa a) (BSide sb b))], continuous f} -> + {in (Interval (BSide sa a) (BSide sb b)) &, {homo f : x y / x < y >-> x < y}}. +Proof. +move=> df dfgt0 cf x y + + xy. +rewrite !itv_boundlr /= => /andP [] ax ? /andP [] ? yb. +have HMVT1: {within `[x, y], continuous f}%classic. + exact/(continuous_subspaceW _ cf)/subset_itvW_bound. +have zab z : z \in `]x, y[ -> z \in `]a, b[. + apply: subset_itvW_bound. + by move: ax; clear; case: sa; rewrite !bnd_simp// => /ltW. + by move: yb; clear; case: sb; rewrite !bnd_simp// => /ltW. +have HMVT0 (z : R^o) : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z). + by move=> zxy; exact/derivableP/df/zab. +rewrite -subr_gt0. +have[z zxy ->]:= MVT xy HMVT0 HMVT1. +rewrite mulr_gt0// ?subr_gt0// dfgt0//. +exact: zab. +Qed. + +Lemma ger0_derive1_homo (R : realType) (f : R^o -> R^o) (a b : R) (sa sb : bool) : + (forall x : R, x \in `]a, b[ -> derivable f x 1) -> + (forall x : R, x \in `]a, b[ -> 0 <= 'D_1 f x) -> + {within [set` (Interval (BSide sa a) (BSide sb b))], continuous f} -> + {in (Interval (BSide sa a) (BSide sb b)) &, {homo f : x y / x <= y >-> x <= y}}. +Proof. +move=> df dfge0 cf x y + + xy. +rewrite !itv_boundlr /= => /andP [] ax ? /andP [] ? yb. +have HMVT1: {within `[x, y], continuous f}%classic. + exact/(continuous_subspaceW _ cf)/subset_itvW_bound. +have zab z : z \in `]x, y[ -> z \in `]a, b[. + apply: subset_itvW_bound. + by move: ax; clear; case: sa; rewrite !bnd_simp// => /ltW. + by move: yb; clear; case: sb; rewrite !bnd_simp// => /ltW. +have HMVT0 (z : R^o) : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z). + by move=> zxy; exact/derivableP/df/zab. +rewrite -subr_ge0. +move: (xy); rewrite le_eqVlt=> /orP [/eqP-> | xy']; first by rewrite subrr. +have[z zxy ->]:= MVT xy' HMVT0 HMVT1. +rewrite mulr_ge0// ?subr_ge0// dfge0//. +exact: zab. +Qed. + +Lemma memB_itv (R : numDomainType) (b0 b1 : bool) (x y z : R) : + (y - z \in Interval (BSide b0 x) (BSide b1 y)) = + (x + z \in Interval (BSide (~~ b1) x) (BSide (~~ b0) y)). +Proof. +rewrite !in_itv /= /Order.lteif !if_neg. +by rewrite gerBl gtrBl lerDl ltrDl lerBrDr ltrBrDr andbC. +Qed. + +(* generalizes mem_1B_itvcc *) +Lemma memB_itv0 (R : numDomainType) (b0 b1 : bool) (x y : R) : + (y - x \in Interval (BSide b0 0) (BSide b1 y)) = + (x \in Interval (BSide (~~ b1) 0) (BSide (~~ b0) y)). +Proof. by rewrite memB_itv add0r. Qed. + +End move_to_somewhere. +Arguments countable_range_comp [T0 T1 T2]. +Arguments finite_range_comp [T0 T1 T2]. + Lemma notin_range_measure d d' (T : measurableType 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. @@ -140,6 +359,12 @@ Lemma integral_distribution (X : {RV P >-> T'}) (f : T' -> \bar R) : \int[distribution P X]_y f y = \int[P]_x (f \o X) x. Proof. by move=> mf intf; rewrite integral_pushforward. Qed. +Lemma probability_setC' A : d.-measurable A -> P A = 1 - P (~` A). +Proof. +move=> mA. rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI (~` A)) -measureD ?setTD ?setCK//; first exact: measurableC. +by rewrite [ltLHS](@probability_setT _ _ _ P) ltry. +Qed. + End transfer_probability. HB.lock Definition expectation {d} {T : measurableType d} {R : realType} @@ -221,10 +446,83 @@ rewrite !big_cons expectationD ?IHX// (_ : _ \o _ = fun x => by apply/funext => t/=; rewrite big_map sumEFin mfun_sum. Qed. +Lemma sum_RV_ge0 (X : seq {RV P >-> R}) x : + (forall Xi, Xi \in X -> 0 <= Xi x)%R -> + (0 <= (\sum_(Xi <- X) Xi) x)%R. +Proof. +elim: X => [|X0 X IHX] Xi_ge0; first by rewrite big_nil. +rewrite big_cons. +rewrite addr_ge0//=; first by rewrite Xi_ge0// in_cons eq_refl. +by rewrite IHX// => Xi XiX; rewrite Xi_ge0// in_cons XiX orbT. +Qed. + End expectation_lemmas. #[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to `expectationZl`")] Notation expectationM := expectationZl (only parsing). + + + +(* Section product_lebesgue_measure. *) +(* Context {R : realType}. *) + +(* Definition p := [the sigma_finite_measure _ _ of *) +(* ([the sigma_finite_measure _ _ of (@lebesgue_measure R)] \x *) +(* [the sigma_finite_measure _ _ of (@lebesgue_measure R)])]%E. *) + +(* Fixpoint iter_mprod (n : nat) : {d & measurableType d} := *) +(* match n with *) +(* | 0%N => existT measurableType _ (salgebraType R.-ocitv.-measurable) *) +(* | n'.+1 => let t' := iter_mprod n' in *) +(* let a := existT measurableType _ (salgebraType R.-ocitv.-measurable) in *) +(* existT _ _ [the measurableType (projT1 a, projT1 t').-prod of *) +(* (projT2 a * projT2 t')%type] *) +(* end. *) + +(* Fixpoint measurable_of_typ (t : typ) : {d & measurableType d} := *) +(* match t with *) +(* | Unit => existT _ _ munit *) +(* | Bool => existT _ _ mbool *) +(* | Nat => existT _ _ (nat : measurableType _) *) +(* | Real => existT _ _ *) +(* [the measurableType _ of (@measurableTypeR R)] *) +(* end. *) + +(* Set Printing All. *) + +(* Fixpoint measurable_of_typ (d : nat) : {d & measurableType d} := *) +(* match d with *) +(* | O => existT _ _ (@lebesgue_measure R) *) +(* | d'.+1 => existT _ _ *) +(* [the measurableType (projT1 (@lebesgue_measure R), *) +(* projT1 (measurable_of_typ d')).-prod%mdisp of *) +(* ((@lebesgue_measure R) \x *) +(* projT2 (measurable_of_typ d'))%E] *) +(* end. *) + +(* Definition mtyp_disp t : measure_display := projT1 (measurable_of_typ t). *) + +(* Definition mtyp t : measurableType (mtyp_disp t) := *) +(* projT2 (measurable_of_typ t). *) + +(* Definition measurable_of_seq (l : seq typ) : {d & measurableType d} := *) +(* iter_mprod (map measurable_of_typ l). *) + + +(* Fixpoint leb_meas (d : nat) := *) +(* match d with *) +(* | 0%N => @lebesgue_measure R *) +(* | d'.+1 => *) +(* ((leb_meas d') \x (@lebesgue_measure R))%E *) +(* end. *) + + + + + +(* End product_lebesgue_measure. *) + + HB.lock Definition covariance {d} {T : measurableType d} {R : realType} (P : probability T R) (X Y : T -> R) := 'E_P[(X \- cst (fine 'E_P[X])) * (Y \- cst (fine 'E_P[Y]))]%E. @@ -559,6 +857,8 @@ HB.instance Definition _ (f : {mfun aT >-> rT}) := End mfun_measurable_realType. +Reserved Notation "'M_ X t" (format "''M_' X t", at level 5, t, X at next level). + Section markov_chebyshev_cantelli. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). @@ -584,6 +884,10 @@ Qed. Definition mmt_gen_fun (X : {RV P >-> R}) (t : R) := 'E_P[expR \o t \o* X]. Local Notation "'M_ X t" := (mmt_gen_fun X t). +Local Notation "'M_ X t" := (mmt_gen_fun X t). + +Definition nth_mmt (X : {RV P >-> R}) (n : nat) := 'E_P[X^+n]. + Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R -> P [set x | X x >= a]%R <= 'M_X r * (expR (- (r * a)))%:E. Proof. @@ -713,6 +1017,7 @@ by rewrite -mulrDl -mulrDr (addrC u0) [in RHS](mulrAC u0) -exprnP expr2 !mulrA. Qed. End markov_chebyshev_cantelli. +Notation "'M_ X t" := (mmt_gen_fun X t) : ereal_scope. HB.mixin Record MeasurableFun_isDiscrete d d' (T : measurableType d) (T' : measurableType d') (X : T -> T') of @MeasurableFun d d' T T' X := { @@ -734,6 +1039,22 @@ Definition discrete_random_variable d d' (T : measurableType d) Notation "{ 'dRV' P >-> T }" := (@discrete_random_variable _ _ _ T _ P) : form_scope. +Section dRV_comp. +Context d1 d2 d3 (T1 : measurableType d1) (T2 : measurableType d2) (T3 : measurableType d3). +Context (R : realType) (P : probability T1 R) (X : {dRV P >-> T2}) (f : {mfun T2 >-> T3}). + +Let countable_range_comp_dRV : countable (range (f \o X)). +Proof. apply: countable_range_comp; left; exact: countable_range. Qed. + +(* +HB.instance Definition _ := + MeasurableFun_isDiscrete.Build _ _ _ _ _ countable_range_comp_dRV. +*) + +Definition dRV_comp (* : {dRV P >-> T3} *) := f \o X. + +End dRV_comp. + Section dRV_definitions. Context {d} {d'} {T : measurableType d} {T' : measurableType d'} {R : realType} (P : probability T R). @@ -817,11 +1138,12 @@ End distribution_dRV. Section discrete_distribution. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) (P : probability T R). +Context d d' (T : measurableType d) (U : measurableType d') (R : realType) (P : probability T R). +Hypothesis mx : forall x : U, measurable [set x]. -Lemma dRV_expectation (X : {dRV P >-> R}) : - P.-integrable [set: T] (EFin \o X) -> - 'E_P[X] = \sum_(n -> U}) (f : {mfun U >-> R}) : + P.-integrable [set: T] (EFin \o f \o X) -> + 'E_P[f \o X] = \sum_(n ix; rewrite unlock. rewrite -[in LHS](_ : \bigcup_k (if k \in dRV_dom X then @@ -839,32 +1161,61 @@ have {tA}/trivIset_mkcond tXA : move/trivIsetP : tA => /(_ i j iX jX) Aij. by rewrite -preimage_setI Aij ?preimage_set0. rewrite integral_bigcup //; last 2 first. - - by move=> k; case: ifPn. + - move=> k; case: ifPn => // k_domX. + rewrite -[X in _ X]setTI. + exact: measurable_funP. - apply: (integrableS measurableT) => //. - by rewrite -bigcup_mkcond; exact: bigcup_measurable. + rewrite -bigcup_mkcond. apply: bigcup_measurable => k k_domX. + rewrite -[X in _ X]setTI. + exact: measurable_funP. transitivity (\sum_(i i _; case: ifPn => iX. by apply: eq_integral => t; rewrite in_setE/= => ->. by rewrite !integral_set0. -transitivity (\sum_(i i _; rewrite -integralZl//; last 2 first. - - by case: ifPn. + - case: ifPn => // i_domX. + rewrite -[X in _ X]setTI. + exact: measurable_funP. - apply/integrableP; split => //. rewrite (eq_integral (cst 1%E)); last by move=> x _; rewrite abse1. - rewrite integral_cst//; last by case: ifPn. + rewrite integral_cst//; last first. + case: ifPn => // i_domX. + rewrite -[X in _ X]setTI. + exact: measurable_funP. rewrite mul1e (@le_lt_trans _ _ 1%E) ?ltey//. - by case: ifPn => // _; exact: probability_le1. + case: ifPn => // _; apply: probability_le1 => //. + rewrite -[X in _ X]setTI. + exact: measurable_funP. by apply: eq_integral => y _; rewrite mule1. apply: eq_eseriesr => k _; case: ifPn => kX. - rewrite /= integral_cst//= mul1e probability_distribution muleC. - by rewrite distribution_dRV_enum. + rewrite /= integral_cst//=; last first. + rewrite -[X in _ X]setTI. + exact: measurable_funP. + by rewrite mul1e probability_distribution muleC distribution_dRV_enum. by rewrite integral_set0 mule0 /enum_prob patchE (negbTE kX) mul0e. Qed. +End discrete_distribution. + +Section discrete_distribution. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +Lemma dRV_expectation (X : {dRV P >-> R}) : + P.-integrable [set: T] (EFin \o X) -> + 'E_P[X] = \sum_(n iX. +have := @dRV_expectation_comp _ _ T R R P (@measurable_set1 R) X. +Admitted. + +(* check that expecation_bernoulli is recoverable by bernoulli_pmf *) + Definition pmf (X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])). Lemma expectation_pmf (X : {dRV P >-> R}) : @@ -875,7 +1226,7 @@ move=> iX; rewrite dRV_expectation// [in RHS]eseries_mkcond. apply: eq_eseriesr => k _. rewrite /enum_prob patchE; case: ifPn => kX; last by rewrite mul0e. by rewrite /pmf fineK// fin_num_measure. -Qed. +Abort. End discrete_distribution. @@ -1387,3 +1738,72 @@ apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=. Qed. End uniform_probability. + +(* Section bernoulli. *) +(* Variables (R : realType) (p : {nonneg R}) (p1 : (p%:num <= 1)%R). *) +(* Local Open Scope ring_scope. *) + +(* Definition bernoulli : set _ -> \bar R := *) +(* measure_add *) +(* [the measure _ _ of mscale p [the measure _ _ of dirac (1%R:R)]] *) +(* [the measure _ _ of mscale (NngNum (onem_ge0 p1)) [the measure _ _ of dirac (0%R:R)]]. *) + +(* HB.instance Definition _ := Measure.on bernoulli. *) + +(* Local Close Scope ring_scope. *) + +(* Let bernoulli_setT : bernoulli [set: _] = 1%E. *) +(* Proof. *) +(* rewrite /bernoulli/= /measure_add/= /msum 2!big_ord_recr/= big_ord0 add0e/=. *) +(* by rewrite /mscale/= !diracT !mule1 -EFinD add_onemK. *) +(* Qed. *) + +(* HB.instance Definition _ := *) +(* @Measure_isProbability.Build _ _ R bernoulli bernoulli_setT. *) + +(* End bernoulli. *) + +(* Section bernoulli_RV. *) +(* Context d (T : measurableType d) (R : realType) (P : probability T R). *) + +(* Definition bernoulli_RV (p : R) : {RV P >-> R} := *) + +(* End bernoulli_RV. *) + +(* Local Open Scope ereal_scope. *) +(* Lemma integral_bernoulli {R : realType} *) +(* (p : {nonneg R}) (p1 : (p%:num <= 1)%R) (f : R -> \bar R) : *) +(* measurable_fun setT f -> *) +(* (forall x, 0 <= f x) -> *) +(* \int[bernoulli p1]_y (f y) = p%:num%:E * f 1%R + (`1-(p%:num))%:E * f 0%R. *) +(* Proof. *) +(* move=> mf f0. *) +(* rewrite ge0_integral_measure_sum//= 2!big_ord_recl/= big_ord0 adde0/=. *) +(* by rewrite !ge0_integral_mscale//= !integral_dirac//= 2!diracT 2!mul1e. *) +(* Qed. *) + +(* Section measurable_fun. *) +(* Local Open Scope ereal_scope. *) +(* Context d (T : measurableType d) (R : realType). *) +(* Implicit Types (D : set T) (f g : T -> R). *) + +(* Lemma measurable_funD D f g : *) +(* measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g). *) +(* Proof. *) +(* move=> /measurable_EFinP mf /measurable_EFinP mg. *) +(* by have /measurable_EFinP := emeasurable_funD mf mg. *) +(* Qed. *) + +(* Lemma measurable_fun_sum D I s (h : I -> (T -> R)) : *) +(* (forall n, measurable_fun D (h n)) -> *) +(* measurable_fun D (fun x => \sum_(i <- s) h i x)%R. *) +(* Proof. *) +(* move=> mh. *) +(* apply/measurable_EFinP. *) +(* rewrite (_ : _ \o _ = (fun t => (\sum_(i <- s) (h i t)%:E))); last first. *) +(* by apply/funext => t/=; rewrite -sumEFin. *) +(* apply/emeasurable_fun_sum => i. *) +(* exact/measurable_EFinP. *) +(* Qed. *) + +(* End measurable_fun. *) diff --git a/theories/sampling.v b/theories/sampling.v new file mode 100644 index 000000000..176d452fb --- /dev/null +++ b/theories/sampling.v @@ -0,0 +1,1043 @@ +(* 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 derive esum measure exp numfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral kernel probability. +From mathcomp Require Import independence. + +Reserved Notation "' P [ A | B ]". + +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 d (T : measurableType d) (R : realType) (P : probability T R). +Local Open Scope ereal_scope. + +Lemma sub_independent_events (I : choiceType) (A B : set I) (E : I -> set T) : + A `<=` B -> independent_events P B E -> independent_events P A E. +Proof. +by move=> AB [mE h]; split=> [i /AB/mE//|C CA]; apply: h; apply: subset_trans AB. +Qed. + +Definition kwise_independent (I : choiceType) (A : set I) (E : I -> set T) k := + (forall i, A i -> measurable (E i)) /\ + forall B : {fset I}, [set` B] `<=` A -> (#|` B | <= k)%nat -> + P (\bigcap_(i in [set` B]) E i) = \prod_(i <- B) P (E i). + +Lemma sub_kwise_independent (I : choiceType) (A B : set I) (E : I -> set T) k : + A `<=` B -> kwise_independent B E k -> kwise_independent A E k. +Proof. +by move=> AB [mE h]; split=> [i /AB/mE//|C CA]; apply: h; apply: subset_trans AB. +Qed. + +Lemma mutual_indep_is_kwise_indep (I : choiceType) (A : set I) (E : I -> set T) k : + independent_events P A E -> kwise_independent A E k. +Proof. +rewrite /independent_events /kwise_independent. +move=> [mE miE]; split=> // B BleA _. +exact: miE. +Qed. + +Lemma nwise_indep_is_mutual_indep (I : choiceType) (A : {fset I}) (E : I -> set T) n : + #|` A | = n -> kwise_independent [set` A] E n -> independent_events P [set` A] E. +Proof. +rewrite /independent_events /kwise_independent. +move=> nA [mE miE]; split=> // B BleA. +apply: miE => //; rewrite -nA fsubset_leq_card//. +by apply/fsubsetP => x xB; exact: (BleA x). +Qed. + +Lemma mutually_independent_weak (I : choiceType) (E : I -> set T) (B : set I) : + (forall b, ~ B b -> E b = setT) -> + independent_events P [set: I] E <-> + independent_events P B E. +Proof. +move=> BE; split; first exact: sub_independent_events. +move=> [mE h]; split=> [i _|C _]. + by have [Bi|Bi] := pselect (B i); [exact: mE|rewrite BE]. +have [CB|CB] := pselect ([set` C] `<=` B); first by rewrite h. +rewrite -(setIT [set` C]) -(setUv B) setIUr bigcap_setU. +rewrite (@bigcapT _ _ (_ `&` ~` _)) ?setIT//; last by move=> i [_ /BE]. +have [D CBD] : exists D : {fset I}, [set` C] `&` B = [set` D]. + exists (fset_set ([set` C] `&` B)). + by rewrite fset_setK//; exact: finite_setIl. +rewrite CBD h; last first. + rewrite -CBD; exact: subIsetr. +rewrite [RHS]fsbig_seq//= [RHS](fsbigID B)//=. +rewrite [X in _ * X](_ : _ = 1) ?mule1; last first. + by rewrite fsbig1// => m [_ /BE] ->; rewrite probability_setT. +by rewrite CBD -fsbig_seq. +Qed. + +Lemma kwise_independent_weak (I : choiceType) (E : I -> set T) (B : set I) k : + (forall b, ~ B b -> E b = setT) -> + kwise_independent [set: I] E k <-> + kwise_independent B E k. +Proof. +move=> BE; split; first exact: sub_kwise_independent. +move=> [mE h]; split=> [i _|C _ Ck]. + by have [Bi|Bi] := pselect (B i); [exact: mE|rewrite BE]. +have [CB|CB] := pselect ([set` C] `<=` B); first by rewrite h. +rewrite -(setIT [set` C]) -(setUv B) setIUr bigcap_setU. +rewrite (@bigcapT _ _ (_ `&` ~` _)) ?setIT//; last by move=> i [_ /BE]. +have [D CBD] : exists D : {fset I}, [set` C] `&` B = [set` D]. + exists (fset_set ([set` C] `&` B)). + by rewrite fset_setK//; exact: finite_setIl. +rewrite CBD h; last 2 first. + - rewrite -CBD; exact: subIsetr. + - rewrite (leq_trans _ Ck)// fsubset_leq_card// -(set_fsetK D) -(set_fsetK C). + by rewrite -fset_set_sub// -CBD; exact: subIsetl. +rewrite [RHS]fsbig_seq//= [RHS](fsbigID B)//=. +rewrite [X in _ * X](_ : _ = 1) ?mule1; last first. + by rewrite fsbig1// => m [_ /BE] ->; rewrite probability_setT. +by rewrite CBD -fsbig_seq. +Qed. + +Lemma kwise_independent_weak01 E1 E2 : + kwise_independent [set: nat] (bigcap2 E1 E2) 2%N <-> + kwise_independent [set 0%N; 1%N] (bigcap2 E1 E2) 2%N. +Proof. +apply: kwise_independent_weak. +by move=> n /= /not_orP[/eqP /negbTE -> /eqP /negbTE ->]. +Qed. + +Lemma independent_events_weak' (I : choiceType) (E : I -> set T) (B : set I) : + (forall b, ~ B b -> E b = setT) -> + independent_events P [set: I] E <-> + independent_events P B E. +Proof. +move=> BE; split; first exact: sub_independent_events. +move=> [mE h]; split=> [i _|C CI]. + by have [Bi|Bi] := pselect (B i); [exact: mE|rewrite BE]. +have [CB|CB] := pselect ([set` C] `<=` B); first by rewrite h. +rewrite -(setIT [set` C]) -(setUv B) setIUr bigcap_setU. +rewrite (@bigcapT _ _ (_ `&` ~` _)) ?setIT//; last by move=> i [_ /BE]. +have [D CBD] : exists D : {fset I}, [set` C] `&` B = [set` D]. + exists (fset_set ([set` C] `&` B)). + by rewrite fset_setK//; exact: finite_setIl. +rewrite CBD h; last first. + - rewrite -CBD; exact: subIsetr. +rewrite [RHS]fsbig_seq//= [RHS](fsbigID B)//=. +rewrite [X in _ * X](_ : _ = 1) ?mule1; last first. + by rewrite fsbig1// => m [_ /BE] ->; rewrite probability_setT. +by rewrite CBD -fsbig_seq. +Qed. + +Definition pairwise_independent E1 E2 := + kwise_independent [set 0; 1]%N (bigcap2 E1 E2) 2. + +Lemma pairwise_independentM_old (E1 E2 : set T) : + pairwise_independent E1 E2 <-> + [/\ d.-measurable E1, d.-measurable E2 & P (E1 `&` E2) = P E1 * P E2]. +Proof. +split. +- move=> [mE1E2 /(_ [fset 0%N; 1%N]%fset)]. + rewrite bigcap_fset !big_fsetU1 ?inE//= !big_seq_fset1/= => ->; last 2 first. + + by rewrite set_fsetU !set_fset1; exact: subset_refl. + + rewrite cardfs2//. + split => //. + + by apply: (mE1E2 0%N) => /=; left. + + by apply: (mE1E2 1%N) => /=; right. +- move=> [mE1 mE2 E1E2M]. + split => //=. + + by move=> [| [| [|]]]//=. + + move=> B _; have [B0|B0] := boolP (0%N \in B); last first. + have [B1|B1] := boolP (1%N \in B); last first. + rewrite big1_fset; last first. + move=> k kB _; rewrite /bigcap2. + move: kB B0; case: ifPn => [/eqP -> ->//|k0 kB B0]. + move: kB B1; case: ifPn => [/eqP -> ->//|_ _ _]. + by rewrite probability_setT. + rewrite bigcapT ?probability_setT// => k/= kB. + move: kB B0 B1; case: ifPn => [/eqP -> ->//|k0]. + by case: ifPn => [/eqP -> ->|]. + rewrite (bigcap_setD1 1%N _ [set` B])//=. + rewrite bigcapT ?setIT; last first. + move=> k [/= kB /eqP /negbTE ->]. + by move: kB B0; case: ifPn => [/eqP -> ->|]. + rewrite (big_fsetD1 1%N)//= big1_fset ?mule1// => k. + rewrite !inE => /andP[/negbTE -> kB] _. + move: kB B0; case: ifPn => [/eqP -> ->//|k0 kB B0]. + by rewrite probability_setT. + rewrite (bigcap_setD1 0%N _ [set` B])//. + have [B1|B1] := boolP (1%N \in B); last first. + rewrite bigcapT ?setIT; last first. + move=> k [/= kB /eqP /negbTE ->]. + by move: kB B1; case: ifPn => [/eqP -> ->|]. + rewrite (big_fsetD1 0%N)//= big1_fset ?mule1// => k. + rewrite !inE => /andP[/negbTE -> kB] _. + move: kB B1; case: ifPn => [/eqP -> ->//|k1 kB B1]. + by rewrite probability_setT. + rewrite (bigcap_setD1 1%N _ ([set` B] `\ 0%N))// bigcapT ?setIT; last first. + by move=> n/= [[nB]/eqP/negbTE -> /eqP/negbTE ->]. + rewrite E1E2M (big_fsetD1 0%N)//= (big_fsetD1 1%N)/=; last by rewrite !inE B1. + rewrite big1_fset ?mule1//= => k. + rewrite !inE => -/and3P[/negbTE -> /negbTE -> kB] _; + by rewrite probability_setT. +Qed. + +Lemma pairwise_independentM (E1 E2 : set T) : + pairwise_independent E1 E2 <-> + [/\ d.-measurable E1, d.-measurable E2 & P (E1 `&` E2) = P E1 * P E2]. +Proof. +split. +- move=> [mE1E2 /(_ [fset 0%N; 1%N]%fset)]. + rewrite bigcap_fset !big_fsetU1 ?inE//= !big_seq_fset1/= => ->; last 2 first. + + by rewrite set_fsetU !set_fset1; exact: subset_refl. + + by rewrite cardfs2. + split => //. + + by apply: (mE1E2 0%N) => /=; left. + + by apply: (mE1E2 1%N) => /=; right. +- move=> [mE1 mE2 E1E2M]. + rewrite /pairwise_independent. + split. + + by move=> [| [| [|]]]//=. + + move=> B B01 B2. + have [B_set0|B_set0|B_set1|B_set01] := subset_set2 B01. + * rewrite B_set0. + move: B_set0 => /eqP; rewrite set_fset_eq0 => /eqP ->. + by rewrite big_nil bigcap_set0 probability_setT. + * rewrite B_set0 bigcap_set1 /=. + by rewrite fsbig_seq//= B_set0 fsbig_set1/=. + * rewrite B_set1 bigcap_set1 /=. + by rewrite fsbig_seq//= B_set1 fsbig_set1/=. + * rewrite B_set01 bigcap_setU1 bigcap_set1/=. + rewrite fsbig_seq//= B_set01. + rewrite fsbigU//=; last first. + by move=> n [/= ->]. + by rewrite !fsbig_set1//=. +Qed. + +Lemma pairwise_independent_setC (E1 E2 : set T) : + pairwise_independent E1 E2 -> pairwise_independent E1 (~` E2). +Proof. +rewrite/pairwise_independent. +move/pairwise_independentM=> [mE1 mE2 h]. +apply/pairwise_independentM; split=> //. +- exact: measurableC. +- rewrite -setDE measureD//; last first. + exact: (le_lt_trans (probability_le1 P mE1) (ltry _)). + rewrite probability_setC// muleBr// ?mule1 -?h//. + by rewrite fin_num_measure. +Qed. + +Lemma pairwise_independentC (E1 E2 : set T) : + pairwise_independent E1 E2 -> pairwise_independent E2 E1. +Proof. +rewrite/pairwise_independent/kwise_independent; move=> [mE1E2 /(_ [fset 0%N; 1%N]%fset)]. +rewrite bigcap_fset !big_fsetU1 ?inE//= !big_seq_fset1/= => h. +split. +- case=> [_|[_|]]//=. + + by apply: (mE1E2 1%N) => /=; right. + + by apply: (mE1E2 0%N) => /=; left. +- move=> B B01 B2. + have [B_set0|B_set0|B_set1|B_set01] := subset_set2 B01. + + rewrite B_set0. + move: B_set0 => /eqP; rewrite set_fset_eq0 => /eqP ->. + by rewrite big_nil bigcap_set0 probability_setT. + + rewrite B_set0 bigcap_set1 /=. + by rewrite fsbig_seq//= B_set0 fsbig_set1/=. + + rewrite B_set1 bigcap_set1 /=. + by rewrite fsbig_seq//= B_set1 fsbig_set1/=. + + rewrite B_set01 bigcap_setU1 bigcap_set1/=. + rewrite fsbig_seq//= B_set01. + rewrite fsbigU//=; last first. + by move=> n [/= ->]. + rewrite !fsbig_set1//= muleC setIC. + apply: h. + * by rewrite set_fsetU !set_fset1; exact: subset_refl. + * by rewrite cardfs2. +Qed. +(* ale: maybe interesting is thm 8.3 and exercise 8.6 from shoup/ntb at this point *) + +End independent_events. + +Section conditional_probability. +Context d (T : measurableType d) (R : realType). +Local Open Scope ereal_scope. + +Definition conditional_probability (P : probability T R) E1 E2 := (fine (P (E1 `&` E2)) / fine (P E2))%:E. +Local Notation "' P [ E1 | E2 ]" := (conditional_probability P E1 E2). + +Lemma conditional_independence (P : probability T R) E1 E2 : + P E2 != 0 -> pairwise_independent P E1 E2 -> 'P [ E1 | E2 ] = P E1. +Proof. +move=> PE2ne0 iE12. +have /= mE1 := (iE12.1 0%N). +have /= mE2 := (iE12.1 1%N). +rewrite/conditional_probability. +have [_ _ ->] := (pairwise_independentM _ _ _).1 iE12. +rewrite fineM ?fin_num_measure//; [|apply: mE1; left=>//|apply: mE2; right=>//]. +rewrite -mulrA mulfV ?mulr1 ?fineK// ?fin_num_measure//; first by apply: mE1; left. +by rewrite fine_eq0// fin_num_measure//; apply: mE2; right. +Qed. + +(* TODO (klenke thm 8.4): if P B > 0 then 'P[.|B] is a probability measure *) + +Lemma conditional_independent_is_pairwise_independent (P : probability T R) E1 E2 : + d.-measurable E1 -> d.-measurable E2 -> + P E2 != 0 -> + 'P[E1 | E2] = P E1 -> pairwise_independent P E1 E2. +Proof. +rewrite /conditional_probability/pairwise_independent=> mE1 mE2 pE20 pE1E2. +split. +- by case=> [|[|]]//=. +- move=> B B01 B2; have [B_set0|B_set0|B_set1|B_set01] := subset_set2 B01. + + rewrite B_set0. + move: B_set0 => /eqP; rewrite set_fset_eq0 => /eqP ->. + by rewrite big_nil bigcap_set0 probability_setT. + + rewrite B_set0 bigcap_set1 /=. + by rewrite fsbig_seq//= B_set0 fsbig_set1/=. + + rewrite B_set1 bigcap_set1 /=. + by rewrite fsbig_seq//= B_set1 fsbig_set1/=. + + rewrite B_set01 bigcap_setU1 bigcap_set1/=. + rewrite fsbig_seq//= B_set01. + rewrite fsbigU//=; last first. + by move=> n [/= ->]. + rewrite !fsbig_set1//= -pE1E2 -{2}(@fineK _ (P E2)). + rewrite -EFinM -mulrA mulVf ?mulr1 ?fine_eq0// ?fineK//. + all: by apply: fin_num_measure => //; apply: measurableI. +Qed. + +Lemma conditional_independentC (P : probability T R) E1 E2 : + d.-measurable E1 -> d.-measurable E2 -> + P E1 != 0 -> P E2 != 0 -> + reflect ('P[E1 | E2] == P E1) ('P[E2 | E1] == P E2). +Proof. +move=> mE1 mE2 pE10 pE20. +apply/(iffP idP)=>/eqP. ++ move/(@conditional_independent_is_pairwise_independent _ _ _ mE2 mE1 pE10). + move/pairwise_independentC. + by move/(conditional_independence pE20)/eqP. ++ move/(@conditional_independent_is_pairwise_independent _ _ _ mE1 mE2 pE20). + move/pairwise_independentC. + by move/(conditional_independence pE10)/eqP. +Qed. + +(* Lemma summation (I : choiceType) (A : {fset I}) E F (P : probability T R) : *) +(* (* the sets are disjoint *) *) +(* P (\bigcap_(i in [set` A]) F i) = 1 -> P E = \prod_(i <- A) ('P [E | F i] * P (F i)). *) +(* Proof. *) +(* move=> pF1. *) + +Lemma bayes (P : probability T R) E F : + d.-measurable E -> d.-measurable F -> + 'P[ E | F ] = ((fine ('P[F | E] * P E)) / (fine (P F)))%:E. +Proof. +rewrite /conditional_probability => mE mF. +have [PE0|PE0] := eqVneq (P E) 0. + have -> : P (E `&` F) = 0. + by apply/eqP; rewrite eq_le -{1}PE0 (@measureIl _ _ _ P E F mE mF)/= measure_ge0. + by rewrite PE0 fine0 invr0 mulr0 mule0 mul0r. +by rewrite -{2}(@fineK _ (P E)) -?EFinM -?(mulrA (fine _)) ?mulVf ?fine_eq0 ?fin_num_measure// mul1r setIC//. +Qed. + +End conditional_probability. +Notation "' P [ E1 | E2 ]" := (conditional_probability P E1 E2). + +From mathcomp Require Import real_interval. + +Section independent_RVs. +Context d (T : measurableType d) (R : realType) (P : probability T R). +Local Open Scope ereal_scope. + +Definition pairwise_independent_RV (X Y : {RV P >-> R}) := + forall s t, pairwise_independent P (X @^-1` s) (Y @^-1` t). + +Lemma conditional_independent_RV (X Y : {RV P >-> R}) : + pairwise_independent_RV X Y -> + forall s t, P (Y @^-1` t) != 0 -> 'P [X @^-1` s | Y @^-1` t] = P (X @^-1` s). +Proof. +move=> iRVXY s t PYtne0. +exact: conditional_independence. +Qed. + +Definition mutually_independent_RV (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) := + forall x_ : I -> R, independent_events P A (fun i => X i @^-1` `[(x_ i), +oo[%classic). + +Definition kwise_independent_RV (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) k := + forall x_ : I -> R, kwise_independent P A (fun i => X i @^-1` `[(x_ i), +oo[%classic) k. + +Lemma nwise_indep_is_mutual_indep_RV (I : choiceType) (A : {fset I}) (X : I -> {RV P >-> R}) n : + #|` A | = n -> kwise_independent_RV [set` A] X n -> mutually_independent_RV [set` A] X. +Proof. +rewrite/mutually_independent_RV/kwise_independent_RV=> nA kwX s. +by apply: nwise_indep_is_mutual_indep; rewrite ?nA. +Qed. + +(* alternative formalization +Definition inde_RV (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) := + forall (s : I -> set R), mutually_independent P A (fun i => X i @^-1` s i). + +Definition kwise_independent_RV (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) k := + forall (s : I -> set R), kwise_independent P A (fun i => X i @^-1` s i) k. + +this should be equivalent according to wikipedia https://en.wikipedia.org/wiki/Independence_(probability_theory)#For_real_valued_random_variables +*) + +(* Remark 2.15 (i) *) +Lemma prob_inde_RV (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) : + mutually_independent_RV A X -> + forall J : {fset I}, [set` J] `<=` A -> + forall x_ : I -> R, + P (\bigcap_(i in [set` J]) X i @^-1` `[(x_ i), +oo[%classic) = + \prod_(i <- J) P (X i @^-1` `[(x_ i), +oo[%classic). +Proof. +move=> iRVX J JleA x_. +apply: (iRVX _).2 => //. +Qed. + +(* +Lemma mutually_independent_RV' (I : choiceType) (A : set I) + (X : I -> {RV P >-> R}) (S : I -> set R) : + mutually_independent_RV A X -> + (forall i, A i -> measurable (S i)) -> + mutually_independent P A (fun i => X i @^-1` S i). +Proof. +move=> miX mS. +split; first by move=> i Ai; exact/measurable_sfunP/(mS i Ai). +move=> B BA. +Abort. +*) + +Lemma inde_expectation (I : choiceType) (A : set I) (X : I -> {RV P >-> R}) : + mutually_independent_RV A X -> + forall B : {fset I}, [set` B] `<=` A -> + 'E_P[\prod_(i <- B) X i] = \prod_(i <- B) 'E_P[X i]. +Proof. +move=> AX B BA. +rewrite [in LHS]unlock. +rewrite /mutually_independent_RV in AX. +rewrite /independent_events in AX. +Abort. + +End independent_RVs. + +Section bool_to_real. +Context d (T : measurableType d) (R : realType) (P : probability T R) (f : {mfun T >-> bool}). +Definition bool_to_real : T -> R := (fun x => x%:R) \o (f : T -> bool). + +Lemma measurable_bool_to_real : measurable_fun [set: T] bool_to_real. +Proof. +rewrite /bool_to_real. +apply: measurableT_comp => //=. +exact: (@measurable_funP _ _ _ _ f). +Qed. +(* HB.about isMeasurableFun.Build. *) +HB.instance Definition _ := + isMeasurableFun.Build _ _ _ _ bool_to_real measurable_bool_to_real. + +Definition btr : {RV P >-> R} := bool_to_real. + +End bool_to_real. + +Section bernoulli. + +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). +Variable p : R. +Hypothesis p01 : (0 <= p <= 1)%R. + +Definition bernoulli_RV (X : {dRV P >-> bool}) := + distribution P X = bernoulli p. + +Lemma bernoulli_RV1 (X : {dRV P >-> bool}) : bernoulli_RV X -> + P [set i | X i == 1%R] = p%:E. +Proof. +move=> [[/(congr1 (fun f => f [set 1%:R]))]]. +rewrite bernoulliE//. +rewrite /mscale/=. +rewrite diracE/= mem_set// mule1// diracE/= memNset//. +rewrite mule0 adde0. +rewrite /distribution /= => <-. +congr (P _). +rewrite /preimage/=. +by apply/seteqP; split => [x /eqP H//|x /eqP]. +Qed. + +Lemma bernoulli_RV2 (X : {dRV P >-> bool}) : bernoulli_RV X -> + P [set i | X i == 0%R] = (`1-p)%:E. +Proof. +move=> [[/(congr1 (fun f => f [set 0%:R]))]]. +rewrite bernoulliE//. +rewrite /mscale/=. +rewrite diracE/= memNset//. +rewrite mule0// diracE/= mem_set// add0e mule1. +rewrite /distribution /= => <-. +congr (P _). +rewrite /preimage/=. +by apply/seteqP; split => [x /eqP H//|x /eqP]. +Qed. + +Lemma bernoulli_expectation (X : {dRV P >-> bool}) : + bernoulli_RV X -> 'E_P[btr P X] = p%:E. +Proof. +move=> bX. +rewrite unlock /btr. +rewrite -(@ge0_integral_distribution _ _ _ _ _ _ X (EFin \o [eta GRing.natmul 1]))//; last first. + by move=> y //=. +rewrite /bernoulli/=. +rewrite (@eq_measure_integral _ _ _ _ (bernoulli p)); last first. + by move=> A mA _/=; rewrite (_ : distribution P X = bernoulli p). +rewrite integral_bernoulli//=. +by rewrite -!EFinM -EFinD mulr0 addr0 mulr1. +Qed. + +Lemma integrable_bernoulli (X : {dRV P >-> bool}) : + bernoulli_RV X -> P.-integrable [set: T] (EFin \o btr P X). +Proof. +move=> bX. +apply/integrableP; split; first by apply: measurableT_comp => //; exact: measurable_bool_to_real. +have -> : \int[P]_x `|(EFin \o btr P X) x| = 'E_P[btr P X]. + rewrite unlock /expectation. + apply: eq_integral => x _. + by rewrite gee0_abs //= lee_fin. +by rewrite bernoulli_expectation// ltry. +Qed. + +Lemma bool_RV_sqr (X : {dRV P >-> bool}) : + ((btr P X ^+ 2) = btr P X :> (T -> R))%R. +Proof. +apply: funext => x /=. +rewrite /GRing.exp /btr/bool_to_real /GRing.mul/=. +by case: (X x) => /=; rewrite ?mulr1 ?mulr0. +Qed. + +Lemma bernoulli_variance (X : {dRV P >-> bool}) : + bernoulli_RV X -> 'V_P[btr P X] = (p * (`1-p))%:E. +Proof. +move=> b. +rewrite (@varianceE _ _ _ _ (btr P X)); + [|rewrite ?[X in _ \o X]bool_RV_sqr; exact: integrable_bernoulli..]. +rewrite [X in 'E_P[X]]bool_RV_sqr !bernoulli_expectation//. +by rewrite expe2 -EFinD onemMr. +Qed. + +Definition is_bernoulli_trial n (X : {dRV P >-> bool}^nat) := + (forall i, (i < n)%nat -> bernoulli_RV (X i)) /\ independent_RVs P `I_n X. + +Definition bernoulli_trial n (X : {dRV P >-> bool}^nat) : {RV P >-> R} := + (\sum_(i-> bool}^nat) n : + is_bernoulli_trial n X -> 'E_P[@bernoulli_trial n X] = (n%:R * p)%:E. +Proof. +move=> bRV. rewrite /bernoulli_trial. +transitivity ('E_P[\sum_(s <- map (btr P \o X) (iota 0 n)) s]). + by rewrite big_map -[in RHS](subn0 n) big_mkord. +rewrite expectation_sum; last first. + by move=> Xi; move/mapP=> [k kn] ->; apply: integrable_bernoulli; apply bRV; rewrite mem_iota leq0n in kn. +rewrite big_map -[in LHS](subn0 n) big_mkord. +transitivity (\sum_(i < n) p%:E). + apply: eq_bigr => k _. + rewrite bernoulli_expectation//. + apply bRV. + by []. +by rewrite sumEFin big_const_ord iter_addr addr0 mulrC mulr_natr. +Qed. + +Definition sumrfct (s : seq {mfun T >-> R}) := (fun x => \sum_(f <- s) f x)%R. + +Lemma measurable_sumrfct s : measurable_fun setT (sumrfct s). +Proof. +rewrite /sumrfct. +pose n := size s. +apply/measurable_EFinP => /=. +have -> : (EFin \o (fun x : T => (\sum_(f <- s) f x)%R)) = (fun x : T => \sum_(i < n) (s`_i x)%:E)%R. + apply: funext => x /=. + rewrite sumEFin. + congr (_%:E). + rewrite big_tnth//. + apply: eq_bigr => i _ /=. + by rewrite (tnth_nth 0%R). +apply: emeasurable_sum => i. +by apply/measurable_EFinP. +Qed. + +HB.about isMeasurableFun.Build. +HB.instance Definition _ s := + isMeasurableFun.Build _ _ _ _ (sumrfct s) (measurable_sumrfct s). + +Lemma sumrfctE' (s : seq {mfun T >-> R}) x : + ((\sum_(f <- s) f) x = sumrfct s x)%R. +Proof. by rewrite/sumrfct; elim/big_ind2 : _ => //= u a v b <- <-. Qed. + +Lemma bernoulli_trial_ge0 (X : {dRV P >-> bool}^nat) n : is_bernoulli_trial n X -> + (forall t, 0 <= bernoulli_trial n X t)%R. +Proof. +move=> [bRV Xn] t. +rewrite /bernoulli_trial. +have -> : (\sum_(i < n) btr P (X i))%R = (\sum_(s <- map (btr P \o X) (iota 0 n)) s)%R. + by rewrite big_map -[in RHS](subn0 n) big_mkord. +have -> : (\sum_(s <- [seq (btr P \o X) i | i <- iota 0 n]) s)%R t = (\sum_(s <- [seq (btr P \o X) i | i <- iota 0 n]) s t)%R. + by rewrite sumrfctE'. +rewrite big_map. +by apply: sumr_ge0 => i _/=; rewrite /bool_to_real/= ler0n. +Qed. + +(* this seems to be provable like in https://www.cs.purdue.edu/homes/spa/courses/pg17/mu-book.pdf page 65 *) +Axiom taylor_ln_le : forall (delta : R), ((1 + delta) * ln (1 + delta) >= delta + delta^+2 / 3)%R. + +Lemma expR_prod d' {U : measurableType d'} (X : seq {mfun U >-> R}) (f : {mfun U >-> R} -> R) : + (\prod_(x <- X) expR (f x) = expR (\sum_(x <- X) f x))%R. +Proof. +elim: X => [|h t ih]; first by rewrite !big_nil expR0. +by rewrite !big_cons ih expRD. +Qed. + +Lemma expR_sum U l Q (f : U -> R) : (expR (\sum_(i <- l | Q i) f i) = \prod_(i <- l | Q i) expR (f i))%R. +Proof. +elim: l; first by rewrite !big_nil expR0. +move=> a l ih. +rewrite !big_cons. +case: ifP => //= aQ. +by rewrite expRD ih. +Qed. + +Lemma sumr_map U d' (V : measurableType d') (l : seq U) Q (f : U -> {mfun V >-> R}) (x : V) : + ((\sum_(i <- l | Q i) f i) x = \sum_(i <- l | Q i) f i x)%R. +Proof. +elim: l; first by rewrite !big_nil. +move=> a l ih. +rewrite !big_cons. +case: ifP => aQ//=. +by rewrite -ih. +Qed. + +Lemma prodr_map U d' (V : measurableType d') (l : seq U) Q (f : U -> {mfun V >-> R}) (x : V) : + ((\prod_(i <- l | Q i) f i) x = \prod_(i <- l | Q i) f i x)%R. +Proof. +elim: l; first by rewrite !big_nil. +move=> a l ih. +rewrite !big_cons. +case: ifP => aQ//=. +by rewrite -ih. +Qed. + +Lemma independent_mmt_gen_fun (X : {dRV P >-> bool}^nat) n t : + let mmtX (i : nat) : {RV P >-> R} := expR \o t \o* (btr P (X i)) in + independent_RVs P `I_n X -> independent_RVs P `I_n mmtX. +Proof. +Admitted. (* from Reynald's PR, independent_RVs2_comp, "when applying a function, the sigma algebra only gets smaller" *) + +Lemma expectation_prod_independent_RVs (X : {RV P >-> R}^nat) n : + independent_RVs P `I_n X -> + 'E_P[\prod_(i < n) (X i)] = \prod_(i < n) 'E_P[X i]. +Proof. +Admitted. + +Lemma bernoulli_trial_mmt_gen_fun (X_ : {dRV P >-> bool}^nat) n (t : R) : + is_bernoulli_trial n X_ -> + let X := bernoulli_trial n X_ in + 'M_X t = \prod_(i < n) 'M_(btr P (X_ i)) t. +Proof. +move=> []bRVX iRVX /=. +rewrite /bernoulli_trial/mmt_gen_fun. +pose mmtX (i : nat) : {RV P >-> R} := expR \o t \o* (btr P (X_ i)). +have iRV_mmtX : independent_RVs P `I_n mmtX. + exact: independent_mmt_gen_fun. +transitivity ('E_P[\prod_(i < n) mmtX i])%R. + congr ('E_P[_]). + apply: funext => x/=. + rewrite sumr_map mulr_suml expR_sum prodr_map. + exact: eq_bigr. +exact: expectation_prod_independent_RVs. +Qed. + +Arguments sub_countable [T U]. +Arguments card_le_finite [T U]. + +Lemma bernoulli_mmt_gen_fun (X : {dRV P >-> bool}) (t : R) : + bernoulli_RV X -> 'M_(btr P X : {RV P >-> R}) t = (p * expR t + (1-p))%:E. +Proof. +move=> bX. rewrite/mmt_gen_fun. +pose mmtX : {RV P >-> R} := expR \o t \o* (btr P X). +set A := X @^-1` [set true]. +set B := X @^-1` [set false]. +have mA: measurable A by exact: measurable_sfunP. +have mB: measurable B by exact: measurable_sfunP. +have dAB: [disjoint A & B] + by rewrite /disj_set /A /B preimage_true preimage_false setICr. +have TAB: setT = A `|` B by rewrite -preimage_setU -setT_bool preimage_setT. +rewrite unlock. +rewrite TAB integral_setU_EFin -?TAB//. +under eq_integral. + move=> x /=. + rewrite /A inE /bool_to_real /= => ->. + rewrite mul1r. + over. +rewrite integral_cst//. +under eq_integral. + move=> x /=. + rewrite /B inE /bool_to_real /= => ->. + rewrite mul0r. + over. +rewrite integral_cst//. +rewrite /A /B /preimage /=. +under eq_set do rewrite (propext (rwP eqP)). +rewrite (bernoulli_RV1 bX). +under eq_set do rewrite (propext (rwP eqP)). +rewrite (bernoulli_RV2 bX). +rewrite -EFinD; congr (_ + _)%:E; rewrite mulrC//. +by rewrite expR0 mulr1. +Qed. + +Lemma iter_mule (n : nat) (x y : \bar R) : iter n ( *%E x) y = (x ^+ n * y)%E. +Proof. by elim: n => [|n ih]; rewrite ?mul1e// [LHS]/= ih expeS muleA. Qed. + +Lemma binomial_mmt_gen_fun (X_ : {dRV P >-> bool}^nat) n (t : R) : + is_bernoulli_trial n X_ -> + let X := bernoulli_trial n X_ : {RV P >-> R} in + 'M_X t = ((p * expR t + (1-p))`^(n%:R))%:E. +Proof. +move: p01 => /andP[p0 p1] bX/=. +rewrite bernoulli_trial_mmt_gen_fun//. +under eq_bigr => i _. + rewrite bernoulli_mmt_gen_fun; last exact: bX.1. + over. +rewrite big_const iter_mule mule1 cardT size_enum_ord -EFin_expe powR_mulrn//. +by rewrite addr_ge0// ?subr_ge0// mulr_ge0// expR_ge0. +Qed. + +(* TODO: add to the PR by reynald that adds the \prod notation to master *) +Lemma prod_EFin U l Q (f : U -> R) : \prod_(i <- l | Q i) ((f i)%:E) = (\prod_(i <- l | Q i) f i)%:E. +Proof. +elim: l; first by rewrite !big_nil. +move=> a l ih. +rewrite !big_cons. +case: ifP => //= aQ. +by rewrite EFinM ih. +Qed. + +Lemma mmt_gen_fun_expectation (X_ : {dRV P >-> bool}^nat) (t : R) n : + (0 <= t)%R -> + is_bernoulli_trial n X_ -> + let X := bernoulli_trial n X_ : {RV P >-> R} in + 'M_X t <= (expR (fine 'E_P[X] * (expR t - 1)))%:E. +Proof. +move=> t0 bX/=. +have /andP[p0 p1] := p01. +rewrite binomial_mmt_gen_fun// lee_fin. +rewrite expectation_bernoulli_trial//. +rewrite addrCA -{2}(mulr1 p) -mulrN -mulrDr. +rewrite -mulrA (mulrC (n%:R)) expRM ge0_ler_powR// ?nnegrE ?expR_ge0//. + by rewrite addr_ge0// mulr_ge0// subr_ge0 -expR0 ler_expR. +exact: expR_ge1Dx. +Qed. + +Lemma end_thm24 (X_ : {dRV P >-> bool}^nat) n (t delta : R) : + is_bernoulli_trial n X_ -> + (0 < delta)%R -> + let X := @bernoulli_trial n X_ in + let mu := 'E_P[X] in + let t := ln (1 + delta) in + (expR (expR t - 1) `^ fine mu)%:E * + (expR (- t * (1 + delta)) `^ fine mu)%:E <= + ((expR delta / (1 + delta) `^ (1 + delta)) `^ fine mu)%:E. +Proof. +move=> bX d0 /=. +rewrite -EFinM lee_fin -powRM ?expR_ge0// ge0_ler_powR ?nnegrE//. +- by rewrite fine_ge0// expectation_ge0// => x; exact: (bernoulli_trial_ge0 bX). +- by rewrite mulr_ge0// expR_ge0. +- by rewrite divr_ge0 ?expR_ge0// powR_ge0. +- rewrite lnK ?posrE ?addr_gt0// addrAC subrr add0r ler_wpmul2l ?expR_ge0//. + by rewrite -powRN mulNr -mulrN expRM lnK// posrE addr_gt0. +Qed. + +(* theorem 2.4 Rajani / thm 4.4.(2) mu-book *) +Theorem bernoulli_trial_inequality1 (X_ : {dRV P >-> bool}^nat) n (delta : R) : + is_bernoulli_trial n X_ -> + (0 < delta)%R -> + let X := @bernoulli_trial n X_ in + let mu := 'E_P[X] in + P [set i | X i >= (1 + delta) * fine mu]%R <= + ((expR delta / ((1 + delta) `^ (1 + delta))) `^ (fine mu))%:E. +Proof. +rewrite /= => bX delta0. +set X := @bernoulli_trial n X_. +set mu := 'E_P[X]. +set t := ln (1 + delta). +have t0 : (0 < t)%R by rewrite ln_gt0// ltr_addl. +apply: (le_trans (chernoff _ _ t0)). +apply: (@le_trans _ _ ((expR (fine mu * (expR t - 1)))%:E * + (expR (- (t * ((1 + delta) * fine mu))))%:E)). + rewrite lee_pmul2r ?lte_fin ?expR_gt0//. + by apply: (mmt_gen_fun_expectation _ bX); rewrite le_eqVlt t0 orbT. +rewrite mulrC expRM -mulNr mulrA expRM. +exact: (end_thm24 _ bX). +Qed. + +(* theorem 2.5 *) +Theorem bernoulli_trial_inequality2 (X : {dRV P >-> bool}^nat) (delta : R) n : + is_bernoulli_trial n X -> + let X' := @bernoulli_trial n X in + let mu := 'E_P[X'] in + (0 < n)%nat -> + (0 < delta < 1)%R -> + P [set i | X' i >= (1 + delta) * fine mu]%R <= + (expR (- (fine mu * delta ^+ 2) / 3))%:E. +Proof. +move=> bX X' mu n0 /andP[delta0 _]. +apply: (@le_trans _ _ (expR ((delta - (1 + delta) * ln (1 + delta)) * fine mu))%:E). + rewrite expRM expRB (mulrC _ (ln _)) expRM lnK; last rewrite posrE addr_gt0//. + apply: (bernoulli_trial_inequality1 bX) => //. +apply: (@le_trans _ _ (expR ((delta - (delta + delta ^+ 2 / 3)) * fine mu))%:E). + rewrite lee_fin ler_expR ler_wpM2r//. + by rewrite fine_ge0//; apply: expectation_ge0 => t; exact: (bernoulli_trial_ge0 bX). + rewrite lerB//. + exact: taylor_ln_le. +rewrite le_eqVlt; apply/orP; left; apply/eqP; congr (expR _)%:E. +by rewrite opprD addrA subrr add0r mulrC mulrN mulNr mulrA. +Qed. + +(* TODO: move *) +Lemma ln_div : {in Num.pos &, {morph ln (R:=R) : x y / (x / y)%R >-> (x - y)%R}}. +Proof. +by move=> x y; rewrite !posrE => x0 y0; rewrite lnM ?posrE ?invr_gt0// lnV ?posrE. +Qed. + +Lemma norm_expR : normr \o expR = (expR : R -> R). +Proof. by apply/funext => x /=; rewrite ger0_norm ?expR_ge0. Qed. + +(* Rajani thm 2.6 / mu-book thm 4.5.(2) *) +Theorem bernoulli_trial_inequality3 (X : {dRV P >-> bool}^nat) (delta : R) n : + is_bernoulli_trial n X -> (0 < delta < 1)%R -> + let X' := @bernoulli_trial n X : {RV P >-> R} in + let mu := 'E_P[X'] in + P [set i | X' i <= (1 - delta) * fine mu]%R <= (expR (-(fine mu * delta ^+ 2) / 2)%R)%:E. +Proof. +move=> bX /andP[delta0 delta1] /=. +set X' := @bernoulli_trial n X : {RV P >-> R}. +set mu := 'E_P[X']. +have /andP[p0 p1] := p01. +apply: (@le_trans _ _ (((expR (- delta) / ((1 - delta) `^ (1 - delta))) `^ (fine mu))%:E)). + (* using Markov's inequality somewhere, see mu's book page 66 *) + have H1 t : (t < 0)%R -> + P [set i | (X' i <= (1 - delta) * fine mu)%R] = P [set i | `|(expR \o t \o* X') i|%:E >= (expR (t * (1 - delta) * fine mu))%:E]. + move=> t0; apply: congr1; apply: eq_set => x /=. + rewrite lee_fin ger0_norm ?expR_ge0// ler_expR (mulrC _ t) -mulrA. + by rewrite -[in RHS]ler_ndivr_mull// mulrA mulVf ?lt_eqF// mul1r. + set t := ln (1 - delta). + have ln1delta : (t < 0)%R. + (* TODO: lacking a lemma here *) + rewrite -oppr0 ltr_oppr -lnV ?posrE ?subr_gt0// ln_gt0//. + by rewrite invf_gt1// ?subr_gt0// ltr_subl_addr ltr_addl. + have {H1}-> := H1 _ ln1delta. + apply: (@le_trans _ _ (((fine 'E_P[normr \o expR \o t \o* X']) / (expR (t * (1 - delta) * fine mu))))%:E). + rewrite EFinM lee_pdivl_mulr ?expR_gt0// muleC fineK. + apply: (@markov _ _ _ P (expR \o t \o* X' : {RV P >-> R}) id (expR (t * (1 - delta) * fine mu))%R _ _ _ _) => //. + - apply: expR_gt0. + - rewrite norm_expR. + have -> : 'E_P[expR \o t \o* X'] = 'M_X' t by []. + by rewrite (binomial_mmt_gen_fun _ bX). + apply: (@le_trans _ _ (((expR ((expR t - 1) * fine mu)) / (expR (t * (1 - delta) * fine mu))))%:E). + rewrite norm_expR lee_fin ler_wpmul2r ?invr_ge0 ?expR_ge0//. + have -> : 'E_P[expR \o t \o* X'] = 'M_X' t by []. + rewrite (binomial_mmt_gen_fun _ bX)/=. + rewrite /mu /X' (expectation_bernoulli_trial bX)/=. + rewrite !lnK ?posrE ?subr_gt0//. + rewrite expRM powRrM powRAC. + rewrite ge0_ler_powR ?ler0n// ?nnegrE ?powR_ge0//. + by rewrite addr_ge0 ?mulr_ge0// subr_ge0// ltW. + rewrite addrAC subrr sub0r -expRM. + rewrite addrCA -{2}(mulr1 p) -mulrBr addrAC subrr sub0r mulrC mulNr. + by apply: expR_ge1Dx. + rewrite !lnK ?posrE ?subr_gt0//. + rewrite -addrAC subrr sub0r -mulrA [X in (_ / X)%R]expRM lnK ?posrE ?subr_gt0//. + rewrite -[in leRHS]powR_inv1 ?powR_ge0// powRM// ?expR_ge0 ?invr_ge0 ?powR_ge0//. + by rewrite powRAC powR_inv1 ?powR_ge0// powRrM expRM. +rewrite lee_fin. +rewrite -mulrN -mulrA [in leRHS]mulrC expRM ge0_ler_powR// ?nnegrE. +- by rewrite fine_ge0// expectation_ge0// => x; exact: (bernoulli_trial_ge0 bX). +- by rewrite divr_ge0 ?expR_ge0// powR_ge0. +- by rewrite expR_ge0. +- rewrite -ler_ln ?posrE ?divr_gt0 ?expR_gt0 ?powR_gt0 ?subr_gt0//. + rewrite expRK// ln_div ?posrE ?expR_gt0 ?powR_gt0 ?subr_gt0//. + rewrite expRK//. + rewrite /powR (*TODO: lemma ln of powR*) gt_eqF ?subr_gt0// expRK. + (* requires analytical argument: see p.66 of mu's book *) + Local Open Scope ring_scope. + rewrite -(@ler_pM2r _ 2)// -mulrA mulVf// mulr1 mulrDl. + rewrite -subr_le0 mulNr opprK. + rewrite addrC !addrA. + have->: delta ^+ 2 - delta * 2 = (1 - delta)^+2 - 1. + rewrite sqrrB expr1n mul1r [RHS]addrC !addrA addNr add0r addrC -mulNrn. + by rewrite -(mulr_natr (- delta) 2) mulNr. + rewrite addrAC subr_le0. + set f := fun (x : R) => x ^+ 2 + - (x * ln x) * 2. + have @idf (x : R^o) : 0 < x -> {df | is_derive x 1 (f : R^o -> R^o) df}. + move=> x0; evar (df : (R : Type)); exists df. + apply: is_deriveD; first by []. + apply: is_deriveM; last by []. + apply: is_deriveN. + apply: is_deriveM; first by []. + exact: is_derive1_ln. + suff: forall x : R, x \in `]0, 1[ -> f x <= 1. + by apply; rewrite memB_itv0 in_itv /= delta0 delta1. + move=> x x01. + have->: 1 = f 1 by rewrite /f expr1n ln1 mulr0 oppr0 mul0r addr0. + apply: (@ger0_derive1_homo _ f 0 1 false false)=> //. + - move=> t /[!in_itv] /= /andP [] + _. + by case/idf=> ? /@ex_derive. + - move=> t /[!in_itv] /= /andP [] t0 t1. + Local Arguments derive_val {R V W a v f df}. + rewrite (derive_val (svalP (idf _ t0))) /=. + clear idf. + rewrite exp_derive derive_cst derive_id . + rewrite scaler0 add0r /GRing.scale /= !mulr1 expr1. + rewrite -mulrDr mulr_ge0// divff ?lt0r_neq0//. + rewrite opprD addrA subr_ge0 -ler_expR. + have:= t0; rewrite -lnK_eq => /eqP ->. + by rewrite -[leLHS]addr0 -(subrr 1) addrCA expR_ge1Dx. + - apply: derivable_within_continuous => t /[!in_itv] /= /andP [] + _. + by case/idf=> ? /@ex_derive. + - by apply: (subset_itvW_bound _ _ x01); rewrite bnd_simp. + - by rewrite in_itv /= ltr01 lexx. + - by move: x01; rewrite in_itv=> /= /andP [] _ /ltW. +Qed. +Local Open Scope ereal_scope. + +Lemma measurable_fun_le D (f g : T -> R) : d.-measurable D -> measurable_fun D f -> + measurable_fun D g -> measurable (D `&` [set x | f x <= g x]%R). +Proof. +move=> mD mf mg. +under eq_set => x do rewrite -lee_fin. +apply: emeasurable_fun_le => //; apply: measurableT_comp => //. +Qed. + +(* Rajani -> corollary 2.7 / mu-book -> corollary 4.7 *) +Corollary bernoulli_trial_inequality4 (X : {dRV P >-> bool}^nat) (delta : R) n : + is_bernoulli_trial n X -> (0 < delta < 1)%R -> + (0 < n)%nat -> + (0 < p)%R -> + let X' := @bernoulli_trial n X in + let mu := 'E_P[X'] in + P [set i | `|X' i - fine mu | >= delta * fine mu]%R <= + (expR (- (fine mu * delta ^+ 2) / 3)%R *+ 2)%:E. +Proof. +move=> bX /andP[d0 d1] n0 p0 /=. +set X' := @bernoulli_trial n X. +set mu := 'E_P[X']. +under eq_set => x. + rewrite ler_normr. + rewrite lerBrDl opprD opprK -{1}(mul1r (fine mu)) -mulrDl. + rewrite -lerBDr -(lerN2 (- _)%R) opprK opprB. + rewrite -{2}(mul1r (fine mu)) -mulrBl. + rewrite -!lee_fin. + over. +rewrite /=. +rewrite set_orb. +rewrite measureU; last 3 first. +- rewrite -(@setIidr _ setT [set _ | _]) ?subsetT//. + apply: emeasurable_fun_le => //. + apply: measurableT_comp => //. +- rewrite -(@setIidr _ setT [set _ | _]) ?subsetT//. + apply: emeasurable_fun_le => //. + apply: measurableT_comp => //. +- rewrite disjoints_subset => x /=. + rewrite /mem /in_mem/= => X0; apply/negP. + rewrite -ltNge. + apply: (@lt_le_trans _ _ _ _ _ _ X0). + rewrite !EFinM. + rewrite lte_pmul2r//; first by rewrite lte_fin ltr_add2l gt0_cp. + by rewrite fineK /mu/X' (expectation_bernoulli_trial bX)// lte_fin mulr_gt0 ?ltr0n. +rewrite mulr2n EFinD lee_add//=. +- by apply: (bernoulli_trial_inequality2 bX); rewrite //d0 d1. +- apply: (le_trans (@bernoulli_trial_inequality3 _ delta _ bX _)); first by rewrite d0 d1. + rewrite lee_fin ler_expR !mulNr ler_opp2. + rewrite ler_pmul//; last by rewrite lef_pinv ?posrE ?ler_nat. + rewrite mulr_ge0 ?fine_ge0 ?sqr_ge0//. + rewrite /mu unlock /expectation integral_ge0// => x _. + by rewrite /X' lee_fin; apply: (bernoulli_trial_ge0 bX). +Qed. + +(* Rajani thm 3.1 / mu-book thm 4.7 *) +Theorem sampling (X : {dRV P >-> bool}^nat) n (theta delta : R) : + let X_sum := bernoulli_trial n X in + let X' x := (X_sum x) / n%:R in + (0 < p)%R -> + is_bernoulli_trial n X -> + (0 < delta <= 1)%R -> (0 < theta < p)%R -> (0 < n)%nat -> + (3 / theta ^+ 2 * ln (2 / delta) <= n%:R)%R -> + P [set i | `| X' i - p | <= theta]%R >= 1 - delta%:E. +Proof. +move=> X_sum X' p0 bX /andP[delta0 delta1] /andP[theta0 thetap] n0 tdn. +have E_X_sum: 'E_P[X_sum] = (p * n%:R)%:E. + by rewrite /X_sum expectation_bernoulli_trial// mulrC. +have /andP[_ p1] := p01. +set epsilon := theta / p. +have epsilon01 : (0 < epsilon < 1)%R. + by rewrite /epsilon ?ltr_pdivrMr ?divr_gt0 ?mul1r. +have thetaE : theta = (epsilon * p)%R. + by rewrite /epsilon -mulrA mulVf ?mulr1// gt_eqF. +have step1 : P [set i | `| X' i - p | >= epsilon * p]%R <= + ((expR (- (p * n%:R * (epsilon ^+ 2)) / 3)) *+ 2)%:E. + rewrite [X in P X <= _](_ : _ = + [set i | `| X_sum i - p * n%:R | >= epsilon * p * n%:R]%R); last first. + apply/seteqP; split => [t|t]/=. + move/(@ler_wpmul2r _ n%:R (ler0n _ _)) => /le_trans; apply. + rewrite -[X in (_ * X)%R](@ger0_norm _ n%:R)// -normrM mulrBl. + by rewrite -mulrA mulVf ?mulr1// gt_eqF ?ltr0n. + move/(@ler_wpmul2r _ n%:R^-1); rewrite invr_ge0// ler0n => /(_ erefl). + rewrite -(mulrA _ _ n%:R^-1) divff ?mulr1 ?gt_eqF ?ltr0n//. + move=> /le_trans; apply. + rewrite -[X in (_ * X)%R](@ger0_norm _ n%:R^-1)// -normrM mulrBl. + by rewrite -mulrA divff ?mulr1// gt_eqF// ltr0n. + rewrite -mulrA. + have -> : (p * n%:R)%R = fine (p * n%:R)%:E by []. + rewrite -E_X_sum. + by apply: (@bernoulli_trial_inequality4 X epsilon _ bX). +have step2 : P [set i | `| X' i - p | >= theta]%R <= + ((expR (- (n%:R * theta ^+ 2) / 3)) *+ 2)%:E. + rewrite thetaE; move/le_trans : step1; apply. + rewrite lee_fin ler_wmuln2r// ler_expR mulNr ler_oppl mulNr opprK. + rewrite -2![in leRHS]mulrA [in leRHS]mulrCA. + rewrite /epsilon -mulrA mulVf ?gt_eqF// mulr1 -!mulrA !ler_wpM2l ?(ltW theta0)//. + rewrite mulrCA ler_wpM2l ?(ltW theta0)//. + rewrite [X in (_ * X)%R]mulrA mulVf ?gt_eqF// -[leLHS]mul1r [in leRHS]mul1r. + by rewrite ler_wpM2r// invf_ge1. +suff : delta%:E >= P [set i | (`|X' i - p| >=(*NB: this >= in the pdf *) theta)%R]. + rewrite [X in P X <= _ -> _](_ : _ = ~` [set i | (`|X' i - p| < theta)%R]); last first. + apply/seteqP; split => [t|t]/=. + by rewrite leNgt => /negP. + by rewrite ltNge => /negP/negPn. + have ? : measurable [set i | (`|X' i - p| < theta)%R]. + under eq_set => x do rewrite -lte_fin. + rewrite -(@setIidr _ setT [set _ | _]) ?subsetT /X'//. + by apply: emeasurable_fun_lt => //; apply: measurableT_comp => //; + apply: measurableT_comp => //; apply: measurable_funD => //; + apply: measurable_funM. + rewrite probability_setC// lee_subel_addr//. + rewrite -lee_subel_addl//; last by rewrite fin_num_measure. + move=> /le_trans; apply. + rewrite le_measure ?inE//. + under eq_set => x do rewrite -lee_fin. + rewrite -(@setIidr _ setT [set _ | _]) ?subsetT /X'//. + by apply: emeasurable_fun_le => //; apply: measurableT_comp => //; + apply: measurableT_comp => //; apply: measurable_funD => //; + apply: measurable_funM. + by move=> t/= /ltW. +(* NB: last step in the pdf *) +apply: (le_trans step2). +rewrite lee_fin -(mulr_natr _ 2) -ler_pdivl_mulr//. +rewrite -(@lnK _ (delta / 2)); last by rewrite posrE divr_gt0. +rewrite ler_expR mulNr ler_oppl -lnV; last by rewrite posrE divr_gt0. +rewrite invf_div ler_pdivlMr// mulrC. +rewrite -ler_pdivrMr; last by rewrite exprn_gt0. +by rewrite mulrAC. +Qed. + +End bernoulli.