From 4d736228816fc9cc3bf6964e9d3f7180f3f19790 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Sun, 8 Oct 2023 09:59:37 +0200 Subject: [PATCH 01/12] start of chernoff proof --- theories/trigo.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/trigo.v b/theories/trigo.v index 86884d3ca..2b3db890e 100644 --- a/theories/trigo.v +++ b/theories/trigo.v @@ -349,7 +349,7 @@ apply: (@pseries_snd_diffs _ _ (`|x| + 1)). Qed. Lemma derivable_cos x : derivable (@cos R) x 1. -Proof. by apply: ex_derive; apply: is_derive_cos. Qed. +Proof. by apply: ex_derive; exact: is_derive_cos. Qed. Lemma continuous_cos : continuous (@cos R). Proof. From 6bb6b42c52233254606ac69b8363a5016b0bf54c Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 12 Oct 2023 14:12:04 +0200 Subject: [PATCH 02/12] proof completed --- theories/probability.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/theories/probability.v b/theories/probability.v index 576b95ccb..d22c58a61 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -566,6 +566,23 @@ rewrite [X in _ <= P X](_ : _ = [set x | a <= X x]%R)//; apply: eq_set => t/=. by rewrite ger0_norm ?expR_ge0// lee_fin ler_expR mulrC ler_pM2r. Qed. +HB.instance Definition _ := isMeasurableFun.Build _ _ _ (@expR R) (@measurable_expR R). + +Lemma measurableT_comp_subproof d1 (T1 : measurableType d1) (f : {mfun R >-> R}) (g : {mfun T1 >-> R}) : + measurable_fun setT (f \o g). +Proof. apply: measurableT_comp. exact. apply: @measurable_funP _ _ _ g. Qed. + +HB.instance Definition _ (d1 : measure_display) (T1 : measurableType d1) + (f : {mfun R >-> R}) (g : {mfun T1 >-> R}) := isMeasurableFun.Build _ _ _ (f \o g) (@measurableT_comp_subproof _ _ _ _). + +Lemma ge0_ler_normr : + {in Num.nneg &, {mono (@normr _ R) : x y / x <= y}}%R. +Proof. by move=> x y; rewrite !nnegrE => x0 y0; rewrite !ger0_norm. Qed. + +Lemma lt0_ger_normr : + {in Num.neg &, {mono (@normr _ R) : x y / x <= y >-> x >= y}}%R. +Proof. by move=> x y; rewrite !negrE => x0 y0; rewrite !ler0_norm ?lter_oppE// ?ltW. Qed. + Lemma chebyshev (X : {RV P >-> R}) (eps : R) : (0 < eps)%R -> P [set x | (eps <= `| X x - fine ('E_P[X])|)%R ] <= (eps ^- 2)%:E * 'V_P[X]. Proof. From 89f2a6fc4d2d6ce50d88f8e7ae4888c933f67c11 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Tue, 17 Oct 2023 13:17:08 +0200 Subject: [PATCH 03/12] moment -> mgf --- theories/probability.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/theories/probability.v b/theories/probability.v index d22c58a61..931a0a2cb 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -549,6 +549,7 @@ apply: (le_trans (@le_integral_comp_abse _ _ _ P _ measurableT (EFin \o X) - by rewrite unlock. Qed. +<<<<<<< HEAD Definition mmt_gen_fun (X : {RV P >-> R}) (t : R) := 'E_P[expR \o t \o* X]. Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R -> @@ -565,6 +566,9 @@ rewrite ger0_norm ?expR_ge0// muleC lee_pmul2l// ?lte_fin ?expR_gt0//. rewrite [X in _ <= P X](_ : _ = [set x | a <= X x]%R)//; apply: eq_set => t/=. by rewrite ger0_norm ?expR_ge0// lee_fin ler_expR mulrC ler_pM2r. Qed. +======= +Definition mgf (X : {RV P >-> R}) (t : R) := 'E_P[expR \o t \o* X]. +>>>>>>> 4ad33acb (moment -> mgf) HB.instance Definition _ := isMeasurableFun.Build _ _ _ (@expR R) (@measurable_expR R). @@ -583,6 +587,27 @@ Lemma lt0_ger_normr : {in Num.neg &, {mono (@normr _ R) : x y / x <= y >-> x >= y}}%R. Proof. by move=> x y; rewrite !negrE => x0 y0; rewrite !ler0_norm ?lter_oppE// ?ltW. Qed. +<<<<<<< HEAD +======= +Lemma chernoff (X : {RV P >-> R}) (t a : R) : (0 < t)%R -> + P [set x | X x >= a]%R * (expR (t * a))%:E <= mgf X t. +Proof. +move=> t0. +rewrite /= /mgf. +have h : (0 < `| expR (t * a) |)%R by rewrite normr_gt0 gt_eqF ?expR_gt0. +pose Y : {RV P >-> R} := [the {mfun T >-> R} of expR \o (t \o* X)]. +have := @markov Y normr (`| expR (t * a)|)%R h (@measurable_normr _ _) (fun r => normr_ge0 r) (monoW_in ge0_ler_normr). +rewrite normr_id. +rewrite ger0_norm ?expR_ge0//. +under eq_set => x. + rewrite /Y /= ger0_norm ?expR_ge0// lee_fin ler_expR. + rewrite mulrC (@ler_pmul2r _ t)//. over. +rewrite /= muleC. +suff -> : (normr \o [eta normr]) \o (expR \o t \o* X) = (expR \o t \o* X) => //. +by apply: funext => x /=; rewrite normr_id ger0_norm ?expR_ge0. +Qed. + +>>>>>>> 4ad33acb (moment -> mgf) Lemma chebyshev (X : {RV P >-> R}) (eps : R) : (0 < eps)%R -> P [set x | (eps <= `| X x - fine ('E_P[X])|)%R ] <= (eps ^- 2)%:E * 'V_P[X]. Proof. From b41bc8b4ba28a3413cedfb6fdbd1b7dbbc904b05 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 26 Oct 2023 15:24:51 +0200 Subject: [PATCH 04/12] start --- theories/probability.v | 25 ------------------------- 1 file changed, 25 deletions(-) diff --git a/theories/probability.v b/theories/probability.v index 931a0a2cb..d22c58a61 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -549,7 +549,6 @@ apply: (le_trans (@le_integral_comp_abse _ _ _ P _ measurableT (EFin \o X) - by rewrite unlock. Qed. -<<<<<<< HEAD Definition mmt_gen_fun (X : {RV P >-> R}) (t : R) := 'E_P[expR \o t \o* X]. Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R -> @@ -566,9 +565,6 @@ rewrite ger0_norm ?expR_ge0// muleC lee_pmul2l// ?lte_fin ?expR_gt0//. rewrite [X in _ <= P X](_ : _ = [set x | a <= X x]%R)//; apply: eq_set => t/=. by rewrite ger0_norm ?expR_ge0// lee_fin ler_expR mulrC ler_pM2r. Qed. -======= -Definition mgf (X : {RV P >-> R}) (t : R) := 'E_P[expR \o t \o* X]. ->>>>>>> 4ad33acb (moment -> mgf) HB.instance Definition _ := isMeasurableFun.Build _ _ _ (@expR R) (@measurable_expR R). @@ -587,27 +583,6 @@ Lemma lt0_ger_normr : {in Num.neg &, {mono (@normr _ R) : x y / x <= y >-> x >= y}}%R. Proof. by move=> x y; rewrite !negrE => x0 y0; rewrite !ler0_norm ?lter_oppE// ?ltW. Qed. -<<<<<<< HEAD -======= -Lemma chernoff (X : {RV P >-> R}) (t a : R) : (0 < t)%R -> - P [set x | X x >= a]%R * (expR (t * a))%:E <= mgf X t. -Proof. -move=> t0. -rewrite /= /mgf. -have h : (0 < `| expR (t * a) |)%R by rewrite normr_gt0 gt_eqF ?expR_gt0. -pose Y : {RV P >-> R} := [the {mfun T >-> R} of expR \o (t \o* X)]. -have := @markov Y normr (`| expR (t * a)|)%R h (@measurable_normr _ _) (fun r => normr_ge0 r) (monoW_in ge0_ler_normr). -rewrite normr_id. -rewrite ger0_norm ?expR_ge0//. -under eq_set => x. - rewrite /Y /= ger0_norm ?expR_ge0// lee_fin ler_expR. - rewrite mulrC (@ler_pmul2r _ t)//. over. -rewrite /= muleC. -suff -> : (normr \o [eta normr]) \o (expR \o t \o* X) = (expR \o t \o* X) => //. -by apply: funext => x /=; rewrite normr_id ger0_norm ?expR_ge0. -Qed. - ->>>>>>> 4ad33acb (moment -> mgf) Lemma chebyshev (X : {RV P >-> R}) (eps : R) : (0 < eps)%R -> P [set x | (eps <= `| X x - fine ('E_P[X])|)%R ] <= (eps ^- 2)%:E * 'V_P[X]. Proof. From 643711d9340c1932bfbcdc09c498b18c80db320a Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 26 Oct 2023 16:31:38 +0200 Subject: [PATCH 05/12] sampling_lemma --- theories/probability.v | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/theories/probability.v b/theories/probability.v index d22c58a61..8f4e84581 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1367,3 +1367,11 @@ apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=. Qed. End uniform_probability. + +(* TODO: formalize https://math.uchicago.edu/~may/REU2019/REUPapers/Rajani.pdf *) +Theorem sampling p (X : {RV P >-> R}^nat) (n : nat) (theta delta : R) : + let X_sum x := \sum_(i < n) (X i x) in + let X' := X_sum / n%:R in + (forall i, bernoulli p (X i)) -> + n > 3 / (theta ^+ 2) * ln (2 / delta) -> + P [set i | `| X' i - p | < theta] >= 1 - delta. From 9f65d6f47ca0b9e77bfbed1854868aa2c7847747 Mon Sep 17 00:00:00 2001 From: Alessandro Bruni Date: Thu, 26 Oct 2023 23:19:00 +0200 Subject: [PATCH 06/12] wip --- theories/probability.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/probability.v b/theories/probability.v index 8f4e84581..3fef4b1a3 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1370,8 +1370,8 @@ End uniform_probability. (* TODO: formalize https://math.uchicago.edu/~may/REU2019/REUPapers/Rajani.pdf *) Theorem sampling p (X : {RV P >-> R}^nat) (n : nat) (theta delta : R) : - let X_sum x := \sum_(i < n) (X i x) in - let X' := X_sum / n%:R in + let X_sum x := \sum_(i < n) (X i x)%:E in + let X' x := X_sum x * (n%:R)^-1%:E in (forall i, bernoulli p (X i)) -> - n > 3 / (theta ^+ 2) * ln (2 / delta) -> - P [set i | `| X' i - p | < theta] >= 1 - delta. + (n%:R > 3 / (theta ^+ 2) * ln (2 / delta))%R -> + P [set i | `| X' i - p%:E | < theta%:E] >= 1 - delta%:E. From 1cdbf491bc064a4034b52a9fc90914f72f0f6f9f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 27 May 2024 16:12:18 +0900 Subject: [PATCH 07/12] copy-pasting the previous Bernoulli PR by Alessandro --- theories/probability.v | 1132 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 1125 insertions(+), 7 deletions(-) diff --git a/theories/probability.v b/theories/probability.v index 3fef4b1a3..ca0251adc 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -1368,10 +1368,1128 @@ Qed. End uniform_probability. -(* TODO: formalize https://math.uchicago.edu/~may/REU2019/REUPapers/Rajani.pdf *) -Theorem sampling p (X : {RV P >-> R}^nat) (n : nat) (theta delta : R) : - let X_sum x := \sum_(i < n) (X i x)%:E in - let X' x := X_sum x * (n%:R)^-1%:E in - (forall i, bernoulli p (X i)) -> - (n%:R > 3 / (theta ^+ 2) * ln (2 / delta))%R -> - P [set i | `| X' i - p%:E | < theta%:E] >= 1 - delta%:E. +Section probability. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +Lemma probability_setC A : d.-measurable A -> P (~` A) = 1 - P A. +Proof. +move=> mA; rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI A) -measureD ?setTD ?setCK//. +by rewrite [ltLHS](@probability_setT _ _ _ P) ltry. +Qed. + +Lemma probability_setC' A : d.-measurable A -> P A = 1 - P (~` A). +Proof. +move=> mA. rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI (~` A)) -measureD ?setTD ?setCK//; first exact: measurableC. +by rewrite [ltLHS](@probability_setT _ _ _ P) ltry. +Qed. + +Lemma probability_fin_num A : d.-measurable A -> P A \is a fin_num. +Proof. +move=> mA. +rewrite fin_numElt. +rewrite (le_lt_trans (probability_le1 P mA) (ltry _)). +by rewrite (lt_le_trans ltNy0 (measure_ge0 P _)). +Qed. + +End probability. + +Notation "\prod_ ( i <- r | P ) F" := + (\big[*%E/1%:E]_(i <- r | P%B) F%E) : ereal_scope. +Notation "\prod_ ( i <- r ) F" := + (\big[*%E/1%:E]_(i <- r) F%E) : ereal_scope. +Notation "\prod_ ( m <= i < n | P ) F" := + (\big[*%E/1%:E]_(m <= i < n | P%B) F%E) : ereal_scope. +Notation "\prod_ ( m <= i < n ) F" := + (\big[*%E/1%:E]_(m <= i < n) F%E) : ereal_scope. +Notation "\prod_ ( i | P ) F" := + (\big[*%E/1%:E]_(i | P%B) F%E) : ereal_scope. +Notation "\prod_ i F" := + (\big[*%E/1%:E]_i F%E) : ereal_scope. +Notation "\prod_ ( i : t | P ) F" := + (\big[*%E/1%:E]_(i : t | P%B) F%E) (only parsing) : ereal_scope. +Notation "\prod_ ( i : t ) F" := + (\big[*%E/1%:E]_(i : t) F%E) (only parsing) : ereal_scope. +Notation "\prod_ ( i < n | P ) F" := + (\big[*%E/1%:E]_(i < n | P%B) F%E) : ereal_scope. +Notation "\prod_ ( i < n ) F" := + (\big[*%E/1%:E]_(i < n) F%E) : ereal_scope. +Notation "\prod_ ( i 'in' A | P ) F" := + (\big[*%E/1%:E]_(i in A | P%B) F%E) : ereal_scope. +Notation "\prod_ ( i 'in' A ) F" := + (\big[*%E/1%:E]_(i in A) F%E) : ereal_scope. + +(* 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. +Local Open Scope ereal_scope. + +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//. + exact: probability_fin_num. +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 ?probability_fin_num//; [|apply: mE1; left=>//|apply: mE2; right=>//]. +rewrite -mulrA mulfV ?mulr1 ?fineK// ?probability_fin_num//; first by apply: mE1; left. +by rewrite fine_eq0// probability_fin_num//; 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: probability_fin_num => //; 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 ?probability_fin_num// mul1r setIC//. +Qed. + +End conditional_probability. +Notation "' P [ E1 | E2 ]" := (conditional_probability P E1 E2). + +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 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. +Admitted. + +End independent_RVs. + +Local Open Scope ereal_scope. + +Section integrable_comp. +Context d1 d2 (X : measurableType d1) (Y : measurableType d2) (R : realType). +Variable phi : X -> Y. +Hypothesis mphi : measurable_fun [set: X] phi. +Variable mu : {measure set X -> \bar R}. +Variable f : Y -> \bar R. +Hypothesis mf : measurable_fun [set: Y] f. +Hypothesis intf : mu.-integrable [set: X] (f \o phi). +Local Open Scope ereal_scope. + +Lemma integrable_comp_funeneg : (pushforward mu mphi).-integrable [set: Y] f^\-. +Proof. +apply/integrableP; split. + exact: measurable_funeneg. +move/integrableP : (intf) => [_]. +apply: le_lt_trans. +rewrite integral_pushforward//=; last first. + apply: measurableT_comp => //=. + exact: measurable_funeneg. +apply: ge0_le_integral => //=. +apply: measurableT_comp => //=. +apply: measurableT_comp => //=. +exact: measurable_funeneg. +apply: measurableT_comp => //=. +apply: measurableT_comp => //=. +move=> x _. +rewrite -/((abse \o (f \o phi)) x). +rewrite (fune_abse (f \o phi)) /=. +rewrite gee0_abs//. +by rewrite lee_addr//. +Qed. + +Lemma integrable_comp_funepos : (pushforward mu mphi).-integrable [set: Y] f^\+. +Proof. +apply/integrableP; split. + exact: measurable_funepos. +move/integrableP : (intf) => [_]. +apply: le_lt_trans. +rewrite integral_pushforward//=; last first. + apply: measurableT_comp => //=. + exact: measurable_funepos. +apply: ge0_le_integral => //=. +apply: measurableT_comp => //=. +apply: measurableT_comp => //=. +exact: measurable_funepos. +apply: measurableT_comp => //=. +apply: measurableT_comp => //=. +move=> x _. +rewrite -/((abse \o (f \o phi)) x). +rewrite (fune_abse (f \o phi)) /=. +rewrite gee0_abs//. +by rewrite lee_addl//. +Qed. + +End integrable_comp. + +Section transfer. +Local Open Scope ereal_scope. +Context d1 d2 (X : measurableType d1) (Y : measurableType d2) (R : realType). +Variables (phi : X -> Y) (mphi : measurable_fun setT phi). +Variables (mu : {measure set X -> \bar R}). + +Lemma integral_pushforward_new (f : Y -> \bar R) : + measurable_fun setT f -> + mu.-integrable setT (f \o phi) -> + \int[pushforward mu mphi]_y f y = \int[mu]_x (f \o phi) x. +Proof. +move=> mf intf. +transitivity (\int[mu]_y ((f^\+ \o phi) \- (f^\- \o phi)) y); last first. + by apply: eq_integral => x _; rewrite [in RHS](funeposneg (f \o phi)). +rewrite integralB//; [|exact: integrable_funepos|exact: integrable_funeneg]. +rewrite -[X in _ = X - _]integral_pushforward//; last first. + exact: measurable_funepos. +rewrite -[X in _ = _ - X]integral_pushforward//; last first. + exact: measurable_funeneg. +rewrite -integralB//=; last first. +- apply: integrable_comp_funepos => //. + exact: measurableT_comp. + exact: integrableN. +- exact: integrable_comp_funepos. +- apply/eq_integral => x _. + by rewrite /= [in LHS](funeposneg f). +Qed. + +End transfer. + +Section transfer_probability. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +Lemma integral_distribution_new (X : {RV P >-> R}) (f : R -> \bar R) : + measurable_fun setT f -> + P.-integrable [set: T] (f \o X) -> + \int[distribution P X]_y f y = \int[P]_x (f \o X) x. +Proof. by move=> mf intf; rewrite integral_pushforward_new. Qed. + +End transfer_probability. + +Section integral_measure_add_new. +Context d (T : measurableType d) (R : realType) + (m1 m2 : {measure set T -> \bar R}) (D : set T). +Hypothesis mD : measurable D. +Variable f : T -> \bar R. +Hypothesis intf1 : m1.-integrable D f. +Hypothesis intf2 : m2.-integrable D f. +Hypothesis mf : measurable_fun D f. + +Lemma integral_measure_add_new : + \int[measure_add m1 m2]_(x in D) f x = \int[m1]_(x in D) f x + \int[m2]_(x in D) f x. +transitivity (\int[m1]_(x in D) (f^\+ \- f^\-) x + + \int[m2]_(x in D) (f^\+ \- f^\-) x); last first. + by congr +%E; apply: eq_integral => x _; rewrite [in RHS](funeposneg f). +rewrite integralB//; last 2 first. + exact: integrable_funepos. + exact: integrable_funeneg. +rewrite integralB//; last 2 first. + exact: integrable_funepos. + exact: integrable_funeneg. +rewrite addeACA. +rewrite -integral_measure_add//; last first. + apply: measurable_funepos. + exact: measurable_int intf1. +rewrite -oppeD; last first. + by rewrite ge0_adde_def// inE integral_ge0. +rewrite -integral_measure_add//; last first. + apply: measurable_funeneg. + exact: measurable_int intf1. +by rewrite integralE. +Qed. + +End integral_measure_add_new. + +Section bernoulli. + +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). +Variable p : {nonneg R}. +Hypothesis p1 : (p%:num <= 1)%R. + +Definition real_of_bool := fun b : bool => b%:R : R. + +Lemma measurable_fun_real_of_bool : measurable_fun setT real_of_bool. +Proof. by []. Qed. + +Lemma real_of_bool1 : real_of_bool @^-1` [set 1%R] = [set true]. +Proof. +by apply/seteqP; split => [x|x ->] //=; case: x => //= /esym/eqP; rewrite oner_eq0. +Qed. + +Lemma real_of_bool0 : real_of_bool @^-1` [set 0%R] = [set false]. +Proof. +by apply/seteqP; split => [x|x ->] //=; case: x => //= /eqP/=; rewrite oner_eq0. +Qed. + +Definition bernoulli_RV (X : {RV P >-> R}) := + distribution P X = pushforward (bernoulli p%:num) measurable_fun_real_of_bool /\ + (range X = [set 0; 1])%R. + +Lemma bernoulli_RV1 (X : {RV P >-> R}) : bernoulli_RV X -> + P [set i | X i == 1%R] == p%:num%:E. +Proof. +move=> [/(congr1 (fun f => f [set 1%:R]))]. +rewrite /bernoulli/= /pushforward ifT; last exact/andP. +rewrite real_of_bool1 fsbig_set1/= /distribution /= => <- _. +apply/eqP; congr (P _). +by apply/seteqP; split => [x /eqP H//|x /eqP]. +Qed. + +Lemma bernoulli_RV2 (X : {RV P >-> R}) : bernoulli_RV X -> + P [set i | X i == 0%R] == (`1-(p%:num))%:E. +Proof. +move=> [[/(congr1 (fun f => f [set 0%:R]))]]. +rewrite /bernoulli/= /pushforward ifT; last exact/andP. +rewrite real_of_bool0 fsbig_set1/= /distribution /= => <- _. +apply/eqP; congr (P _). +by apply/seteqP; split => [x /eqP H//|x /eqP]. +Qed. + +Lemma bernoulli_ge0 (X : {RV P >-> R}) : bernoulli_RV X -> + forall t, (X t >= 0)%R. +Proof. +move=> bX t. +suff: (range X) (X t) by rewrite bX.2 => -[] ->. +by exists t. +Qed. + +Lemma bernoulli_expectation (X : {RV P >-> R}) : + bernoulli_RV X -> 'E_P[X] = p%:num%:E. +Proof. +move=> bX. +rewrite unlock. +transitivity (\int[P]_w `|X w|%:E). + apply: eq_integral => t _. + by rewrite ger0_norm// bernoulli_ge0. +rewrite -(@integral_distribution _ _ _ _ _ (EFin \o normr))//; last first. + by move=> y //=. + exact: measurableT_comp. +rewrite bX.1. +rewrite integral_pushforward/=; last 2 first. + exact: measurableT_comp. + by move=> /= r; rewrite lee_fin. +rewrite integral_bernoulli//; last exact/andP. +by rewrite /real_of_bool normr1 normr0 !mule0 adde0 mule1. +Qed. + +Lemma bernoulli_sqr (X : {RV P >-> R}) : + bernoulli_RV X -> bernoulli_RV (X ^+ 2 : {RV P >-> R})%R. +Proof. +rewrite /bernoulli_RV => -[Xp1 X01]; split. + rewrite -Xp1; apply/funext => A. + rewrite /distribution /pushforward/=; congr (P _). + by apply/seteqP; split => [t|t]; + (have : (range X) (X t) by exists t); + rewrite X01/= /GRing.mul/= => -[] ->; rewrite ?(mul0r,mul1r). +rewrite -X01; apply/seteqP; split => [x|x]. +- move=> [t _] /=; rewrite /GRing.mul/= -expr2 => <-; + (have : (range X) (X t) by exists t); + by rewrite X01/= /GRing.mul/= => -[] Xt; + exists t => //; rewrite Xt ?(expr0n,expr1n). +- move=> [t _] /=; rewrite /GRing.mul/= => <-; + (have : (range X) (X t) by exists t); + by rewrite X01/= => -[] Xt; + exists t => //=; rewrite Xt/= ?(mulr0,mulr1). +Qed. + +Lemma integrable_bernoulli (X : {RV P >-> R}) : + bernoulli_RV X -> P.-integrable [set: T] (EFin \o X). +Proof. +move=> bX. +apply/integrableP; split; first by apply: measurableT_comp. +have -> : \int[P]_x `|(EFin \o X) x| = 'E_P[X]. + rewrite unlock /expectation. + apply: eq_integral => x _. + rewrite gee0_abs //= lee_fin. + by rewrite bernoulli_ge0//. +by rewrite bernoulli_expectation// ltry. +Qed. + +Lemma bernoulli_variance (X : {RV P >-> R}) : +(* NB(rei): no need for that? + P.-integrable setT (EFin \o X) -> + P.-integrable [set: T] (EFin \o (X ^+ 2)%R) ->*) +bernoulli_RV X -> 'V_P[X] = (p%:num * (`1-(p%:num)))%:E. +move=> b. +rewrite varianceE; last 2 first. + exact: integrable_bernoulli. + exact: integrable_bernoulli (bernoulli_sqr b). +rewrite (bernoulli_expectation b). +have b2 := bernoulli_sqr b. +rewrite (bernoulli_expectation b2) /=. +by rewrite -EFinD mulrDr mulr1 mulrN. +Qed. + +Definition independent (X Y : {RV P >-> R}) := 'E_P[X * Y] = 'E_P[X] * 'E_P[Y]. + +Definition independent_RVs (X : seq {RV P >-> R}) := + forall Xi, Xi \in X -> forall Xj, Xj \in X -> independent Xi Xj. + +Lemma independent_RVs_expectation (X : seq {RV P >-> R}) : + independent_RVs X -> 'E_P[\prod_(Xi <- X) Xi] = \prod_(Xi <- X) 'E_P[Xi]. +Proof. +elim: X => [_|X0 X IH hRVs]. + by rewrite !big_nil expectation_cst. +rewrite !big_cons. +rewrite -IH. +Admitted. + +(* +Definition independent_RVs (X : seq {RV P >-> R}) := forall t, + (fine ('E_P[expR \o t \o* \sum_(Xi <- X) Xi]) = \prod_(Xi <- X) fine ('E_P[expR \o t \o* Xi]))%R. +*) + +Definition is_bernoulli_trial (X : seq {RV P >-> R}) n := + (forall Xi, Xi \in X -> bernoulli_RV Xi) /\ + independent_RVs X /\ + size X = n(*NB: used n.-tuple instead of seq*). + +Definition bernoulli_trial (X : seq {RV P >-> R}) := + (\sum_(Xi <- X) Xi)%R. + +Lemma expectation_bernoulli_trial (X : seq {RV P >-> R}) n : + is_bernoulli_trial X n -> 'E_P[@bernoulli_trial X] = (n%:R * p%:num)%:E. +Proof. +move=> [bRV [_ Xn]]; rewrite expectation_sum; last first. + by move=> Xi XiX; exact: (integrable_bernoulli (bRV _ XiX)). +under eq_big_seq => Xi XiX. + by rewrite (bernoulli_expectation (bRV Xi _))//; over. +rewrite /= -Xn -sum1_size natr_sum big_distrl/= sumEFin; congr EFin. +by under [RHS]eq_bigr do rewrite mul1r. +Qed. + +Lemma bernoulli_trial_ge0 (X : seq {RV P >-> R}) n : is_bernoulli_trial X n -> + (forall t, 0 <= bernoulli_trial X t)%R. +Proof. +move=> [bRV Xn] t. +rewrite /bernoulli_trial [leRHS](_ : _ = \sum_(Xi <- X) Xi t)%R; last first. + by rewrite {bRV Xn}; elim/big_ind2 : _ => //= _ f _ g <- <-. + (* NB: this maybe need to be a lemma*) +by rewrite big_seq; apply: sumr_ge0 => i iX; exact/bernoulli_ge0/bRV. +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 (X : seq {RV P >-> R}) (f : {RV P >-> 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 bernoulli_mmt_gen_fun (X : {RV P >-> R}) (t : R) : + bernoulli_RV X -> 'E_P[expR \o t \o* X] = (p%:num * expR t + (1-p%:num))%:E. +Admitted. + +Lemma binomial_mmt_gen_fun (X_ : seq {RV P >-> R}) n (t : R) : + is_bernoulli_trial X_ n -> + let X := bernoulli_trial X_ : {RV P >-> R} in + mmt_gen_fun X t = ((p%:num * expR t + (1-p%:num))`^(n%:R))%:E. +Proof. +rewrite /is_bernoulli_trial /independent_RVs /bernoulli_trial. +move=> [bX1 [bX2 bX3]] /=. +rewrite -[LHS]fineK; last first. + rewrite /mmt_gen_fun unlock /expectation. + apply: integral_fune_fin_num => //. + admit. +(*rewrite bX2 big_seq. +apply: congr1. +under eq_bigr => Xi XiX do rewrite (bernoulli_mmt_gen_fun _ (bX1 _ _))//=.*) +Admitted. + +Lemma lm23 (X_ : seq {RV P >-> R}) (t : R) n : + (0 <= t)%R -> + is_bernoulli_trial X_ n -> + let X := bernoulli_trial X_ : {RV P >-> R} in + let mu := 'E_P[X] in + mmt_gen_fun X t <= (expR (fine mu * (expR t - 1)))%:E. +Proof. +rewrite /= => t0 bX. +set X := bernoulli_trial X_. +set mu := 'E_P[X]. +have -> : @mmt_gen_fun _ _ _ P X t = (\prod_(Xi <- X_) fine (mmt_gen_fun Xi t))%:E. + rewrite -[LHS]fineK; last rewrite (binomial_mmt_gen_fun _ bX)//. + apply: congr1; (*apply: bX.2.1 => //*) admit. +under eq_big_seq => Xi XiX. + have -> : @mmt_gen_fun _ _ _ P Xi t = (1 + p%:num * (expR t - 1))%:E. + rewrite /mmt_gen_fun. + rewrite bernoulli_mmt_gen_fun//; last exact: bX.1. + apply: congr1. + by rewrite mulrBr mulr1 addrCA. + over. +rewrite lee_fin /=. +apply: (le_trans (@ler_prod _ _ _ _ _ (fun x => expR (p%:num * (expR t - 1)))%R _)). + move=> Xi _. + rewrite addr_ge0 ?mulr_ge0 ?subr_ge0 ?andTb//; last first. + rewrite -expR0 ler_expR//. + by rewrite expR_ge1Dx ?mulr_ge0// subr_ge0 -expR0 ler_expR. +rewrite expR_prod -mulr_suml. +move: t0; rewrite le_eqVlt => /predU1P[<-|t0]. + by rewrite expR0 subrr !mulr0. +rewrite ler_expR ler_pmul2r; last first. + by rewrite subr_gt0 -expR0 ltr_expR. +rewrite /mu big_seq expectation_sum; last first. + move=> Xi XiX; apply: integrable_bernoulli; exact: bX.1. +rewrite big_seq -sum_fine. + by apply: ler_sum => Xi XiX; rewrite bernoulli_expectation //=; exact: bX.1. +move=> Xi XiX. rewrite bernoulli_expectation //=; exact: bX.1. +Admitted. + +Lemma expR_powR (x y : R) : (expR (x * y) = (expR x) `^ y)%R. +Proof. by rewrite /powR gt_eqF ?expR_gt0// expRK mulrC. Qed. + +Lemma end_thm24 (X_ : seq {RV P >-> R}) n (t delta : R) : + is_bernoulli_trial X_ n -> + (0 < delta)%R -> + let X := @bernoulli_trial 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 expR_powR lnK// posrE addr_gt0. +Qed. + +(* theorem 2.4 Rajani / thm 4.4.(2) mu-book *) +Theorem thm24 (X_ : seq {RV P >-> R}) n (delta : R) : + is_bernoulli_trial X_ n -> + (0 < delta)%R -> + let X := @bernoulli_trial 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 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: (lm23 _ bX); rewrite le_eqVlt t0 orbT. +rewrite mulrC expR_powR -mulNr mulrA expR_powR. +exact: (end_thm24 _ bX). +Qed. + +(* theorem 2.5 *) +Theorem poisson_ineq (X : seq {RV P >-> R}) (delta : R) n : + is_bernoulli_trial X n -> + let X' := @bernoulli_trial 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 expR_powR expRB (mulrC _ (ln _)) expR_powR lnK; last rewrite posrE addr_gt0//. + apply: (thm24 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. + +Require Import derive. + +Lemma le01_expR_ge1Dx (x : R) : (-1 <= x <= 0 -> 1 + x <= expR x)%R. +Proof. +move=> /andP [N1x x0]. +pose f : R^o -> R := (expR \- (cst 1 \+ id))%R. +rewrite -subr_ge0 (_ : 0%R = f 0%R); last by rewrite /f !fctE/= expR0 addr0 subrr. +pose f' : R^o -> R := (expR \- (cst 0 \+ cst 1))%R. +move: N1x; rewrite le_eqVlt => /predU1P[<-|N1x]. + by rewrite /f !fctE /= expR0 addr0 subrr subr0 expR_ge0. +move: x0; rewrite le_eqVlt => /predU1P[<-//|x0]. +have [c cx] : exists2 c, c \in `]x, 0%R[ & (f 0 - f x)%R = (f' c * (0 - x))%R. + apply: MVT => //. + admit. +rewrite -[leRHS]/(f x) -subr_le0 sub0r /f' => ->; apply: mulr_le0_ge0. + by rewrite /=subr_le0 add0r -expR0 ler_expR; move: cx; rewrite in_itv => /andP[_ /ltW]. +by rewrite ler_oppr oppr0 ltW. +Admitted. + +(* Rajani thm 2.6 / mu-book thm 4.5.(2) *) +Theorem thm26 (X : seq {RV P >-> R}) (delta : R) n : + is_bernoulli_trial X n -> (0 < delta < 1)%R -> + let X' := @bernoulli_trial 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 X : {RV P >-> R}. +set mu := 'E_P[X']. +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. + - admit. (* oops *) + - rewrite norm_expR. + have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun 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'] = mmt_gen_fun X' t by []. + rewrite (binomial_mmt_gen_fun _ bX)/=. + rewrite /mu /X' (expectation_bernoulli_trial bX)/=. + rewrite !lnK ?posrE ?subr_gt0//. + rewrite expR_powR powRrM powRAC. + rewrite ge0_ler_powR ?ler0n// ?nnegrE ?powR_ge0//. + by rewrite addr_ge0 ?mulr_ge0// subr_ge0// ltW. + rewrite addrAC subrr sub0r -expR_powR. + rewrite addrCA -{2}(mulr1 (p%:num)) -mulrBr addrAC subrr sub0r mulrC mulNr. + apply: le01_expR_ge1Dx. + rewrite ler_oppl opprK mulr_ile1//=; [|exact: ltW..]. + by rewrite ler_oppl oppr0 mulr_ge0// ltW. + rewrite !lnK ?posrE ?subr_gt0//. + rewrite -addrAC subrr sub0r -mulrA [X in (_ / X)%R]expR_powR 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 expR_powR. +rewrite lee_fin. +rewrite -mulrN -mulrA [in leRHS]mulrC expR_powR 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 *) + admit. +Admitted. + +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 cor27 (X : seq {RV P >-> R}) (delta : R) n : + is_bernoulli_trial X n -> (0 < delta < 1)%R -> + (0 < n)%nat -> + (0 < p%:num)%R -> + let X' := @bernoulli_trial 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 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: (poisson_ineq bX); rewrite //d0 d1. +- apply: (le_trans (@thm26 _ 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 : seq {RV P >-> R}) (theta delta : R) : + let n := size X in + let X_sum := bernoulli_trial X in + let X' x := (X_sum x) / n%:R in + (0 < p%:num)%R -> + is_bernoulli_trial X n -> + (0 < delta <= 1)%R -> (0 < theta < p%:num)%R -> (0 < n)%nat -> + (3 / theta ^+ 2 * ln (2 / delta) <= n%:R)%R -> + P [set i | `| X' i - p%:num | <= theta]%R >= 1 - delta%:E. +Proof. +move=> n X_sum X' p0 bX /andP[delta0 delta1] /andP[theta0 thetap] n0 tdn. +have E_X_sum: 'E_P[X_sum] = (p%:num * n%:R)%:E. + rewrite expectation_sum/=; last first. + by move=> Xi XiX; exact: integrable_bernoulli (bX.1 Xi XiX). + rewrite big_seq. + under eq_bigr. + move=> Xi XiX; rewrite (bernoulli_expectation (bX.1 _ XiX)); over. + rewrite /= sumEFin big_const_seq iter_addr_0/= mulr_natr; congr ((_ *+ _)%:E). + by rewrite /n -count_predT; apply: eq_in_count => x ->. +set epsilon := theta / p%:num. +have epsilon01 : (0 < epsilon < 1)%R. + by rewrite /epsilon ?ltr_pdivr_mulr ?divr_gt0 ?mul1r. +have thetaE : theta = (epsilon * p%:num)%R. + by rewrite /epsilon -mulrA mulVf ?mulr1// gt_eqF. +have step1 : P [set i | `| X' i - p%:num | >= epsilon * p%:num]%R <= + ((expR (- (p%:num * n%:R * (epsilon ^+ 2)) / 3)) *+ 2)%:E. + rewrite [X in P X <= _](_ : _ = + [set i | `| X_sum i - p%:num * n%:R | >= epsilon * p%:num * 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%:num * n%:R)%R = fine (p%:num * n%:R)%:E by []. + rewrite -E_X_sum. + by apply: (@cor27 X epsilon _ bX). +have step2 : P [set i | `| X' i - p%:num | >= 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 -[in leLHS]mulrA ler_wpmul2l//. + rewrite (mulrC epsilon) exprMn -mulrA ler_wpmul2r//. + by rewrite divr_ge0// sqr_ge0. + by rewrite expr2 ler_pimull.*) admit. +suff : delta%:E >= P [set i | (`|X' i - p%:num| >=(*NB: this >= in the pdf *) theta)%R]. + rewrite [X in P X <= _ -> _](_ : _ = ~` [set i | (`|X' i - p%:num| < 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%:num| < 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. +Admitted. + +End bernoulli. From 2b65f0798c5fec7f9f15a6106088ade68157cfa2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 27 May 2024 17:37:34 +0900 Subject: [PATCH 08/12] reboot work on independent RVs Co-authored-by: Alessandro Bruni Co-authored-by: Takafumi Saikawa --- _CoqProject | 1 + theories/Make | 1 + theories/probability.v | 1132 +--------------------------------------- theories/sampling.v | 1086 ++++++++++++++++++++++++++++++++++++++ 4 files changed, 1091 insertions(+), 1129 deletions(-) create mode 100644 theories/sampling.v diff --git a/_CoqProject b/_CoqProject index 65ec68c2e..12d95056a 100644 --- a/_CoqProject +++ b/_CoqProject @@ -45,6 +45,7 @@ theories/lebesgue_integral.v theories/ftc.v theories/hoelder.v theories/probability.v +theories/sampling.v theories/summability.v theories/signed.v theories/itv.v diff --git a/theories/Make b/theories/Make index f4e9346fc..83866f1dc 100644 --- a/theories/Make +++ b/theories/Make @@ -33,6 +33,7 @@ lebesgue_integral.v ftc.v hoelder.v probability.v +sampling.v lebesgue_stieltjes_measure.v summability.v signed.v diff --git a/theories/probability.v b/theories/probability.v index ca0251adc..463dcfa86 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -4,9 +4,9 @@ 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. -Require Import exp numfun lebesgue_measure lebesgue_integral. -Require Import reals ereal signed topology normedtype sequences esum measure. -Require Import exp numfun lebesgue_measure lebesgue_integral kernel. +Require Import real_interval exp numfun lebesgue_measure lebesgue_integral. +Require Import reals ereal signed topology normedtype derive sequences esum. +Require Import measure exp numfun lebesgue_measure lebesgue_integral kernel. (**md**************************************************************************) (* # Probability *) @@ -1367,1129 +1367,3 @@ apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=. Qed. End uniform_probability. - -Section probability. -Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) (P : probability T R). - -Lemma probability_setC A : d.-measurable A -> P (~` A) = 1 - P A. -Proof. -move=> mA; rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI A) -measureD ?setTD ?setCK//. -by rewrite [ltLHS](@probability_setT _ _ _ P) ltry. -Qed. - -Lemma probability_setC' A : d.-measurable A -> P A = 1 - P (~` A). -Proof. -move=> mA. rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI (~` A)) -measureD ?setTD ?setCK//; first exact: measurableC. -by rewrite [ltLHS](@probability_setT _ _ _ P) ltry. -Qed. - -Lemma probability_fin_num A : d.-measurable A -> P A \is a fin_num. -Proof. -move=> mA. -rewrite fin_numElt. -rewrite (le_lt_trans (probability_le1 P mA) (ltry _)). -by rewrite (lt_le_trans ltNy0 (measure_ge0 P _)). -Qed. - -End probability. - -Notation "\prod_ ( i <- r | P ) F" := - (\big[*%E/1%:E]_(i <- r | P%B) F%E) : ereal_scope. -Notation "\prod_ ( i <- r ) F" := - (\big[*%E/1%:E]_(i <- r) F%E) : ereal_scope. -Notation "\prod_ ( m <= i < n | P ) F" := - (\big[*%E/1%:E]_(m <= i < n | P%B) F%E) : ereal_scope. -Notation "\prod_ ( m <= i < n ) F" := - (\big[*%E/1%:E]_(m <= i < n) F%E) : ereal_scope. -Notation "\prod_ ( i | P ) F" := - (\big[*%E/1%:E]_(i | P%B) F%E) : ereal_scope. -Notation "\prod_ i F" := - (\big[*%E/1%:E]_i F%E) : ereal_scope. -Notation "\prod_ ( i : t | P ) F" := - (\big[*%E/1%:E]_(i : t | P%B) F%E) (only parsing) : ereal_scope. -Notation "\prod_ ( i : t ) F" := - (\big[*%E/1%:E]_(i : t) F%E) (only parsing) : ereal_scope. -Notation "\prod_ ( i < n | P ) F" := - (\big[*%E/1%:E]_(i < n | P%B) F%E) : ereal_scope. -Notation "\prod_ ( i < n ) F" := - (\big[*%E/1%:E]_(i < n) F%E) : ereal_scope. -Notation "\prod_ ( i 'in' A | P ) F" := - (\big[*%E/1%:E]_(i in A | P%B) F%E) : ereal_scope. -Notation "\prod_ ( i 'in' A ) F" := - (\big[*%E/1%:E]_(i in A) F%E) : ereal_scope. - -(* 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. -Local Open Scope ereal_scope. - -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//. - exact: probability_fin_num. -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 ?probability_fin_num//; [|apply: mE1; left=>//|apply: mE2; right=>//]. -rewrite -mulrA mulfV ?mulr1 ?fineK// ?probability_fin_num//; first by apply: mE1; left. -by rewrite fine_eq0// probability_fin_num//; 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: probability_fin_num => //; 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 ?probability_fin_num// mul1r setIC//. -Qed. - -End conditional_probability. -Notation "' P [ E1 | E2 ]" := (conditional_probability P E1 E2). - -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 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. -Admitted. - -End independent_RVs. - -Local Open Scope ereal_scope. - -Section integrable_comp. -Context d1 d2 (X : measurableType d1) (Y : measurableType d2) (R : realType). -Variable phi : X -> Y. -Hypothesis mphi : measurable_fun [set: X] phi. -Variable mu : {measure set X -> \bar R}. -Variable f : Y -> \bar R. -Hypothesis mf : measurable_fun [set: Y] f. -Hypothesis intf : mu.-integrable [set: X] (f \o phi). -Local Open Scope ereal_scope. - -Lemma integrable_comp_funeneg : (pushforward mu mphi).-integrable [set: Y] f^\-. -Proof. -apply/integrableP; split. - exact: measurable_funeneg. -move/integrableP : (intf) => [_]. -apply: le_lt_trans. -rewrite integral_pushforward//=; last first. - apply: measurableT_comp => //=. - exact: measurable_funeneg. -apply: ge0_le_integral => //=. -apply: measurableT_comp => //=. -apply: measurableT_comp => //=. -exact: measurable_funeneg. -apply: measurableT_comp => //=. -apply: measurableT_comp => //=. -move=> x _. -rewrite -/((abse \o (f \o phi)) x). -rewrite (fune_abse (f \o phi)) /=. -rewrite gee0_abs//. -by rewrite lee_addr//. -Qed. - -Lemma integrable_comp_funepos : (pushforward mu mphi).-integrable [set: Y] f^\+. -Proof. -apply/integrableP; split. - exact: measurable_funepos. -move/integrableP : (intf) => [_]. -apply: le_lt_trans. -rewrite integral_pushforward//=; last first. - apply: measurableT_comp => //=. - exact: measurable_funepos. -apply: ge0_le_integral => //=. -apply: measurableT_comp => //=. -apply: measurableT_comp => //=. -exact: measurable_funepos. -apply: measurableT_comp => //=. -apply: measurableT_comp => //=. -move=> x _. -rewrite -/((abse \o (f \o phi)) x). -rewrite (fune_abse (f \o phi)) /=. -rewrite gee0_abs//. -by rewrite lee_addl//. -Qed. - -End integrable_comp. - -Section transfer. -Local Open Scope ereal_scope. -Context d1 d2 (X : measurableType d1) (Y : measurableType d2) (R : realType). -Variables (phi : X -> Y) (mphi : measurable_fun setT phi). -Variables (mu : {measure set X -> \bar R}). - -Lemma integral_pushforward_new (f : Y -> \bar R) : - measurable_fun setT f -> - mu.-integrable setT (f \o phi) -> - \int[pushforward mu mphi]_y f y = \int[mu]_x (f \o phi) x. -Proof. -move=> mf intf. -transitivity (\int[mu]_y ((f^\+ \o phi) \- (f^\- \o phi)) y); last first. - by apply: eq_integral => x _; rewrite [in RHS](funeposneg (f \o phi)). -rewrite integralB//; [|exact: integrable_funepos|exact: integrable_funeneg]. -rewrite -[X in _ = X - _]integral_pushforward//; last first. - exact: measurable_funepos. -rewrite -[X in _ = _ - X]integral_pushforward//; last first. - exact: measurable_funeneg. -rewrite -integralB//=; last first. -- apply: integrable_comp_funepos => //. - exact: measurableT_comp. - exact: integrableN. -- exact: integrable_comp_funepos. -- apply/eq_integral => x _. - by rewrite /= [in LHS](funeposneg f). -Qed. - -End transfer. - -Section transfer_probability. -Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) (P : probability T R). - -Lemma integral_distribution_new (X : {RV P >-> R}) (f : R -> \bar R) : - measurable_fun setT f -> - P.-integrable [set: T] (f \o X) -> - \int[distribution P X]_y f y = \int[P]_x (f \o X) x. -Proof. by move=> mf intf; rewrite integral_pushforward_new. Qed. - -End transfer_probability. - -Section integral_measure_add_new. -Context d (T : measurableType d) (R : realType) - (m1 m2 : {measure set T -> \bar R}) (D : set T). -Hypothesis mD : measurable D. -Variable f : T -> \bar R. -Hypothesis intf1 : m1.-integrable D f. -Hypothesis intf2 : m2.-integrable D f. -Hypothesis mf : measurable_fun D f. - -Lemma integral_measure_add_new : - \int[measure_add m1 m2]_(x in D) f x = \int[m1]_(x in D) f x + \int[m2]_(x in D) f x. -transitivity (\int[m1]_(x in D) (f^\+ \- f^\-) x + - \int[m2]_(x in D) (f^\+ \- f^\-) x); last first. - by congr +%E; apply: eq_integral => x _; rewrite [in RHS](funeposneg f). -rewrite integralB//; last 2 first. - exact: integrable_funepos. - exact: integrable_funeneg. -rewrite integralB//; last 2 first. - exact: integrable_funepos. - exact: integrable_funeneg. -rewrite addeACA. -rewrite -integral_measure_add//; last first. - apply: measurable_funepos. - exact: measurable_int intf1. -rewrite -oppeD; last first. - by rewrite ge0_adde_def// inE integral_ge0. -rewrite -integral_measure_add//; last first. - apply: measurable_funeneg. - exact: measurable_int intf1. -by rewrite integralE. -Qed. - -End integral_measure_add_new. - -Section bernoulli. - -Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) (P : probability T R). -Variable p : {nonneg R}. -Hypothesis p1 : (p%:num <= 1)%R. - -Definition real_of_bool := fun b : bool => b%:R : R. - -Lemma measurable_fun_real_of_bool : measurable_fun setT real_of_bool. -Proof. by []. Qed. - -Lemma real_of_bool1 : real_of_bool @^-1` [set 1%R] = [set true]. -Proof. -by apply/seteqP; split => [x|x ->] //=; case: x => //= /esym/eqP; rewrite oner_eq0. -Qed. - -Lemma real_of_bool0 : real_of_bool @^-1` [set 0%R] = [set false]. -Proof. -by apply/seteqP; split => [x|x ->] //=; case: x => //= /eqP/=; rewrite oner_eq0. -Qed. - -Definition bernoulli_RV (X : {RV P >-> R}) := - distribution P X = pushforward (bernoulli p%:num) measurable_fun_real_of_bool /\ - (range X = [set 0; 1])%R. - -Lemma bernoulli_RV1 (X : {RV P >-> R}) : bernoulli_RV X -> - P [set i | X i == 1%R] == p%:num%:E. -Proof. -move=> [/(congr1 (fun f => f [set 1%:R]))]. -rewrite /bernoulli/= /pushforward ifT; last exact/andP. -rewrite real_of_bool1 fsbig_set1/= /distribution /= => <- _. -apply/eqP; congr (P _). -by apply/seteqP; split => [x /eqP H//|x /eqP]. -Qed. - -Lemma bernoulli_RV2 (X : {RV P >-> R}) : bernoulli_RV X -> - P [set i | X i == 0%R] == (`1-(p%:num))%:E. -Proof. -move=> [[/(congr1 (fun f => f [set 0%:R]))]]. -rewrite /bernoulli/= /pushforward ifT; last exact/andP. -rewrite real_of_bool0 fsbig_set1/= /distribution /= => <- _. -apply/eqP; congr (P _). -by apply/seteqP; split => [x /eqP H//|x /eqP]. -Qed. - -Lemma bernoulli_ge0 (X : {RV P >-> R}) : bernoulli_RV X -> - forall t, (X t >= 0)%R. -Proof. -move=> bX t. -suff: (range X) (X t) by rewrite bX.2 => -[] ->. -by exists t. -Qed. - -Lemma bernoulli_expectation (X : {RV P >-> R}) : - bernoulli_RV X -> 'E_P[X] = p%:num%:E. -Proof. -move=> bX. -rewrite unlock. -transitivity (\int[P]_w `|X w|%:E). - apply: eq_integral => t _. - by rewrite ger0_norm// bernoulli_ge0. -rewrite -(@integral_distribution _ _ _ _ _ (EFin \o normr))//; last first. - by move=> y //=. - exact: measurableT_comp. -rewrite bX.1. -rewrite integral_pushforward/=; last 2 first. - exact: measurableT_comp. - by move=> /= r; rewrite lee_fin. -rewrite integral_bernoulli//; last exact/andP. -by rewrite /real_of_bool normr1 normr0 !mule0 adde0 mule1. -Qed. - -Lemma bernoulli_sqr (X : {RV P >-> R}) : - bernoulli_RV X -> bernoulli_RV (X ^+ 2 : {RV P >-> R})%R. -Proof. -rewrite /bernoulli_RV => -[Xp1 X01]; split. - rewrite -Xp1; apply/funext => A. - rewrite /distribution /pushforward/=; congr (P _). - by apply/seteqP; split => [t|t]; - (have : (range X) (X t) by exists t); - rewrite X01/= /GRing.mul/= => -[] ->; rewrite ?(mul0r,mul1r). -rewrite -X01; apply/seteqP; split => [x|x]. -- move=> [t _] /=; rewrite /GRing.mul/= -expr2 => <-; - (have : (range X) (X t) by exists t); - by rewrite X01/= /GRing.mul/= => -[] Xt; - exists t => //; rewrite Xt ?(expr0n,expr1n). -- move=> [t _] /=; rewrite /GRing.mul/= => <-; - (have : (range X) (X t) by exists t); - by rewrite X01/= => -[] Xt; - exists t => //=; rewrite Xt/= ?(mulr0,mulr1). -Qed. - -Lemma integrable_bernoulli (X : {RV P >-> R}) : - bernoulli_RV X -> P.-integrable [set: T] (EFin \o X). -Proof. -move=> bX. -apply/integrableP; split; first by apply: measurableT_comp. -have -> : \int[P]_x `|(EFin \o X) x| = 'E_P[X]. - rewrite unlock /expectation. - apply: eq_integral => x _. - rewrite gee0_abs //= lee_fin. - by rewrite bernoulli_ge0//. -by rewrite bernoulli_expectation// ltry. -Qed. - -Lemma bernoulli_variance (X : {RV P >-> R}) : -(* NB(rei): no need for that? - P.-integrable setT (EFin \o X) -> - P.-integrable [set: T] (EFin \o (X ^+ 2)%R) ->*) -bernoulli_RV X -> 'V_P[X] = (p%:num * (`1-(p%:num)))%:E. -move=> b. -rewrite varianceE; last 2 first. - exact: integrable_bernoulli. - exact: integrable_bernoulli (bernoulli_sqr b). -rewrite (bernoulli_expectation b). -have b2 := bernoulli_sqr b. -rewrite (bernoulli_expectation b2) /=. -by rewrite -EFinD mulrDr mulr1 mulrN. -Qed. - -Definition independent (X Y : {RV P >-> R}) := 'E_P[X * Y] = 'E_P[X] * 'E_P[Y]. - -Definition independent_RVs (X : seq {RV P >-> R}) := - forall Xi, Xi \in X -> forall Xj, Xj \in X -> independent Xi Xj. - -Lemma independent_RVs_expectation (X : seq {RV P >-> R}) : - independent_RVs X -> 'E_P[\prod_(Xi <- X) Xi] = \prod_(Xi <- X) 'E_P[Xi]. -Proof. -elim: X => [_|X0 X IH hRVs]. - by rewrite !big_nil expectation_cst. -rewrite !big_cons. -rewrite -IH. -Admitted. - -(* -Definition independent_RVs (X : seq {RV P >-> R}) := forall t, - (fine ('E_P[expR \o t \o* \sum_(Xi <- X) Xi]) = \prod_(Xi <- X) fine ('E_P[expR \o t \o* Xi]))%R. -*) - -Definition is_bernoulli_trial (X : seq {RV P >-> R}) n := - (forall Xi, Xi \in X -> bernoulli_RV Xi) /\ - independent_RVs X /\ - size X = n(*NB: used n.-tuple instead of seq*). - -Definition bernoulli_trial (X : seq {RV P >-> R}) := - (\sum_(Xi <- X) Xi)%R. - -Lemma expectation_bernoulli_trial (X : seq {RV P >-> R}) n : - is_bernoulli_trial X n -> 'E_P[@bernoulli_trial X] = (n%:R * p%:num)%:E. -Proof. -move=> [bRV [_ Xn]]; rewrite expectation_sum; last first. - by move=> Xi XiX; exact: (integrable_bernoulli (bRV _ XiX)). -under eq_big_seq => Xi XiX. - by rewrite (bernoulli_expectation (bRV Xi _))//; over. -rewrite /= -Xn -sum1_size natr_sum big_distrl/= sumEFin; congr EFin. -by under [RHS]eq_bigr do rewrite mul1r. -Qed. - -Lemma bernoulli_trial_ge0 (X : seq {RV P >-> R}) n : is_bernoulli_trial X n -> - (forall t, 0 <= bernoulli_trial X t)%R. -Proof. -move=> [bRV Xn] t. -rewrite /bernoulli_trial [leRHS](_ : _ = \sum_(Xi <- X) Xi t)%R; last first. - by rewrite {bRV Xn}; elim/big_ind2 : _ => //= _ f _ g <- <-. - (* NB: this maybe need to be a lemma*) -by rewrite big_seq; apply: sumr_ge0 => i iX; exact/bernoulli_ge0/bRV. -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 (X : seq {RV P >-> R}) (f : {RV P >-> 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 bernoulli_mmt_gen_fun (X : {RV P >-> R}) (t : R) : - bernoulli_RV X -> 'E_P[expR \o t \o* X] = (p%:num * expR t + (1-p%:num))%:E. -Admitted. - -Lemma binomial_mmt_gen_fun (X_ : seq {RV P >-> R}) n (t : R) : - is_bernoulli_trial X_ n -> - let X := bernoulli_trial X_ : {RV P >-> R} in - mmt_gen_fun X t = ((p%:num * expR t + (1-p%:num))`^(n%:R))%:E. -Proof. -rewrite /is_bernoulli_trial /independent_RVs /bernoulli_trial. -move=> [bX1 [bX2 bX3]] /=. -rewrite -[LHS]fineK; last first. - rewrite /mmt_gen_fun unlock /expectation. - apply: integral_fune_fin_num => //. - admit. -(*rewrite bX2 big_seq. -apply: congr1. -under eq_bigr => Xi XiX do rewrite (bernoulli_mmt_gen_fun _ (bX1 _ _))//=.*) -Admitted. - -Lemma lm23 (X_ : seq {RV P >-> R}) (t : R) n : - (0 <= t)%R -> - is_bernoulli_trial X_ n -> - let X := bernoulli_trial X_ : {RV P >-> R} in - let mu := 'E_P[X] in - mmt_gen_fun X t <= (expR (fine mu * (expR t - 1)))%:E. -Proof. -rewrite /= => t0 bX. -set X := bernoulli_trial X_. -set mu := 'E_P[X]. -have -> : @mmt_gen_fun _ _ _ P X t = (\prod_(Xi <- X_) fine (mmt_gen_fun Xi t))%:E. - rewrite -[LHS]fineK; last rewrite (binomial_mmt_gen_fun _ bX)//. - apply: congr1; (*apply: bX.2.1 => //*) admit. -under eq_big_seq => Xi XiX. - have -> : @mmt_gen_fun _ _ _ P Xi t = (1 + p%:num * (expR t - 1))%:E. - rewrite /mmt_gen_fun. - rewrite bernoulli_mmt_gen_fun//; last exact: bX.1. - apply: congr1. - by rewrite mulrBr mulr1 addrCA. - over. -rewrite lee_fin /=. -apply: (le_trans (@ler_prod _ _ _ _ _ (fun x => expR (p%:num * (expR t - 1)))%R _)). - move=> Xi _. - rewrite addr_ge0 ?mulr_ge0 ?subr_ge0 ?andTb//; last first. - rewrite -expR0 ler_expR//. - by rewrite expR_ge1Dx ?mulr_ge0// subr_ge0 -expR0 ler_expR. -rewrite expR_prod -mulr_suml. -move: t0; rewrite le_eqVlt => /predU1P[<-|t0]. - by rewrite expR0 subrr !mulr0. -rewrite ler_expR ler_pmul2r; last first. - by rewrite subr_gt0 -expR0 ltr_expR. -rewrite /mu big_seq expectation_sum; last first. - move=> Xi XiX; apply: integrable_bernoulli; exact: bX.1. -rewrite big_seq -sum_fine. - by apply: ler_sum => Xi XiX; rewrite bernoulli_expectation //=; exact: bX.1. -move=> Xi XiX. rewrite bernoulli_expectation //=; exact: bX.1. -Admitted. - -Lemma expR_powR (x y : R) : (expR (x * y) = (expR x) `^ y)%R. -Proof. by rewrite /powR gt_eqF ?expR_gt0// expRK mulrC. Qed. - -Lemma end_thm24 (X_ : seq {RV P >-> R}) n (t delta : R) : - is_bernoulli_trial X_ n -> - (0 < delta)%R -> - let X := @bernoulli_trial 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 expR_powR lnK// posrE addr_gt0. -Qed. - -(* theorem 2.4 Rajani / thm 4.4.(2) mu-book *) -Theorem thm24 (X_ : seq {RV P >-> R}) n (delta : R) : - is_bernoulli_trial X_ n -> - (0 < delta)%R -> - let X := @bernoulli_trial 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 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: (lm23 _ bX); rewrite le_eqVlt t0 orbT. -rewrite mulrC expR_powR -mulNr mulrA expR_powR. -exact: (end_thm24 _ bX). -Qed. - -(* theorem 2.5 *) -Theorem poisson_ineq (X : seq {RV P >-> R}) (delta : R) n : - is_bernoulli_trial X n -> - let X' := @bernoulli_trial 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 expR_powR expRB (mulrC _ (ln _)) expR_powR lnK; last rewrite posrE addr_gt0//. - apply: (thm24 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. - -Require Import derive. - -Lemma le01_expR_ge1Dx (x : R) : (-1 <= x <= 0 -> 1 + x <= expR x)%R. -Proof. -move=> /andP [N1x x0]. -pose f : R^o -> R := (expR \- (cst 1 \+ id))%R. -rewrite -subr_ge0 (_ : 0%R = f 0%R); last by rewrite /f !fctE/= expR0 addr0 subrr. -pose f' : R^o -> R := (expR \- (cst 0 \+ cst 1))%R. -move: N1x; rewrite le_eqVlt => /predU1P[<-|N1x]. - by rewrite /f !fctE /= expR0 addr0 subrr subr0 expR_ge0. -move: x0; rewrite le_eqVlt => /predU1P[<-//|x0]. -have [c cx] : exists2 c, c \in `]x, 0%R[ & (f 0 - f x)%R = (f' c * (0 - x))%R. - apply: MVT => //. - admit. -rewrite -[leRHS]/(f x) -subr_le0 sub0r /f' => ->; apply: mulr_le0_ge0. - by rewrite /=subr_le0 add0r -expR0 ler_expR; move: cx; rewrite in_itv => /andP[_ /ltW]. -by rewrite ler_oppr oppr0 ltW. -Admitted. - -(* Rajani thm 2.6 / mu-book thm 4.5.(2) *) -Theorem thm26 (X : seq {RV P >-> R}) (delta : R) n : - is_bernoulli_trial X n -> (0 < delta < 1)%R -> - let X' := @bernoulli_trial 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 X : {RV P >-> R}. -set mu := 'E_P[X']. -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. - - admit. (* oops *) - - rewrite norm_expR. - have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun 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'] = mmt_gen_fun X' t by []. - rewrite (binomial_mmt_gen_fun _ bX)/=. - rewrite /mu /X' (expectation_bernoulli_trial bX)/=. - rewrite !lnK ?posrE ?subr_gt0//. - rewrite expR_powR powRrM powRAC. - rewrite ge0_ler_powR ?ler0n// ?nnegrE ?powR_ge0//. - by rewrite addr_ge0 ?mulr_ge0// subr_ge0// ltW. - rewrite addrAC subrr sub0r -expR_powR. - rewrite addrCA -{2}(mulr1 (p%:num)) -mulrBr addrAC subrr sub0r mulrC mulNr. - apply: le01_expR_ge1Dx. - rewrite ler_oppl opprK mulr_ile1//=; [|exact: ltW..]. - by rewrite ler_oppl oppr0 mulr_ge0// ltW. - rewrite !lnK ?posrE ?subr_gt0//. - rewrite -addrAC subrr sub0r -mulrA [X in (_ / X)%R]expR_powR 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 expR_powR. -rewrite lee_fin. -rewrite -mulrN -mulrA [in leRHS]mulrC expR_powR 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 *) - admit. -Admitted. - -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 cor27 (X : seq {RV P >-> R}) (delta : R) n : - is_bernoulli_trial X n -> (0 < delta < 1)%R -> - (0 < n)%nat -> - (0 < p%:num)%R -> - let X' := @bernoulli_trial 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 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: (poisson_ineq bX); rewrite //d0 d1. -- apply: (le_trans (@thm26 _ 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 : seq {RV P >-> R}) (theta delta : R) : - let n := size X in - let X_sum := bernoulli_trial X in - let X' x := (X_sum x) / n%:R in - (0 < p%:num)%R -> - is_bernoulli_trial X n -> - (0 < delta <= 1)%R -> (0 < theta < p%:num)%R -> (0 < n)%nat -> - (3 / theta ^+ 2 * ln (2 / delta) <= n%:R)%R -> - P [set i | `| X' i - p%:num | <= theta]%R >= 1 - delta%:E. -Proof. -move=> n X_sum X' p0 bX /andP[delta0 delta1] /andP[theta0 thetap] n0 tdn. -have E_X_sum: 'E_P[X_sum] = (p%:num * n%:R)%:E. - rewrite expectation_sum/=; last first. - by move=> Xi XiX; exact: integrable_bernoulli (bX.1 Xi XiX). - rewrite big_seq. - under eq_bigr. - move=> Xi XiX; rewrite (bernoulli_expectation (bX.1 _ XiX)); over. - rewrite /= sumEFin big_const_seq iter_addr_0/= mulr_natr; congr ((_ *+ _)%:E). - by rewrite /n -count_predT; apply: eq_in_count => x ->. -set epsilon := theta / p%:num. -have epsilon01 : (0 < epsilon < 1)%R. - by rewrite /epsilon ?ltr_pdivr_mulr ?divr_gt0 ?mul1r. -have thetaE : theta = (epsilon * p%:num)%R. - by rewrite /epsilon -mulrA mulVf ?mulr1// gt_eqF. -have step1 : P [set i | `| X' i - p%:num | >= epsilon * p%:num]%R <= - ((expR (- (p%:num * n%:R * (epsilon ^+ 2)) / 3)) *+ 2)%:E. - rewrite [X in P X <= _](_ : _ = - [set i | `| X_sum i - p%:num * n%:R | >= epsilon * p%:num * 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%:num * n%:R)%R = fine (p%:num * n%:R)%:E by []. - rewrite -E_X_sum. - by apply: (@cor27 X epsilon _ bX). -have step2 : P [set i | `| X' i - p%:num | >= 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 -[in leLHS]mulrA ler_wpmul2l//. - rewrite (mulrC epsilon) exprMn -mulrA ler_wpmul2r//. - by rewrite divr_ge0// sqr_ge0. - by rewrite expr2 ler_pimull.*) admit. -suff : delta%:E >= P [set i | (`|X' i - p%:num| >=(*NB: this >= in the pdf *) theta)%R]. - rewrite [X in P X <= _ -> _](_ : _ = ~` [set i | (`|X' i - p%:num| < 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%:num| < 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. -Admitted. - -End bernoulli. diff --git a/theories/sampling.v b/theories/sampling.v new file mode 100644 index 000000000..b4f2def48 --- /dev/null +++ b/theories/sampling.v @@ -0,0 +1,1086 @@ +(* 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. +Require Import real_interval exp numfun lebesgue_measure lebesgue_integral. +Require Import reals ereal signed topology normedtype derive sequences esum. +Require Import measure exp numfun lebesgue_measure lebesgue_integral kernel. +Require Import probability. + +(**md**************************************************************************) +(* # Sampling experiment (wip) *) +(******************************************************************************) + +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 probability. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +Lemma probability_setC A : d.-measurable A -> P (~` A) = 1 - P A. +Proof. +move=> mA; rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI A) -measureD ?setTD ?setCK//. +by rewrite [ltLHS](@probability_setT _ _ _ P) ltry. +Qed. + +Lemma probability_setC' A : d.-measurable A -> P A = 1 - P (~` A). +Proof. +move=> mA. rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI (~` A)) -measureD ?setTD ?setCK//; first exact: measurableC. +by rewrite [ltLHS](@probability_setT _ _ _ P) ltry. +Qed. + +Lemma probability_fin_num A : d.-measurable A -> P A \is a fin_num. +Proof. +move=> mA. +rewrite fin_numElt. +rewrite (le_lt_trans (probability_le1 P mA) (ltry _)). +by rewrite (lt_le_trans ltNy0 (measure_ge0 P _)). +Qed. + +End probability. + +Notation "\prod_ ( i <- r | P ) F" := + (\big[*%E/1%:E]_(i <- r | P%B) F%E) : ereal_scope. +Notation "\prod_ ( i <- r ) F" := + (\big[*%E/1%:E]_(i <- r) F%E) : ereal_scope. +Notation "\prod_ ( m <= i < n | P ) F" := + (\big[*%E/1%:E]_(m <= i < n | P%B) F%E) : ereal_scope. +Notation "\prod_ ( m <= i < n ) F" := + (\big[*%E/1%:E]_(m <= i < n) F%E) : ereal_scope. +Notation "\prod_ ( i | P ) F" := + (\big[*%E/1%:E]_(i | P%B) F%E) : ereal_scope. +Notation "\prod_ i F" := + (\big[*%E/1%:E]_i F%E) : ereal_scope. +Notation "\prod_ ( i : t | P ) F" := + (\big[*%E/1%:E]_(i : t | P%B) F%E) (only parsing) : ereal_scope. +Notation "\prod_ ( i : t ) F" := + (\big[*%E/1%:E]_(i : t) F%E) (only parsing) : ereal_scope. +Notation "\prod_ ( i < n | P ) F" := + (\big[*%E/1%:E]_(i < n | P%B) F%E) : ereal_scope. +Notation "\prod_ ( i < n ) F" := + (\big[*%E/1%:E]_(i < n) F%E) : ereal_scope. +Notation "\prod_ ( i 'in' A | P ) F" := + (\big[*%E/1%:E]_(i in A | P%B) F%E) : ereal_scope. +Notation "\prod_ ( i 'in' A ) F" := + (\big[*%E/1%:E]_(i in A) F%E) : ereal_scope. + +Section independent_events. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +(* def 2.3, independence of events *) +(* TODO: rename to mutually_independent_events *) +Definition mutually_independent (I : choiceType) (A : I -> set T) := +(* (forall i, J i -> measurable (A i)) /\*) + forall J : {fset I}, + P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i). + +End independent_events. + +(* independent class of events, klenke def 2.11, p.59 *) +Section independent_class. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Definition independent_class (I : choiceType) (C : I -> set (set T)) := + (forall i, C i `<=` @measurable _ T) /\ + forall J : {fset I}, + forall E : I -> set T, + (forall i : I, i \in J -> E i \in C i) -> + P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j). + +End independent_class. + +Section independent_RV. +Context {R : realType} d (T : measurableType d). +Variable P : probability T R. + +Definition generated_salgebra (X : {RV P >-> R}) : set (set T) := + preimage_class setT X (@measurable _ R). + +Definition independent_RV (I : choiceType) (X : I -> {RV P >-> R}) := + independent_class P (fun i : I => generated_salgebra (X i)). + +Definition independent_RV_tuple n (X : n.-tuple {RV P >-> R}) := + independent_class P (fun i => generated_salgebra (X `_ i)). + +Lemma independent_RV_tuple_thead_prod_behead n (X : n.+1.-tuple {RV P >-> R}) : + independent_RV_tuple X -> + independent_RV_tuple [tuple thead X; (\prod_(j <- behead X) j)%R]. +Proof. +move: X; elim: n => [X [h1 h2]|]. + have -> : behead X = nil. admit. + rewrite big_nil. + rewrite /independent_RV_tuple/independent_class/=. + split. + case => //=. + by move: (h1 0); rewrite {1}(tuple_eta X). + case => //=. + rewrite /generated_salgebra /preimage_class. + admit. + case => /= [|_]. + admit. + admit. + admit. +(*rewrite /independent_RV_tuple/independent_class/= => [[h1 h2]]. +split. + admit. +move=> J E h3. +rewrite h2// => i iJ. +have := h3 i iJ. +move: iJ. +case: i => [//|i _].*) +Admitted. + +Lemma independent_RV_tuple_behead n (X : n.-tuple {RV P >-> R}) : + independent_RV_tuple X -> independent_RV_tuple [tuple of behead X]. +Proof. +move: X; case: n => [X|n X]. + by rewrite tuple0. +rewrite /independent_RV_tuple/independent_class/=. +move=> [iXm iX]. +split; first by move=> i; rewrite nth_behead; exact: iXm. +move=> J E h. +pose E' n := match n with + 0 => setT + | S m => E m + end. +have := (@iX (0 |` [fset i.+1 | i in J])%fset E'). +have ? : 0 \notin [fset i.+1 | i in J]%fset. + apply/negP. + move/imfsetP. + by case. +rewrite big_fsetU1//=. +rewrite setTI big_fsetU1//=. +rewrite probability_setT mul1e. +rewrite big_imfset/=; last first. + move=> x y _ _; exact: succn_inj. +move=> ->; last first. + elim. + move=> _. + rewrite/generated_salgebra/preimage_class. + (* TODO: make lemma *) + rewrite inE/=. + exists setT => //. + by rewrite setTI preimage_setT. + rewrite /E' => l _ h1. + have := (h l). + rewrite /generated_salgebra. + rewrite nth_behead => -> //. + move: h1. + move/fset1UP => []//. + move/imfsetP. + case => k/= kJ. + by case => ->. +rewrite big_imfset//=. +move=> x y _ _; exact: succn_inj. +Qed. + +End independent_RV. + +Lemma indic_setI {R : ringType} T (A B : set T) : + \1_A \* \1_B = \1_(A `&` B) :> (T -> R). +Proof. +by apply/funext => x/=; rewrite /indic in_setI/= -natrM mulnb. +Qed. + +Lemma preimage_class_mindic {R : realType} d {T : measurableType d} + (A : set T) (mA : measurable A) : + preimage_class [set: T] (mindic R mA) measurable A. +Proof. +exists [set 1%R] => //; rewrite setTI preimage_indic/=. +by rewrite mem_set// memNset//=; apply/eqP; rewrite eq_sym oner_eq0. +Qed. + +(* TODO: move near nnfun_muleindic_ge0 *) +Section nnfun_mulrindic_ge0. + +Lemma mulrf_ge0 (R : realDomainType) x (f : R -> R) : + 0 <= f x -> (x < 0 -> f x = 0) -> 0 <= x * f x. +Proof. +move=> A0 xA /=; have [x0|x0] := ltP x 0%R; first by rewrite (xA x0) mulr0. +by rewrite mulr_ge0. +Qed. + +Lemma nnfun_mulrindic_ge0 d (T : measurableType d) (R : realDomainType) + (f : {nnfun T >-> R}) r z : (0 <= r * (\1_(f @^-1` [set r]) z))%R. +Proof. +apply: (@mulrf_ge0 _ _ (fun r => \1_(f @^-1` [set r]) z)). + by rewrite indicE. +by move=> r0; rewrite preimage_nnfun0// indic0. +Qed. + +End nnfun_mulrindic_ge0. + +(* TODO: move to lebesgue_integral.v *) +Section integrable_comp. +Local Open Scope ereal_scope. + +Context d1 d2 (X : measurableType d1) (Y : measurableType d2) (R : realType). +Variable phi : X -> Y. +Hypothesis mphi : measurable_fun [set: X] phi. +Variable mu : {measure set X -> \bar R}. +Variable f : Y -> \bar R. +Hypothesis mf : measurable_fun [set: Y] f. +Hypothesis intf : mu.-integrable [set: X] (f \o phi). +Local Open Scope ereal_scope. + +Lemma integrable_comp_funeneg : (pushforward mu mphi).-integrable [set: Y] f^\-. +Proof. +apply/integrableP; split. + exact: measurable_funeneg. +move/integrableP : (intf) => [_]. +apply: le_lt_trans. +rewrite ge0_integral_pushforward//=; last first. + apply: measurableT_comp => //=. + exact: measurable_funeneg. +apply: ge0_le_integral => //=. +apply: measurableT_comp => //=. +apply: measurableT_comp => //=. +exact: measurable_funeneg. +apply: measurableT_comp => //=. +apply: measurableT_comp => //=. +move=> x _. +rewrite -/((abse \o (f \o phi)) x). +rewrite (fune_abse (f \o phi)) /=. +rewrite gee0_abs//. +by rewrite lee_addr//. +Qed. + +Lemma integrable_comp_funepos : (pushforward mu mphi).-integrable [set: Y] f^\+. +Proof. +apply/integrableP; split. + exact: measurable_funepos. +move/integrableP : (intf) => [_]. +apply: le_lt_trans. +rewrite ge0_integral_pushforward//=; last first. + apply: measurableT_comp => //=. + exact: measurable_funepos. +apply: ge0_le_integral => //=. +apply: measurableT_comp => //=. +apply: measurableT_comp => //=. +exact: measurable_funepos. +apply: measurableT_comp => //=. +apply: measurableT_comp => //=. +move=> x _. +rewrite -/((abse \o (f \o phi)) x). +rewrite (fune_abse (f \o phi)) /=. +rewrite gee0_abs//. +by rewrite lee_addl//. +Qed. + +End integrable_comp. + +Section transfer. +Local Open Scope ereal_scope. +Context d1 d2 (X : measurableType d1) (Y : measurableType d2) (R : realType). +Variables (phi : X -> Y) (mphi : measurable_fun setT phi). +Variables (mu : {measure set X -> \bar R}). + +Lemma integral_pushforward (f : Y -> \bar R) : + measurable_fun setT f -> + mu.-integrable setT (f \o phi) -> + \int[pushforward mu mphi]_y f y = \int[mu]_x (f \o phi) x. +Proof. +move=> mf intf. +transitivity (\int[mu]_y ((f^\+ \o phi) \- (f^\- \o phi)) y); last first. + by apply: eq_integral => x _; rewrite [in RHS](funeposneg (f \o phi)). +rewrite integralB//; [|exact: integrable_funepos|exact: integrable_funeneg]. +rewrite -[X in _ = X - _]ge0_integral_pushforward//; last first. + exact: measurable_funepos. +rewrite -[X in _ = _ - X]ge0_integral_pushforward//; last first. + exact: measurable_funeneg. +rewrite -integralB//=; last first. +- apply: integrable_comp_funepos => //. + exact: measurableT_comp. + exact: integrableN. +- exact: integrable_comp_funepos. +- apply/eq_integral => x _. + by rewrite /= [in LHS](funeposneg f). +Qed. + +End transfer. + +Section transfer_probability. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +(* TODO: rename integral_distribution to ge0_integral_distribution *) +Lemma integral_distribution' (X : {RV P >-> R}) (f : R -> \bar R) : + measurable_fun setT f -> + P.-integrable [set: T] (f \o X) -> + \int[distribution P X]_y f y = \int[P]_x (f \o X) x. +Proof. by move=> mf intf; rewrite integral_pushforward. Qed. + +End transfer_probability. + +Section integral_measure_add. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) + (m1 m2 : {measure set T -> \bar R}) (D : set T). +Hypothesis mD : measurable D. +Variable f : T -> \bar R. +Hypothesis intf1 : m1.-integrable D f. +Hypothesis intf2 : m2.-integrable D f. +Hypothesis mf : measurable_fun D f. + +Lemma integral_measure_add : + \int[measure_add m1 m2]_(x in D) f x = \int[m1]_(x in D) f x + \int[m2]_(x in D) f x. +Proof. +transitivity (\int[m1]_(x in D) (f^\+ \- f^\-) x + + \int[m2]_(x in D) (f^\+ \- f^\-) x); last first. + by congr +%E; apply: eq_integral => x _; rewrite [in RHS](funeposneg f). +rewrite integralB//; last 2 first. + exact: integrable_funepos. + exact: integrable_funeneg. +rewrite integralB//; last 2 first. + exact: integrable_funepos. + exact: integrable_funeneg. +rewrite addeACA. +rewrite -ge0_integral_measure_add//; last first. + apply: measurable_funepos. + exact: measurable_int intf1. +rewrite -oppeD; last first. + by rewrite ge0_adde_def// inE integral_ge0. +rewrite -ge0_integral_measure_add//; last first. + apply: measurable_funeneg. + exact: measurable_int intf1. +by rewrite integralE. +Qed. + +End integral_measure_add. + +Section independent_product. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Let independent_RVs_expectation2_prob (A B : set T) + (mA : measurable A) (mB : measurable B) : + independent_RV_tuple [tuple of [:: mindic R mA : {RV P >-> R}; + mindic R mB : {RV P >-> R}]] -> + P (A `&` B) = P A * P B. +Proof. +move=> AB. +pose O1 := [fset 0; 1]%N%fset. +pose funO1 := [eta fun=> set0 with 0 |-> A, 1 |-> B]%N. +have : forall i : nat, i \in O1 -> + funO1 i \in @generated_salgebra _ _ _ P [:: mindic R mA : {RV P >-> R} ; + mindic R mB : {RV P >-> R}]`_i. + move=> [|[|?]]; rewrite /O1 ?inE//= => _. + + by rewrite /generated_salgebra; exact: preimage_class_mindic. + + by rewrite /generated_salgebra; exact: preimage_class_mindic. +move/AB.2. +by rewrite /O1 !big_fsetU1/= ?inE// !big_seq_fset1/=. +Qed. + +Let independent_RVs_expectation2_indic (A B : set T) + (mA : measurable A) (mB : measurable B) : + independent_RV_tuple [tuple of [:: mindic R mA : {RV P >-> R}; + mindic R mB : {RV P >-> R}]] -> + 'E_P[\1_A * \1_B] = 'E_P[\1_A] * 'E_P[\1_B]. +Proof. +move=> AB. +transitivity ('E_P[\1_(A `&` B)]). + by rewrite -indic_setI. +rewrite !expectation_indic//; last exact: measurableI. +exact: independent_RVs_expectation2_prob. +Qed. + +Let independent_RVs_expectation2_nnsfun (f g : {nnsfun T >-> R}) : + independent_RV_tuple [tuple of [:: f : {RV P >-> R} ; + g : {RV P >-> R}]] -> + 'E_P[f \* g] = 'E_P[f] * 'E_P[g]. +Proof. +move=> fg. +rewrite [in RHS]unlock. +under [X in _ = X * _]eq_integral do rewrite (fimfunE f) -fsumEFin//. +under [X in _ = _ * X]eq_integral do rewrite (fimfunE g) -fsumEFin//. +rewrite ge0_integral_fsum//; last 2 first. + by move=> n; apply/measurableT_comp => //; exact/measurable_funM. + by move=> n x _/=; rewrite lee_fin//=; exact: nnfun_mulrindic_ge0. +rewrite ge0_integral_fsum//; last 2 first. + by move=> n; apply/measurableT_comp => //; exact/measurable_funM. + by move=> n x _/=; rewrite lee_fin//=; exact: nnfun_mulrindic_ge0. +under [in X in _ = X * _]eq_fsbigr. + move=> x xf. + rewrite (integralZl_indic measurableT (fun k => f @^-1` [set x]))//; last first. + exact: preimage_nnfun0. + rewrite integral_indic// setIT. + over. +rewrite /=. +under [in X in _ = _ * X]eq_fsbigr. + move=> x xf. + rewrite (integralZl_indic measurableT (fun k => g @^-1` [set x]))//; last first. + exact: preimage_nnfun0. + rewrite integral_indic// setIT. + over. +rewrite /=. +rewrite !fsbig_finite//=. +rewrite ge0_sume_distrl; last by move=> r _; rewrite nnsfun_mulemu_ge0. +under eq_bigr. + move=> r _. + rewrite ge0_sume_distrr; last by move=> s _; rewrite nnsfun_mulemu_ge0. + under eq_bigr do rewrite muleACA. + over. +rewrite /=. +transitivity ( + (\sum_(i <- fset_set (range f)) + \sum_(i0 <- fset_set (range g)) + (i%:E * i0%:E * (P (f @^-1` [set i] `&` g @^-1` [set i0])))%E)%R +); last first. + rewrite big_seq [RHS]big_seq; apply: eq_bigr => r rf. + rewrite big_seq [RHS]big_seq; apply: eq_bigr => s sf. + congr *%E. + rewrite -[in RHS](setIT (f @^-1` [set r])). + rewrite -[in RHS](setIT (g @^-1` [set s])). + do 2 rewrite -[in RHS]integral_indic//. + do 2 rewrite integral_indic//. + rewrite !setIT. + apply: independent_RVs_expectation2_prob => /=. + rewrite /independent_RV_tuple/independent_class/= in fg. + case: (fg) => _. + admit. +transitivity ( + \int[P]_x (\sum_(i <- fset_set (range f)) + \sum_(i0 <- fset_set (range g)) + (i%:E * i0%:E * (\1_(f @^-1` [set i] `&` g @^-1` [set i0]) x)%:E)%E)%R +); last first. + rewrite ge0_integral_sum//=; last 2 first. + move=> r; apply: emeasurable_fun_sum => // s. + apply: emeasurable_funM => //. + apply: measurableT_comp => //. + apply: measurable_indic. + exact: measurableI. + move=> r t _. + apply: sume_ge0 => // s _. + rewrite -indic_setI/= EFinM. + by rewrite -muleACA mule_ge0//; exact: nnfun_muleindic_ge0. + apply: eq_bigr => r _. + rewrite ge0_integral_sum//=; last 2 first. + move=> s; apply: emeasurable_funM => //. + apply: measurableT_comp => //. + apply: measurable_indic. + exact: measurableI. + move=> s t _. + rewrite -indic_setI/= EFinM. + by rewrite -muleACA mule_ge0//; exact: nnfun_muleindic_ge0. + apply: eq_bigr => s _. + under eq_integral do rewrite -muleA. + rewrite integralZl//; last first. + admit. + rewrite -muleA. + congr *%E. + rewrite integralZl//; last first. + admit. + congr *%E. + rewrite integral_indic ?setIT//. + exact: measurableI. +rewrite unlock. +apply: eq_integral => x _. +under eq_bigr do rewrite sumEFin. +rewrite sumEFin. +congr EFin. +rewrite /=. +rewrite (fimfunE f). +rewrite (fimfunE g). +rewrite !fsbig_finite//=. +rewrite big_distrl//=. +apply: eq_bigr => r _. +rewrite big_distrr//=. +apply: eq_bigr => s _. +rewrite mulrACA. +by rewrite -indic_setI. +Admitted. + +Let independent_RVs_expectation2_ge0 (X Y : {RV P >-> R}) : + independent_RV_tuple [tuple of [:: X; Y]] -> + (forall x, 0 <= X x)%R -> + (forall x, 0 <= Y x)%R -> + 'E_P[X * Y] = 'E_P[X] * 'E_P[Y]. +Proof. +move=> XY X0 Y0. +have mX : measurable_fun setT (EFin \o X) by exact/measurableT_comp. +have mY : measurable_fun setT (EFin \o Y) by exact/measurableT_comp. +have [X_ [ndX_ X_X]] := approximation measurableT mX (fun t _ => X0 t). +have [Y_ [ndY_ Y_Y]] := approximation measurableT mY (fun t _ => Y0 t). +transitivity (limn (fun n => \int[P]_x ((X_ n \* Y_ n) x)%:E)). + admit. +transitivity (limn (fun n => \int[P]_x ((X_ n) x)%:E * \int[P]_y ((Y_ n) y)%:E)). + admit. +transitivity (\int[P]_x 'E_P [X] * \int[P]_y 'E_P [Y]). + admit. +Admitted. + +Lemma independent_RVs_expectation2 (X Y : {RV P >-> R}) : + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) -> + independent_RV_tuple [tuple of [:: X; Y]] -> + 'E_P[X * Y] = 'E_P[X] * 'E_P[Y]. +Proof. +move=> iX iY XY. +have iXY : P.-integrable setT (EFin \o (X \* Y)%R). + admit. +have dX := funeposneg (EFin \o X). +have dY := funeposneg (EFin \o X). +Admitted. + +(* +Lemma independent_RVs_expectation (X : seq {RV P >-> R}) : + independent_RV X -> 'E_P[\prod_(Xi <- X) Xi] = \prod_(Xi <- X) 'E_P[Xi]. +Proof. +elim: n X => [|n ih X iX]. + move=> X _. + have -> : X = nil by exact/tuple0. + by rewrite !big_nil expectation_cst. +have XE := tuple_eta X. +rewrite XE !big_cons. +rewrite independent_RVs_expectation2//; last 3 first. + admit. + admit. + exact: independent_RV_tuple_thead_prod_behead. +congr *%E. +apply: (ih [tuple of behead X]). +exact: independent_RV_tuple_behead. +Admitted. +*) + +End independent_product. + +(* 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 +*) + + +(* this seems to be provable like in https://www.cs.purdue.edu/homes/spa/courses/pg17/mu-book.pdf page 65 *) +Lemma taylor_ln_le {R : realType} : + forall (delta : R), ((1 + delta) * ln (1 + delta) >= delta + delta^+2 / 3)%R. +Admitted. + +Lemma expR_prod d (T : measurableType d) (R : realType) (P : probability T R) + (X : seq {RV P >-> R}) (f : {RV P >-> 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. + +(* TODO: move *) +Lemma ln_div {R : realType} : {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 {R : realType} : normr \o expR = (expR : R -> R). +Proof. by apply/funext => x /=; rewrite ger0_norm ?expR_ge0. Qed. + +Lemma le01_expR_ge1Dx {R : realType} (x : R) : (-1 <= x <= 0 -> 1 + x <= expR x)%R. +Proof. +move=> /andP [N1x x0]. +pose f : R^o -> R := (expR \- (cst 1 \+ id))%R. +rewrite -subr_ge0 (_ : 0%R = f 0%R); last by rewrite /f !fctE/= expR0 addr0 subrr. +pose f' : R^o -> R := (expR \- (cst 0 \+ cst 1))%R. +move: N1x; rewrite le_eqVlt => /predU1P[<-|N1x]. + by rewrite /f !fctE /= expR0 addr0 subrr subr0 expR_ge0. +move: x0; rewrite le_eqVlt => /predU1P[<-//|x0]. +have [c cx] : exists2 c, c \in `]x, 0%R[ & (f 0 - f x)%R = (f' c * (0 - x))%R. + apply: MVT => //. + admit. (* TODO(rei) *) +rewrite -[leRHS]/(f x) -subr_le0 sub0r /f' => ->; apply: mulr_le0_ge0. + by rewrite /=subr_le0 add0r -expR0 ler_expR; move: cx; rewrite in_itv => /andP[_ /ltW]. +by rewrite lerNr oppr0 ltW. +Admitted. + +Section bernoulli_trial. + +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). +Variable p : {nonneg R}. +Hypothesis p1 : (p%:num <= 1)%R. + +Definition real_of_bool (b : bool) : R := b%:R. + +Lemma measurable_fun_real_of_bool : measurable_fun [set: bool] real_of_bool. +Proof. by []. Qed. + +Lemma real_of_bool1 : real_of_bool @^-1` [set 1%R] = [set true]. +Proof. +by apply/seteqP; split => [x|x ->]; case: x => // /esym/eqP; rewrite oner_eq0. +Qed. + +Lemma real_of_bool0 : real_of_bool @^-1` [set 0%R] = [set false]. +Proof. +by apply/seteqP; split => [x|x ->]; case: x => //= /eqP/=; rewrite oner_eq0. +Qed. + +Definition bernoulli_RV (X : {RV P >-> R}) := + distribution P X = pushforward (bernoulli p%:num) measurable_fun_real_of_bool + /\ range X = [set 0; 1]%R. + +Lemma bernoulli_RV1 (X : {RV P >-> R}) : bernoulli_RV X -> + P [set i | X i == 1%R] == p%:num%:E. +Proof. +move=> [/(congr1 (fun f => f [set 1%:R]))]. +rewrite /bernoulli/= /pushforward ifT; last exact/andP. +rewrite real_of_bool1 fsbig_set1/= /distribution /= => <- _. +apply/eqP; congr (P _). +by apply/seteqP; split => [x /eqP H//|x /eqP]. +Qed. + +Lemma bernoulli_RV2 (X : {RV P >-> R}) : bernoulli_RV X -> + P [set i | X i == 0%R] == (`1-(p%:num))%:E. +Proof. +move=> [[/(congr1 (fun f => f [set 0%:R]))]]. +rewrite /bernoulli/= /pushforward ifT; last exact/andP. +rewrite real_of_bool0 fsbig_set1/= /distribution /= => <- _. +apply/eqP; congr (P _). +by apply/seteqP; split => [x /eqP H//|x /eqP]. +Qed. + +Lemma bernoulli_ge0 (X : {RV P >-> R}) : bernoulli_RV X -> + forall t, (X t >= 0)%R. +Proof. +move=> bX t. +suff: (range X) (X t) by rewrite bX.2 => -[] ->. +by exists t. +Qed. + +Lemma bernoulli_expectation (X : {RV P >-> R}) : + bernoulli_RV X -> 'E_P[X] = p%:num%:E. +Proof. +move=> bX. +rewrite unlock. +transitivity (\int[P]_w `|X w|%:E). + apply: eq_integral => t _. + by rewrite ger0_norm// bernoulli_ge0. +rewrite -(@integral_distribution _ _ _ _ _ (EFin \o normr))//; last first. + by move=> y //=. + exact: measurableT_comp. +rewrite bX.1. +rewrite ge0_integral_pushforward/=; last 2 first. + exact: measurableT_comp. + by move=> /= r; rewrite lee_fin. +rewrite integral_bernoulli//; last exact/andP. +by rewrite /real_of_bool normr1 normr0 !mule0 adde0 mule1. +Qed. + +Lemma bernoulli_sqr (X : {RV P >-> R}) : + bernoulli_RV X -> bernoulli_RV (X ^+ 2 : {RV P >-> R})%R. +Proof. +rewrite /bernoulli_RV => -[Xp1 X01]; split. + rewrite -Xp1; apply/funext => A. + rewrite /distribution /pushforward/=; congr (P _). + by apply/seteqP; split => [t|t]; + (have : (range X) (X t) by exists t); + rewrite X01/= /GRing.mul/= => -[] ->; rewrite ?(mul0r,mul1r). +rewrite -X01; apply/seteqP; split => [x|x]. +- move=> [t _] /=; rewrite /GRing.mul/= -expr2 => <-; + (have : (range X) (X t) by exists t); + by rewrite X01/= /GRing.mul/= => -[] Xt; + exists t => //; rewrite Xt ?(expr0n,expr1n). +- move=> [t _] /=; rewrite /GRing.mul/= => <-; + (have : (range X) (X t) by exists t); + by rewrite X01/= => -[] Xt; + exists t => //=; rewrite Xt/= ?(mulr0,mulr1). +Qed. + +Lemma integrable_bernoulli (X : {RV P >-> R}) : + bernoulli_RV X -> P.-integrable [set: T] (EFin \o X). +Proof. +move=> bX. +apply/integrableP; split; first by apply: measurableT_comp. +have -> : \int[P]_x `|(EFin \o X) x| = 'E_P[X]. + rewrite unlock /expectation. + apply: eq_integral => x _. + rewrite gee0_abs //= lee_fin. + by rewrite bernoulli_ge0//. +by rewrite bernoulli_expectation// ltry. +Qed. + +Lemma bernoulli_variance (X : {RV P >-> R}) : +(* NB(rei): no need for that? + P.-integrable setT (EFin \o X) -> + P.-integrable [set: T] (EFin \o (X ^+ 2)%R) ->*) +bernoulli_RV X -> 'V_P[X] = (p%:num * (`1-(p%:num)))%:E. +move=> b. +rewrite varianceE; last 2 first. + exact: integrable_bernoulli. + exact: integrable_bernoulli (bernoulli_sqr b). +rewrite (bernoulli_expectation b). +have b2 := bernoulli_sqr b. +rewrite (bernoulli_expectation b2) /=. +by rewrite -EFinD mulrDr mulr1 mulrN. +Qed. + +Definition is_bernoulli_trial n (X : n.-tuple {RV P >-> R}) := + (forall Xi, Xi \in X -> bernoulli_RV Xi) /\ + independent_RV_tuple X. + +Definition bernoulli_trial (X : seq {RV P >-> R}) := + (\sum_(Xi <- X) Xi)%R. + +Lemma expectation_bernoulli_trial n (X : n.-tuple {RV P >-> R}) : + is_bernoulli_trial X -> 'E_P[@bernoulli_trial X] = (n%:R * p%:num)%:E. +Proof. +move=> [bRV [_ Xn]]; rewrite expectation_sum; last first. + by move=> Xi XiX; exact: (integrable_bernoulli (bRV _ XiX)). +under eq_big_seq => Xi XiX. + by rewrite (bernoulli_expectation (bRV Xi _))//; over. +rewrite /= -[in RHS](size_tuple X). +rewrite -sum1_size natr_sum big_distrl/= sumEFin; congr EFin. +by under [RHS]eq_bigr do rewrite mul1r. +Qed. + +Lemma bernoulli_trial_ge0 n (X : n.-tuple {RV P >-> R}) : is_bernoulli_trial X -> + (forall t, 0 <= bernoulli_trial X t)%R. +Proof. +move=> [bRV Xn] t. +rewrite /bernoulli_trial [leRHS](_ : _ = \sum_(Xi <- X) Xi t)%R; last first. + by rewrite {bRV Xn}; elim/big_ind2 : _ => //= _ f _ g <- <-. + (* NB: this maybe need to be a lemma*) +by rewrite big_seq; apply: sumr_ge0 => i iX; exact/bernoulli_ge0/bRV. +Qed. + +Lemma bernoulli_mmt_gen_fun (X : {RV P >-> R}) (t : R) : + bernoulli_RV X -> 'E_P[expR \o t \o* X] = (p%:num * expR t + (1-p%:num))%:E. +Admitted. + +Lemma binomial_mmt_gen_fun n (X_ : n.-tuple {RV P >-> R}) (t : R) : + is_bernoulli_trial X_ -> + let X := bernoulli_trial X_ : {RV P >-> R} in + mmt_gen_fun X t = ((p%:num * expR t + (1-p%:num))`^(n%:R))%:E. +Proof. +rewrite /is_bernoulli_trial /independent_RV /bernoulli_trial. +move=> [bX1 [bX2 bX3]] /=. +rewrite -[LHS]fineK; last first. + rewrite /mmt_gen_fun unlock /expectation. + apply: integral_fune_fin_num => //. + admit. +(* TODO(ale) *) +(*rewrite bX2 big_seq. +apply: congr1. +under eq_bigr => Xi XiX do rewrite (bernoulli_mmt_gen_fun _ (bX1 _ _))//=.*) +Admitted. + +Lemma lm23 n (X_ : n.-tuple {RV P >-> R}) (t : R) : + (0 <= t)%R -> + is_bernoulli_trial X_ -> + let X := bernoulli_trial X_ : {RV P >-> R} in + let mu := 'E_P[X] in + mmt_gen_fun X t <= (expR (fine mu * (expR t - 1)))%:E. +Proof. +rewrite /= => t0 bX. +set X := bernoulli_trial X_. +set mu := 'E_P[X]. +have -> : @mmt_gen_fun _ _ _ P X t = (\prod_(Xi <- X_) fine (mmt_gen_fun Xi t))%:E. + rewrite -[LHS]fineK; last by rewrite (binomial_mmt_gen_fun _ bX). + congr EFin. + rewrite /mmt_gen_fun. + transitivity (fine 'E_P[expR \o t \o* (\sum_(i < n) tnth X_ i)%R]). + congr (fine 'E_P[ _ ]). + apply/funext => x/=. + congr expR. + rewrite /X /bernoulli_trial /=. + admit. + transitivity (fine 'E_P[\prod_(i < n ) (expR \o t \o* (tnth X_ i))]). + congr (fine 'E_P[ _ ]). + apply/funext => x/=. + (* TODO: use expR_prod *) + admit. + admit. +under eq_big_seq => Xi XiX. + have -> : @mmt_gen_fun _ _ _ P Xi t = (1 + p%:num * (expR t - 1))%:E. + rewrite /mmt_gen_fun. + rewrite bernoulli_mmt_gen_fun//; last exact: bX.1. + apply: congr1. + by rewrite mulrBr mulr1 addrCA. + over. +rewrite lee_fin /=. +apply: (le_trans (@ler_prod _ _ _ _ _ (fun x => expR (p%:num * (expR t - 1)))%R _)). + move=> Xi _. + rewrite addr_ge0 ?mulr_ge0 ?subr_ge0 ?andTb//; last first. + rewrite -expR0 ler_expR//. + by rewrite expR_ge1Dx ?mulr_ge0// subr_ge0 -expR0 ler_expR. +rewrite expR_prod -mulr_suml. +move: t0; rewrite le_eqVlt => /predU1P[<-|t0]. + by rewrite expR0 subrr !mulr0. +rewrite ler_expR ler_pmul2r; last first. + by rewrite subr_gt0 -expR0 ltr_expR. +rewrite /mu big_seq expectation_sum; last first. + move=> Xi XiX; apply: integrable_bernoulli; exact: bX.1. +rewrite big_seq -sum_fine. + by apply: ler_sum => Xi XiX; rewrite bernoulli_expectation //=; exact: bX.1. +move=> Xi XiX. rewrite bernoulli_expectation //=; exact: bX.1. +Admitted. + +Lemma end_thm24 n (X_ : n.-tuple {RV P >-> R}) (t delta : R) : + is_bernoulli_trial X_ -> + (0 < delta)%R -> + let X := @bernoulli_trial 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 thm24 n (X_ : n.-tuple {RV P >-> R}) (delta : R) : + is_bernoulli_trial X_ -> + (0 < delta)%R -> + let X := @bernoulli_trial 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 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: (lm23 _ bX); rewrite le_eqVlt t0 orbT. +rewrite mulrC expRM -mulNr mulrA expRM. +exact: (end_thm24 _ bX). +Qed. + +(* theorem 2.5 *) +Theorem poisson_ineq n (X : n.-tuple {RV P >-> R}) (delta : R) : + is_bernoulli_trial X -> + let X' := @bernoulli_trial 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: (thm24 bX) => //. +apply: (@le_trans _ _ (expR ((delta - (delta + delta ^+ 2 / 3)) * fine mu))%:E). + rewrite lee_fin ler_expR ler_wpM2r//. + by rewrite fine_ge0//; apply: expectation_ge0 => t; exact: (bernoulli_trial_ge0 bX). + rewrite 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. + +(* Rajani thm 2.6 / mu-book thm 4.5.(2) *) +Theorem thm26 n (X : n.-tuple {RV P >-> R}) (delta : R) : + is_bernoulli_trial X -> (0 < delta < 1)%R -> + let X' := @bernoulli_trial 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 X : {RV P >-> R}. +set mu := 'E_P[X']. +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 ltrNr -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 _ _ _ _) => //. + - exact: expR_gt0. + - rewrite norm_expR. + have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun 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_wpM2r ?invr_ge0 ?expR_ge0//. + have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun 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%:num)) -mulrBr addrAC subrr sub0r mulrC mulNr. + apply: le01_expR_ge1Dx. + rewrite ler_oppl opprK mulr_ile1//=; [|exact: ltW..]. + by rewrite ler_oppl oppr0 mulr_ge0// ltW. + 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 *) + admit. (* TODO(rei) *) +Admitted. + +(* Rajani -> corollary 2.7 / mu-book -> corollary 4.7 *) +Corollary cor27 n (X : n.-tuple {RV P >-> R}) (delta : R) : + is_bernoulli_trial X -> (0 < delta < 1)%R -> + (0 < n)%nat -> + (0 < p%:num)%R -> + let X' := @bernoulli_trial 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 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 => //. + exact: measurableT_comp. +- rewrite -(@setIidr _ setT [set _ | _]) ?subsetT//. + apply: emeasurable_fun_le => //. + exact: 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: (poisson_ineq bX); rewrite //d0 d1. +- apply: (le_trans (@thm26 _ _ delta bX _)); first by rewrite d0 d1. + rewrite lee_fin ler_expR !mulNr lerN2. + rewrite ler_pM//; 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 n (X : n.-tuple {RV P >-> R}) (theta delta : R) : + let X_sum := bernoulli_trial X in + let X' x := (X_sum x) / n%:R in + (0 < p%:num)%R -> + is_bernoulli_trial X -> + (0 < delta <= 1)%R -> (0 < theta < p%:num)%R -> (0 < n)%nat -> + (3 / theta ^+ 2 * ln (2 / delta) <= n%:R)%R -> + P [set i | `| X' i - p%:num | <= 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%:num * n%:R)%:E. + rewrite expectation_sum/=; last first. + by move=> Xi XiX; exact: integrable_bernoulli (bX.1 Xi XiX). + rewrite big_seq. + under eq_bigr. + move=> Xi XiX; rewrite (bernoulli_expectation (bX.1 _ XiX)); over. + rewrite /= -[in RHS](size_tuple X). + by rewrite -sum1_size natr_sum big_distrr/= sumEFin mulr1 -big_seq. +set epsilon := theta / p%:num. +have epsilon01 : (0 < epsilon < 1)%R. + by rewrite /epsilon ?ltr_pdivr_mulr ?divr_gt0 ?mul1r. +have thetaE : theta = (epsilon * p%:num)%R. + by rewrite /epsilon -mulrA mulVf ?mulr1// gt_eqF. +have step1 : P [set i | `| X' i - p%:num | >= epsilon * p%:num]%R <= + ((expR (- (p%:num * n%:R * (epsilon ^+ 2)) / 3)) *+ 2)%:E. + rewrite [X in P X <= _](_ : _ = + [set i | `| X_sum i - p%:num * n%:R | >= epsilon * p%:num * 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%:num * n%:R)%R = fine (p%:num * n%:R)%:E by []. + rewrite -E_X_sum. + by apply: (@cor27 _ X epsilon bX). +have step2 : P [set i | `| X' i - p%:num | >= 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![leRHS]mulrA. + rewrite [leRHS]mulrCA. + rewrite -[leLHS]mulrA. + rewrite ler_wpM2l//. + rewrite (mulrC epsilon) exprMn -mulrA ler_wpmul2r//. + by rewrite divr_ge0// sqr_ge0. + by rewrite expr2 ler_pimull. +suff : delta%:E >= P [set i | (`|X' i - p%:num| >=(*NB: this >= in the pdf *) theta)%R]. + rewrite [X in P X <= _ -> _](_ : _ = ~` [set i | (`|X' i - p%:num| < 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%:num| < 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_pdivrMr; last by rewrite exprn_gt0. +by rewrite mulrAC. +Qed. + +End bernoulli_trial. From 447e47d434284b62ce3252eccc095a9c43225195 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 7 Jun 2024 19:33:31 +0900 Subject: [PATCH 09/12] minor progress --- theories/sampling.v | 586 +++++++++++++++++++++++++------------------- 1 file changed, 333 insertions(+), 253 deletions(-) diff --git a/theories/sampling.v b/theories/sampling.v index b4f2def48..6df9380b8 100644 --- a/theories/sampling.v +++ b/theories/sampling.v @@ -11,6 +11,11 @@ Require Import probability. (**md**************************************************************************) (* # Sampling experiment (wip) *) +(* *) +(* ref: *) +(* - Rajani https://math.uchicago.edu/~may/REU2019/REUPapers/Rajani.pdf *) +(* - Mitzenmacher Upfal Probability and Computing *) +(* https://www.cs.purdue.edu/homes/spa/courses/pg17/mu-book.pdf *) (******************************************************************************) Set Implicit Arguments. @@ -23,28 +28,25 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. +(* TODO: move *) Section probability. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). Lemma probability_setC A : d.-measurable A -> P (~` A) = 1 - P A. Proof. -move=> mA; rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI A) -measureD ?setTD ?setCK//. +move=> mA. +rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI A). +rewrite -measureD ?setTD ?setCK//. by rewrite [ltLHS](@probability_setT _ _ _ P) ltry. Qed. Lemma probability_setC' A : d.-measurable A -> P A = 1 - P (~` A). Proof. -move=> mA. rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI (~` A)) -measureD ?setTD ?setCK//; first exact: measurableC. -by rewrite [ltLHS](@probability_setT _ _ _ P) ltry. -Qed. - -Lemma probability_fin_num A : d.-measurable A -> P A \is a fin_num. -Proof. move=> mA. -rewrite fin_numElt. -rewrite (le_lt_trans (probability_le1 P mA) (ltry _)). -by rewrite (lt_le_trans ltNy0 (measure_ge0 P _)). +rewrite -(@probability_setT _ _ _ P) -[in RHS](setTI (~` A)). +rewrite -measureD ?setTD ?setCK//; first exact: measurableC. +by rewrite [ltLHS](@probability_setT _ _ _ P) ltry. Qed. End probability. @@ -74,122 +76,6 @@ Notation "\prod_ ( i 'in' A | P ) F" := Notation "\prod_ ( i 'in' A ) F" := (\big[*%E/1%:E]_(i in A) F%E) : ereal_scope. -Section independent_events. -Context {R : realType} d {T : measurableType d}. -Variable P : probability T R. -Local Open Scope ereal_scope. - -(* def 2.3, independence of events *) -(* TODO: rename to mutually_independent_events *) -Definition mutually_independent (I : choiceType) (A : I -> set T) := -(* (forall i, J i -> measurable (A i)) /\*) - forall J : {fset I}, - P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i). - -End independent_events. - -(* independent class of events, klenke def 2.11, p.59 *) -Section independent_class. -Context {R : realType} d {T : measurableType d}. -Variable P : probability T R. -Local Open Scope ereal_scope. - -Definition independent_class (I : choiceType) (C : I -> set (set T)) := - (forall i, C i `<=` @measurable _ T) /\ - forall J : {fset I}, - forall E : I -> set T, - (forall i : I, i \in J -> E i \in C i) -> - P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j). - -End independent_class. - -Section independent_RV. -Context {R : realType} d (T : measurableType d). -Variable P : probability T R. - -Definition generated_salgebra (X : {RV P >-> R}) : set (set T) := - preimage_class setT X (@measurable _ R). - -Definition independent_RV (I : choiceType) (X : I -> {RV P >-> R}) := - independent_class P (fun i : I => generated_salgebra (X i)). - -Definition independent_RV_tuple n (X : n.-tuple {RV P >-> R}) := - independent_class P (fun i => generated_salgebra (X `_ i)). - -Lemma independent_RV_tuple_thead_prod_behead n (X : n.+1.-tuple {RV P >-> R}) : - independent_RV_tuple X -> - independent_RV_tuple [tuple thead X; (\prod_(j <- behead X) j)%R]. -Proof. -move: X; elim: n => [X [h1 h2]|]. - have -> : behead X = nil. admit. - rewrite big_nil. - rewrite /independent_RV_tuple/independent_class/=. - split. - case => //=. - by move: (h1 0); rewrite {1}(tuple_eta X). - case => //=. - rewrite /generated_salgebra /preimage_class. - admit. - case => /= [|_]. - admit. - admit. - admit. -(*rewrite /independent_RV_tuple/independent_class/= => [[h1 h2]]. -split. - admit. -move=> J E h3. -rewrite h2// => i iJ. -have := h3 i iJ. -move: iJ. -case: i => [//|i _].*) -Admitted. - -Lemma independent_RV_tuple_behead n (X : n.-tuple {RV P >-> R}) : - independent_RV_tuple X -> independent_RV_tuple [tuple of behead X]. -Proof. -move: X; case: n => [X|n X]. - by rewrite tuple0. -rewrite /independent_RV_tuple/independent_class/=. -move=> [iXm iX]. -split; first by move=> i; rewrite nth_behead; exact: iXm. -move=> J E h. -pose E' n := match n with - 0 => setT - | S m => E m - end. -have := (@iX (0 |` [fset i.+1 | i in J])%fset E'). -have ? : 0 \notin [fset i.+1 | i in J]%fset. - apply/negP. - move/imfsetP. - by case. -rewrite big_fsetU1//=. -rewrite setTI big_fsetU1//=. -rewrite probability_setT mul1e. -rewrite big_imfset/=; last first. - move=> x y _ _; exact: succn_inj. -move=> ->; last first. - elim. - move=> _. - rewrite/generated_salgebra/preimage_class. - (* TODO: make lemma *) - rewrite inE/=. - exists setT => //. - by rewrite setTI preimage_setT. - rewrite /E' => l _ h1. - have := (h l). - rewrite /generated_salgebra. - rewrite nth_behead => -> //. - move: h1. - move/fset1UP => []//. - move/imfsetP. - case => k/= kJ. - by case => ->. -rewrite big_imfset//=. -move=> x y _ _; exact: succn_inj. -Qed. - -End independent_RV. - Lemma indic_setI {R : ringType} T (A B : set T) : \1_A \* \1_B = \1_(A `&` B) :> (T -> R). Proof. @@ -255,8 +141,7 @@ apply: measurableT_comp => //=. move=> x _. rewrite -/((abse \o (f \o phi)) x). rewrite (fune_abse (f \o phi)) /=. -rewrite gee0_abs//. -by rewrite lee_addr//. +by rewrite gee0_abs// leeDr. Qed. Lemma integrable_comp_funepos : (pushforward mu mphi).-integrable [set: Y] f^\+. @@ -277,8 +162,7 @@ apply: measurableT_comp => //=. move=> x _. rewrite -/((abse \o (f \o phi)) x). rewrite (fune_abse (f \o phi)) /=. -rewrite gee0_abs//. -by rewrite lee_addl//. +by rewrite gee0_abs// leeDl. Qed. End integrable_comp. @@ -362,6 +246,216 @@ Qed. End integral_measure_add. +Lemma expR_prod d (T : measurableType d) (R : realType) (P : probability T R) + (X : seq {RV P >-> R}) (f : {RV P >-> 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. + +(* TODO: move *) +Lemma ln_div {R : realType} : + {in Num.pos &, {morph ln (R:=R) : x y / (x / y)%R >-> (x - y)%R}}. +Proof. +move=> x y; rewrite !posrE => x0 y0. +by rewrite lnM ?posrE ?invr_gt0// lnV ?posrE. +Qed. + +Lemma norm_expR {R : realType} : normr \o expR = (expR : R -> R). +Proof. by apply/funext => x /=; rewrite ger0_norm ?expR_ge0. Qed. + +Lemma le01_expR_ge1Dx {R : realType} (x : R) : + (-1 <= x <= 0 -> 1 + x <= expR x)%R. +Proof. +move=> /andP [N1x x0]. +pose f : R^o -> R := (expR \- (cst 1 \+ id))%R. +rewrite -subr_ge0 (_ : 0%R = f 0%R); last first. + by rewrite /f !fctE/= expR0 addr0 subrr. +pose f' : R^o -> R := (expR \- (cst 0 \+ cst 1))%R. +move: N1x; rewrite le_eqVlt => /predU1P[<-|N1x]. + by rewrite /f !fctE /= expR0 addr0 subrr subr0 expR_ge0. +move: x0; rewrite le_eqVlt => /predU1P[<-//|x0]. +have [c cx] : exists2 c, c \in `]x, 0%R[ & (f 0 - f x)%R = (f' c * (0 - x))%R. + apply: MVT => //. + apply: continuous_subspaceT => /= z. + apply: cvgB; first exact: continuous_expR. + by apply: cvgD => //; exact: cvg_cst. +rewrite -[leRHS]/(f x) -subr_le0 sub0r /f' => ->; apply: mulr_le0_ge0. + rewrite /=subr_le0 add0r -expR0 ler_expR. + by move: cx; rewrite in_itv => /andP[_ /ltW]. +by rewrite lerNr oppr0 ltW. +Qed. + +(* mu-book p. 66 *) +Lemma analytical_argument_thm22 {R : realType} (delta : R) : + 0 <= delta <= 1 -> + (- delta - (1 - delta) * ln (1 - delta) <= - delta ^+ 2 / 2)%R. +Proof. +move=> d01. +pose f (x : R) := - x - (1 - x) * ln (1 - x) + x ^+2 / 2. +pose f' (x : R) := ln (1 - x) + x. +pose f'' (x : R) := - (1 - x)^-1 + 1. +have f''01 (x : R) : 0 <= x <= 1 -> f'' x < 0. + admit. +have f'0 : f' 0 = 0 by rewrite /f' subr0 ln1 addr0. +have f'01 (x : R) : 0 <= x <= 1 -> f' x <= 0. + admit. +have f0 : f 0 = 0 :> R. + by rewrite /f subr0 ln1 mulr0 expr0n mul0r subr0 addrC subrr. +have f01 (x : R) : 0 <= x <= 1 -> f x <= 0. + admit. +rewrite -subr_le0. +rewrite mulNr opprK. +exact: f01. +Admitted. + +(* mu-book p. 65 *) +Lemma analytical_argument_thm26 {R : realType} (delta : R) : + 0 <= delta <= 1 -> + ((1 + delta) * ln (1 + delta) >= delta + delta^+2 / 3)%R. +Proof. +move=> d01. +pose f x : R := x - (1 + x) * ln (1 + x) + x^+2 / 3. +pose f' x : R := 1 - (1 + x) / (1 - x) - ln (1 + x) + (2 / 3) * x. +have f'E x : f' x = - ln (1 + x) + (2 / 3) * x. + admit. +pose f'' x : R := - (1 + x)^-1 + 2 / 3. +have f''P1 (x : R) : 0 <= x < 1/2 -> f'' x < 0. + admit. +have f''P2 x : x > 1/2 -> f'' x > 0. + admit. +have f'0 : f' 0 = 0. + by rewrite /f' subr0 divr1 mulr0 addr0 ln1 subr0 subrr addr0. +have f'1 : f' 1 < 0. + admit. +have f'01 (x : R) : 0 <= x <= 1 -> f' x <= 0. + admit. +have f0 : f 0 = 0. + by rewrite /f addr0 expr0n/= mul0r ln1 mulr0 subrr addr0. +have f01 (x : R) : 0 <= x <= 1 -> f x <= 0. + admit. +have := f01 _ d01. +by rewrite /f addrAC subr_le0. +Admitted. + +(* WIP *) +Section independent_events. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +(* def 2.3, independence of events *) +(* TODO: rename to mutually_independent_events *) +Definition mutually_independent (I : choiceType) (A : I -> set T) := +(* (forall i, J i -> measurable (A i)) /\*) + forall J : {fset I}, + P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i). + +End independent_events. + +(* independent class of events, klenke def 2.11, p.59 *) +Section independent_class. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. +Local Open Scope ereal_scope. + +Definition independent_class (I : choiceType) (C : I -> set (set T)) := + (forall i, C i `<=` @measurable _ T) /\ + forall J : {fset I}, + forall E : I -> set T, + (forall i : I, i \in J -> E i \in C i) -> + P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j). + +End independent_class. + +Section independent_RV. +Context {R : realType} d (T : measurableType d). +Variable P : probability T R. + +Definition generated_salgebra (X : {RV P >-> R}) : set (set T) := + preimage_class setT X (@measurable _ R). + +Definition independent_RV (I : choiceType) (X : I -> {RV P >-> R}) := + independent_class P (fun i : I => generated_salgebra (X i)). + +Definition independent_RV_tuple n (X : n.-tuple {RV P >-> R}) := + independent_class P (fun i => generated_salgebra (X `_ i)). + +Lemma independent_RV_tuple_thead_prod_behead n (X : n.+1.-tuple {RV P >-> R}) : + independent_RV_tuple X -> + independent_RV_tuple [tuple thead X; (\prod_(j <- behead X) j)%R]. +Proof. +move: X; elim: n => [X [h1 h2]|]. + have -> : behead X = nil. admit. + rewrite big_nil. + rewrite /independent_RV_tuple/independent_class/=. + split. + case => //=. + by move: (h1 0); rewrite {1}(tuple_eta X). + case => //=. + rewrite /generated_salgebra /preimage_class. + admit. + case => /= [|_]. + admit. + admit. + admit. +(*rewrite /independent_RV_tuple/independent_class/= => [[h1 h2]]. +split. + admit. +move=> J E h3. +rewrite h2// => i iJ. +have := h3 i iJ. +move: iJ. +case: i => [//|i _].*) +Admitted. + +Lemma independent_RV_tuple_behead n (X : n.-tuple {RV P >-> R}) : + independent_RV_tuple X -> independent_RV_tuple [tuple of behead X]. +Proof. +move: X; case: n => [X|n X]. + by rewrite tuple0. +rewrite /independent_RV_tuple/independent_class/=. +move=> [iXm iX]. +split; first by move=> i; rewrite nth_behead; exact: iXm. +move=> J E h. +pose E' n := match n with + 0 => setT + | S m => E m + end. +have := (@iX (0 |` [fset i.+1 | i in J])%fset E'). +have ? : 0 \notin [fset i.+1 | i in J]%fset. + apply/negP. + move/imfsetP. + by case. +rewrite big_fsetU1//=. +rewrite setTI big_fsetU1//=. +rewrite probability_setT mul1e. +rewrite big_imfset/=; last first. + move=> x y _ _; exact: succn_inj. +move=> ->; last first. + elim. + move=> _. + rewrite/generated_salgebra/preimage_class. + (* TODO: make lemma *) + rewrite inE/=. + exists setT => //. + by rewrite setTI preimage_setT. + rewrite /E' => l _ h1. + have := (h l). + rewrite /generated_salgebra. + rewrite nth_behead => -> //. + move: h1. + move/fset1UP => []//. + move/imfsetP. + case => k/= kJ. + by case => ->. +rewrite big_imfset//=. +move=> x y _ _; exact: succn_inj. +Qed. + +End independent_RV. + Section independent_product. Context {R : realType} d {T : measurableType d}. Variable P : probability T R. @@ -566,52 +660,8 @@ Definition kwise_independent_RV (I : choiceType) (A : set I) (X : I -> {RV P >-> this should be equivalent according to wikipedia https://en.wikipedia.org/wiki/Independence_(probability_theory)#For_real_valued_random_variables *) - -(* this seems to be provable like in https://www.cs.purdue.edu/homes/spa/courses/pg17/mu-book.pdf page 65 *) -Lemma taylor_ln_le {R : realType} : - forall (delta : R), ((1 + delta) * ln (1 + delta) >= delta + delta^+2 / 3)%R. -Admitted. - -Lemma expR_prod d (T : measurableType d) (R : realType) (P : probability T R) - (X : seq {RV P >-> R}) (f : {RV P >-> 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. - -(* TODO: move *) -Lemma ln_div {R : realType} : {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 {R : realType} : normr \o expR = (expR : R -> R). -Proof. by apply/funext => x /=; rewrite ger0_norm ?expR_ge0. Qed. - -Lemma le01_expR_ge1Dx {R : realType} (x : R) : (-1 <= x <= 0 -> 1 + x <= expR x)%R. -Proof. -move=> /andP [N1x x0]. -pose f : R^o -> R := (expR \- (cst 1 \+ id))%R. -rewrite -subr_ge0 (_ : 0%R = f 0%R); last by rewrite /f !fctE/= expR0 addr0 subrr. -pose f' : R^o -> R := (expR \- (cst 0 \+ cst 1))%R. -move: N1x; rewrite le_eqVlt => /predU1P[<-|N1x]. - by rewrite /f !fctE /= expR0 addr0 subrr subr0 expR_ge0. -move: x0; rewrite le_eqVlt => /predU1P[<-//|x0]. -have [c cx] : exists2 c, c \in `]x, 0%R[ & (f 0 - f x)%R = (f' c * (0 - x))%R. - apply: MVT => //. - admit. (* TODO(rei) *) -rewrite -[leRHS]/(f x) -subr_le0 sub0r /f' => ->; apply: mulr_le0_ge0. - by rewrite /=subr_le0 add0r -expR0 ler_expR; move: cx; rewrite in_itv => /andP[_ /ltW]. -by rewrite lerNr oppr0 ltW. -Admitted. - -Section bernoulli_trial. - -Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) (P : probability T R). -Variable p : {nonneg R}. -Hypothesis p1 : (p%:num <= 1)%R. +Section real_of_bool. +Context {R : realType}. Definition real_of_bool (b : bool) : R := b%:R. @@ -628,6 +678,14 @@ Proof. by apply/seteqP; split => [x|x ->]; case: x => //= /eqP/=; rewrite oner_eq0. Qed. +End real_of_bool. + +Section bernoulli_trial. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). +Variable p : {nonneg R}. +Hypothesis p1 : (p%:num <= 1)%R. + Definition bernoulli_RV (X : {RV P >-> R}) := distribution P X = pushforward (bernoulli p%:num) measurable_fun_real_of_bool /\ range X = [set 0; 1]%R. @@ -645,7 +703,7 @@ Qed. Lemma bernoulli_RV2 (X : {RV P >-> R}) : bernoulli_RV X -> P [set i | X i == 0%R] == (`1-(p%:num))%:E. Proof. -move=> [[/(congr1 (fun f => f [set 0%:R]))]]. +move=> [/(congr1 (fun f => f [set 0%:R]))]. rewrite /bernoulli/= /pushforward ifT; last exact/andP. rewrite real_of_bool0 fsbig_set1/= /distribution /= => <- _. apply/eqP; congr (P _). @@ -668,11 +726,10 @@ rewrite unlock. transitivity (\int[P]_w `|X w|%:E). apply: eq_integral => t _. by rewrite ger0_norm// bernoulli_ge0. -rewrite -(@integral_distribution _ _ _ _ _ (EFin \o normr))//; last first. - by move=> y //=. +rewrite -(@integral_distribution _ _ _ _ _ (EFin \o normr))//; last 2 first. exact: measurableT_comp. -rewrite bX.1. -rewrite ge0_integral_pushforward/=; last 2 first. + by move=> y //=. +rewrite bX.1 ge0_integral_pushforward/=; last 2 first. exact: measurableT_comp. by move=> /= r; rewrite lee_fin. rewrite integral_bernoulli//; last exact/andP. @@ -746,7 +803,8 @@ rewrite -sum1_size natr_sum big_distrl/= sumEFin; congr EFin. by under [RHS]eq_bigr do rewrite mul1r. Qed. -Lemma bernoulli_trial_ge0 n (X : n.-tuple {RV P >-> R}) : is_bernoulli_trial X -> +Lemma bernoulli_trial_ge0 n (X : n.-tuple {RV P >-> R}) : + is_bernoulli_trial X -> (forall t, 0 <= bernoulli_trial X t)%R. Proof. move=> [bRV Xn] t. @@ -777,9 +835,18 @@ apply: congr1. under eq_bigr => Xi XiX do rewrite (bernoulli_mmt_gen_fun _ (bX1 _ _))//=.*) Admitted. +End bernoulli_trial. + +Section rajani. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). +Variable p : {nonneg R}. +Hypothesis p1 : (p%:num <= 1)%R. + +(* Rajani lem 2.3 *) Lemma lm23 n (X_ : n.-tuple {RV P >-> R}) (t : R) : (0 <= t)%R -> - is_bernoulli_trial X_ -> + is_bernoulli_trial p X_ -> let X := bernoulli_trial X_ : {RV P >-> R} in let mu := 'E_P[X] in mmt_gen_fun X t <= (expR (fine mu * (expR t - 1)))%:E. @@ -788,7 +855,7 @@ rewrite /= => t0 bX. set X := bernoulli_trial X_. set mu := 'E_P[X]. have -> : @mmt_gen_fun _ _ _ P X t = (\prod_(Xi <- X_) fine (mmt_gen_fun Xi t))%:E. - rewrite -[LHS]fineK; last by rewrite (binomial_mmt_gen_fun _ bX). + rewrite -[LHS]fineK; last by rewrite (binomial_mmt_gen_fun p1 _ bX). congr EFin. rewrite /mmt_gen_fun. transitivity (fine 'E_P[expR \o t \o* (\sum_(i < n) tnth X_ i)%R]). @@ -796,6 +863,7 @@ have -> : @mmt_gen_fun _ _ _ P X t = (\prod_(Xi <- X_) fine (mmt_gen_fun Xi t))% apply/funext => x/=. congr expR. rewrite /X /bernoulli_trial /=. + rewrite big_tnth//. admit. transitivity (fine 'E_P[\prod_(i < n ) (expR \o t \o* (tnth X_ i))]). congr (fine 'E_P[ _ ]). @@ -806,32 +874,34 @@ have -> : @mmt_gen_fun _ _ _ P X t = (\prod_(Xi <- X_) fine (mmt_gen_fun Xi t))% under eq_big_seq => Xi XiX. have -> : @mmt_gen_fun _ _ _ P Xi t = (1 + p%:num * (expR t - 1))%:E. rewrite /mmt_gen_fun. - rewrite bernoulli_mmt_gen_fun//; last exact: bX.1. + rewrite (bernoulli_mmt_gen_fun p1)//; last exact: bX.1. apply: congr1. by rewrite mulrBr mulr1 addrCA. over. rewrite lee_fin /=. -apply: (le_trans (@ler_prod _ _ _ _ _ (fun x => expR (p%:num * (expR t - 1)))%R _)). +apply: (le_trans (@ler_prod _ _ _ _ _ + (fun x => expR (p%:num * (expR t - 1)))%R _)). move=> Xi _. rewrite addr_ge0 ?mulr_ge0 ?subr_ge0 ?andTb//; last first. - rewrite -expR0 ler_expR//. + by rewrite -expR0 ler_expR. by rewrite expR_ge1Dx ?mulr_ge0// subr_ge0 -expR0 ler_expR. rewrite expR_prod -mulr_suml. move: t0; rewrite le_eqVlt => /predU1P[<-|t0]. by rewrite expR0 subrr !mulr0. -rewrite ler_expR ler_pmul2r; last first. +rewrite ler_expR ler_pM2r; last first. by rewrite subr_gt0 -expR0 ltr_expR. rewrite /mu big_seq expectation_sum; last first. - move=> Xi XiX; apply: integrable_bernoulli; exact: bX.1. + move=> Xi XiX; apply: (integrable_bernoulli p1); exact: bX.1. rewrite big_seq -sum_fine. - by apply: ler_sum => Xi XiX; rewrite bernoulli_expectation //=; exact: bX.1. -move=> Xi XiX. rewrite bernoulli_expectation //=; exact: bX.1. + apply: ler_sum => Xi XiX; rewrite (bernoulli_expectation p1) //=. + exact: bX.1. +by move=> Xi XiX; rewrite (bernoulli_expectation p1) //=; exact: bX.1. Admitted. Lemma end_thm24 n (X_ : n.-tuple {RV P >-> R}) (t delta : R) : - is_bernoulli_trial X_ -> + is_bernoulli_trial p X_ -> (0 < delta)%R -> - let X := @bernoulli_trial X_ in + let X := bernoulli_trial X_ in let mu := 'E_P[X] in let t := ln (1 + delta) in (expR (expR t - 1) `^ fine mu)%:E * @@ -843,24 +913,24 @@ 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//. +- rewrite lnK ?posrE ?addr_gt0// addrAC subrr add0r ler_wpM2l ?expR_ge0//. by rewrite -powRN mulNr -mulrN expRM lnK// posrE addr_gt0. Qed. -(* theorem 2.4 Rajani / thm 4.4.(2) mu-book *) +(* Rajani thm 2.4 Rajani / mu-book thm 4.4.(2) *) Theorem thm24 n (X_ : n.-tuple {RV P >-> R}) (delta : R) : - is_bernoulli_trial X_ -> + is_bernoulli_trial p X_ -> (0 < delta)%R -> - let X := @bernoulli_trial X_ in + let X := bernoulli_trial 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. + ((expR delta / ((1 + delta) `^ (1 + delta))) `^ (fine mu))%:E. Proof. rewrite /= => bX delta0. -set X := @bernoulli_trial X_. +set X := bernoulli_trial X_. set mu := 'E_P[X]. set t := ln (1 + delta). -have t0 : (0 < t)%R by rewrite ln_gt0// ltr_addl. +have t0 : (0 < t)%R by rewrite ln_gt0// ltrDl. apply: (le_trans (chernoff _ _ t0)). apply: (@le_trans _ _ ((expR (fine mu * (expR t - 1)))%:E * (expR (- (t * ((1 + delta) * fine mu))))%:E)). @@ -870,64 +940,73 @@ rewrite mulrC expRM -mulNr mulrA expRM. exact: (end_thm24 _ bX). Qed. -(* theorem 2.5 *) +(* Rajani thm 2.5 *) Theorem poisson_ineq n (X : n.-tuple {RV P >-> R}) (delta : R) : - is_bernoulli_trial X -> - let X' := @bernoulli_trial X in + is_bernoulli_trial p X -> + let X' := bernoulli_trial 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. + (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: (thm24 bX) => //. +move=> bX X' mu n0 /andP[delta0 delta1]. +apply: (@le_trans _ _ + (expR ((delta - (1 + delta) * ln (1 + delta)) * fine mu))%:E). + rewrite expRM expRB (mulrC _ (ln _)) expRM lnK; last by rewrite posrE addr_gt0. + exact: (thm24 bX). apply: (@le_trans _ _ (expR ((delta - (delta + delta ^+ 2 / 3)) * fine mu))%:E). rewrite lee_fin ler_expR ler_wpM2r//. - by rewrite fine_ge0//; apply: expectation_ge0 => t; exact: (bernoulli_trial_ge0 bX). - rewrite ler_sub//. - exact: taylor_ln_le. + rewrite fine_ge0//; apply: expectation_ge0 => t. + exact: (bernoulli_trial_ge0 bX). + by rewrite lerB// analytical_argument_thm26// (ltW delta0) (ltW delta1). rewrite le_eqVlt; apply/orP; left; apply/eqP; congr (expR _)%:E. by rewrite opprD addrA subrr add0r mulrC mulrN mulNr mulrA. Qed. (* Rajani thm 2.6 / mu-book thm 4.5.(2) *) Theorem thm26 n (X : n.-tuple {RV P >-> R}) (delta : R) : - is_bernoulli_trial X -> (0 < delta < 1)%R -> - let X' := @bernoulli_trial X : {RV P >-> R} in + is_bernoulli_trial p X -> (0 < delta < 1)%R -> + let X' : {RV P >-> R} := bernoulli_trial X 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. + 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 X : {RV P >-> R}. +set X' := bernoulli_trial X : {RV P >-> R}. set mu := 'E_P[X']. -apply: (@le_trans _ _ (((expR (- delta) / ((1 - delta) `^ (1 - delta))) `^ (fine mu))%:E)). +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]. + 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. + by rewrite -[in RHS]ler_ndivrMl// mulrA mulVf ?lt_eqF// mul1r. set t := ln (1 - delta). have ln1delta : (t < 0)%R. (* TODO: lacking a lemma here *) rewrite -oppr0 ltrNr -lnV ?posrE ?subr_gt0// ln_gt0//. - by rewrite invf_gt1// ?subr_gt0// ltr_subl_addr ltr_addl. + by rewrite invf_gt1// ?subr_gt0// ltrBlDr ltrDl. have {H1}-> := H1 _ ln1delta. - apply: (@le_trans _ _ (((fine 'E_P[normr \o expR \o t \o* X']) / (expR (t * (1 - delta) * fine mu))))%:E). + 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: (@markov _ _ _ P (expR \o t \o* X' : {RV P >-> R}) id + (expR (t * (1 - delta) * fine mu))%R _ _ _ _) => //. - exact: expR_gt0. - rewrite norm_expR. have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun 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). + by rewrite (binomial_mmt_gen_fun p1 _ bX). + apply: (@le_trans _ _ ((expR ((expR t - 1) * fine mu)) / + (expR (t * (1 - delta) * fine mu)))%:E). rewrite norm_expR lee_fin ler_wpM2r ?invr_ge0 ?expR_ge0//. have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun X' t by []. - rewrite (binomial_mmt_gen_fun _ bX)/=. - rewrite /mu /X' (expectation_bernoulli_trial bX)/=. + rewrite (binomial_mmt_gen_fun p1 _ bX)/=. + rewrite /mu /X' (expectation_bernoulli_trial p1 bX)/=. rewrite !lnK ?posrE ?subr_gt0//. rewrite expRM powRrM powRAC. rewrite ge0_ler_powR ?ler0n// ?nnegrE ?powR_ge0//. @@ -935,8 +1014,8 @@ apply: (@le_trans _ _ (((expR (- delta) / ((1 - delta) `^ (1 - delta))) `^ (fine rewrite addrAC subrr sub0r -expRM. rewrite addrCA -{2}(mulr1 (p%:num)) -mulrBr addrAC subrr sub0r mulrC mulNr. apply: le01_expR_ge1Dx. - rewrite ler_oppl opprK mulr_ile1//=; [|exact: ltW..]. - by rewrite ler_oppl oppr0 mulr_ge0// ltW. + rewrite lerNl opprK mulr_ile1//=; [|exact: ltW..]. + by rewrite lerNl oppr0 mulr_ge0// ltW. 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//. @@ -950,27 +1029,27 @@ rewrite -mulrN -mulrA [in leRHS]mulrC expRM ge0_ler_powR// ?nnegrE. 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 *) - admit. (* TODO(rei) *) -Admitted. + apply: analytical_argument_thm22. + by rewrite (ltW delta0) (ltW delta1). +Qed. -(* Rajani -> corollary 2.7 / mu-book -> corollary 4.7 *) +(* Rajani corollary 2.7 / mu-book -> corollary 4.6 *) Corollary cor27 n (X : n.-tuple {RV P >-> R}) (delta : R) : - is_bernoulli_trial X -> (0 < delta < 1)%R -> + is_bernoulli_trial p X -> (0 < delta < 1)%R -> (0 < n)%nat -> (0 < p%:num)%R -> - let X' := @bernoulli_trial X in + let X' := bernoulli_trial 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. + (expR (- (fine mu * delta ^+ 2) / 3)%R *+ 2)%:E. Proof. move=> bX /andP[d0 d1] n0 p0 /=. -set X' := @bernoulli_trial X. +set X' := bernoulli_trial 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 lerBrDl opprD opprK -{1}(mul1r (fine mu)) -mulrDl. + rewrite -lerBDr -(lerN2 (- _)%R) opprK opprB. rewrite -{2}(mul1r (fine mu)) -mulrBl. rewrite -!lee_fin. over. @@ -988,13 +1067,14 @@ rewrite measureU; last 3 first. 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//=. + rewrite lte_pmul2r//; first by rewrite lte_fin ltrD2l gt0_cp. + rewrite fineK /mu/X' (expectation_bernoulli_trial p1 bX)// lte_fin. + by rewrite mulr_gt0 ?ltr0n. +rewrite mulr2n EFinD leeD//=. - by apply: (poisson_ineq bX); rewrite //d0 d1. - apply: (le_trans (@thm26 _ _ delta bX _)); first by rewrite d0 d1. rewrite lee_fin ler_expR !mulNr lerN2. - rewrite ler_pM//; last by rewrite lef_pinv ?posrE ?ler_nat. + rewrite ler_pM//; last by rewrite lef_pV2 ?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). @@ -1005,7 +1085,7 @@ Theorem sampling n (X : n.-tuple {RV P >-> R}) (theta delta : R) : let X_sum := bernoulli_trial X in let X' x := (X_sum x) / n%:R in (0 < p%:num)%R -> - is_bernoulli_trial X -> + is_bernoulli_trial p X -> (0 < delta <= 1)%R -> (0 < theta < p%:num)%R -> (0 < n)%nat -> (3 / theta ^+ 2 * ln (2 / delta) <= n%:R)%R -> P [set i | `| X' i - p%:num | <= theta]%R >= 1 - delta%:E. @@ -1016,12 +1096,12 @@ have E_X_sum: 'E_P[X_sum] = (p%:num * n%:R)%:E. by move=> Xi XiX; exact: integrable_bernoulli (bX.1 Xi XiX). rewrite big_seq. under eq_bigr. - move=> Xi XiX; rewrite (bernoulli_expectation (bX.1 _ XiX)); over. + move=> Xi XiX; rewrite (bernoulli_expectation p1 (bX.1 _ XiX)); over. rewrite /= -[in RHS](size_tuple X). by rewrite -sum1_size natr_sum big_distrr/= sumEFin mulr1 -big_seq. set epsilon := theta / p%:num. have epsilon01 : (0 < epsilon < 1)%R. - by rewrite /epsilon ?ltr_pdivr_mulr ?divr_gt0 ?mul1r. + by rewrite /epsilon ?ltr_pdivrMr ?divr_gt0 ?mul1r. have thetaE : theta = (epsilon * p%:num)%R. by rewrite /epsilon -mulrA mulVf ?mulr1// gt_eqF. have step1 : P [set i | `| X' i - p%:num | >= epsilon * p%:num]%R <= @@ -1029,10 +1109,10 @@ have step1 : P [set i | `| X' i - p%:num | >= epsilon * p%:num]%R <= rewrite [X in P X <= _](_ : _ = [set i | `| X_sum i - p%:num * n%:R | >= epsilon * p%:num * n%:R]%R); last first. apply/seteqP; split => [t|t]/=. - move/(@ler_wpmul2r _ n%:R (ler0n _ _)) => /le_trans; apply. + move/(@ler_wpM2r _ 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). + move/(@ler_wpM2r _ 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. @@ -1044,14 +1124,14 @@ have step1 : P [set i | `| X' i - p%:num | >= epsilon * p%:num]%R <= have step2 : P [set i | `| X' i - p%:num | >= 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 lee_fin ler_wMn2r// ler_expR mulNr lerNl mulNr opprK. rewrite -2![leRHS]mulrA. rewrite [leRHS]mulrCA. rewrite -[leLHS]mulrA. rewrite ler_wpM2l//. - rewrite (mulrC epsilon) exprMn -mulrA ler_wpmul2r//. + rewrite (mulrC epsilon) exprMn -mulrA ler_wpM2r//. by rewrite divr_ge0// sqr_ge0. - by rewrite expr2 ler_pimull. + by rewrite expr2 ler_piMl. suff : delta%:E >= P [set i | (`|X' i - p%:num| >=(*NB: this >= in the pdf *) theta)%R]. rewrite [X in P X <= _ -> _](_ : _ = ~` [set i | (`|X' i - p%:num| < theta)%R]); last first. apply/seteqP; split => [t|t]/=. @@ -1075,12 +1155,12 @@ suff : delta%:E >= P [set i | (`|X' i - p%:num| >=(*NB: this >= in the pdf *) th by move=> t/= /ltW. (* NB: last step in the pdf *) apply: (le_trans step2). -rewrite lee_fin -(mulr_natr _ 2) -ler_pdivl_mulr//. +rewrite lee_fin -(mulr_natr _ 2) -ler_pdivlMr//. 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_expR mulNr lerNl -lnV; last by rewrite posrE divr_gt0. +rewrite invf_div ler_pdivlMr// mulrC. rewrite -ler_pdivrMr; last by rewrite exprn_gt0. by rewrite mulrAC. Qed. -End bernoulli_trial. +End rajani. From 975c6939d6b9af9a6c6f45eb2175394b1499d243 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 7 Jun 2024 19:52:36 +0900 Subject: [PATCH 10/12] avoid nneg and <= 1 hypos --- theories/sampling.v | 116 +++++++++++++++++++++++--------------------- 1 file changed, 61 insertions(+), 55 deletions(-) diff --git a/theories/sampling.v b/theories/sampling.v index 6df9380b8..0454c45af 100644 --- a/theories/sampling.v +++ b/theories/sampling.v @@ -683,28 +683,28 @@ End real_of_bool. Section bernoulli_trial. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). -Variable p : {nonneg R}. -Hypothesis p1 : (p%:num <= 1)%R. +Variable p : R. +Hypothesis p01 : (0 <= p <= 1)%R. Definition bernoulli_RV (X : {RV P >-> R}) := - distribution P X = pushforward (bernoulli p%:num) measurable_fun_real_of_bool + distribution P X = pushforward (bernoulli p) measurable_fun_real_of_bool /\ range X = [set 0; 1]%R. Lemma bernoulli_RV1 (X : {RV P >-> R}) : bernoulli_RV X -> - P [set i | X i == 1%R] == p%:num%:E. + P [set i | X i == 1%R] == p%:E. Proof. move=> [/(congr1 (fun f => f [set 1%:R]))]. -rewrite /bernoulli/= /pushforward ifT; last exact/andP. +rewrite /bernoulli/= /pushforward ifT//. rewrite real_of_bool1 fsbig_set1/= /distribution /= => <- _. apply/eqP; congr (P _). by apply/seteqP; split => [x /eqP H//|x /eqP]. Qed. Lemma bernoulli_RV2 (X : {RV P >-> R}) : bernoulli_RV X -> - P [set i | X i == 0%R] == (`1-(p%:num))%:E. + P [set i | X i == 0%R] == (`1-p)%:E. Proof. move=> [/(congr1 (fun f => f [set 0%:R]))]. -rewrite /bernoulli/= /pushforward ifT; last exact/andP. +rewrite /bernoulli/= /pushforward ifT//. rewrite real_of_bool0 fsbig_set1/= /distribution /= => <- _. apply/eqP; congr (P _). by apply/seteqP; split => [x /eqP H//|x /eqP]. @@ -719,7 +719,7 @@ by exists t. Qed. Lemma bernoulli_expectation (X : {RV P >-> R}) : - bernoulli_RV X -> 'E_P[X] = p%:num%:E. + bernoulli_RV X -> 'E_P[X] = p%:E. Proof. move=> bX. rewrite unlock. @@ -732,7 +732,7 @@ rewrite -(@integral_distribution _ _ _ _ _ (EFin \o normr))//; last 2 first. rewrite bX.1 ge0_integral_pushforward/=; last 2 first. exact: measurableT_comp. by move=> /= r; rewrite lee_fin. -rewrite integral_bernoulli//; last exact/andP. +rewrite integral_bernoulli//. by rewrite /real_of_bool normr1 normr0 !mule0 adde0 mule1. Qed. @@ -773,7 +773,8 @@ Lemma bernoulli_variance (X : {RV P >-> R}) : (* NB(rei): no need for that? P.-integrable setT (EFin \o X) -> P.-integrable [set: T] (EFin \o (X ^+ 2)%R) ->*) -bernoulli_RV X -> 'V_P[X] = (p%:num * (`1-(p%:num)))%:E. + bernoulli_RV X -> 'V_P[X] = (p * (`1-p))%:E. +Proof. move=> b. rewrite varianceE; last 2 first. exact: integrable_bernoulli. @@ -792,7 +793,7 @@ Definition bernoulli_trial (X : seq {RV P >-> R}) := (\sum_(Xi <- X) Xi)%R. Lemma expectation_bernoulli_trial n (X : n.-tuple {RV P >-> R}) : - is_bernoulli_trial X -> 'E_P[@bernoulli_trial X] = (n%:R * p%:num)%:E. + is_bernoulli_trial X -> 'E_P[@bernoulli_trial X] = (n%:R * p)%:E. Proof. move=> [bRV [_ Xn]]; rewrite expectation_sum; last first. by move=> Xi XiX; exact: (integrable_bernoulli (bRV _ XiX)). @@ -815,13 +816,13 @@ by rewrite big_seq; apply: sumr_ge0 => i iX; exact/bernoulli_ge0/bRV. Qed. Lemma bernoulli_mmt_gen_fun (X : {RV P >-> R}) (t : R) : - bernoulli_RV X -> 'E_P[expR \o t \o* X] = (p%:num * expR t + (1-p%:num))%:E. + bernoulli_RV X -> 'E_P[expR \o t \o* X] = (p * expR t + (1-p))%:E. Admitted. Lemma binomial_mmt_gen_fun n (X_ : n.-tuple {RV P >-> R}) (t : R) : is_bernoulli_trial X_ -> let X := bernoulli_trial X_ : {RV P >-> R} in - mmt_gen_fun X t = ((p%:num * expR t + (1-p%:num))`^(n%:R))%:E. + mmt_gen_fun X t = ((p * expR t + (1 - p)) `^ n%:R)%:E. Proof. rewrite /is_bernoulli_trial /independent_RV /bernoulli_trial. move=> [bX1 [bX2 bX3]] /=. @@ -840,8 +841,8 @@ End bernoulli_trial. Section rajani. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). -Variable p : {nonneg R}. -Hypothesis p1 : (p%:num <= 1)%R. +Variable p : R. +Hypothesis p01 : (0 <= p <= 1)%R. (* Rajani lem 2.3 *) Lemma lm23 n (X_ : n.-tuple {RV P >-> R}) (t : R) : @@ -855,7 +856,7 @@ rewrite /= => t0 bX. set X := bernoulli_trial X_. set mu := 'E_P[X]. have -> : @mmt_gen_fun _ _ _ P X t = (\prod_(Xi <- X_) fine (mmt_gen_fun Xi t))%:E. - rewrite -[LHS]fineK; last by rewrite (binomial_mmt_gen_fun p1 _ bX). + rewrite -[LHS]fineK; last by rewrite (binomial_mmt_gen_fun p01 _ bX). congr EFin. rewrite /mmt_gen_fun. transitivity (fine 'E_P[expR \o t \o* (\sum_(i < n) tnth X_ i)%R]). @@ -872,30 +873,31 @@ have -> : @mmt_gen_fun _ _ _ P X t = (\prod_(Xi <- X_) fine (mmt_gen_fun Xi t))% admit. admit. under eq_big_seq => Xi XiX. - have -> : @mmt_gen_fun _ _ _ P Xi t = (1 + p%:num * (expR t - 1))%:E. + have -> : @mmt_gen_fun _ _ _ P Xi t = (1 + p * (expR t - 1))%:E. rewrite /mmt_gen_fun. - rewrite (bernoulli_mmt_gen_fun p1)//; last exact: bX.1. + rewrite (bernoulli_mmt_gen_fun p01)//; last exact: bX.1. apply: congr1. by rewrite mulrBr mulr1 addrCA. over. rewrite lee_fin /=. -apply: (le_trans (@ler_prod _ _ _ _ _ - (fun x => expR (p%:num * (expR t - 1)))%R _)). +apply: (le_trans (@ler_prod _ _ _ _ _ (fun x => expR (p * (expR t - 1)))%R _)). move=> Xi _. - rewrite addr_ge0 ?mulr_ge0 ?subr_ge0 ?andTb//; last first. - by rewrite -expR0 ler_expR. - by rewrite expR_ge1Dx ?mulr_ge0// subr_ge0 -expR0 ler_expR. + rewrite addr_ge0//=; last first. + rewrite mulr_ge0//; first by case/andP : p01. + by rewrite subr_ge0 -expR0 ler_expR. + rewrite expR_ge1Dx// mulr_ge0//; first by case/andP : p01. + by rewrite subr_ge0 -expR0 ler_expR. rewrite expR_prod -mulr_suml. move: t0; rewrite le_eqVlt => /predU1P[<-|t0]. by rewrite expR0 subrr !mulr0. rewrite ler_expR ler_pM2r; last first. by rewrite subr_gt0 -expR0 ltr_expR. rewrite /mu big_seq expectation_sum; last first. - move=> Xi XiX; apply: (integrable_bernoulli p1); exact: bX.1. + by move=> Xi XiX; apply: (integrable_bernoulli p01); exact: bX.1. rewrite big_seq -sum_fine. - apply: ler_sum => Xi XiX; rewrite (bernoulli_expectation p1) //=. - exact: bX.1. -by move=> Xi XiX; rewrite (bernoulli_expectation p1) //=; exact: bX.1. + apply: ler_sum => Xi XiX; rewrite (bernoulli_expectation p01) //=. + exact: bX.1. +by move=> Xi XiX; rewrite (bernoulli_expectation p01) //=; exact: bX.1. Admitted. Lemma end_thm24 n (X_ : n.-tuple {RV P >-> R}) (t delta : R) : @@ -1000,22 +1002,25 @@ apply: (@le_trans _ _ - exact: expR_gt0. - rewrite norm_expR. have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun X' t by []. - by rewrite (binomial_mmt_gen_fun p1 _ bX). + by rewrite (binomial_mmt_gen_fun p01 _ bX). apply: (@le_trans _ _ ((expR ((expR t - 1) * fine mu)) / (expR (t * (1 - delta) * fine mu)))%:E). rewrite norm_expR lee_fin ler_wpM2r ?invr_ge0 ?expR_ge0//. have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun X' t by []. - rewrite (binomial_mmt_gen_fun p1 _ bX)/=. - rewrite /mu /X' (expectation_bernoulli_trial p1 bX)/=. + rewrite (binomial_mmt_gen_fun p01 _ bX)/=. + rewrite /mu /X' (expectation_bernoulli_trial p01 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 addr_ge0// ?subr_ge0; last by case/andP : p01. + rewrite mulr_ge0//; first by case/andP : p01. + by rewrite subr_ge0// ltW. rewrite addrAC subrr sub0r -expRM. - rewrite addrCA -{2}(mulr1 (p%:num)) -mulrBr addrAC subrr sub0r mulrC mulNr. + rewrite addrCA -{2}(mulr1 p) -mulrBr addrAC subrr sub0r mulrC mulNr. apply: le01_expR_ge1Dx. - rewrite lerNl opprK mulr_ile1//=; [|exact: ltW..]. - by rewrite lerNl oppr0 mulr_ge0// ltW. + rewrite lerNl opprK mulr_ile1//=; + [|exact: ltW|by case/andP : p01 |exact: ltW|by case/andP : p01]. + by rewrite lerNl oppr0 mulr_ge0//; [exact: ltW|case/andP : p01]. 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//. @@ -1037,7 +1042,7 @@ Qed. Corollary cor27 n (X : n.-tuple {RV P >-> R}) (delta : R) : is_bernoulli_trial p X -> (0 < delta < 1)%R -> (0 < n)%nat -> - (0 < p%:num)%R -> + (p != 0)%R -> let X' := bernoulli_trial X in let mu := 'E_P[X'] in P [set i | `|X' i - fine mu | >= delta * fine mu]%R <= @@ -1068,8 +1073,8 @@ rewrite measureU; last 3 first. apply: (@lt_le_trans _ _ _ _ _ _ X0). rewrite !EFinM. rewrite lte_pmul2r//; first by rewrite lte_fin ltrD2l gt0_cp. - rewrite fineK /mu/X' (expectation_bernoulli_trial p1 bX)// lte_fin. - by rewrite mulr_gt0 ?ltr0n. + rewrite fineK /mu/X' (expectation_bernoulli_trial p01 bX)// lte_fin. + by rewrite mulr_gt0// ?ltr0n// lt_neqAle eq_sym p0; case/andP : p01. rewrite mulr2n EFinD leeD//=. - by apply: (poisson_ineq bX); rewrite //d0 d1. - apply: (le_trans (@thm26 _ _ delta bX _)); first by rewrite d0 d1. @@ -1084,30 +1089,31 @@ Qed. Theorem sampling n (X : n.-tuple {RV P >-> R}) (theta delta : R) : let X_sum := bernoulli_trial X in let X' x := (X_sum x) / n%:R in - (0 < p%:num)%R -> + p != 0%R -> is_bernoulli_trial p X -> - (0 < delta <= 1)%R -> (0 < theta < p%:num)%R -> (0 < n)%nat -> + (0 < delta <= 1)%R -> (0 < theta < p)%R -> (0 < n)%N -> (3 / theta ^+ 2 * ln (2 / delta) <= n%:R)%R -> - P [set i | `| X' i - p%:num | <= theta]%R >= 1 - delta%:E. + 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%:num * n%:R)%:E. +have E_X_sum: 'E_P[X_sum] = (p * n%:R)%:E. rewrite expectation_sum/=; last first. by move=> Xi XiX; exact: integrable_bernoulli (bX.1 Xi XiX). rewrite big_seq. under eq_bigr. - move=> Xi XiX; rewrite (bernoulli_expectation p1 (bX.1 _ XiX)); over. + move=> Xi XiX; rewrite (bernoulli_expectation p01 (bX.1 _ XiX)); over. rewrite /= -[in RHS](size_tuple X). by rewrite -sum1_size natr_sum big_distrr/= sumEFin mulr1 -big_seq. -set epsilon := theta / p%:num. +set epsilon := theta / p. have epsilon01 : (0 < epsilon < 1)%R. - by rewrite /epsilon ?ltr_pdivrMr ?divr_gt0 ?mul1r. -have thetaE : theta = (epsilon * p%:num)%R. + by rewrite /epsilon ?ltr_pdivrMr ?divr_gt0 ?mul1r//; + rewrite lt_neqAle eq_sym p0; case/andP : p01. +have thetaE : theta = (epsilon * p)%R. by rewrite /epsilon -mulrA mulVf ?mulr1// gt_eqF. -have step1 : P [set i | `| X' i - p%:num | >= epsilon * p%:num]%R <= - ((expR (- (p%:num * n%:R * (epsilon ^+ 2)) / 3)) *+ 2)%:E. +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%:num * n%:R | >= epsilon * p%:num * n%:R]%R); last first. + [set i | `| X_sum i - p * n%:R | >= epsilon * p * n%:R]%R); last first. apply/seteqP; split => [t|t]/=. move/(@ler_wpM2r _ n%:R (ler0n _ _)) => /le_trans; apply. rewrite -[X in (_ * X)%R](@ger0_norm _ n%:R)// -normrM mulrBl. @@ -1118,10 +1124,10 @@ have step1 : P [set i | `| X' i - p%:num | >= epsilon * p%:num]%R <= rewrite -[X in (_ * X)%R](@ger0_norm _ n%:R^-1)// -normrM mulrBl. by rewrite -mulrA divff ?mulr1// gt_eqF// ltr0n. rewrite -mulrA. - have -> : (p%:num * n%:R)%R = fine (p%:num * n%:R)%:E by []. + have -> : (p * n%:R)%R = fine (p * n%:R)%:E by []. rewrite -E_X_sum. - by apply: (@cor27 _ X epsilon bX). -have step2 : P [set i | `| X' i - p%:num | >= theta]%R <= + exact: (@cor27 _ 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_wMn2r// ler_expR mulNr lerNl mulNr opprK. @@ -1131,13 +1137,13 @@ have step2 : P [set i | `| X' i - p%:num | >= theta]%R <= rewrite ler_wpM2l//. rewrite (mulrC epsilon) exprMn -mulrA ler_wpM2r//. by rewrite divr_ge0// sqr_ge0. - by rewrite expr2 ler_piMl. -suff : delta%:E >= P [set i | (`|X' i - p%:num| >=(*NB: this >= in the pdf *) theta)%R]. - rewrite [X in P X <= _ -> _](_ : _ = ~` [set i | (`|X' i - p%:num| < theta)%R]); last first. + by rewrite expr2 ler_piMl//; case/andP : p01. +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%:num| < theta)%R]. + 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 => //; From 1ca334bfae9527edd498cc93d776082bf46f1b03 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 7 Jun 2024 23:30:52 +0900 Subject: [PATCH 11/12] thm 2.13(i) --- theories/sampling.v | 41 ++++++++++++++++++++++++++++++++++++----- 1 file changed, 36 insertions(+), 5 deletions(-) diff --git a/theories/sampling.v b/theories/sampling.v index 0454c45af..89fe71457 100644 --- a/theories/sampling.v +++ b/theories/sampling.v @@ -345,16 +345,15 @@ Context {R : realType} d {T : measurableType d}. Variable P : probability T R. Local Open Scope ereal_scope. -(* def 2.3, independence of events *) -(* TODO: rename to mutually_independent_events *) -Definition mutually_independent (I : choiceType) (A : I -> set T) := +(* klenke def 2.3 (independence of events) *) +Definition mutually_independent_events (I : choiceType) (A : I -> set T) := (* (forall i, J i -> measurable (A i)) /\*) forall J : {fset I}, - P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i). + P (\big[setI/setT]_(i <- J) A i) = \prod_(i <- J) P (A i). End independent_events. -(* independent class of events, klenke def 2.11, p.59 *) +(* iklenke def 2.11, p.59 (independence of classed of events) *) Section independent_class. Context {R : realType} d {T : measurableType d}. Variable P : probability T R. @@ -369,6 +368,38 @@ Definition independent_class (I : choiceType) (C : I -> set (set T)) := End independent_class. +Section thm213. +Local Open Scope ereal_scope. +Context {R : realType} d {T : measurableType d}. +Variable P : probability T R. + +Lemma thm213i (I : finType) (C : I -> set (set T)) : + (forall i : I, C i `<=` @measurable _ T /\ [set: T] \in C i) -> + independent_class P C <-> + forall E : I -> set T, + (forall i : I, E i \in C i) -> + P (\big[setI/setT]_(j in I) E j) = \prod_(j in I) P (E j). +Proof. +move=> mCT; split => [PC E EC|]. + move: PC => [_] => /(_ [fset i in I]%fset) /(_ E). + rewrite !big_imfset//= !big_enum; apply => i _. + exact: EC. +move=> h; split=> [i|J E EC]; first by have [] := mCT i. +pose F i := if i \in J then E i else setT. +have {}/h : forall i, F i \in C i. + by move=> i; rewrite /F; case: ifPn => [|iJ]; [exact: EC|by have [] := mCT i]. +rewrite [in X in X = _ -> _](bigID (mem J))/=. +rewrite [X in _ `&` X]big1 ?setIT; last by move=> i iJ; rewrite /F (negbTE iJ). +rewrite [in X in _ = X -> _](bigID (mem J))/=. +rewrite [X in _ * X]big1 ?mule1; last first. + by move=> i iJ; rewrite /F (negbTE iJ) probability_setT. +rewrite (eq_bigr E); last by move=> i iJ; rewrite /F iJ. +rewrite [X in _ = X -> _](eq_bigr (P \o E)); last by move=> i iJ; rewrite /F iJ. +by do 2 rewrite big_uniq/= ?fset_uniq//. +Qed. + +End thm213. + Section independent_RV. Context {R : realType} d (T : measurableType d). Variable P : probability T R. From 85a2a3bd3d7caf5b151d15c02fc5562ae7a9378e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 7 Jun 2024 23:50:44 +0900 Subject: [PATCH 12/12] add idx to the def of inde_class --- theories/sampling.v | 45 ++++++++++++++++++++++++++------------------- 1 file changed, 26 insertions(+), 19 deletions(-) diff --git a/theories/sampling.v b/theories/sampling.v index 89fe71457..be583ee9d 100644 --- a/theories/sampling.v +++ b/theories/sampling.v @@ -359,9 +359,10 @@ Context {R : realType} d {T : measurableType d}. Variable P : probability T R. Local Open Scope ereal_scope. -Definition independent_class (I : choiceType) (C : I -> set (set T)) := - (forall i, C i `<=` @measurable _ T) /\ +Definition independent_class (I : choiceType) (D : set I) (C : I -> set (set T)) := + (forall i, D i -> C i `<=` @measurable _ T) /\ forall J : {fset I}, + [set` J] `<=` D -> forall E : I -> set T, (forall i : I, i \in J -> E i \in C i) -> P (\big[setI/setT]_(j <- J) E j) = \prod_(j <- J) P (E j). @@ -373,21 +374,23 @@ Local Open Scope ereal_scope. Context {R : realType} d {T : measurableType d}. Variable P : probability T R. -Lemma thm213i (I : finType) (C : I -> set (set T)) : - (forall i : I, C i `<=` @measurable _ T /\ [set: T] \in C i) -> - independent_class P C <-> +Lemma thm213i (I : choiceType) (D : {fset I}) (C : I -> set (set T)) : + (forall i : I, i \in D -> C i `<=` @measurable _ T /\ [set: T] \in C i) -> + independent_class P [set` D] C <-> forall E : I -> set T, - (forall i : I, E i \in C i) -> - P (\big[setI/setT]_(j in I) E j) = \prod_(j in I) P (E j). + (forall i : I, i \in D -> E i \in C i) -> + P (\big[setI/setT]_(j <- D) E j) = \prod_(j <- D) P (E j). Proof. move=> mCT; split => [PC E EC|]. - move: PC => [_] => /(_ [fset i in I]%fset) /(_ E). - rewrite !big_imfset//= !big_enum; apply => i _. - exact: EC. -move=> h; split=> [i|J E EC]; first by have [] := mCT i. + move: PC => [_]. + move=> /(_ D). + move=> /(_ (@subset_refl _ _)). + by move=> /(_ E EC). +move=> h; split=> [i Di|J JD E EC]. + by have [] := mCT i Di. pose F i := if i \in J then E i else setT. -have {}/h : forall i, F i \in C i. - by move=> i; rewrite /F; case: ifPn => [|iJ]; [exact: EC|by have [] := mCT i]. +have {}/h : forall i, i \in D -> F i \in C i. + by move=> i iD; rewrite /F; case: ifPn => [|iJ]; [exact: EC|have [] := mCT i iD]. rewrite [in X in X = _ -> _](bigID (mem J))/=. rewrite [X in _ `&` X]big1 ?setIT; last by move=> i iJ; rewrite /F (negbTE iJ). rewrite [in X in _ = X -> _](bigID (mem J))/=. @@ -395,7 +398,11 @@ rewrite [X in _ * X]big1 ?mule1; last first. by move=> i iJ; rewrite /F (negbTE iJ) probability_setT. rewrite (eq_bigr E); last by move=> i iJ; rewrite /F iJ. rewrite [X in _ = X -> _](eq_bigr (P \o E)); last by move=> i iJ; rewrite /F iJ. -by do 2 rewrite big_uniq/= ?fset_uniq//. +rewrite big_fset_condE/=. +have DJJ : [fset i | i in D & i \in J]%fset = J. + by apply/fsetP => i; rewrite !inE/= andb_idl// => /JD. +rewrite DJJ => ->. +by rewrite big_fset_condE/= DJJ. Qed. End thm213. @@ -408,10 +415,10 @@ Definition generated_salgebra (X : {RV P >-> R}) : set (set T) := preimage_class setT X (@measurable _ R). Definition independent_RV (I : choiceType) (X : I -> {RV P >-> R}) := - independent_class P (fun i : I => generated_salgebra (X i)). + independent_class P setT (fun i : I => generated_salgebra (X i)). Definition independent_RV_tuple n (X : n.-tuple {RV P >-> R}) := - independent_class P (fun i => generated_salgebra (X `_ i)). + independent_class P setT (fun i => generated_salgebra (X `_ i)). Lemma independent_RV_tuple_thead_prod_behead n (X : n.+1.-tuple {RV P >-> R}) : independent_RV_tuple X -> @@ -449,12 +456,12 @@ move: X; case: n => [X|n X]. rewrite /independent_RV_tuple/independent_class/=. move=> [iXm iX]. split; first by move=> i; rewrite nth_behead; exact: iXm. -move=> J E h. +move=> J _ E h. pose E' n := match n with 0 => setT | S m => E m end. -have := (@iX (0 |` [fset i.+1 | i in J])%fset E'). +have := (@iX (0 |` [fset i.+1 | i in J])%fset (@subsetT _ _) E'). have ? : 0 \notin [fset i.+1 | i in J]%fset. apply/negP. move/imfsetP. @@ -507,7 +514,7 @@ have : forall i : nat, i \in O1 -> move=> [|[|?]]; rewrite /O1 ?inE//= => _. + by rewrite /generated_salgebra; exact: preimage_class_mindic. + by rewrite /generated_salgebra; exact: preimage_class_mindic. -move/AB.2. +move/AB.2 => /(_ (@subsetT _ _)). by rewrite /O1 !big_fsetU1/= ?inE// !big_seq_fset1/=. Qed.