From 5d91e11de749164c3a60f263b04d5cfcfac27689 Mon Sep 17 00:00:00 2001 From: saito ayumu Date: Wed, 6 Mar 2024 18:13:46 +0900 Subject: [PATCH] casion example (wip) - use change of variables from charge.v to prove lemma integral_beta_nat (wip) - beta_nat_bern_bern --- theories/lang_syntax.v | 274 ------------------- theories/lang_syntax_examples_wip.v | 351 ++++++++++++++++-------- theories/prob_lang.v | 409 ++++++++++++++++++++++++++-- 3 files changed, 633 insertions(+), 401 deletions(-) diff --git a/theories/lang_syntax.v b/theories/lang_syntax.v index 6908912a4..b1f7e2450 100644 --- a/theories/lang_syntax.v +++ b/theories/lang_syntax.v @@ -345,280 +345,6 @@ End accessor_functions. Arguments acc_typ {R} s n. Arguments measurable_acc_typ {R} s n. - -Lemma factD n m : (n`! * m`! <= (n + m).+1`!)%N. -Proof. -elim: n m => /= [m|n ih m]. - by rewrite fact0 mul1n add0n factS leq_pmull. -rewrite 2!factS [in X in (_ <= _ * X)%N]addSn -mulnA leq_mul//. -by rewrite ltnS addSnnS leq_addr. -Qed. - -Lemma factD' n m : (n`! * m.-1`! <= (n + m)`!)%N. -Proof. -case: m => //= [|m]. - by rewrite fact0 muln1 addn0. -by rewrite addnS factD. -Qed. - -Lemma leq_prod2 (x y n m : nat) : (n <= x)%N -> (m <= y)%N -> - (\prod_(m <= i < y) i * \prod_(n <= i < x) i <= \prod_(n + m <= i < x + y) i)%N. -Proof. -move=> nx my. -rewrite big_addn. -rewrite -addnBA//. -rewrite {3}/index_iota. -rewrite -addnBAC//. -rewrite iotaD. -rewrite big_cat/=. -rewrite mulnC. -rewrite leq_mul//. - rewrite /index_iota. - apply: leq_prod. - by move=> i _; rewrite leq_addr. -rewrite subnKC//. -rewrite -{1}(add0n m). -rewrite big_addn. -rewrite {2}(_ : (y - m) = ((y - m + x) - x))%N; last first. - by rewrite -addnBA// subnn addn0. -rewrite -{1}(add0n x). -rewrite big_addn. -rewrite -addnBA// subnn addn0. -apply: leq_prod => i _. -by rewrite leq_add2r leq_addr. -Qed. - -Lemma leq_fact2 (x y n m : nat) : - (n <= x) %N -> (m <= y)%N -> - (x`! * y`! * ((n + m).+1)`! <= n`! * m`! * ((x + y).+1)`!)%N. -Proof. -move=> nx my. -rewrite (_ : x`! = n`! * \prod_(n.+1 <= i < x.+1) i)%N; last first. - by rewrite -fact_split. -rewrite -!mulnA leq_mul2l; apply/orP; right. -rewrite (_ : y`! = m`! * \prod_(m.+1 <= i < y.+1) i)%N; last first. - by rewrite -fact_split. -rewrite mulnCA -!mulnA leq_mul2l; apply/orP; right. -rewrite (_ : (x + y).+1`! = (n + m).+1`! * \prod_((n + m).+2 <= i < (x + y).+2) i)%N; last first. - rewrite -fact_split//. - by rewrite ltnS leq_add. -rewrite mulnA mulnC leq_mul2l; apply/orP; right. -rewrite -addSn -addnS. -rewrite -addSn -addnS. -exact: leq_prod2. -Qed. - -(* part of the step from casino3 to casino4 *) -Section casino3_casino4. -Context {R : realType}. -Variables a b a' b' : nat. - -Local Notation mu := lebesgue_measure. - -Open Scope ring_scope. -Import Notations. - -Program Definition beta_nat_bern : R.-sfker munit ~> mbool := - @letin' _ _ _ munit _ mbool _ - (sample_cst [the probability _ _ of beta_nat a b]) - (sample (bernoulli_trunc \o ubeta_nat_pdf a'.+1 b'.+1 \o @fst (measurableTypeR R) _ ) _). -Next Obligation. -apply: measurableT_comp. - apply: measurableT_comp. - exact: measurable_bernoulli_trunc. - exact: measurable_ubeta_nat_pdf. -exact: (measurable_acc_typ [:: Real] 0). -Qed. - -Local Notation B := beta_nat_norm. - -Definition Baa'bb'Bab : R := (beta_nat_norm (a + a') (b + b')) / beta_nat_norm a b. - -Lemma Baa'bb'Bab_ge0 : 0 <= Baa'bb'Bab. -Proof. by rewrite /Baa'bb'Bab divr_ge0// beta_nat_norm_ge0. Qed. - -Definition Baa'bb'Bab_nneg : {nonneg R} := NngNum Baa'bb'Bab_ge0. - -Lemma Baa'bb'Bab_le1 : Baa'bb'Bab_nneg%:num <= 1. -Proof. -rewrite /Baa'bb'Bab_nneg/= /Baa'bb'Bab. -rewrite ler_pdivrMr// ?mul1r ?beta_nat_norm_gt0//. -rewrite /B /beta_nat_norm. -rewrite ler_pdivrMr ?ltr0n ?fact_gt0//. -rewrite mulrAC. -rewrite ler_pdivlMr ?ltr0n ?fact_gt0//. -rewrite -!natrM ler_nat. -case: a. - rewrite /= fact0 mul1n !add0n. - case: b => /=. - case: a' => //. - case: b' => //= m. - by rewrite fact0 !mul1n muln1. - move=> n/=. - by rewrite fact0 add0n muln1 mul1n factD'. - move=> m. - rewrite mulnC leq_mul// mulnC. - by rewrite (leq_trans (factD' _ _))// addSn addnS//= addnC. -move=> n. -rewrite addSn. -case: b. - rewrite !fact0 add0n muln1 [leqRHS]mulnC addn0/= leq_mul//. - by rewrite factD'. -move=> m. -clear a b. -rewrite [(n + a').+1.-1]/=. -rewrite [n.+1.-1]/=. -rewrite [m.+1.-1]/=. -rewrite addnS. -rewrite [(_ + m).+1.-1]/=. -rewrite (addSn m b'). -rewrite [(m + _).+1.-1]/=. -rewrite (addSn (n + a')). -rewrite [_.+1.-1]/=. -rewrite addSn addnS. -by rewrite leq_fact2// leq_addr. -Qed. - -Lemma onem_Baa'bb'Bab_ge0 : 0 <= 1 - (Baa'bb'Bab_nneg%:num). -Proof. by rewrite subr_ge0 Baa'bb'Bab_le1. Qed. - -Lemma onem_Baa'bb'Bab_ge0_fix : 0 <= B a b * (1 - Baa'bb'Bab_nneg%:num). -Proof. -rewrite mulr_ge0//. - rewrite /B. - exact: beta_nat_norm_ge0. -rewrite subr_ge0. -exact: Baa'bb'Bab_le1. -Qed. - -Lemma ubeta_nat_pdf_ge0' t : 0 <= ubeta_nat_pdf a'.+1 b'.+1 t :> R. -Proof. -apply: ubeta_nat_pdf_ge0. (* TODO: needs 0 <= t <= 1 *) -Admitted. - -Lemma ubeta_nat_pdf_le1' t : (NngNum (ubeta_nat_pdf_ge0' t))%:num <= 1 :> R. -Proof. -rewrite /=. -rewrite /ubeta_nat_pdf. -rewrite /ubeta_nat_pdf'. (* TODO: needs 0 <= t <= 1 *) -Admitted. - -Lemma integral_ubeta_nat : - (\int[ubeta_nat a b]_x (ubeta_nat_pdf a'.+1 b'.+1 x)%:E = - \int[mu]_(x in `[0%R, 1%R]) - (x ^+ a'.-1 * `1-x ^+ b'.-1 * x ^+ a * `1-x ^+ b)%:E :> \bar R)%E. -Proof. -rewrite /ubeta_nat/ubeta_nat_pdf. -Admitted. - -Lemma beta_nat_bern_bern U : - beta_nat_bern tt U = - sample_cst (bernoulli Baa'bb'Bab_le1) tt U. -Proof. -rewrite /beta_nat_bern. -rewrite [LHS]letin'E/=. -transitivity ((\int[beta_nat a b]_y - (@bernoulli R (NngNum (ubeta_nat_pdf_ge0' y)) (ubeta_nat_pdf_le1' y) U))%E). - apply: eq_integral => /= r _. - rewrite /bernoulli_trunc/=. - case: sumbool_ler; last first. - admit. - move=> H_ge0. - case: sumbool_ler; last first. - admit. - move=> H_le1. - rewrite /=/bernoulli !measure_addE/= /mscale/=. - by congr _%E. -rewrite /beta_nat/=. -transitivity (((B a b)^-1%:E * \int[ubeta_nat a b]_x bernoulli (ubeta_nat_pdf_le1' x) U)%E). - rewrite ge0_integral_mscale //=. - admit. -rewrite {2}/bernoulli. -suff: (\int[ubeta_nat a b]_x bernoulli (ubeta_nat_pdf_le1' x) U)%E = - measure_add - (mscale (NngNum (beta_nat_norm_ge0 (a + a') (b + b'))) \d_true) - (mscale (NngNum (onem_Baa'bb'Bab_ge0_fix)) \d_false) U. - rewrite /= => ->. - rewrite !measure_addE/= /mscale/=. - rewrite /Baa'bb'Bab/=. - rewrite muleDr//. - congr (_ + _)%E. - rewrite -EFinM. - rewrite mulrA. - rewrite (mulrC (_^-1)). - by rewrite EFinM. - rewrite muleA. - congr (_ * _)%E. - rewrite -EFinM. - rewrite mulrA mulVr ?mul1r ?unitfE//. - rewrite gt_eqF//. - by rewrite beta_nat_norm_gt0. -transitivity ( - \int[ubeta_nat a b]_x (mscale (NngNum (ubeta_nat_pdf_ge0' x)) \d_true U) - + - \int[ubeta_nat a b]_x (mscale (onem_nonneg (ubeta_nat_pdf_le1' x)) \d_false) U)%E. - rewrite /bernoulli/=. - under eq_integral do rewrite measure_addE/=. - rewrite ge0_integralD//=. - rewrite /mscale/=. - apply: emeasurable_funM => //. - by apply/EFin_measurable_fun; exact: measurable_ubeta_nat_pdf. - apply/EFin_measurable_fun => /=. - apply: measurable_funM => //. - apply: measurable_funB => //. - exact: measurable_ubeta_nat_pdf. -rewrite measure_addE. -congr adde. - rewrite [in LHS]/mscale/= [in RHS]/mscale/=. - suff: (\int[ubeta_nat a b]_x ((ubeta_nat_pdf a'.+1 b'.+1 x)%:E) - = (B (a + a') (b + b'))%:E :> \bar R)%E. - move=> <-. - rewrite muleC. - rewrite -ge0_integralZl//=. - by under eq_integral do rewrite muleC. - apply/EFin_measurable_fun. - exact: measurable_ubeta_nat_pdf. - move=> x _. - rewrite lee_fin ubeta_nat_pdf_ge0//. - admit. (* 0 <= x <= 1 *) - transitivity ( (* calculating distribution (13) *) - \int[mu]_(x in `[(0:R)%R, (1:R)%R]%classic) - ((x ^+ a'.-1 * (`1- x) ^+ b'.-1 * x ^+ a * (`1- x) ^+ b)%:E) - )%E. - by rewrite integral_ubeta_nat. - transitivity ( - (\int[mu]_(x in `[0%R, 1%R]) - ((x ^+ (a + a').-1 * `1-x ^+ (b + b').-1)%:E))%E : \bar R). - apply: eq_integral => /= t. - rewrite inE/= in_itv/= => /andP[t0 t1]. - congr EFin. - admit. - by rewrite beta_nat_normE. -rewrite [in LHS]/mscale/= [in RHS]/mscale/=. -suff: (\int[ubeta_nat a b]_x (`1-(ubeta_nat_pdf a'.+1 b'.+1 x))%:E = - (B a b - B ((a + a')) ((b + b')))%:E :> \bar R)%E. - rewrite /Baa'bb'Bab. - admit. -under eq_integral do rewrite EFinB/=. -rewrite integralB_EFin//=; last 2 first. - admit. - admit. -rewrite integral_cst//= mul1e. -rewrite {1}/ubeta_nat setTI. -rewrite EFinB. -congr (_ - _)%E. - by rewrite -beta_nat_normE. -rewrite integral_ubeta_nat//. -rewrite beta_nat_normE /ubeta_nat_pdf. -rewrite /ubeta_nat_pdf'. -under eq_integral => x _. - rewrite -mulrA -mulrCA !mulrA/= -exprD -mulrA [X in _ * X]mulrC -exprD. -over. -rewrite /=. -Admitted. - -End casino3_casino4. - Section context. Variables (R : realType). Definition ctx := seq (string * typ). diff --git a/theories/lang_syntax_examples_wip.v b/theories/lang_syntax_examples_wip.v index fc74b7e3b..475897e7d 100644 --- a/theories/lang_syntax_examples_wip.v +++ b/theories/lang_syntax_examples_wip.v @@ -4,8 +4,8 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. From mathcomp.classical Require Import mathcomp_extra boolp classical_sets. From mathcomp.classical Require Import functions cardinality fsbigop. Require Import signed reals ereal topology normedtype sequences esum measure. -Require Import lebesgue_measure numfun lebesgue_integral kernel prob_lang. -Require Import lang_syntax_util lang_syntax. +Require Import charge lebesgue_measure numfun lebesgue_integral kernel. +Require Import prob_lang lang_syntax_util lang_syntax lang_syntax_examples. From mathcomp Require Import ring lra. (******************************************************************************) @@ -23,61 +23,86 @@ Local Open Scope classical_set_scope. Local Open Scope ring_scope. (* Local Open Scope ereal_scope. *) -Section trunc_lemmas. -Open Scope ring_scope. -Open Scope lang_scope. -Context (R : realType). - -Lemma bernoulli_truncE (p : R) U : - (0 <= p <= 1)%R -> - (bernoulli_trunc p U = - p%:E * \d_true U + (`1-p)%:E * \d_false U)%E. -Proof. -move=> /andP[p0 p1]. -rewrite /bernoulli_trunc. -case: (sumbool_ler 0 p) => [{}p0/=|]. - case: (sumbool_ler p 1) => [{}p1/=|]. - by rewrite /bernoulli/= measure_addE. - by rewrite ltNge p1. -by rewrite ltNge p0. -Qed. - -Lemma __ p p1 : - @execD R [::] _ (exp_bernoulli p p1) = - execD (exp_bernoulli_trunc [{p%:num}:R]). -Proof. -apply: eq_execD. -rewrite execD_bernoulli execD_bernoulli_trunc execD_real/=. -apply: funext=> x /=. -rewrite /bernoulli_trunc. -case: (sumbool_ler 0 p%:num) => [{}p0/=|]. - case: (sumbool_ler p%:num 1) => [{}p1'/=|]. - admit. -Abort. - -End trunc_lemmas. - Section beta_example. Open Scope ring_scope. Open Scope lang_scope. -Context (R : realType). - -Let p610 : ((6 / 10%:R)%:nng : {nonneg R})%:num <= 1. -Proof. admit. Admitted. +Context {R : realType}. -Lemma beta_bernoulli : - @execP R [::] _ [let "p" := Sample {exp_beta 6 4} in Sample {exp_bernoulli_trunc [#{"p"}]}] = - execP [Sample {@exp_bernoulli _ _ (6 / 10%:R)%:nng p610}]. +Lemma beta_bern610 : + @execP R [::] _ + [let "p" := + Sample {exp_beta 6 4} in Sample {exp_bernoulli_trunc [#{"p"}]}] = + execP [Sample {exp_bernoulli_trunc [{6 / 10}:R]}]. Proof. -rewrite execP_letin !execP_sample !execD_beta_nat !execD_bernoulli/=. -rewrite execD_bernoulli_trunc exp_var'E !(execD_var_erefl "p")/=. +rewrite execP_letin !execP_sample !execD_beta_nat !execD_bernoulli_trunc/=. +rewrite execD_real exp_var'E !(execD_var_erefl "p")/=. apply: eq_sfkernel=> x U. rewrite letin'E/=. -rewrite /beta_nat/mscale/=. -transitivity (bernoulli_trunc ((@beta_nat_norm R 7 4) / (@beta_nat_norm R 6 4)) U); last first. - (* congr (bernoulli_trunc _ _). *) - (* rewrite /beta_nat_norm/= factE/=; lra. *) -(* apply: beta_nat_bern_bern. *) +transitivity ((\int[beta_nat 6 4]_(y in `[0%R, 1%R]) bernoulli_trunc y U)%E : \bar R). + rewrite [in RHS]integral_mkcond /=. + apply: eq_integral => y _. + rewrite patchE. + case: ifPn => //. + (* Unset Printing Notations. *) + simpl in *. + rewrite mem_setE /= in_itv /= negb_and -!ltNge => /orP[y0|y1]; + rewrite /bernoulli_trunc/=. + case: sumbool_ler. + move=> a. + by rewrite ltNge a in y0. + rewrite /prob_lang.bernoulli0 /bernoulli => _. + rewrite [LHS]measure_addE/= /mscale/=. + (* match default value *) + admit. + admit. + rewrite integral_beta_nat. +under eq_integral => y y01. + rewrite bernoulli_truncE. + rewrite muleC muleDr// !muleA muleC [X in _ + X]muleC. + over. + admit. +rewrite /= bernoulli_truncE. +rewrite integralD//. +congr (_ + _)%E. +rewrite integralZl//. +rewrite muleC. +congr (_ * _)%E. +(* rewrite /= setTI. *) +rewrite /beta_nat_pdf. +rewrite /ubeta_nat_pdf/ubeta_nat_pdf'/=. +transitivity (\int[@lebesgue_measure R]_(x0 in `[0%R, 1%R]) + ((ubeta_nat_pdf 7 4 x0 / beta_nat_norm 6 4)%:E))%E. + apply: eq_integral => p _. + rewrite muleC -EFinM. + rewrite -[X in X * _]divr1 mulf_div. + congr (_ / _)%:E; last by rewrite mul1r. + by rewrite /ubeta_nat_pdf/= /ubeta_nat_pdf' mulrA -exprS. +under eq_integral do rewrite mulrC EFinM. +rewrite integralZl//=. +rewrite -beta_nat_normE /beta_nat_norm/= factE. +rewrite -!EFinM/=. +congr _%:E; lra. + admit. + admit. +rewrite integralZl//. +rewrite muleC. +congr (_ * _)%E. +rewrite /beta_nat_pdf. +rewrite /ubeta_nat_pdf/ubeta_nat_pdf'/=. +transitivity (\int[@lebesgue_measure R]_(x0 in `[0%R, 1%R]) + ((ubeta_nat_pdf 6 5 x0 / beta_nat_norm 6 4)%:E))%E. + apply: eq_integral => p _. + by rewrite mulrC -EFinM -2!mulrA -exprSr mulrC. +under eq_integral do rewrite mulrC EFinM. +rewrite integralZl//=. +rewrite -beta_nat_normE /beta_nat_norm/= factE. +rewrite -!EFinM/onem/=. +congr _%:E; lra. + admit. + admit. + admit. + admit. + lra. Admitted. End beta_example. @@ -240,6 +265,22 @@ apply: s01. by rewrite inE in p01. Qed. +(* Lemma measurable_mtyp (t : typ) (U : set (@mtyp R t)) : measurable U. +Proof. +induction t => //. *) + +Lemma congr_letinl g t1 t2 str (e1 e2 : @exp _ _ g t1) +(e : @exp _ _ (_ :: g) t2) x U : + (forall y V, execP e1 y V = execP e2 y V) -> + measurable U -> + @execP R g t2 [let str := e1 in e] x U = + @execP R g t2 [let str := e2 in e] x U. +Proof. +move=> He mU. +apply eq_sfkernel in He. +by rewrite !execP_letin He. +Qed. + Lemma congr_letin 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. @@ -338,14 +379,17 @@ Lemma exec_beta_a1 U : Proof. rewrite execP_letin !execP_sample execD_beta_nat !execD_bernoulli_trunc/=. rewrite !execD_real/= exp_var'E (execD_var_erefl "p")/=. -transitivity (beta_nat_bern 6 4 1 0 tt U : \bar R). +transitivity (beta_nat_bern 6 4 1 0 U : \bar R). rewrite /beta_nat_bern !letin'E/= /ubeta_nat_pdf/= /onem. apply: eq_integral => x _. rewrite /=. do 2 f_equal. by rewrite /ubeta_nat_pdf' expr1 expr0 mulr1. -rewrite beta_nat_bern_bern/= /bernoulli/= bernoulli_truncE; last by lra. -rewrite measure_addE/= /mscale/=. +rewrite beta_nat_bern_bern// !bernoulli_truncE; last 2 first. + by lra. + apply/andP; split. + by apply/Baa'bb'Bab_ge0. + by apply/Baa'bb'Bab_le1. congr (_ * _ + _ * _)%:E. rewrite /Baa'bb'Bab /beta_nat_norm/=. rewrite !factS/= fact0. @@ -356,19 +400,47 @@ by field. Qed. Definition casino0 : @exp R _ [::] _ := - [Normalize - let "p" := Sample {exp_uniform 0 1 a01} in - let "a1" := Sample {exp_binomial_trunc 8 [#{"p"}]} in - let "_" := if #{"a1"} == {5}:N then return TT else Score {0}:R in - let "a2" := Sample {exp_binomial_trunc 3 [#{"p"}]} in - return {1}:N <= #{"a2"}]. + [Normalize + let "p" := Sample {exp_uniform 0 1 a01} in + let "a1" := Sample {exp_binomial_trunc 8 [#{"p"}]} in + let "_" := if #{"a1"} == {5}:N then return TT else Score {0}:R in + let "a2" := Sample {exp_binomial_trunc 3 [#{"p"}]} in + return {1}:N <= #{"a2"}]. Definition casino1 : @exp R _ [::] _ := - [Normalize - let "p" := Sample {exp_uniform 0 1 a01} in - let "a1" := Sample {exp_binomial_trunc 8 [#{"p"}]} in - let "_" := if #{"a1"} == {5}:N then return TT else Score {0}:R in - Sample {exp_bernoulli_trunc [{1}:R - {[{1}:R - #{"p"}]} ^+ {3%nat}]}]. + [Normalize + let "p" := Sample {exp_uniform 0 1 a01} in + let "a1" := Sample {exp_binomial_trunc 8 [#{"p"}]} in + let "_" := if #{"a1"} == {5}:N then return TT else Score {0}:R in + Sample {exp_bernoulli_trunc [{1}:R - {[{1}:R - #{"p"}]} ^+ {3%nat}]}]. + +Definition casino2 : @exp R _ [::] _ := + [Normalize + let "p" := Sample {exp_uniform 0 1 a01} in + let "_" := + Score {[{56}:R * #{"p"} ^+ {5%nat} * {[{1}:R - #{"p"}]} ^+ {3%nat}]} in + Sample {exp_bernoulli_trunc [{1}:R - {[{1}:R - #{"p"}]} ^+ {3%nat}]}]. + +Definition casino2' : @exp R _ [::] _ := + [Normalize + let "p" := Sample {exp_beta 1 1} in + let "_" := Score + {[{56}:R * #{"p"} ^+ {5%nat} * {[{1}:R - #{"p"}]} ^+ {3%nat}]} in + Sample {exp_bernoulli_trunc [{1}:R - {[{1}:R - #{"p"}]} ^+ {3%nat}]}]. + +Definition casino3 : @exp R _ [::] _ := + [Normalize + let "_" := Score {1 / 9}:R in + let "p" := Sample {exp_beta 6 4} in + Sample {exp_bernoulli_trunc [{1}:R - {[{1}:R - #{"p"}]} ^+ {3%nat}]}]. + +Definition casino4 : @exp R _ [::] _ := + [Normalize + let "_" := Score {1 / 9}:R in + Sample {exp_bernoulli_trunc [{10 / 11}:R]}]. + +Definition casino5 : @exp R _ [::] _ := + [Normalize Sample {exp_bernoulli_trunc [{10 / 11}:R]}]. Lemma casino01 : execD casino0 = execD casino1. @@ -391,12 +463,6 @@ move: r01 => /andP[r0 r1]. by apply/binomial_over1/andP. Qed. -Definition casino2 : @exp R _ [::] _ := - [Normalize - let "p" := Sample {exp_uniform 0 1 a01} in - let "_" := Score {[{56}:R * #{"p"} ^+ {5%nat} * {[{1}:R - #{"p"}]} ^+ {3%nat}]} in - Sample {exp_bernoulli_trunc [{1}:R - {[{1}:R - #{"p"}]} ^+ {3%nat}]}]. - Lemma casino12 : execD casino1 = execD casino2. Proof. @@ -431,11 +497,87 @@ apply/exprn_ge0. by rewrite subr_ge0. Qed. -Definition casino3 : @exp R _ [::] _ := - [Normalize - let "_" := Score {1 / 9}:R in - let "p" := Sample {exp_beta 6 4} in - Sample {exp_bernoulli_trunc [{1}:R - {[{1}:R - #{"p"}]} ^+ {3%nat}]}]. +Lemma casino22' : + execD casino2 = execD casino2'. +Proof. +apply: eq_execD. +f_equal. +apply: congr_normalize => //= x U. +apply: congr_letinl => //= y V. +rewrite !execP_sample execD_uniform execD_beta_nat/=. +rewrite beta11_uniform//. +rewrite /=. +apply: sub_sigma_algebra. +rewrite //. +admit. +Admitted. + +Lemma casino23 : + execD casino2' = execD casino3. +Proof. +apply: eq_execD. +f_equal. +apply: congr_normalize => x U. +rewrite !execP_letin !execP_sample !execP_score !execD_beta_nat. +rewrite !execD_bernoulli_trunc/= !(@execD_bin _ _ binop_mult). +rewrite !execD_pow !(@execD_bin _ _ binop_minus) !execD_real/=. +rewrite !execD_pow !(@execD_bin _ _ binop_minus) !execD_real/=. +rewrite !exp_var'E !(execD_var_erefl "p")/=. +rewrite !letin'E/= ![in RHS]ge0_integral_mscale//=. +rewrite /=. +under eq_integral => y _. + rewrite letin'E/= /mscale/=. + over. +rewrite /=. +(* set f := letin' _ _. *) +transitivity (\int[beta_nat 1 1]_(y in `[0%R, 1%R]) f (y, x) U)%E. + rewrite [in RHS]integral_mkcond /=. + apply: eq_integral => y _. + rewrite patchE. + case: ifPn => //. + simpl in *. + rewrite mem_setE /= in_itv /= negb_and -!ltNge => /orP[y0|y1]; + rewrite /bernoulli_trunc/=. + case: sumbool_ler. + move=> a. + by rewrite ltNge a in y0. + rewrite /prob_lang.bernoulli0 /bernoulli => _. + rewrite [LHS]measure_addE/= /mscale/=. + (* match default value *) + admit. + admit. + rewrite integral_beta_nat. + admit. +rewrite (integral_beta_nat 6 4). + rewrite ger0_norm// integral_dirac// diracT mul1e letin'E/=. + transitivity (((1 / 9)%:E * \int[beta_nat 6 4]_(y in `[0%R, 1%R]) + bernoulli_trunc (1 - (1 - y) ^+ 3) U)%E : \bar R); last first. + admit. +rewrite (integral_beta_nat 6 4)//=. +rewrite -integralZl//=. + apply: eq_integral => y y01. + rewrite /f letin'E /= !ge0_integral_mscale//= integral_dirac// diracT mul1e. + rewrite -muleAC muleC -[in RHS]muleCA. + congr (_ * _)%E. + rewrite ger0_norm. + rewrite /beta_nat_pdf ubeta_nat_pdf11/= muleC -!EFinM. + rewrite !div1r. + rewrite /beta_nat_norm/= /ubeta_nat_pdf/ubeta_nat_pdf' factE/=/onem. + congr _%:E; lra. + rewrite inE/= in_itv/= in y01. + move: y01 => /andP[y0 y1]. + apply/mulr_ge0/exprn_ge0 => //. + apply/mulr_ge0/exprn_ge0 => //. + lra. +admit. +admit. +admit. +apply: (@measurableT_comp _ _ _ _ _ _ (fun x0 => f x0 U)). + apply: measurable_kernel. + done. +apply: measurable_pair2. +admit. +Admitted. Lemma casino34' U : @execP R [::] _ [let "p" := Sample {exp_beta 6 4} in @@ -445,39 +587,34 @@ Proof. rewrite execP_letin !execP_sample execD_beta_nat !execD_bernoulli_trunc/=. rewrite execD_pow/= (@execD_bin _ _ binop_minus) !execD_real/=. rewrite exp_var'E (execD_var_erefl "p")/=. -transitivity (beta_nat_bern 6 4 0 3 tt U : \bar R). - rewrite /beta_nat_bern !letin'E/= /ubeta_nat_pdf/= /onem. - apply: eq_integral => x _. - do 2 f_equal. - rewrite /ubeta_nat_pdf'. - rewrite expr0. - by rewrite mul1r. -rewrite bernoulli_truncE; last by lra. -rewrite beta_nat_bern_bern/= /bernoulli/=. -rewrite measure_addE/= /mscale/=. -congr (_ * _ + _ * _)%:E; rewrite /onem. - rewrite /Baa'bb'Bab /beta_nat_norm/=. - by rewrite !factS/= fact0; field. -rewrite /Baa'bb'Bab /beta_nat_norm/=. -by rewrite !factS/= fact0; field. +(* TODO: generalize *) +rewrite letin'E/=. +have := (@beta_nat_bern_bern R 6 4 0 3 U). +rewrite /beta_nat_bern /ubeta_nat_pdf/ubeta_nat_pdf'/=. +under eq_integral do rewrite expr0 mul1r. +move=> ->//. +rewrite /Baa'bb'Bab addn0 /beta_nat_norm/= factE/=. +by congr (bernoulli_trunc _ _); field. Qed. Lemma bern_onem (f : _ -> R) U p : - (\int[beta_nat 6 4]_y bernoulli_trunc (f y) U = p%:E * \d_true U + `1-p%:E * \d_false U)%E -> - (\int[beta_nat 6 4]_y bernoulli_trunc (1 - f y) U = `1-p%:E * \d_true U + p%:E * \d_false U)%E. + (forall x, 0 <= f x <= 1) -> + (\int[beta_nat 6 4]_y bernoulli_trunc (f y) U = + p%:E * \d_true U + `1-p%:E * \d_false U)%E -> + (\int[beta_nat 6 4]_y bernoulli_trunc (1 - f y) U + = `1-p%:E * \d_true U + p%:E * \d_false U)%E. Proof. +move=> f01. under eq_integral => x _. rewrite bernoulli_truncE. over. -admit. -rewrite /= /beta_nat/mscale/= /beta_nat_norm/= /ubeta_nat/ubeta_nat_pdf. +done. +move=> h1. +rewrite /= in h1. +rewrite /bernoulli_trunc. +(* /beta_nat/mscale/= /beta_nat_norm/= /ubeta_nat/ubeta_nat_pdf/=. *) Admitted. -Definition casino4 : @exp R _ [::] _ := - [Normalize - let "_" := Score {1 / 9}:R in - Sample {exp_bernoulli_trunc [{10 / 11}:R]}]. - Lemma casino34 : execD casino3 = execD casino4. Proof. @@ -493,21 +630,24 @@ transitivity (\int[beta_nat 6 4]_y bernoulli_trunc (1 - (1 - y) ^+ 3) U : \bar R rewrite bernoulli_truncE; last by lra. have -> := (@bern_onem (fun x => (1 - x) ^+ 3) U (1 / 11) _). congr (_ * _ + _ * _)%E; congr _%:E; rewrite /onem; lra. -transitivity (beta_nat_bern 6 4 0 3 tt U : \bar R). - rewrite /beta_nat_bern !letin'E/= /ubeta_nat_pdf/= /onem. + admit. +transitivity (beta_nat_bern 6 4 0 3 U : \bar R). + rewrite /beta_nat_bern /ubeta_nat_pdf/= /onem. apply: eq_integral => y0 _. do 2 f_equal. rewrite /ubeta_nat_pdf'/=. rewrite expr0. by rewrite mul1r. -rewrite beta_nat_bern_bern/= /bernoulli/=. -rewrite measure_addE/= /mscale/=. +rewrite beta_nat_bern_bern//= bernoulli_truncE; last first. + apply/andP; split. + apply/Baa'bb'Bab_ge0. + apply/Baa'bb'Bab_le1. congr (_ * _ + _ * _)%:E; rewrite /onem. rewrite /Baa'bb'Bab /beta_nat_norm/=. by rewrite !factS/= fact0; field. rewrite /Baa'bb'Bab /beta_nat_norm/=. by rewrite !factS/= fact0; field. -Qed. +Admitted. Lemma norm_score_bern g p1 p2 (p10 : p1 != 0) (p1_ge0 : 0 <= p1) (p201 : 0 <= p2 <= 1) : @@ -544,9 +684,6 @@ rewrite integral_dirac//= diracT !diracE. by rewrite muleC muleA -EFinM mulVf// invr1 /onem !(mul1r, mule1). Qed. -Definition casino5 : @exp R _ [::] _ := - [Normalize Sample {exp_bernoulli_trunc [{10 / 11}:R]}]. - Lemma casino45 : execD casino4 = execD casino5. Proof. diff --git a/theories/prob_lang.v b/theories/prob_lang.v index 908c32c58..04cdcb5c0 100644 --- a/theories/prob_lang.v +++ b/theories/prob_lang.v @@ -5,14 +5,21 @@ From mathcomp Require Import rat. From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import functions cardinality fsbigop. Require Import reals ereal signed topology normedtype sequences esum measure. -Require Import lebesgue_measure numfun lebesgue_integral exp kernel. +Require Import charge lebesgue_measure numfun lebesgue_integral exp kernel. From mathcomp Require Import ring lra. -(******************************************************************************) -(* Semantics of a probabilistic programming language using s-finite kernels *) -(* *) -(* bernoulli r1 == Bernoulli probability with r1 a proof that *) -(* r : {nonneg R} is smaller than 1 *) +(**md**************************************************************************) +(* # Semantics of a probabilistic programming language using s-finite kernels *) +(* bernoulli p1 == Bernoulli probability with p1 a proof that *) +(* p : {nonneg R} is smaller than 1 *) +(* bernoulli_trunc r == Bernoulli probability with real number r *) +(* bino_term 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 *) +(* binomial_probability n p1 == binomial probability with n and p1 a proof *) +(* that p : {nonneg R} is smaller than 1 *) +(* binomial_probability_trunc n r == binomial probability with n and real *) +(* number r *) (* uniform_probability a b ab0 == uniform probability over the interval [a,b] *) (* sample mP == sample according to the probability P where mP is a *) (* proof that P is a measurable function *) @@ -194,7 +201,21 @@ Definition bernoulli_trunc (p : R) := match sumbool_ler 0%R p with | inr _ => bernoulli0 end. -(*HB.instance Definition _ (p : R) := Probability.on (bernoulli_trunc p).*) +Lemma bernoulli_truncE (p : R) U : + (0 <= p <= 1)%R -> + (bernoulli_trunc p U = + p%:E * \d_true U + (`1-p)%:E * \d_false U)%E. +Proof. +move=> /andP[p0 p1]. +rewrite /bernoulli_trunc. +case: (sumbool_ler 0 p) => [{}p0/=|]. + case: (sumbool_ler p 1) => [{}p1/=|]. + by rewrite /bernoulli/= measure_addE. + by rewrite ltNge p1. +by rewrite ltNge p0. +Qed. + +(* HB.instance Definition _ (p : R) := Probability.on (bernoulli_trunc p). *) Let simpe := (@mule0 R, @adde0 R, @mule1 R, @add0e R). @@ -686,6 +707,15 @@ Definition ubeta_nat (U : set (measurableTypeR R)) : \bar R := \int[mu]_(x in U `&` `[0, 1](*NB: is this correct?*)) (ubeta_nat_pdf x)%:E. (* TODO: define as \int[uniform_probability p01]_(t in U) (ubeta_nat_pdf t)%:E ? *) +Lemma ubeta_natE U : + (ubeta_nat U = + \int[mu]_(x in U `&` `[0%R, 1%R]) (ubeta_nat_pdf x)%:E :> \bar R)%E. +Proof. by []. Qed. + +Lemma ubeta_nat_lty U : (ubeta_nat U < +oo)%E. +Proof. +Admitted. + Let ubeta_nat0 : ubeta_nat set0 = 0%:E. Proof. by rewrite /ubeta_nat set0I integral_set0. Qed. @@ -743,19 +773,6 @@ Proof. move=> /= F mF tF mUF; exact: measure_semi_sigma_additive. Qed. HB.instance Definition _ := isMeasure.Build _ _ _ beta_nat beta_nat0 beta_nat_ge0 beta_nat_sigma_additive. -(* HB.instance Definition _ := Measure.on beta_nat. *) - -(*Let beta_nat0 : beta_nat set0 = 0. -Proof. exact: measure0. Qed. - -Let beta_nat_ge0 U : (0 <= beta_nat U)%E. -Proof. exact: measure_ge0. Qed. - -Let beta_nat_sigma_additive : semi_sigma_additive beta_nat. -Proof. move=> /= F mF tF mUF; exact: measure_semi_sigma_additive. Qed. - -HB.instance Definition _ := isMeasure.Build _ _ _ beta_nat beta_nat0 beta_nat_ge0 beta_nat_sigma_additive.*) - Let beta_nat_setT : beta_nat setT = 1%:E. Proof. rewrite /beta_nat /= /mscale /=. @@ -775,6 +792,8 @@ Qed. End beta_probability. +Arguments beta_nat {R}. + Section beta_probability11. Local Open Scope ring_scope. Context {R : realType}. @@ -796,6 +815,356 @@ Qed. End beta_probability11. +Lemma factD n m : (n`! * m`! <= (n + m).+1`!)%N. +Proof. +elim: n m => /= [m|n ih m]. + by rewrite fact0 mul1n add0n factS leq_pmull. +rewrite 2!factS [in X in (_ <= _ * X)%N]addSn -mulnA leq_mul//. +by rewrite ltnS addSnnS leq_addr. +Qed. + +Lemma factD' n m : (n`! * m.-1`! <= (n + m)`!)%N. +Proof. +case: m => //= [|m]. + by rewrite fact0 muln1 addn0. +by rewrite addnS factD. +Qed. + +Lemma leq_prod2 (x y n m : nat) : (n <= x)%N -> (m <= y)%N -> + (\prod_(m <= i < y) i * \prod_(n <= i < x) i <= \prod_(n + m <= i < x + y) i)%N. +Proof. +move=> nx my. +rewrite big_addn. +rewrite -addnBA//. +rewrite {3}/index_iota. +rewrite -addnBAC//. +rewrite iotaD. +rewrite big_cat/=. +rewrite mulnC. +rewrite leq_mul//. + rewrite /index_iota. + apply: leq_prod. + by move=> i _; rewrite leq_addr. +rewrite subnKC//. +rewrite -{1}(add0n m). +rewrite big_addn. +rewrite {2}(_ : (y - m) = ((y - m + x) - x))%N; last first. + by rewrite -addnBA// subnn addn0. +rewrite -{1}(add0n x). +rewrite big_addn. +rewrite -addnBA// subnn addn0. +apply: leq_prod => i _. +by rewrite leq_add2r leq_addr. +Qed. + +Lemma leq_fact2 (x y n m : nat) : + (n <= x) %N -> (m <= y)%N -> + (x`! * y`! * ((n + m).+1)`! <= n`! * m`! * ((x + y).+1)`!)%N. +Proof. +move=> nx my. +rewrite (_ : x`! = n`! * \prod_(n.+1 <= i < x.+1) i)%N; last first. + by rewrite -fact_split. +rewrite -!mulnA leq_mul2l; apply/orP; right. +rewrite (_ : y`! = m`! * \prod_(m.+1 <= i < y.+1) i)%N; last first. + by rewrite -fact_split. +rewrite mulnCA -!mulnA leq_mul2l; apply/orP; right. +rewrite (_ : (x + y).+1`! = (n + m).+1`! * \prod_((n + m).+2 <= i < (x + y).+2) i)%N; last first. + rewrite -fact_split//. + by rewrite ltnS leq_add. +rewrite mulnA mulnC leq_mul2l; apply/orP; right. +rewrite -addSn -addnS. +rewrite -addSn -addnS. +exact: leq_prod2. +Qed. + +Section integral_beta. +Context {R : realType}. +Variables a b a' b' : nat. + +Local Notation mu := lebesgue_measure. + +Lemma integralMl f g1 g2 A : +measurable A -> measurable_fun A f -> + measurable_fun A g1 -> measurable_fun A g2 -> +(ae_eq mu A g1 (EFin \o g2)) -> + \int[mu]_(x in A) (f x * g1 x) = + \int[mu]_(x in A) (f x * (g2 x)%:E) :> \bar R. +Proof. +move=> mA mf mg1 mg2 Hg. +apply: ae_eq_integral => //. + by apply: emeasurable_funM. + apply: emeasurable_funM => //. + by apply/EFin_measurable_fun. +by apply: ae_eq_mul2l. +Qed. + +Let beta_nat_dom : (@beta_nat R a b `<< mu). +Proof. +move=> A mA muA0. +rewrite /beta_nat /mscale/= /ubeta_nat. +have -> : \int[mu]_(x0 in A `&` `[0%R, 1%R]) (ubeta_nat_pdf a b x0)%:E = 0%:E. + apply/eqP; rewrite eq_le. + apply/andP; split; last first. + apply: integral_ge0 => x [Ax /=]. + rewrite in_itv /= => x01. + by rewrite lee_fin ubeta_nat_pdf_ge0. + apply: le_trans. + apply: (@subset_integral _ _ _ _ _ A). + by apply: measurableI. + by []. + apply/EFin_measurable_fun. + apply: (@measurable_funS _ _ _ _ setT) => //=. + apply: measurable_ubeta_nat_pdf. + move=> x Ax. + have : (`[0%R, 1%R]%classic x). + admit. + rewrite /= in_itv/=. + apply: ubeta_nat_pdf_ge0. + apply: subIsetl. + rewrite /=. + (* rewrite integral_abs_eq0. *) (* without abs *) + admit. +by rewrite mule0. +Admitted. + +Lemma integral_beta_nat f : + measurable_fun setT f -> + \int[beta_nat a b]_(x in `[0%R, 1%R]) `|f x| < +oo -> + \int[beta_nat a b]_(x in `[0%R, 1%R]) f x = + \int[mu]_(x in `[0%R, 1%R]) (f x * (beta_nat_pdf a b x)%:E) :> \bar R. +Proof. +move=> mf finf. +rewrite -(Radon_Nikodym_change_of_variables beta_nat_dom) //=. +apply: integralMl => //. + apply: (@measurable_funS _ _ _ _ [set: R]) => //. + apply: (@measurable_funS _ _ _ _ [set: R]) => //. + rewrite Radon_NikodymE. + by exact: beta_nat_dom. + move=> /= H. + case: cid => /= h [h1 h2 h3]. + have : (measurable_fun setT h /\ \int[mu]_x `|h x| < +oo). + apply/integrableP/h2. + move=> /= [mh _]. + apply: mh. + apply: (@measurable_funS _ _ _ _ [set: R]) => //. + apply: measurable_beta_nat_pdf. + rewrite Radon_NikodymE => /= A. + by exact: beta_nat_dom. +case: cid => /= h [h1 h2 h3]. +apply: integral_ae_eq => //. + apply: integrableS h2 => //. (* integrableST? *) + apply: (@measurable_funS _ _ _ _ [set: R]) => //. + apply: measurableT_comp => //. + apply: measurable_beta_nat_pdf. + move=> E E01 mE. + have mB : measurable_fun E (EFin \o ubeta_nat_pdf a b). + apply: measurableT_comp => //. + apply: (@measurable_funS _ _ _ _ [set: R]) => //. + apply: measurable_ubeta_nat_pdf. + rewrite -(h3 _ mE). + rewrite /beta_nat/mscale/ubeta_nat/beta_nat_pdf/=. + under eq_integral do rewrite mulrC EFinM. + rewrite (integralZl mE). + rewrite /ubeta_nat setIidl //. + rewrite /=. + apply/integrableP; split. + by apply: mB. + under eq_integral => x x01. + rewrite gee0_abs /=. + over. + apply: ubeta_nat_pdf_ge0. + have : x \in `[0%R, 1%R]. + apply: (@subset_trans _ _ `[x,x] _ _ E01). + by rewrite set_interval.set_itv1 sub1set x01. + by rewrite /= in_itv/= lexx. + by rewrite in_itv/=. + rewrite /=. + have <- := (setIidl E01). + by rewrite -ubeta_natE ubeta_nat_lty. +apply/integrableP; split. + by apply: (@measurable_funS _ _ _ _ [set: R]). +exact: finf. +Qed. + +Local Open Scope ring_scope. + +(* TODO: `[0, 1]? *) +Definition beta_nat_bern U : \bar R := + \int[beta_nat a b]_y bernoulli_trunc (ubeta_nat_pdf a'.+1 b'.+1 y) U. + +Local Notation B := beta_nat_norm. + +Definition Baa'bb'Bab : R := (beta_nat_norm (a + a') (b + b')) / beta_nat_norm a b. + +Lemma Baa'bb'Bab_ge0 : 0 <= Baa'bb'Bab. +Proof. by rewrite /Baa'bb'Bab divr_ge0// beta_nat_norm_ge0. Qed. + +Definition Baa'bb'Bab_nneg : {nonneg R} := NngNum Baa'bb'Bab_ge0. + +Lemma Baa'bb'Bab_le1 : Baa'bb'Bab_nneg%:num <= 1. +Proof. +rewrite /Baa'bb'Bab_nneg/= /Baa'bb'Bab. +rewrite ler_pdivrMr// ?mul1r ?beta_nat_norm_gt0//. +rewrite /B /beta_nat_norm. +rewrite ler_pdivrMr ?ltr0n ?fact_gt0//. +rewrite mulrAC. +rewrite ler_pdivlMr ?ltr0n ?fact_gt0//. +rewrite -!natrM ler_nat. +case: a. + rewrite /= fact0 mul1n !add0n. + case: b => /=. + case: a' => //. + case: b' => //= m. + by rewrite fact0 !mul1n muln1. + move=> n/=. + by rewrite fact0 add0n muln1 mul1n factD'. + move=> m. + rewrite mulnC leq_mul// mulnC. + by rewrite (leq_trans (factD' _ _))// addSn addnS//= addnC. +move=> n. +rewrite addSn. +case: b. + rewrite !fact0 add0n muln1 [leqRHS]mulnC addn0/= leq_mul//. + by rewrite factD'. +move=> m. +clear a b. +rewrite [(n + a').+1.-1]/=. +rewrite [n.+1.-1]/=. +rewrite [m.+1.-1]/=. +rewrite addnS. +rewrite [(_ + m).+1.-1]/=. +rewrite (addSn m b'). +rewrite [(m + _).+1.-1]/=. +rewrite (addSn (n + a')). +rewrite [_.+1.-1]/=. +rewrite addSn addnS. +by rewrite leq_fact2// leq_addr. +Qed. + +Lemma onem_Baa'bb'Bab_ge0 : 0 <= 1 - (Baa'bb'Bab_nneg%:num). +Proof. by rewrite subr_ge0 Baa'bb'Bab_le1. Qed. + +Lemma onem_Baa'bb'Bab_ge0_fix : 0 <= B a b * (1 - Baa'bb'Bab_nneg%:num). +Proof. +rewrite mulr_ge0//. + rewrite /B. + exact: beta_nat_norm_ge0. +rewrite subr_ge0. +exact: Baa'bb'Bab_le1. +Qed. + +Lemma ubeta_nat_pdf_ge0' t : 0 <= ubeta_nat_pdf a'.+1 b'.+1 t :> R. +Proof. +apply: ubeta_nat_pdf_ge0. (* TODO: needs 0 <= t <= 1 *) +Admitted. + +Lemma ubeta_nat_pdf_le1' t : (NngNum (ubeta_nat_pdf_ge0' t))%:num <= 1 :> R. +Proof. +rewrite /=. +rewrite /ubeta_nat_pdf. +rewrite /ubeta_nat_pdf'. (* TODO: needs 0 <= t <= 1 *) +Admitted. + +Lemma integral_ubeta_nat' : + (\int[ubeta_nat a b]_x (ubeta_nat_pdf a'.+1 b'.+1 x)%:E = + \int[mu]_(x in `[0%R, 1%R]) + (x ^+ a'.-1 * `1-x ^+ b'.-1 * x ^+ a * `1-x ^+ b)%:E :> \bar R)%E. +Proof. +rewrite /ubeta_nat/ubeta_nat_pdf. +Admitted. + +Lemma beta_nat_bern_bern U : + (a > 0)%N -> (b > 0)%N -> + beta_nat_bern U = + bernoulli_trunc Baa'bb'Bab U. +Proof. +rewrite /beta_nat_bern. +transitivity ((\int[beta_nat a b]_(y in `[0%R, 1%R]) + bernoulli_trunc (ubeta_nat_pdf a'.+1 b'.+1 y) U)%E : \bar R). + admit. +rewrite integral_beta_nat /=; last 2 first. + apply: (@measurableT_comp _ _ _ _ _ _ (bernoulli_trunc ^~ U)). + apply: (measurability (ErealGenInftyO.measurableE R)) => //=. + move=> /= _ [_ [x ->] <-]; apply: measurableI => //. + admit. + exact: measurable_ubeta_nat_pdf. + admit. +under eq_integral => x. + rewrite inE/= in_itv/= => x01. + rewrite bernoulli_truncE. + over. + apply/andP; split. + apply/ubeta_nat_pdf_ge0/x01. + apply/ubeta_nat_pdf_le1/x01. +rewrite /=. +rewrite bernoulli_truncE; last first. + apply/andP; split. + exact: Baa'bb'Bab_ge0. + exact: Baa'bb'Bab_le1. +under eq_integral => x _. + rewrite muleC muleDr//. + over. +rewrite integralD//=; last 2 first. + (* TODO: integrableM *) + admit. + admit. +congr (_ + _). + under eq_integral do rewrite muleA muleC. + rewrite integralZl//=; last first. + admit. + rewrite muleC. + congr (_ * _)%E. + rewrite /beta_nat_pdf. + under eq_integral do rewrite EFinM -muleA muleC -muleA. + rewrite integralZl//=; last first. + admit. + transitivity (((beta_nat_norm a b)^-1)%:E * \int[lebesgue_measure]_(x in `[0%R, 1%R]) ((ubeta_nat_pdf (a+a') (b+b') x)%:E) : \bar R)%E. + congr (_ * _)%E. + apply: eq_integral => x x01. + rewrite /ubeta_nat_pdf /ubeta_nat_pdf' muleC /onem -EFinM/=. + rewrite mulrCA -mulrA -exprD mulrA -exprD. + congr (_ ^+ _ * _ ^+ _)%:E. + rewrite -!subn1 subDnCA//. + rewrite addnC -!subn1 subDnCA//. + rewrite -beta_nat_normE. + rewrite /Baa'bb'Bab/B -!EFinM. + congr _%:E. + rewrite mulrC//. +under eq_integral do rewrite muleA muleC. +rewrite integralZl//=; last first. + admit. +rewrite muleC. +congr (_ * _)%E. +rewrite /beta_nat_pdf. +under eq_integral do rewrite EFinM -muleA muleC -muleA. +rewrite integralZl//=; last first. + admit. +transitivity (((beta_nat_norm a b)^-1)%:E * \int[lebesgue_measure]_(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. + congr (_ - _)%E. + rewrite /ubeta_nat_pdf /ubeta_nat_pdf'/=. + rewrite mulrCA -mulrA -exprD mulrA -exprD. + congr (_ ^+ _ * _ ^+ _)%:E. + rewrite addnC -!subn1 subDnCA//. + rewrite -!subn1 subDnCA//. +rewrite integralB_EFin//=; last 2 first. + admit. + admit. +rewrite -!beta_nat_normE -EFinM mulrBr /onem mulVf; last first. + rewrite /B mulf_eq0 negb_or. + apply/andP; split. + rewrite mulf_eq0 negb_or. + rewrite gt_eqF ?ltr0n ?fact_gt0//=. + rewrite gt_eqF ?ltr0n ?fact_gt0//=. + rewrite invr_eq0 gt_eqF ?ltr0n ?fact_gt0//=. +congr (_ - _)%:E. +by rewrite mulrC. +Admitted. + +End integral_beta. + Section mscore. Context d (T : measurableType d) (R : realType). Variable f : T -> R.