Skip to content

Commit

Permalink
renamings
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Dec 3, 2024
1 parent 9c18d41 commit f947149
Showing 1 changed file with 43 additions and 35 deletions.
78 changes: 43 additions & 35 deletions theories/probability.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -263,7 +263,7 @@ by apply: (@subset_trans _ [set` Interval x z]);
[exact: subset_itvr | exact: subset_itvl].
Qed.

Lemma gtr0_derive1_homo (R : realType) (f : R -> R) (a b : R) (sa sb : bool) :
Lemma gtr0_derive1_homo (R : realType) (f : R^o -> R^o) (a b : R) (sa sb : bool) :
(forall x : R, x \in `]a, b[ -> derivable f x 1) ->
(forall x : R, x \in `]a, b[ -> 0 < 'D_1 f x) ->
{within [set` (Interval (BSide sa a) (BSide sb b))], continuous f} ->
Expand All @@ -277,15 +277,15 @@ have zab z : z \in `]x, y[ -> z \in `]a, b[.
apply: subset_itvW_bound.
by move: ax; clear; case: sa; rewrite !bnd_simp// => /ltW.
by move: yb; clear; case: sb; rewrite !bnd_simp// => /ltW.
have HMVT0 z : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
have HMVT0 (z : R^o) : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
by move=> zxy; exact/derivableP/df/zab.
rewrite -subr_gt0.
have[z zxy ->]:= MVT xy HMVT0 HMVT1.
rewrite mulr_gt0// ?subr_gt0// dfgt0//.
exact: zab.
Qed.

Lemma ger0_derive1_homo (R : realType) (f : R -> R) (a b : R) (sa sb : bool) :
Lemma ger0_derive1_homo (R : realType) (f : R^o -> R^o) (a b : R) (sa sb : bool) :
(forall x : R, x \in `]a, b[ -> derivable f x 1) ->
(forall x : R, x \in `]a, b[ -> 0 <= 'D_1 f x) ->
{within [set` (Interval (BSide sa a) (BSide sb b))], continuous f} ->
Expand All @@ -299,7 +299,7 @@ have zab z : z \in `]x, y[ -> z \in `]a, b[.
apply: subset_itvW_bound.
by move: ax; clear; case: sa; rewrite !bnd_simp// => /ltW.
by move: yb; clear; case: sb; rewrite !bnd_simp// => /ltW.
have HMVT0 z : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
have HMVT0 (z : R^o) : z \in `]x, y[ -> is_derive z 1 f ('D_1 f z).
by move=> zxy; exact/derivableP/df/zab.
rewrite -subr_ge0.
move: (xy); rewrite le_eqVlt=> /orP [/eqP-> | xy']; first by rewrite subrr.
Expand All @@ -311,6 +311,7 @@ Qed.
Lemma memB_itv (R : numDomainType) (b0 b1 : bool) (x y z : R) :
(y - z \in Interval (BSide b0 x) (BSide b1 y)) =
(x + z \in Interval (BSide (~~ b1) x) (BSide (~~ b0) y)).
Proof.
rewrite !in_itv /= /Order.lteif !if_neg.
by rewrite gerBl gtrBl lerDl ltrDl lerBrDr ltrBrDr andbC.
Qed.
Expand Down Expand Up @@ -961,7 +962,7 @@ move=> AX B BA.
rewrite [in LHS]unlock.
rewrite /mutually_independent_RV in AX.
rewrite /mutually_independent in AX.
Admitted.
Abort.

End independent_RVs.

Expand Down Expand Up @@ -1299,6 +1300,8 @@ HB.instance Definition _ (f : {mfun aT >-> rT}) :=

End mfun_measurable_realType.

Reserved Notation "'M_ X t" (format "''M_' X t", at level 5, t, X at next level).

Section markov_chebyshev_cantelli.
Local Open Scope ereal_scope.
Context d (T : measurableType d) (R : realType) (P : probability T R).
Expand All @@ -1322,10 +1325,13 @@ apply: (le_trans (@le_integral_comp_abse _ _ _ P _ measurableT (EFin \o X)
Qed.

Definition mmt_gen_fun (X : {RV P >-> R}) (t : R) := 'E_P[expR \o t \o* X].

Local Notation "'M_ X t" := (mmt_gen_fun X t).

Definition nth_mmt (X : {RV P >-> R}) (n : nat) := 'E_P[X^+n].

Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R ->
P [set x | X x >= a]%R <= mmt_gen_fun X r * (expR (- (r * a)))%:E.
P [set x | X x >= a]%R <= 'M_X r * (expR (- (r * a)))%:E.
Proof.
move=> t0.
rewrite /mmt_gen_fun; have -> : expR \o r \o* X =
Expand Down Expand Up @@ -1454,6 +1460,8 @@ Qed.

End markov_chebyshev_cantelli.

Notation "'M_ X t" := (mmt_gen_fun X t) : ereal_scope.

HB.mixin Record MeasurableFun_isDiscrete d d' (T : measurableType d) (U : measurableType d')
(X : T -> U) of @MeasurableFun d _ T U X := {
countable_range : countable (range X)
Expand Down Expand Up @@ -1658,7 +1666,7 @@ move=> iX; rewrite dRV_expectation// [in RHS]eseries_mkcond.
apply: eq_eseriesr => k _.
rewrite /enum_prob patchE; case: ifPn => kX; last by rewrite mul0e.
by rewrite /pmf fineK// fin_num_measure.
Qed.
Abort.

End discrete_distribution.

Expand Down Expand Up @@ -3101,17 +3109,19 @@ Qed.
Lemma independent_mmt_gen_fun (X : {dRV P >-> bool}^nat) n t :
let mmtX (i : nat) : {RV P >-> R} := expR \o t \o* (btr P (X i)) in
independent_RVs P `I_n X -> independent_RVs P `I_n mmtX.
Proof.
Admitted. (* from Reynald's PR, independent_RVs2_comp, "when applying a function, the sigma algebra only gets smaller" *)

Lemma expectation_prod_independent_RVs (X : {RV P >-> R}^nat) n :
independent_RVs P `I_n X ->
'E_P[\prod_(i < n) (X i)] = \prod_(i < n) 'E_P[X i].
Proof.
Admitted.

Lemma bernoulli_trial_mmt_gen_fun (X_ : {dRV P >-> bool}^nat) n (t : R) :
is_bernoulli_trial n X_ ->
let X := bernoulli_trial n X_ in
mmt_gen_fun X t = \prod_(i < n) mmt_gen_fun (btr P (X_ i)) t.
'M_X t = \prod_(i < n) 'M_(btr P (X_ i)) t.
Proof.
move=> []bRVX iRVX /=.
rewrite /bernoulli_trial/mmt_gen_fun.
Expand All @@ -3130,7 +3140,7 @@ Arguments sub_countable [T U].
Arguments card_le_finite [T U].

Lemma bernoulli_mmt_gen_fun (X : {dRV P >-> bool}) (t : R) :
bernoulli_RV X -> mmt_gen_fun (btr P X : {RV P >-> R}) t = (p * expR t + (1-p))%:E.
bernoulli_RV X -> 'M_(btr P X : {RV P >-> R}) t = (p * expR t + (1-p))%:E.
Proof.
move=> bX. rewrite/mmt_gen_fun.
pose mmtX : {RV P >-> R} := expR \o t \o* (btr P X).
Expand Down Expand Up @@ -3170,7 +3180,7 @@ Proof. by elim: n => [|n ih]; rewrite ?mul1e// [LHS]/= ih expeS muleA. Qed.
Lemma binomial_mmt_gen_fun (X_ : {dRV P >-> bool}^nat) n (t : R) :
is_bernoulli_trial n X_ ->
let X := bernoulli_trial n X_ : {RV P >-> R} in
mmt_gen_fun X t = ((p * expR t + (1-p))`^(n%:R))%:E.
'M_X t = ((p * expR t + (1-p))`^(n%:R))%:E.
Proof.
move: p01 => /andP[p0 p1] bX/=.
rewrite bernoulli_trial_mmt_gen_fun//.
Expand All @@ -3181,6 +3191,7 @@ rewrite big_const iter_mule mule1 cardT size_enum_ord -EFin_expe powR_mulrn//.
by rewrite addr_ge0// ?subr_ge0// mulr_ge0// expR_ge0.
Qed.

(* TODO: add to the PR by reynald that adds the \prod notation to master *)
Lemma prod_EFin U l Q (f : U -> R) : \prod_(i <- l | Q i) ((f i)%:E) = (\prod_(i <- l | Q i) f i)%:E.
Proof.
elim: l; first by rewrite !big_nil.
Expand All @@ -3190,11 +3201,11 @@ case: ifP => //= aQ.
by rewrite EFinM ih.
Qed.

Lemma lm23 (X_ : {dRV P >-> bool}^nat) (t : R) n :
Lemma mmt_gen_fun_expectation (X_ : {dRV P >-> bool}^nat) (t : R) n :
(0 <= t)%R ->
is_bernoulli_trial n X_ ->
let X := bernoulli_trial n X_ : {RV P >-> R} in
mmt_gen_fun X t <= (expR (fine 'E_P[X] * (expR t - 1)))%:E.
'M_X t <= (expR (fine 'E_P[X] * (expR t - 1)))%:E.
Proof.
move=> t0 bX/=.
have /andP[p0 p1] := p01.
Expand All @@ -3206,9 +3217,6 @@ rewrite -mulrA (mulrC (n%:R)) expRM ge0_ler_powR// ?nnegrE ?expR_ge0//.
exact: expR_ge1Dx.
Qed.

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_ : {dRV P >-> bool}^nat) n (t delta : R) :
is_bernoulli_trial n X_ ->
(0 < delta)%R ->
Expand All @@ -3225,11 +3233,11 @@ rewrite -EFinM lee_fin -powRM ?expR_ge0// ge0_ler_powR ?nnegrE//.
- 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.
by rewrite -powRN mulNr -mulrN expRM lnK// posrE addr_gt0.
Qed.

(* theorem 2.4 Rajani / thm 4.4.(2) mu-book *)
Theorem thm24 (X_ : {dRV P >-> bool}^nat) n (delta : R) :
Theorem bernoulli_trial_inequality1 (X_ : {dRV P >-> bool}^nat) n (delta : R) :
is_bernoulli_trial n X_ ->
(0 < delta)%R ->
let X := @bernoulli_trial n X_ in
Expand All @@ -3246,13 +3254,13 @@ 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.
by apply: (mmt_gen_fun_expectation _ bX); rewrite le_eqVlt t0 orbT.
rewrite mulrC expRM -mulNr mulrA expRM.
exact: (end_thm24 _ bX).
Qed.

(* theorem 2.5 *)
Theorem poisson_ineq (X : {dRV P >-> bool}^nat) (delta : R) n :
Theorem bernoulli_trial_inequality2 (X : {dRV P >-> bool}^nat) (delta : R) n :
is_bernoulli_trial n X ->
let X' := @bernoulli_trial n X in
let mu := 'E_P[X'] in
Expand All @@ -3263,8 +3271,8 @@ Theorem poisson_ineq (X : {dRV P >-> bool}^nat) (delta : R) n :
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) => //.
rewrite expRM expRB (mulrC _ (ln _)) expRM lnK; last rewrite posrE addr_gt0//.
apply: (bernoulli_trial_inequality1 bX) => //.
apply: (@le_trans _ _ (expR ((delta - (delta + delta ^+ 2 / 3)) * fine mu))%:E).
rewrite lee_fin ler_expR ler_wpmul2r//.
by rewrite fine_ge0//; apply: expectation_ge0 => t; exact: (bernoulli_trial_ge0 bX).
Expand All @@ -3284,7 +3292,7 @@ Lemma norm_expR : normr \o expR = (expR : R -> R).
Proof. by apply/funext => x /=; rewrite ger0_norm ?expR_ge0. Qed.

(* Rajani thm 2.6 / mu-book thm 4.5.(2) *)
Theorem thm26 (X : {dRV P >-> bool}^nat) (delta : R) n :
Theorem bernoulli_trial_inequality3 (X : {dRV P >-> bool}^nat) (delta : R) n :
is_bernoulli_trial n X -> (0 < delta < 1)%R ->
let X' := @bernoulli_trial n X : {RV P >-> R} in
let mu := 'E_P[X'] in
Expand Down Expand Up @@ -3312,26 +3320,26 @@ apply: (@le_trans _ _ (((expR (- delta) / ((1 - delta) `^ (1 - delta))) `^ (fine
apply: (@markov _ _ _ P (expR \o t \o* X' : {RV P >-> R}) id (expR (t * (1 - delta) * fine mu))%R _ _ _ _) => //.
- apply: expR_gt0.
- rewrite norm_expR.
have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun X' t by [].
have -> : 'E_P[expR \o t \o* X'] = 'M_X' t by [].
by rewrite (binomial_mmt_gen_fun _ bX).
apply: (@le_trans _ _ (((expR ((expR t - 1) * fine mu)) / (expR (t * (1 - delta) * fine mu))))%:E).
rewrite norm_expR lee_fin ler_wpmul2r ?invr_ge0 ?expR_ge0//.
have -> : 'E_P[expR \o t \o* X'] = mmt_gen_fun X' t by [].
have -> : 'E_P[expR \o t \o* X'] = 'M_X' t by [].
rewrite (binomial_mmt_gen_fun _ bX)/=.
rewrite /mu /X' (expectation_bernoulli_trial bX)/=.
rewrite !lnK ?posrE ?subr_gt0//.
rewrite expR_powR powRrM powRAC.
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 -expR_powR.
rewrite addrAC subrr sub0r -expRM.
rewrite addrCA -{2}(mulr1 p) -mulrBr addrAC subrr sub0r mulrC mulNr.
by apply: expR_ge1Dx.
rewrite !lnK ?posrE ?subr_gt0//.
rewrite -addrAC subrr sub0r -mulrA [X in (_ / X)%R]expR_powR 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 expR_powR.
by rewrite powRAC powR_inv1 ?powR_ge0// powRrM expRM.
rewrite lee_fin.
rewrite -mulrN -mulrA [in leRHS]mulrC expR_powR ge0_ler_powR// ?nnegrE.
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.
Expand All @@ -3349,7 +3357,7 @@ rewrite -mulrN -mulrA [in leRHS]mulrC expR_powR ge0_ler_powR// ?nnegrE.
by rewrite -(mulr_natr (- delta) 2) mulNr.
rewrite addrAC subr_le0.
set f := fun (x : R) => x ^+ 2 + - (x * ln x) * 2.
have @idf (x : R) : 0 < x -> {df | is_derive x 1 f df}.
have @idf (x : R^o) : 0 < x -> {df | is_derive x 1 (f : R^o -> R^o) df}.
move=> x0; evar (df : (R : Type)); exists df.
apply: is_deriveD; first by [].
apply: is_deriveM; last by [].
Expand Down Expand Up @@ -3390,7 +3398,7 @@ apply: emeasurable_fun_le => //; apply: measurableT_comp => //.
Qed.

(* Rajani -> corollary 2.7 / mu-book -> corollary 4.7 *)
Corollary cor27 (X : {dRV P >-> bool}^nat) (delta : R) n :
Corollary bernoulli_trial_inequality4 (X : {dRV P >-> bool}^nat) (delta : R) n :
is_bernoulli_trial n X -> (0 < delta < 1)%R ->
(0 < n)%nat ->
(0 < p)%R ->
Expand Down Expand Up @@ -3426,8 +3434,8 @@ rewrite measureU; last 3 first.
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.
- by apply: (bernoulli_trial_inequality2 bX); rewrite //d0 d1.
- apply: (le_trans (@bernoulli_trial_inequality3 _ delta _ bX _)); first by rewrite d0 d1.
rewrite lee_fin ler_expR !mulNr ler_opp2.
rewrite ler_pmul//; last by rewrite lef_pinv ?posrE ?ler_nat.
rewrite mulr_ge0 ?fine_ge0 ?sqr_ge0//.
Expand Down Expand Up @@ -3470,7 +3478,7 @@ have step1 : P [set i | `| X' i - p | >= epsilon * p]%R <=
rewrite -mulrA.
have -> : (p * n%:R)%R = fine (p * n%:R)%:E by [].
rewrite -E_X_sum.
by apply: (@cor27 X epsilon _ bX).
by apply: (@bernoulli_trial_inequality4 X epsilon _ bX).
have step2 : P [set i | `| X' i - p | >= theta]%R <=
((expR (- (n%:R * theta ^+ 2) / 3)) *+ 2)%:E.
rewrite thetaE; move/le_trans : step1; apply.
Expand Down

0 comments on commit f947149

Please sign in to comment.