From aac3fa2ce470fa4c73924d120591c150e4adc290 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 8 May 2024 23:14:10 +0900 Subject: [PATCH] cleaning --- theories/lang_syntax.v | 23 ++-- theories/lang_syntax_examples.v | 8 +- theories/lang_syntax_table_game.v | 38 +++---- theories/prob_lang.v | 181 +++++++++++++----------------- 4 files changed, 105 insertions(+), 145 deletions(-) diff --git a/theories/lang_syntax.v b/theories/lang_syntax.v index 110fe48c60..432d41797f 100644 --- a/theories/lang_syntax.v +++ b/theories/lang_syntax.v @@ -696,21 +696,20 @@ move=> /andP[x0 x1]; rewrite ler_norml; apply/andP; split. by rewrite lerBlDr lerDl. Qed. -Lemma beta_nat_bernE a' b' U : (a > 0)%N -> (b > 0)%N -> +Lemma beta_nat_bernoulliE a' b' U : (a > 0)%N -> (b > 0)%N -> beta_nat_bernoulli a' b' U = bernoulli (div_beta_nat_norm a' b') U. Proof. move=> a0 b0. rewrite /beta_nat_bernoulli. under eq_integral => x. rewrite inE/= in_itv/= => x01. - rewrite bernoulliE_ext/= ?ubeta_nat_pdf_ge0 ?ubeta_nat_pdf_le1//. + rewrite bernoulliE/= ?ubeta_nat_pdf_ge0 ?ubeta_nat_pdf_le1//. over. rewrite /=. -rewrite [in RHS]bernoulliE_ext/= ?div_beta_nat_norm_ge0 ?div_beta_nat_norm_le1//=. +rewrite [in RHS]bernoulliE/= ?div_beta_nat_norm_ge0 ?div_beta_nat_norm_le1//=. under eq_integral => x x01. - rewrite /ubeta_nat_pdf. rewrite inE /=in_itv/= in x01. - rewrite x01. + rewrite /ubeta_nat_pdf x01. over. rewrite /=. rewrite integralD//=; last 2 first. @@ -785,7 +784,8 @@ rewrite integralZl//=; last first. by rewrite mulr_ile1// ?exprn_ge0 ?exprn_ile1// ?onem_ge0 ?onem_le1//; case/andP: t01. - exact: integrableS (integrable_ubeta_nat_pdf _ _). transitivity (((beta_nat_norm a b)^-1)%:E * - \int[mu]_(x in `[0%R, 1%R]) ((ubeta_nat_pdf a b x)%:E - (ubeta_nat_pdf (a+a') (b+b') x)%:E) : \bar R)%E. + \int[mu]_(x in `[0%R, 1%R]) ((ubeta_nat_pdf a b x)%:E - + (ubeta_nat_pdf (a + a') (b + b') x)%:E) : \bar R)%E. congr (_ * _)%E. apply: eq_integral => x x01. rewrite /onem -EFinM mulrBl mul1r EFinB. @@ -1280,7 +1280,7 @@ Inductive evalD : forall g t, exp D g t -> | eval_binomial g n e r mr : e -D> r ; mr -> (exp_binomial n e : exp D g _) -D> binomial_prob n \o r ; - measurableT_comp (measurable_binomial_probT n) mr + measurableT_comp (measurable_binomial_prob n) mr | eval_uniform g (a b : R) (ab : (a < b)%R) : (exp_uniform a b ab : exp D g _) -D> cst (uniform_prob ab) ; @@ -1858,7 +1858,7 @@ Proof. exact/execD_evalD/eval_bernoulli/evalD_execD. Qed. Lemma execD_binomial g n e : @execD g _ (exp_binomial n e) = existT _ ((binomial_prob n : R -> pprobability nat R) \o projT1 (execD e)) - (measurableT_comp (measurable_binomial_probT n) (projT2 (execD e))). + (measurableT_comp (measurable_binomial_prob n) (projT2 (execD e))). Proof. exact/execD_evalD/eval_binomial/evalD_execD. Qed. Lemma execD_uniform g a b ab0 : @@ -1926,10 +1926,13 @@ Lemma congr_letinl {R : realType} g t1 t2 str (e1 e2 : @exp _ _ g t1) @execP R g t2 [let str := e2 in e] x U. Proof. by move=> + mU; move/eq_sfkernel => He; rewrite !execP_letin He. Qed. -Lemma congr_letinr {R : realType} g t1 t2 str (e : @exp _ _ _ t1) (e1 e2 : @exp _ _ (_ :: g) t2) x U : +Lemma congr_letinr {R : realType} g t1 t2 str (e : @exp _ _ _ t1) + (e1 e2 : @exp _ _ (_ :: g) t2) x U : (forall y V, execP e1 (y, x) V = execP e2 (y, x) V) -> @execP R g t2 [let str := e in e1] x U = @execP R g t2 [let str := e in e2] x U. -Proof. by move=> He; rewrite !execP_letin !letin'E; apply: eq_integral => ? _; exact: He. Qed. +Proof. +by move=> He; rewrite !execP_letin !letin'E; apply: eq_integral => ? _; exact: He. +Qed. Lemma congr_normalize {R : realType} g t (e1 e2 : @exp R _ g t) : (forall x U, execP e1 x U = execP e2 x U) -> diff --git a/theories/lang_syntax_examples.v b/theories/lang_syntax_examples.v index 1dd864a7e1..d4944f704a 100644 --- a/theories/lang_syntax_examples.v +++ b/theories/lang_syntax_examples.v @@ -277,7 +277,7 @@ rewrite ger0_norm//. rewrite !integral_dirac//= !diracT !mul1e ger0_norm//. rewrite exp_var'E (execD_var_erefl "x")/=. rewrite !indicT/= !mulr1. -rewrite bernoulliE_ext//=; last lra. +rewrite bernoulliE//=; last lra. by rewrite muleDl//; congr (_ + _)%E; rewrite -!EFinM; congr (_%:E); rewrite !indicE /onem /=; case: (_ \in _); field. @@ -317,7 +317,7 @@ rewrite !ge0_integral_mscale//=. rewrite ger0_norm//. rewrite !integral_dirac//= !diracT !mul1e ger0_norm//. rewrite exp_var'E (execD_var_erefl "x")/=. -rewrite bernoulliE_ext//=; last lra. +rewrite bernoulliE//=; last lra. rewrite !mul1r. rewrite muleDl//; congr (_ + _)%E; rewrite -!EFinM; @@ -361,7 +361,7 @@ rewrite !letin'E/= !iteE/=. rewrite !ge0_integral_mscale//=. rewrite ger0_norm//. rewrite !integral_dirac//= !diracT !mul1e ger0_norm//. -rewrite bernoulliE_ext//=; last lra. +rewrite bernoulliE//=; last lra. rewrite muleDl//; congr (_ + _)%E; rewrite -!EFinM; congr (_%:E); @@ -648,7 +648,7 @@ transitivity (beta_nat_bernoulli 6 4 1 0 U : \bar R). by rewrite expr0 expr1 mulr1. rewrite !mul0r !mule0. by case: ifPn. -rewrite beta_nat_bernE// !bernoulliE_ext//=; last 2 first. +rewrite beta_nat_bernoulliE// !bernoulliE//=; last 2 first. lra. by rewrite div_beta_nat_norm_ge0 div_beta_nat_norm_le1. congr (_ * _ + _ * _)%:E. diff --git a/theories/lang_syntax_table_game.v b/theories/lang_syntax_table_game.v index b40a114fb7..255c1ee897 100644 --- a/theories/lang_syntax_table_game.v +++ b/theories/lang_syntax_table_game.v @@ -9,7 +9,7 @@ Require Import prob_lang lang_syntax_util lang_syntax lang_syntax_examples. From mathcomp Require Import ring lra. (**md**************************************************************************) -(* # Edd's table game example *) +(* # Eddy's table game example *) (* *) (* ref: *) (* - Chung-chieh Shan, Equational reasoning for probabilistic programming, *) @@ -276,7 +276,7 @@ rewrite (@execD_bin _ _ binop_minus) !execD_real/= !execD_nat. rewrite !exp_var'E !(execD_var_erefl "p") !(execD_var_erefl "a2")/=. rewrite !letin'E/=. move: r01 => /andP[r0 r1]. -by apply/integral_binomial_bernoulli/andP. +by apply/integral_binomial_prob/andP. Qed. Lemma casino12 : execD casino1 = execD casino2. @@ -443,7 +443,7 @@ transitivity (\int[beta_nat 6 4]_(y in `[0%R, 1%R]%classic : set R) rewrite patchE; case: ifPn => //. rewrite /beta_nat_pdf /ubeta_nat_pdf notin_setE/= in_itv/= => /negP/negbTE ->. by rewrite mul0r mule0. -have := (@beta_nat_bernE R 6 4 0 3 U) isT isT. +have := (@beta_nat_bernoulliE R 6 4 0 3 U) isT isT. rewrite /beta_nat_bernoulli /ubeta_nat_pdf /=. under eq_integral. move=> x. @@ -468,7 +468,7 @@ have f1 x : x \in (`[0%R, 1%R]%classic : set R) -> (f x <= 1)%R. by move => /f01/andP[]. under eq_integral => x. move=> x01. - rewrite bernoulliE_ext//=; last first. + rewrite bernoulliE//=; last first. by rewrite subr_ge0 f1//= lerBlDr addrC -lerBlDr subrr f0. over. rewrite /=. @@ -501,8 +501,7 @@ rewrite [X in _ + X = _]ge0_integralZr//=; last 2 first. by apply/EFin_measurable_fun; exact: measurable_beta_nat_pdf. by move=> x x01; rewrite mule_ge0// lee_fin// ?f0// ?inE// beta_nat_pdf_ge0. under [in RHS]eq_integral => x x01. - rewrite bernoulliE_ext//=; last first. - by rewrite f0//= f1. + rewrite bernoulliE//=; last by rewrite f0//= f1. rewrite muleDl//. over. rewrite /= ge0_integralD//=; last 4 first. @@ -653,7 +652,7 @@ rewrite (@execD_bin _ _ binop_minus) execD_pow/= (@execD_bin _ _ binop_minus). rewrite !execD_real/= exp_var'E (execD_var_erefl "p")/=. transitivity (\int[beta_nat 6 4]_y bernoulli (1 - (1 - y) ^+ 3) U : \bar R)%E. by rewrite /beta_nat_bernoulli !letin'E/= /onem. -rewrite bernoulliE_ext//=; last lra. +rewrite bernoulliE//=; last lra. rewrite integral_beta_nat//; last first. by have := @integral_beta_bernoulli_onem_lty R _ _ _ U. apply: (measurableT_comp (measurable_bernoulli2 _)) => //. @@ -678,15 +677,9 @@ rewrite (@integral_bernoulli_beta_nat_pdf (fun x => (1 - x) ^+ 3)%R U (1 / 11))/ rewrite [RHS]integral_beta_nat//; last 2 first. apply: (measurableT_comp (measurable_bernoulli2 _)) => //. apply: measurable_fun_if => //. - apply: measurable_and => //. - apply: (measurable_fun_bool true) => //=. - rewrite (_ : _ @^-1` _ = `[0%R, +oo[%classic)//. - by apply/seteqP; split => [z|z] /=; rewrite in_itv/= andbT. - apply: (measurable_fun_bool true) => //=. - by rewrite (_ : _ @^-1` _ = `]-oo, 1%R]%classic). + by apply: measurable_and => //; exact: measurable_fun_ler. apply: measurable_funTS; apply: measurable_funM => //. - apply: measurable_fun_pow => //. - by apply: measurable_funB => //. + by apply: measurable_fun_pow => //; exact: measurable_funB. rewrite (le_lt_trans _ (integral_beta_bernoulli_expn_lty 3 6 4 U))//. rewrite integral_mkcond /=; apply: ge0_le_integral => //=. by move=> z _; rewrite patchE expr0 mul1r; case: ifPn. @@ -694,12 +687,7 @@ rewrite (@integral_bernoulli_beta_nat_pdf (fun x => (1 - x) ^+ 3)%R U (1 / 11))/ apply: measurable_funTS; apply: measurableT_comp => //=. apply: (measurableT_comp (measurable_bernoulli2 _)) => //=. apply: measurable_fun_if => //=. - apply: measurable_and => //. - apply: (measurable_fun_bool true) => //=. - rewrite (_ : _ @^-1` _ = `[0%R, +oo[%classic)//. - by apply/seteqP; split => [z|z] /=; rewrite in_itv/= andbT. - apply: (measurable_fun_bool true) => //=. - by rewrite (_ : _ @^-1` _ = `]-oo, 1%R]%classic). + by apply: measurable_and => //; exact: measurable_fun_ler. apply: measurable_funTS; apply: measurable_funM => //. by apply: measurable_fun_pow => //; exact: measurable_funB. by apply/measurableT_comp => //; exact: measurable_bernoulli_expn. @@ -709,7 +697,7 @@ rewrite (@integral_bernoulli_beta_nat_pdf (fun x => (1 - x) ^+ 3)%R U (1 / 11))/ apply: eq_integral => z z01. rewrite inE/= in_itv/= in z01. by rewrite z01 expr0 mul1r. - rewrite beta_nat_bernE//= bernoulliE_ext//=; last first. + rewrite beta_nat_bernoulliE//= bernoulliE//=; last first. by rewrite div_beta_nat_norm_ge0// div_beta_nat_norm_le1. rewrite probability_setT. by congr (_ * _ + _ * _)%:E; rewrite /onem; @@ -730,12 +718,12 @@ rewrite !execP_sample !execD_bernoulli !execD_real/=. apply: funext=> x. apply: eq_probability=> /= y. rewrite !normalizeE/=. -rewrite !bernoulliE_ext//=; [|lra..]. +rewrite !bernoulliE//=; [|lra..]. rewrite !diracT !mule1 -EFinD add_onemK onee_eq0/=. rewrite !letin'E. under eq_integral. move=> x0 _ /=. - rewrite !bernoulliE_ext//=; [|lra..]. + rewrite !bernoulliE//=; [|lra..]. rewrite !diracT !mule1 -EFinD add_onemK. over. rewrite !ge0_integral_mscale//= (ger0_norm (ltW p0))//. @@ -743,7 +731,7 @@ rewrite integral_dirac// !diracT !indicT /= !mule1. rewrite gt_eqF ?lte_fin//=. rewrite integral_dirac//= diracT !mul1e !mulr1. rewrite addrCA subrr addr0 invr1 mule1. -rewrite !bernoulliE_ext//=; [|lra..]. +rewrite !bernoulliE//=; [|lra..]. by rewrite muleAC -EFinM divff// ?gt_eqF// mul1r EFinD. Qed. diff --git a/theories/prob_lang.v b/theories/prob_lang.v index 60a2e48484..14daaaea05 100644 --- a/theories/prob_lang.v +++ b/theories/prob_lang.v @@ -18,13 +18,15 @@ From mathcomp Require Import ring lra. (* ``` *) (* bernoulli_pmf p == Bernoulli pmf *) (* bernoulli p == Bernoulli probability measure when 0 <= p <= 1 *) +(* and \d_false otherwise *) (* binomial_pmf n p == binomial pmf *) (* binomial_prob n p == binomial probability measure when 0 <= p <= 1 *) +(* and \d_0%N otherwise *) (* bin_prob n k p == $\binom{n}{k}p^k (1-p)^(n-k)$ *) (* Computes a binomial distribution term for *) (* k successes in n trials with success rate p *) (* uniform_pdf a b == uniform pdf *) -(* uniform_prob a b ab0 == uniform probability over the interval [a,b] *) +(* uniform_prob a b ab == uniform probability over the interval [a,b] *) (* with ab0 a proof that 0 < b - a *) (* poisson_pdf == Poisson pdf *) (* exponential_pdf == exponential distribution pdf *) @@ -71,19 +73,12 @@ Definition onem_nonneg (R : numDomainType) (p : {nonneg R}) (* /TODO: PR? *) Lemma nneseries_sum_bigcup {R : realType} (T : choiceType) (F : (set T)^nat) - (f : T -> \bar R) : - trivIset [set: nat] F -> - (forall i, 0 <= f i)%E -> - (\esum_(i in \bigcup_n F n) f i)%R = - \big[+%R/0%R]_(0 <= i \bar R) : trivIset [set: nat] F -> (forall i, 0 <= f i)%E -> + \esum_(i in \bigcup_n F n) f i = \sum_(0 <= i (*finUF*) tF f0. -rewrite esum_bigcupT//. -rewrite nneseries_esum//; last first. - move=> k _. - by apply: esum_ge0. -rewrite fun_true. -by apply: eq_esum => /= i _. +move=> tF f0; rewrite esum_bigcupT// nneseries_esum//; last first. + by move=> k _; exact: esum_ge0. +by rewrite fun_true; apply: eq_esum => /= i _. Qed. Lemma eq_probability R d (Y : measurableType d) (m1 m2 : probability Y R) : @@ -179,10 +174,11 @@ apply: cvg_toP. apply: lee_sum_nneg_natr => // k _ _. rewrite fsbig_finite//= sumEFin lee_fin. by apply: sumr_ge0 => /= b _; exact: bernoulli_pmf_ge0. -transitivity (\big[+%R/0%R]_(0 <= i k _; rewrite esum_fset//= => b _. by rewrite lee_fin bernoulli_pmf_ge0. -rewrite -nneseries_sum_bigcup//=; last by move=> b; rewrite lee_fin bernoulli_pmf_ge0. +rewrite -nneseries_sum_bigcup//=; last first. + by move=> b; rewrite lee_fin bernoulli_pmf_ge0. by rewrite esum_fset//= => b _; rewrite lee_fin bernoulli_pmf_ge0. Qed. @@ -204,8 +200,8 @@ Section bernoulli_measure. Context {R : realType}. Variables (p : R) (p0 : (0 <= p)%R) (p1 : ((NngNum p0)%:num <= 1)%R). -Lemma bernoulliE : bernoulli p = measure_add - (mscale (NngNum p0) (dirac true)) (mscale (onem_nonneg p1) (dirac false)). +Lemma bernoulli_dirac : bernoulli p = measure_add + (mscale (NngNum p0) \d_true) (mscale (onem_nonneg p1) \d_false). Proof. apply/funext => U; rewrite /bernoulli; case: ifPn => [p01|]; last first. by rewrite p0/= p1. @@ -231,15 +227,13 @@ Section integral_bernoulli. Context {R : realType}. Variables (p : R) (p01 : (0 <= p <= 1)%R). -Lemma bernoulliE_ext A : - bernoulli p A = p%:E * \d_true A + (`1-p)%:E * \d_false A. -Proof. by case/andP : p01 => p0 p1; rewrite bernoulliE// measure_addE. Qed. +Lemma bernoulliE A : bernoulli p A = p%:E * \d_true A + (`1-p)%:E * \d_false A. +Proof. by case/andP : p01 => p0 p1; rewrite bernoulli_dirac// measure_addE. Qed. Lemma integral_bernoulli (f : bool -> \bar R) : (forall x, 0 <= f x) -> \int[bernoulli p]_y (f y) = p%:E * f true + (`1-p)%:E * f false. Proof. -move=> f0; case/andP : p01 => p0 p1. -rewrite bernoulliE/=. +move=> f0; case/andP : p01 => p0 p1; rewrite bernoulli_dirac/=. rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. by rewrite !ge0_integral_mscale//= !integral_dirac//= !diracT !mul1e. Qed. @@ -258,10 +252,7 @@ apply: (@measurability _ _ _ _ _ _ (@pset _ _ _ : set (set (pprobability _ R)))) => //. move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=. apply: measurable_fun_if => //=. - apply: measurable_and => //; apply: (measurable_fun_bool true) => //=. - rewrite (_ : _ @^-1` _ = `[0, +oo[%classic)//. - by apply/seteqP; split => [x|x] /=; rewrite in_itv/= andbT. - by rewrite (_ : _ @^-1` _ = `]-oo, 1]%classic). + by apply: measurable_and => //; exact: measurable_fun_ler. apply: (eq_measurable_fun (fun t => \sum_(b <- fset_set Ys) (bernoulli_pmf t b)%:E)). move=> x /set_mem[_/= x01]. @@ -288,8 +279,7 @@ Definition binomial_pmf k := p ^+ k * (`1-p) ^+ (n - k) *+ 'C(n, k). Lemma binomial_pmf_ge0 k (p01 : (0 <= p <= 1)%R) : 0 <= binomial_pmf k. Proof. -move: p01 => /andP[p0 p1]. -rewrite /binomial_pmf mulrn_wge0// mulr_ge0// ?exprn_ge0//. +move: p01 => /andP[p0 p1]; rewrite mulrn_wge0// mulr_ge0// ?exprn_ge0//. exact: onem_ge0. Qed. @@ -306,7 +296,7 @@ Qed. Definition binomial_prob {R : realType} (n : nat) (p : R) : set nat -> \bar R := fun U => if (0 <= p <= 1)%R then - \esum_(k in U) (binomial_pmf n p k)%:E else \d_O U. + \esum_(k in U) (binomial_pmf n p k)%:E else \d_0%N U. Section binomial. Context {R : realType} (n : nat) (p : R). @@ -314,14 +304,11 @@ Context {R : realType} (n : nat) (p : R). Local Notation binomial := (binomial_prob n p). Let binomial0 : binomial set0 = 0. -Proof. -by rewrite /binomial measure0; case: ifPn => //; rewrite esum_set0. -Qed. +Proof. by rewrite /binomial measure0; case: ifPn => //; rewrite esum_set0. Qed. Let binomial_ge0 U : 0 <= binomial U. Proof. -rewrite /binomial; case: ifPn => // p01. -apply: esum_ge0 => /= k Uk. +rewrite /binomial; case: ifPn => // p01; apply: esum_ge0 => /= k Uk. by rewrite lee_fin binomial_pmf_ge0. Qed. @@ -333,8 +320,7 @@ apply: cvg_toP. apply: ereal_nondecreasing_is_cvgn => a b ab. apply: lee_sum_nneg_natr => // k _ _. by apply: esum_ge0 => /= ? _; exact: binomial_pmf_ge0. -rewrite nneseries_sum_bigcup// => i. -by rewrite lee_fin binomial_pmf_ge0. +by rewrite nneseries_sum_bigcup// => i; rewrite lee_fin binomial_pmf_ge0. Qed. HB.instance Definition _ := isMeasure.Build _ _ _ binomial @@ -344,15 +330,15 @@ Let binomial_setT : binomial [set: _] = 1. Proof. rewrite /binomial; case: ifPn; last by move=> _; rewrite probability_setT. move=> p01; rewrite /binomial_pmf. -have ? : forall k, 0%R <= (p ^+ k * `1-p ^+ (n - k) *+ 'C(n, k))%:E. - move=> k; case/andP : p01 => p1 p2. +have pkn k : 0%R <= (p ^+ k * `1-p ^+ (n - k) *+ 'C(n, k))%:E. + case/andP : p01 => p0 p1. by rewrite lee_fin mulrn_wge0// mulr_ge0 ?exprn_ge0 ?subr_ge0. -rewrite (esumID (`I_n.+1))// [X in _ + X]esum1 ?adde0; last first. +rewrite (esumID `I_n.+1)// [X in _ + X]esum1 ?adde0; last first. by move=> /= k [_ /negP]; rewrite -leqNgt => nk; rewrite bin_small. rewrite setTI esum_fset// -fsbig_ord//=. under eq_bigr do rewrite mulrC. rewrite sumEFin -exprDn_comm; last exact: mulrC. -by rewrite subrK expr1n. +by rewrite addrC add_onemK expr1n. Qed. HB.instance Definition _ := @@ -362,10 +348,11 @@ End binomial. Section binomial_probability. Local Open Scope ring_scope. -Context {R : realType} (n : nat) (p : R) (p0 : (0 <= p)%R) (p1 : ((NngNum p0)%:num <= 1)%R). +Context {R : realType} (n : nat) (p : R) + (p0 : (0 <= p)%R) (p1 : ((NngNum p0)%:num <= 1)%R). Definition bin_prob (k : nat) : {nonneg R} := - ((NngNum p0)%:num^+k * (NngNum (onem_ge0 p1))%:num^+(n-k)%N *+ 'C(n, k))%:nng. + ((NngNum p0)%:num ^+ k * (NngNum (onem_ge0 p1))%:num ^+ (n - k)%N *+ 'C(n, k))%:nng. Lemma bin_prob0 : bin_prob 0 = ((NngNum (onem_ge0 p1))%:num^+n)%:nng. Proof. @@ -373,71 +360,66 @@ rewrite /bin_prob bin0 subn0/=; apply/val_inj => /=. by rewrite expr0 mul1r mulr1n. Qed. -Lemma bin_prob1 : - bin_prob 1 = ((NngNum p0)%:num * (NngNum (onem_ge0 p1))%:num^+(n-1)%N *+ n)%:nng. -Proof. by rewrite /bin_prob bin1/=; apply/val_inj => /=; rewrite expr1. Qed. +Lemma bin_prob1 : bin_prob 1 = + ((NngNum p0)%:num * (NngNum (onem_ge0 p1))%:num ^+ n.-1 *+ n)%:nng. +Proof. +by rewrite /bin_prob bin1/=; apply/val_inj => /=; rewrite expr1 subn1. +Qed. -Lemma binomialE : binomial_prob n p = - @msum _ _ R (fun k => mscale (bin_prob k) \d_k) n.+1. +Lemma binomial_msum : + binomial_prob n p = msum (fun k => mscale (bin_prob k) \d_k) n.+1. Proof. -apply/funext => U; rewrite /binomial_prob; case: ifPn => [_|]; last by rewrite p1 p0. +apply/funext => U. +rewrite /binomial_prob; case: ifPn => [_|]; last by rewrite p1 p0. rewrite /msum/= /mscale/= /binomial_pmf. -have ? : forall k, (0%R <= (p ^+ k * `1-p ^+ (n - k) *+ 'C(n, k))%:E)%E. - move=> k. +have pkn k : (0%R <= (p ^+ k * `1-p ^+ (n - k) *+ 'C(n, k))%:E)%E. by rewrite lee_fin mulrn_wge0// mulr_ge0 ?exprn_ge0 ?subr_ge0. -rewrite (esumID (`I_n.+1))// [X in _ + X]esum1 ?adde0; last first. +rewrite (esumID `I_n.+1)//= [X in _ + X]esum1 ?adde0; last first. by move=> /= k [_ /negP]; rewrite -leqNgt => nk; rewrite bin_small. rewrite esum_mkcondl esum_fset//; last by move=> i /= _; case: ifPn. rewrite -fsbig_ord//=; apply: eq_bigr => i _. by rewrite diracE; case: ifPn => /= iU; [rewrite mule1|rewrite mule0]. Qed. -Lemma binomialE_ext U : binomial_prob n p U = +Lemma binomial_probE U : binomial_prob n p U = (\sum_(k < n.+1) (bin_prob k)%:num%:E * (\d_(nat_of_ord k) U))%E. -Proof. by rewrite binomialE /msum//=. Qed. +Proof. by rewrite binomial_msum. Qed. Lemma integral_binomial (f : nat -> \bar R) : (forall x, 0 <= f x)%E -> - (\int[binomial_prob n p]_y (f y) = \sum_(k < n.+1) (bin_prob k)%:num%:E * f k)%E. + (\int[binomial_prob n p]_y (f y) = + \sum_(k < n.+1) (bin_prob k)%:num%:E * f k)%E. Proof. -move=> f0; rewrite binomialE ge0_integral_measure_sum//=; apply: eq_bigr => i _. +move=> f0; rewrite binomial_msum ge0_integral_measure_sum//=. +apply: eq_bigr => i _. by rewrite ge0_integral_mscale//= integral_dirac//= diracT mul1e. Qed. End binomial_probability. -Lemma integral_binomial_bernoulli (R : realType) n p U : - (0 <= p <= 1)%R -> - \int[binomial_prob n p]_y \d_(0 < y)%N U = bernoulli (1 - `1-p ^+ n) U :> \bar R. +Lemma integral_binomial_prob (R : realType) n p U : (0 <= p <= 1)%R -> + \int[binomial_prob n p]_y \d_(0 < y)%N U = + bernoulli (1 - `1-p ^+ n) U :> \bar R. Proof. -move=> /andP[p0 p1]. -rewrite bernoulliE_ext//=; last first. - rewrite subr_ge0 exprn_ile1//=; last 2 first. - exact/onem_ge0. - exact/onem_le1. +move=> /andP[p0 p1]; rewrite bernoulliE//=; last first. + rewrite subr_ge0 exprn_ile1//=; [|exact/onem_ge0|exact/onem_le1]. by rewrite lerBlDr addrC -lerBlDr subrr; exact/exprn_ge0/onem_ge0. -rewrite (@integral_binomial _ n p _ _ (fun y => \d_(1 <= y)%N U))//; last first. +rewrite (@integral_binomial _ n p _ _ (fun y => \d_(1 <= y)%N U))//. rewrite !big_ord_recl/=. -rewrite /bump. -under eq_bigr => i _. - rewrite /=. - have -> : (0 < 1 + i)%N => //. - over. -rewrite addeC -ge0_sume_distrl. -- congr (_ * _ + _ * _). - + have -> : \sum_(i < n) (p ^+ (1 + i) * `1-p ^+ (n - (1 + i)) *+ 'C(n, 1 + i))%:E = - \sum_(i < n.+1) (p ^+ i * `1-p ^+ (n - i) *+ 'C(n, i))%:E - (`1-p ^+ n)%:E. - rewrite big_ord_recl/= expr0 subn0 mul1r bin0 mulr1n addeC addeA. - by rewrite (addeC _ (_ ^+ n)%:E) EFinN subee// add0e. - rewrite sumEFin !EFinB EFin_expe. - congr (_ - _)%E. - under eq_bigr do rewrite mulrC. - rewrite -(@exprDn_comm _ `1-p p n); last first. - by rewrite /GRing.comm/onem mulrC. - by rewrite /onem subrK expr1n. - + rewrite subn0 expr0 bin0 mulr1n /onem. - by rewrite mul1r opprB addrCA subrr addr0. -- move=> i _. +rewrite expr0 mul1r subn0 bin0 ltnn mulr1n addrC. +rewrite onemD opprK onem1 add0r; congr +%E. +rewrite /bump; under eq_bigr do rewrite leq0n add1n ltnS leq0n. +rewrite -ge0_sume_distrl; last first. + move=> i _. by apply/mulrn_wge0/mulr_ge0; apply/exprn_ge0 => //; exact/onem_ge0. +congr *%E. +transitivity (\sum_(i < n.+1) (`1-p ^+ (n - i) * p ^+ i *+ 'C(n, i))%:E - + (`1-p ^+ n)%:E). + rewrite big_ord_recl/=. + rewrite expr0 mulr1 subn0 bin0 mulr1n addrAC -EFinD subrr add0e. + by rewrite /bump; under [RHS]eq_bigr do rewrite leq0n add1n mulrC. +rewrite sumEFin -(@exprDn_comm _ `1-p p n)//. + by rewrite subrK expr1n. +by rewrite /GRing.comm/onem mulrC. Qed. Section binomial_total. @@ -445,7 +427,7 @@ Local Open Scope ring_scope. Variables (R : realType) (n : nat). Implicit Type p : R. -Lemma measurable_binomial_probT : +Lemma measurable_binomial_prob : measurable_fun setT (binomial_prob n : R -> pprobability _ _). Proof. apply: (@measurability _ _ _ _ _ _ @@ -454,10 +436,7 @@ move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=. rewrite /binomial_prob/=. set f := (X in measurable_fun _ X). apply: measurable_fun_if => //=. - apply: measurable_and => //; apply: (measurable_fun_bool true) => //=. - rewrite (_ : _ @^-1` _ = `[0, +oo[%classic)//. - by apply/seteqP; split => [x|x] /=; rewrite in_itv/= andbT. - by rewrite (_ : _ @^-1` _ = `]-oo, 1]%classic). + by apply: measurable_and => //; exact: measurable_fun_ler. apply: (eq_measurable_fun (fun t => \sum_(k x /set_mem[_/= x01]. @@ -471,7 +450,7 @@ Qed. End binomial_total. Arguments binomial_prob {R}. -Arguments measurable_binomial_probT {R}. +Arguments measurable_binomial_prob {R}. Section uniform_probability. Local Open Scope ring_scope. @@ -488,12 +467,7 @@ Qed. Lemma measurable_uniform_pdf : measurable_fun setT uniform_pdf. Proof. rewrite /uniform_pdf /=; apply: measurable_fun_if => //=. -apply: measurable_and => //. - apply: (measurable_fun_bool true) => //=. - rewrite (_ : _ @^-1` _ = `[a, +oo[%classic)//. - by apply/seteqP; split => [z|z] /=; rewrite in_itv/= andbT. -apply: (measurable_fun_bool true) => //=. -by rewrite (_ : _ @^-1` _ = `]-oo, b]%classic). +by apply: measurable_and => //; exact: measurable_fun_ler. Qed. Local Notation mu := lebesgue_measure. @@ -537,8 +511,7 @@ Proof. apply/integrableP; split. by apply: measurableT_comp => //; exact: measurable_uniform_pdf. under eq_integral. - move=> x _; rewrite gee0_abs//; last first. - by rewrite lee_fin uniform_pdf_ge0. + move=> x _; rewrite gee0_abs//; last by rewrite lee_fin uniform_pdf_ge0. over. by rewrite /= integral_uniform_pdf1 ?ltry// -subr_gt0. Qed. @@ -664,7 +637,6 @@ Section poisson_pdf. Variable R : realType. Local Open Scope ring_scope. -(* density function for Poisson *) Definition poisson_pdf k r : R := if r > 0 then r ^+ k / k`!%:R^-1 * expR (- r) else 1%:R. @@ -683,9 +655,7 @@ Qed. Lemma measurable_poisson_pdf k : measurable_fun setT (poisson_pdf k). Proof. rewrite /poisson_pdf; apply: measurable_fun_if => //. - apply: (measurable_fun_bool true). - rewrite (_ : _ @^-1` _ = `]0, +oo[%classic)//. - by apply/seteqP; split => x /=; rewrite in_itv/= andbT. + exact: measurable_fun_ltr. by apply: measurable_funM => /=; [exact: measurable_funM|exact: measurableT_comp]. Qed. @@ -812,8 +782,7 @@ Context d (T : measurableType d) (R : realType). Variable f : T -> R. Definition mscore t : {measure set unit -> \bar R} := - let p := NngNum (normr_ge0 (f t)) in - mscale p (dirac tt). + let p := NngNum (normr_ge0 (f t)) in mscale p \d_tt. Lemma mscoreE t U : mscore t U = if U == set0 then 0 else `| (f t)%:E |. Proof. @@ -897,7 +866,7 @@ rewrite (_ : (fun x => _) = (fun x => x * apply/funext => x; case: ifPn => ix; first by rewrite indicE/= mem_set ?mule1. by rewrite indicE/= memNset ?mule0// /= in_itv/=; exact/negP. apply: emeasurable_funM => //=; apply/EFin_measurable_fun. -by rewrite (_ : \1__ = mindic R (emeasurable_itv `[(i%:R)%:E, (i.+1%:R)%:E[)). +by rewrite (_ : \1__ = mindic R (emeasurable_itv `[i%:R%:E, i.+1%:R%:E[)). Qed. Definition mk i t := [the measure _ _ of k mf i t]. @@ -2130,7 +2099,7 @@ rewrite muleDr//= -muleDl//. rewrite !muleA -addeA -muleDl// -!EFinM !onem1S/= -splitr mulr1. have -> : (1 / 2 * (1 / 2) = 1 / 4%:R :> R)%R by rewrite mulf_div mulr1// -natrM. rewrite [in RHS](_ : 1 / 4 = (1 / 4)%:nng%:num)%R//. -rewrite (bernoulliE p14). +rewrite (bernoulli_dirac p14). rewrite measure_addE/= /mscale/= -!EFinM; congr( _ + (_ * _)%:E). have -> : (1 / 2 = 2 / 4%:R :> R)%R. by apply/eqP; rewrite eqr_div// ?pnatr_eq0// mul1r -natrM.