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/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/probability.v b/theories/probability.v index 989163dfc..52e3ef0b6 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -34,10 +34,6 @@ From mathcomp Require Import lebesgue_integral kernel hoelder derive. (* 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 *) (* ``` *) (* *) (* ``` *) @@ -543,428 +539,6 @@ Notation expectationM := expectationMl (only parsing). (* End product_lebesgue_measure. *) -(* independent class of events, klenke def 2.11, p.59 *) -Section independent_class. -Context {d : measure_display} {T : measurableType d} {R : realType} - {P : probability T R}. -Variable (I : choiceType) (E : I -> set (set T)). -Hypothesis mE : forall i, E i `<=` measurable. - -Definition independent_class := - forall J : {fset I}, - forall e : I -> set T, (forall i, (E i) (e i)) -> - P (\big[setI/setT]_(i <- J) e i) = (\prod_(i <- J) P (e i))%E. - -End independent_class. - -Section independent_events. -Context d (T : measurableType d) (R : realType) (P : probability T R). -Local Open Scope ereal_scope. - -Definition mutually_independent (I : choiceType) (A : set I) (E : I -> set T) := - (forall i, A i -> measurable (E i)) /\ - forall B : {fset I}, [set` B] `<=` A -> - P (\bigcap_(i in [set` B]) E i) = \prod_(i <- B) P (E i). - -Lemma sub_mutually_independent (I : choiceType) (A B : set I) (E : I -> set T) : - A `<=` B -> mutually_independent B E -> mutually_independent 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 : - mutually_independent A E -> kwise_independent A E k. -Proof. -rewrite/mutually_independent/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 -> mutually_independent [set` A] E. -Proof. -rewrite/mutually_independent/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) -> - mutually_independent [set: I] E <-> - mutually_independent B E. -Proof. -move=> BE; split; first exact: sub_mutually_independent. -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 mutually_independent_weak' (I : choiceType) (E : I -> set T) (B : set I) : - (forall b, ~ B b -> E b = setT) -> - mutually_independent [set: I] E <-> - mutually_independent B E. -Proof. -move=> BE; split; first exact: sub_mutually_independent. -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, mutually_independent 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 /mutually_independent in AX. -Abort. - -End independent_RVs. HB.lock Definition covariance {d} {T : measurableType d} {R : realType} (P : probability T R) (X Y : T -> R) := @@ -1670,47 +1244,6 @@ Abort. 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}. @@ -1734,374 +1267,6 @@ 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. @@ -2797,106 +1962,6 @@ rewrite -(image_id B) -bigcup_imset1 preimage_bigcup. exact: bigcup_finite. Qed. -(* TODO : PR in progress *) -Lemma countable_measurable d {T : measurableType d} (S : set T) : - (forall (a : T), measurable [set a]) -> countable S -> measurable S. -Proof. -move=> ma. -move/countable_injP => [f injf]. -have [->//|/set0P[a Sa]] := eqVneq S set0. -rewrite -(injpinv_image (fun=> a) injf). -rewrite [X in _ X](_ :_= \bigcup_(x in f @` S) [set 'pinv_(fun=> a) S f x]); last first. - rewrite eqEsubset; split => x/=. - move=> [n [xn Sxn xnn nx]]. - exists n => //=. - by exists xn. - move=> [n [xn Sxn xnn] /= xinvn]. - exists n => //=. - by exists xn. -apply: bigcup_measurable => n _. -apply: ma. -Qed. - -Section independent_classes. -Context {R : realType} d {T : measurableType d}. -Variable P : probability T R. -Local Open Scope ereal_scope. - -Definition independent_classes (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 independent_classes. - -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 generated_sigma_algebra. -Context {d'} (T : pointedType) (T' : measurableType d'). -Variable f : T -> T'. - -Let g_sigma_algebra_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 g_sigma_algebra_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 g_sigma_algebra_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 default_measure_display - (g_sigma_algebra_mappingType f) (g_sigma_algebra_mapping f) - g_sigma_algebra_mapping_set0 g_sigma_algebra_mapping_setC - g_sigma_algebra_mapping_bigcup. - -End generated_sigma_algebra. - -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 measurable_fun. *) (* Local Open Scope ereal_scope. *) (* Context d (T : measurableType d) (R : realType). *) @@ -2922,601 +1987,3 @@ End bool_to_real. (* Qed. *) (* End measurable_fun. *) - -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 -(@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_fun_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_wpmul2r//. - by rewrite fine_ge0//; apply: expectation_ge0 => t; exact: (bernoulli_trial_ge0 bX). - rewrite ler_sub//. - 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 ler_subr_addl opprD opprK -{1}(mul1r (fine mu)) -mulrDl. - rewrite -ler_sub_addr -(ler_opp2 (- _)%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_pdivr_mulr ?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_pdivl_mulr// mulrC. -rewrite -ler_pdivr_mulr; last by rewrite exprn_gt0. -by rewrite mulrAC. -Qed. - -End bernoulli. diff --git a/theories/sampling.v b/theories/sampling.v new file mode 100644 index 000000000..68c0358ee --- /dev/null +++ b/theories/sampling.v @@ -0,0 +1,1046 @@ +(* 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. + +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. + +Definition mutually_independent (I : choiceType) (A : set I) (E : I -> set T) := + (forall i, A i -> measurable (E i)) /\ + forall B : {fset I}, [set` B] `<=` A -> + P (\bigcap_(i in [set` B]) E i) = \prod_(i <- B) P (E i). + +Lemma sub_mutually_independent (I : choiceType) (A B : set I) (E : I -> set T) : + A `<=` B -> mutually_independent B E -> mutually_independent 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 : + mutually_independent A E -> kwise_independent A E k. +Proof. +rewrite/mutually_independent/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 -> mutually_independent [set` A] E. +Proof. +rewrite/mutually_independent/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) -> + mutually_independent [set: I] E <-> + mutually_independent B E. +Proof. +move=> BE; split; first exact: sub_mutually_independent. +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 mutually_independent_weak' (I : choiceType) (E : I -> set T) (B : set I) : + (forall b, ~ B b -> E b = setT) -> + mutually_independent [set: I] E <-> + mutually_independent B E. +Proof. +move=> BE; split; first exact: sub_mutually_independent. +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, mutually_independent 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 /mutually_independent 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 -(@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_fun_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_wpmul2r//. + by rewrite fine_ge0//; apply: expectation_ge0 => t; exact: (bernoulli_trial_ge0 bX). + rewrite ler_sub//. + 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 ler_subr_addl opprD opprK -{1}(mul1r (fine mu)) -mulrDl. + rewrite -ler_sub_addr -(ler_opp2 (- _)%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_pdivr_mulr ?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_pdivl_mulr// mulrC. +rewrite -ler_pdivr_mulr; last by rewrite exprn_gt0. +by rewrite mulrAC. +Qed. + +End bernoulli.