From b3b8a8d8bc8fbdb2f63c1478db152b30d5671c50 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 10 Apr 2024 16:49:31 +0900 Subject: [PATCH 1/4] bernoulli, binomial, uniform distr --- theories/probability.v | 488 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 486 insertions(+), 2 deletions(-) diff --git a/theories/probability.v b/theories/probability.v index c471b1b42..b1acd306f 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -2,11 +2,11 @@ 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. +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. +Require Import exp numfun lebesgue_measure lebesgue_integral kernel. (**md**************************************************************************) (* # Probability *) @@ -828,3 +828,487 @@ by rewrite /pmf fineK// fin_num_measure. Qed. End discrete_distribution. + +(* TODO: move *) +Lemma onem_nonneg_proof (R : numDomainType) (p : {nonneg R}) : + (p%:num <= 1 -> 0 <= `1-(p%:num))%R. +Proof. by rewrite /onem/= subr_ge0. Qed. + +Definition onem_nonneg (R : numDomainType) (p : {nonneg R}) + (p1 : (p%:num <= 1)%R) := + NngNum (onem_nonneg_proof p1). + +Section bernoulli. +Local Open Scope ereal_scope. +Variables (R : realType) (p : {nonneg R}) (p1 : (p%:num <= 1)%R). + +Definition bernoulli : set bool -> \bar R := measure_add + (mscale p (dirac true)) (mscale (onem_nonneg p1) (dirac false)). + +HB.instance Definition _ := Measure.on bernoulli. + +Let bernoulli_setT : bernoulli [set: _] = 1. +Proof. +rewrite /bernoulli/= measure_addE/= /mscale/= !diracT !mule1. +by rewrite -EFinD add_onemK. +Qed. + +HB.instance Definition _ := + @Measure_isProbability.Build _ _ R bernoulli bernoulli_setT. + +Lemma integral_bernoulli (f : bool -> \bar R) : (forall x, 0 <= f x) -> + \int[bernoulli]_y (f y) = p%:num%:E * f true + (`1-(p%:num))%:E * f false. +Proof. +move=> f0. +rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. +by rewrite !ge0_integral_mscale//= !integral_dirac//= !diracT !mul1e. +Qed. + +End bernoulli. + +(* TODO: move *) +Lemma sumbool_ler {R : realDomainType} (x y : R) : (x <= y)%R + (x > y)%R. +Proof. by have [_|_] := leP x y; [exact: inl|exact: inr]. Qed. + +Lemma measurable_fun_TF d1 (T1 : measurableType d1) (D : set T1) (f : T1 -> bool) : + measurable (D `&` f @^-1` [set true]) -> + measurable (D `&` f @^-1` [set false]) -> measurable_fun D f. +Proof. +move=> mT mF mD /= Y mY. +have := @subsetT _ Y; rewrite setT_bool => YT. +move: mY; have [-> _|-> _|-> _ |-> _] := subset_set2 YT. +- by rewrite preimage0 ?setI0. +- exact: mT. +- exact: mF. +- by rewrite -setT_bool preimage_setT setIT. +Qed. + +Lemma measurable_and d1 (T1 : measurableType d1) (D : set T1) + (f : T1 -> bool) (g : T1 -> bool) : + measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x && g x). +Proof. +move=> mf mg mD; apply: measurable_fun_TF => //. +- rewrite [X in measurable X](_ : _ = + D `&` f @^-1` [set true] `&` (D `&` g @^-1` [set true])); last first. + rewrite setICA !setIA setIid -setIA; congr (_ `&` _). + by apply/seteqP; split => x /andP. + by apply: measurableI; [exact: mf|exact: mg]. +- rewrite [X in measurable X](_ : _ = + D `&` f @^-1` [set false] `|` (D `&` g @^-1` [set false])); last first. + rewrite -setIUr; congr (_ `&` _). + apply/seteqP; split => x /=. + by case: (f x); case: (g x); [|right|left|left]. + by case: (f x); case: (g x) => //= -[]. + by apply: measurableU; [exact: mf|exact: mg]. +Qed. + +Lemma measurable_fun_pow d (T : measurableType d) (R : realType) (D : set T) + (f : T -> R) n : measurable_fun D f -> + measurable_fun D (fun x => f x ^+ n). +Proof. +move=> mf. +exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). +Qed. + +Section bernoulli_total. +Local Open Scope ring_scope. +Variable R : realType. +Implicit Type p : R. + +Definition bernoulli0 := @bernoulli R 0%:nng ler01. + +HB.instance Definition _ := Probability.on bernoulli0. + +Definition bernoulliT p : probability bool R := + if sumbool_ler 0 p is inl l0p then + if sumbool_ler (NngNum l0p)%:num 1%R is inl lp1 then + bernoulli lp1 + else bernoulli0 + else bernoulli0. + +Lemma bernoulliTE p U : 0 <= p <= 1 -> + (bernoulliT p U = p%:E * \d_true U + (`1-p)%:E * \d_false U)%E. +Proof. +move=> /andP[p0 p1]. +rewrite /bernoulliT; case: sumbool_ler => [{}p0/=|]; last first. + by rewrite ltNge p0. +case: sumbool_ler => [{}p1/=|]; last by rewrite ltNge p1. +by rewrite /bernoulli/= measure_addE. +Qed. + +Lemma bernoulliT_le1 p U : (bernoulliT p U <= 1)%E. +Proof. +rewrite /bernoulliT; case: sumbool_ler => //= p0; last first. + by rewrite probability_le1. +by case: sumbool_ler => //= p1; rewrite probability_le1. +Qed. + +Lemma measurable_bernoulliT : + measurable_fun setT (bernoulliT : R -> pprobability bool R). +Proof. +apply: (@measurability _ _ _ _ _ _ + (@pset _ _ _ : set (set (pprobability _ R)))) => //. +move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=. +rewrite /bernoulliT. +have := @subsetT _ Ys; rewrite setT_bool => UT. +have [->|->|->|->] /= := subset_set2 UT. +- rewrite [X in measurable_fun _ X](_ : _ = cst 0%E)//. + by apply/funext => x/=; case: sumbool_ler. +- rewrite [X in measurable_fun _ X](_ : _ = + (fun x => if 0 <= x <= 1 then x%:E else 0%E))//. + apply: measurable_fun_ifT => //=; 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). + apply/funext => x/=; case: sumbool_ler => /= x0. + case: sumbool_ler => /= x1. + rewrite x0 x1/= /bernoulli/= measure_addE/= /mscale/= !diracE. + by rewrite mem_set//= memNset//= mule0 adde0 mule1. + rewrite x0/= leNgt x1/= /bernoulli0 /bernoulli /= measure_addE/= /mscale/=. + by rewrite mul0e add0e diracE memNset//= mule0. + rewrite leNgt x0/= /bernoulli0 /bernoulli /= measure_addE/= /mscale/=. + by rewrite mul0e add0e diracE memNset//= mule0. +- rewrite [X in measurable_fun _ X](_ : _ = + (fun x => if 0 <= x <= 1 then (`1-x)%:E else 1%E))//. + apply: measurable_fun_ifT => //=. + 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). + exact/EFin_measurable_fun/measurable_funB. + apply/funext => x/=; case: sumbool_ler => /= x0. + case: sumbool_ler => /= x1. + rewrite /bernoulli/= measure_addE/= /mscale/=. + by rewrite !diracE memNset//= mule0 add0e mem_set//= mule1 x0 x1. + rewrite /bernoulli0 /bernoulli /= measure_addE/= /mscale/=. + by rewrite mul0e add0e onem0 mul1e diracE mem_set//= x0/= leNgt x1. + rewrite /bernoulli0 /bernoulli /= measure_addE/= /mscale/=. + by rewrite mul0e add0e onem0 mul1e diracE mem_set//= leNgt x0. +- rewrite [X in measurable_fun _ X](_ : _ = cst 1%E)//; apply/funext => x/=. + case: sumbool_ler => /= x0. + case: sumbool_ler => /= x1. + rewrite /bernoulli/= measure_addE/=. + by rewrite /mscale/= -setT_bool !diracT !mule1 -EFinD add_onemK. + rewrite /bernoulli0 /bernoulli/= measure_addE/=. + by rewrite /mscale/= -setT_bool !diracT mul0e mule1 add0e onem0. + rewrite /bernoulli0 /bernoulli/= measure_addE/=. + by rewrite /mscale/= -setT_bool !diracT mul0e add0e mule1 onem0. +Qed. + +Lemma measurable_bernoulliT2 U : measurable U -> + measurable_fun setT (bernoulliT ^~ U : R -> \bar R). +Proof. +by move=> ?; exact: (measurable_kernel (kprobability measurable_bernoulliT)). +Qed. + +Lemma integral_bernoulliT p (f : bool -> \bar R) : + 0 <= p <= 1 -> (forall x, 0 <= f x)%E -> + (\int[bernoulliT p]_y (f y) = p%:E * f true + (`1-p)%:E * f false)%E. +Proof. +move=> /andP[p0 p1] f0; rewrite /bernoulliT; case: sumbool_ler => [? /=|]. + case: (sumbool_ler p 1) => [? /=|]; last by rewrite ltNge p1. + by rewrite integral_bernoulli. +by rewrite ltNge p0. +Qed. + +End bernoulli_total. +Arguments bernoulliT {R}. +Arguments measurable_bernoulliT {R}. + +Section binomial_probability. +Local Open Scope ring_scope. +Context {R : realType} (n : nat) (p : {nonneg R}) (p1 : p%:num <= 1). + +Definition bin_prob (k : nat) : {nonneg R} := + (p%: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. +rewrite /bin_prob bin0 subn0/=; apply/val_inj => /=. +by rewrite expr0 mul1r mulr1n. +Qed. + +Lemma bin_prob1 : + bin_prob 1 = (p%:num * (NngNum (onem_ge0 p1))%:num^+(n-1)%N *+ n)%:nng. +Proof. by rewrite /bin_prob bin1/=; apply/val_inj => /=; rewrite expr1. Qed. + +Definition binomial_prob : set nat -> \bar R := + msum (fun k => mscale (bin_prob k) \d_k) n.+1. + +HB.instance Definition _ := Measure.on binomial_prob. + +Let binomial_setT : binomial_prob [set: _] = 1%:E. +Proof. +rewrite /binomial_prob /msum /mscale /bin_prob/= /mscale/=. +under eq_bigr do rewrite diracT mule1. +rewrite sumEFin. +under eq_bigr do rewrite mulrC. +by rewrite -exprDn_comm ?subrK ?expr1n//; exact: mulrC. +Qed. + +HB.instance Definition _ := + Measure_isProbability.Build _ _ R binomial_prob binomial_setT. + +Lemma integral_binomial (f : nat -> \bar R) : (forall x, 0 <= f x)%E -> + (\int[binomial_prob]_y (f y) = \sum_(k < n.+1) (bin_prob k)%:num%:E * f k)%E. +Proof. +move=> f0; rewrite ge0_integral_measure_sum//=; apply: eq_bigr => i _. +by rewrite ge0_integral_mscale//= integral_dirac//= diracT mul1e. +Qed. + +End binomial_probability. + +Section binomial_total. +Local Open Scope ring_scope. +Variables (R : realType) (n : nat). +Implicit Type p : R. + +Definition binomial_prob0 := @binomial_prob R 0 0%:nng ler01. + +Definition binomial_probT p : probability nat R := + if sumbool_ler 0 p is inl l0p then + if sumbool_ler (NngNum l0p)%:num 1 is inl lp1 then + @binomial_prob R n (NngNum l0p) lp1 + else binomial_prob0 + else binomial_prob0. + +Lemma measurable_binomial_probT : + measurable_fun setT (binomial_probT : R -> pprobability _ _). +Proof. +apply: (@measurability _ _ _ _ _ _ + (@pset _ _ _ : set (set (pprobability _ R)))) => //. +move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=. +rewrite /binomial_probT/=. +set f := (X in measurable_fun _ X). +rewrite (_ : f = fun x => if 0 <= x <= 1 then (\sum_(m < n.+1) + if sumbool_ler 0 x is inl l0p then + if sumbool_ler x 1 is inl lp1 then + mscale (@bin_prob _ n (NngNum l0p) lp1 m) (\d_(nat_of_ord m)) Ys + else + (x ^+ m * `1-x ^+ (n - m) *+ 'C(n, m))%:E * \d_(nat_of_ord m) Ys + else (x ^+ m * `1-x ^+ (n - m) *+ 'C(n, m))%:E * \d_(nat_of_ord m) Ys)%E + else \d_0%N Ys)//. + move=> _; apply: measurable_fun_ifT => //=. + 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). + apply: emeasurable_fun_sum => m /=. + rewrite /mscale/= [X in measurable_fun _ X](_ : _ = (fun x => + (x ^+ m * `1-x ^+ (n - m) *+ 'C(n, m))%:E * \d_(nat_of_ord m) Ys)%E); last first. + by apply:funext => x; case: sumbool_ler => // x0; case: sumbool_ler. + apply: emeasurable_funM => //; apply/EFin_measurable_fun => //. + under eq_fun do rewrite -mulr_natr. + do 2 apply: measurable_funM => //. + exact/measurable_fun_pow/measurable_funB. +rewrite {}/f; apply/funext => x. +case: sumbool_ler => /= x0; last first. + rewrite leNgt x0/= /binomial_prob /= /msum big_ord_recl/= big_ord0 /mscale. + by rewrite bin_prob0/= expr0 mul1e adde0. +rewrite x0/=; case: sumbool_ler => /= x1; last first. + rewrite (leNgt x) x1/= /binomial_prob /msum big_ord_recl/=/=. + by rewrite bin_prob0/= big_ord0 adde0 /mscale/= expr0 mul1e. +by rewrite x1. +Qed. + +Lemma integral_binomial_probT p (p0 : 0 <= p) (p1 : (NngNum p0)%:num <= 1) + (f : nat -> \bar R) : (forall x, 0 <= f x)%E -> + (\int[binomial_probT p]_y (f y) = \sum_(k < n.+1) (bin_prob n p1 k)%:num%:E * f k)%E. +Proof. +move=> f0; rewrite /binomial_probT/=; case: sumbool_ler => [? /=|]; last first. + by rewrite ltNge p0. +case: sumbool_ler => [?/=|]; last by rewrite ltNge p1. +by rewrite integral_binomial. +Qed. + +End binomial_total. +Arguments binomial_probT {R}. +Arguments measurable_binomial_probT {R}. + +Section uniform_probability. +Local Open Scope ring_scope. +Context (R : realType) (a b : R). + +Definition uniform_pdf x := if a <= x <= b then (b - a)^-1 else 0. + +Lemma uniform_pdf_ge0 x : a < b -> 0 <= uniform_pdf x. +Proof. +move=> ab; rewrite /uniform_pdf; case: ifPn => // axb. +by rewrite invr_ge0// ltW// subr_gt0. +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). +Qed. + +Local Notation mu := lebesgue_measure. + +Lemma integral_uniform_pdf U : + (\int[mu]_(x in U) (uniform_pdf x)%:E = + \int[mu]_(x in U `&` `[a, b]) (uniform_pdf x)%:E)%E. +Proof. +rewrite [RHS]integral_mkcondr/=; apply: eq_integral => x xU. +rewrite patchE; case: ifPn => //. +rewrite notin_set/= in_itv/= => /negP/negbTE xab. +by rewrite /uniform_pdf xab. +Qed. + +Lemma integral_uniform_pdf1 A (ab : a < b) : `[a, b] `<=` A -> + (\int[mu]_(x in A) (uniform_pdf x)%:E = 1)%E. +Proof. +move=> abA; rewrite integral_uniform_pdf setIidr//. +rewrite (eq_integral (fun=> (b - a)^-1%:E)); last first. + by move=> x; rewrite inE/= in_itv/= /uniform_pdf => ->. +rewrite integral_cst//= lebesgue_measure_itv/= lte_fin. +by rewrite ab -EFinD -EFinM mulVf// gt_eqF// subr_gt0. +Qed. + +Definition uniform_prob (ab : a < b) : set _ -> \bar R := + fun U => (\int[mu]_(x in U) (uniform_pdf x)%:E)%E. + +Hypothesis ab : (a < b)%R. + +Let uniform0 : uniform_prob ab set0 = 0. +Proof. by rewrite /uniform_prob integral_set0. Qed. + +Let uniform_ge0 U : (0 <= uniform_prob ab U)%E. +Proof. +by apply: integral_ge0 => /= x Ux; rewrite lee_fin uniform_pdf_ge0. +Qed. + +Lemma integrable_uniform_pdf : + mu.-integrable setT (fun x => (uniform_pdf x)%:E). +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. + over. +by rewrite /= integral_uniform_pdf1 ?ltry// -subr_gt0. +Qed. + +Let uniform_sigma_additive : semi_sigma_additive (uniform_prob ab). +Proof. +move=> /= F mF tF mUF; rewrite /uniform_prob; apply: cvg_toP. + apply: ereal_nondecreasing_is_cvgn => m n mn. + apply: lee_sum_nneg_natr => // k _ _. + by apply: integral_ge0 => /= x Fkx; rewrite lee_fin uniform_pdf_ge0. +rewrite ge0_integral_bigcup//=. +- by apply: integrableS; [| | | exact: integrable_uniform_pdf]. +- by move=> x _; rewrite lee_fin uniform_pdf_ge0. +Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ (uniform_prob ab) + uniform0 uniform_ge0 uniform_sigma_additive. + +Let uniform_setT : uniform_prob ab [set: _] = 1%:E. +Proof. by rewrite /uniform_prob /mscale/= integral_uniform_pdf1. Qed. + +HB.instance Definition _ := @Measure_isProbability.Build _ _ R + (uniform_prob ab) uniform_setT. + +Lemma dominates_uniform_prob : uniform_prob ab `<< mu. +Proof. +move=> A mA muA0; rewrite /uniform_prob integral_uniform_pdf. +apply/eqP; rewrite eq_le; apply/andP; split; last first. + apply: integral_ge0 => x [Ax /=]; rewrite in_itv /= => xab. + by rewrite lee_fin uniform_pdf_ge0. +apply: (@le_trans _ _ + (\int[mu]_(x in A `&` `[a, b]%classic) (b - a)^-1%:E))%E; last first. + rewrite integral_cst//= ?mul1e//. + by rewrite pmule_rle0 ?lte_fin ?invr_gt0// ?subr_gt0// -muA0 measureIl. + exact: measurableI. +apply: ge0_le_integral => //=. +- exact: measurableI. +- by move=> x [Ax]; rewrite /= in_itv/= => axb; rewrite lee_fin uniform_pdf_ge0. +- by apply/EFin_measurable_fun/measurable_funTS; exact: measurable_uniform_pdf. +- by move=> x [Ax _]; rewrite lee_fin invr_ge0// ltW// subr_gt0. +- by move=> x [Ax]; rewrite in_itv/= /uniform_pdf => ->. +Qed. + +Let integral_uniform_indic E : measurable E -> + (\int[uniform_prob ab]_x (\1_E x)%:E = + (b - a)^-1%:E * \int[mu]_(x in `[a, b]) (\1_E x)%:E)%E. +Proof. +move=> mE; rewrite integral_indic//= /uniform_prob setIT -ge0_integralZl//=. +- rewrite [LHS]integral_mkcond/= [RHS]integral_mkcond/=. + apply: eq_integral => x _; rewrite !patchE; case: ifPn => xE. + case: ifPn. + rewrite inE/= in_itv/= => xab. + by rewrite /uniform_pdf xab indicE xE mule1. + by rewrite notin_set/= in_itv/= => /negP/negbTE; rewrite /uniform_pdf => ->. + case: ifPn => //. + by rewrite inE/= in_itv/= => axb; rewrite indicE (negbTE xE) mule0. +- exact/EFin_measurable_fun/measurable_indic. +- by move=> x _; rewrite lee_fin. +- by rewrite lee_fin invr_ge0// ltW// subr_gt0. +Qed. + +Let integral_uniform_nnsfun (f : {nnsfun _ >-> R}) : + (\int[uniform_prob ab]_x (f x)%:E = + (b - a)^-1%:E * \int[mu]_(x in `[a, b]) (f x)%:E)%E. +Proof. +under [LHS]eq_integral do rewrite fimfunE -fsumEFin//. +rewrite [LHS]ge0_integral_fsum//; last 2 first. + - by move=> r; exact/EFin_measurable_fun/measurableT_comp. + - by move=> n x _; rewrite EFinM nnfun_muleindic_ge0. +rewrite -[RHS]ge0_integralZl//; last 3 first. + - exact/EFin_measurable_fun/measurable_funTS. + - by move=> x _; rewrite lee_fin. + - by rewrite lee_fin invr_ge0// ltW// subr_gt0. +under [RHS]eq_integral. + move=> x xD; rewrite fimfunE -fsumEFin// ge0_mule_fsumr; last first. + by move=> r; rewrite EFinM nnfun_muleindic_ge0. + over. +rewrite [RHS]ge0_integral_fsum//; last 2 first. + - by move=> r; apply/EFin_measurable_fun; do 2 apply/measurableT_comp => //. + - move=> n x _; rewrite EFinM mule_ge0//; last by rewrite nnfun_muleindic_ge0. + by rewrite lee_fin invr_ge0// ltW// subr_gt0. +apply: eq_fsbigr => r _; rewrite ge0_integralZl//. +- by rewrite !integralZl_indic_nnsfun//= integral_uniform_indic// muleCA. +- exact/EFin_measurable_fun/measurableT_comp. +- by move=> t _; rewrite nnfun_muleindic_ge0. +- by rewrite lee_fin invr_ge0// ltW// subr_gt0. +Qed. + +Lemma integral_uniform (f : _ -> \bar R) : + measurable_fun setT f -> (forall x, 0 <= f x)%E -> + (\int[uniform_prob ab]_x f x = (b - a)^-1%:E * \int[mu]_(x in `[a, b]) f x)%E. +Proof. +move=> mf f0. +have [f_ [ndf_ f_f]] := approximation measurableT mf (fun y _ => f0 y). +transitivity (lim (\int[uniform_prob ab]_x (f_ n x)%:E @[n --> \oo])%E). + rewrite -monotone_convergence//=. + - apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //=. + exact: f_f. + - by move=> n; exact/EFin_measurable_fun/measurable_funTS. + - by move=> n ? _; rewrite lee_fin. + - by move=> ? _ ? ? mn; rewrite lee_fin; exact/lefP/ndf_. +rewrite [X in _ = (_ * X)%E](_ : _ = lim + (\int[mu]_(x in `[a, b]) (f_ n x)%:E @[n --> \oo])%E); last first. + rewrite -monotone_convergence//=. + - by apply: eq_integral => ? /[!inE] xD; apply/esym/cvg_lim => //; exact: f_f. + - by move=> n; exact/EFin_measurable_fun/measurable_funTS. + - by move=> n ? _; rewrite lee_fin. + - by move=> ? _ ? ? /ndf_ /lefP; rewrite lee_fin. +rewrite -limeMl//. + by apply: congr_lim; apply/funext => n /=; exact: integral_uniform_nnsfun. +apply/ereal_nondecreasing_is_cvgn => x y xy; apply: ge0_le_integral => //=. +- by move=> ? _; rewrite lee_fin. +- exact/EFin_measurable_fun/measurable_funTS. +- by move=> ? _; rewrite lee_fin. +- exact/EFin_measurable_fun/measurable_funTS. +- by move=> ? _; rewrite lee_fin; move/ndf_ : xy => /lefP. +Qed. + +End uniform_probability. From 36e280d18914ffdf5783b7b2ac5fae03f6527913 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 8 May 2024 23:42:00 +0900 Subject: [PATCH 2/4] improvements --- theories/kernel.v | 87 +++--- theories/lebesgue_integral.v | 37 ++- theories/lebesgue_measure.v | 14 + theories/measure.v | 30 ++ theories/probability.v | 533 +++++++++++++++++++---------------- 5 files changed, 408 insertions(+), 293 deletions(-) diff --git a/theories/kernel.v b/theories/kernel.v index 74b2a0342..821974a20 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -132,7 +132,7 @@ Lemma measurable_fun_kseries (U : set Y) : measurable U -> measurable_fun [set: X] (kseries ^~ U). Proof. move=> mU. -by apply: ge0_emeasurable_fun_sum => // n; exact/measurable_kernel. +by apply: ge0_emeasurable_fun_sum => // n _; exact/measurable_kernel. Qed. HB.instance Definition _ := @@ -506,7 +506,7 @@ Variable k : X * Y -> \bar R. Lemma measurable_fun_xsection_integral (l : X -> {measure set Y -> \bar R}) - (k_ : ({nnsfun [the measurableType _ of X * Y] >-> R})^nat) + (k_ : {nnsfun (X * Y) >-> R}^nat) (ndk_ : nondecreasing_seq (k_ : (X * Y -> R)^nat)) (k_k : forall z, (k_ n z)%:E @[n --> \oo] --> k z) : (forall n r, @@ -585,7 +585,7 @@ have [l_ hl_] := sfinite_kernel l. rewrite (_ : (fun x => _) = (fun x => mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first. by apply/funext => x; rewrite hl_//; exact/measurable_xsection. -apply: ge0_emeasurable_fun_sum => // m. +apply: ge0_emeasurable_fun_sum => // m _. by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. Qed. @@ -614,7 +614,7 @@ Qed. HB.instance Definition _ := isKernel.Build _ _ _ _ _ (kdirac mf) measurable_fun_kdirac. -Let kdirac_prob x : kdirac mf x setT = 1. +Let kdirac_prob x : kdirac mf x [set: Y] = 1. Proof. by rewrite /kdirac/= diracT. Qed. HB.instance Definition _ := Kernel_isProbability.Build _ _ _ _ _ @@ -717,46 +717,14 @@ HB.instance Definition _ t := Kernel_isFinite.Build _ _ _ _ R (kadd k1 k2) kadd_finite_uub. End fkadd. -Lemma measurable_fun_mnormalize d d' (X : measurableType d) - (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) : - measurable_fun [set: X] (fun x => - [the probability _ _ of mnormalize (k x) point] : pprobability Y R). -Proof. -apply: (@measurability _ _ _ _ _ _ - (@pset _ _ _ : set (set (pprobability Y R)))) => //. -move=> _ -[_ [r r01] [Ys mYs <-]] <-. -rewrite /mnormalize /mset /preimage/=. -apply: emeasurable_fun_infty_o => //. -rewrite /mnormalize/=. -rewrite (_ : (fun x => _) = (fun x => if (k x setT == 0) || (k x setT == +oo) - then \d_point Ys else k x Ys * ((fine (k x setT))^-1)%:E)); last first. - by apply/funext => x/=; case: ifPn. -apply: measurable_fun_if => //. -- apply: (measurable_fun_bool true) => //. - rewrite (_ : _ @^-1` _ = [set t | k t setT == 0] `|` - [set t | k t setT == +oo]); last first. - by apply/seteqP; split=> x /= /orP//. - by apply: measurableU; exact: kernel_measurable_eq_cst. -- apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel. - apply/EFin_measurable_fun; rewrite setTI. - apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]). - + exact: open_measurable. - + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey. - + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0. - exact: inv_continuous. - + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel. -Qed. - Section knormalize. Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). Variable f : R.-ker X ~> Y. Definition knormalize (P : probability Y R) : X -> {measure set Y -> \bar R} := - fun x => [the measure _ _ of mnormalize (f x) P]. - -Variable P : probability Y R. + fun x => mnormalize (f x) P. -Let measurable_fun_knormalize U : +Let measurable_knormalize (P : probability Y R) U : measurable U -> measurable_fun [set: X] (knormalize P ^~ U). Proof. move=> mU; rewrite /knormalize/= /mnormalize /=. @@ -773,7 +741,7 @@ apply: measurable_fun_if => //. - apply: (@measurable_funS _ _ _ _ setT) => //. exact: kernel_measurable_fun_eq_cst. - apply: emeasurable_funM. - by have := measurable_kernel f U mU; exact: measurable_funS. + exact: measurable_funS (measurable_kernel f U mU). apply/EFin_measurable_fun. apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]) => //. + exact: open_measurable. @@ -786,17 +754,48 @@ apply: measurable_fun_if => //. by have := measurable_kernel f _ measurableT; exact: measurable_funS. Qed. -HB.instance Definition _ := isKernel.Build _ _ _ _ R (knormalize P) - measurable_fun_knormalize. +HB.instance Definition _ (P : probability Y R) := + isKernel.Build _ _ _ _ R (knormalize P) (measurable_knormalize P). -Let knormalize1 x : knormalize P x [set: Y] = 1. +Let knormalize1 (P : probability Y R) x : knormalize P x [set: Y] = 1. Proof. by rewrite /knormalize/= probability_setT. Qed. -HB.instance Definition _ := - @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) knormalize1. +HB.instance Definition _ (P : probability Y R):= + @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) (knormalize1 P). End knormalize. +(* TODO: useful? *) +Lemma measurable_fun_mnormalize d d' (X : measurableType d) + (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) : + measurable_fun [set: X] (fun x => + [the probability _ _ of mnormalize (k x) point] : pprobability Y R). +Proof. +apply: (@measurability _ _ _ _ _ _ + (@pset _ _ _ : set (set (pprobability Y R)))) => //. +move=> _ -[_ [r r01] [Ys mYs <-]] <-. +rewrite /mnormalize /mset /preimage/=. +apply: emeasurable_fun_infty_o => //. +rewrite /mnormalize/=. +rewrite (_ : (fun x => _) = (fun x => if (k x setT == 0) || (k x setT == +oo) + then \d_point Ys else k x Ys * ((fine (k x setT))^-1)%:E)); last first. + by apply/funext => x/=; case: ifPn. +apply: measurable_fun_if => //. +- apply: (measurable_fun_bool true) => //. + rewrite (_ : _ @^-1` _ = [set t | k t setT == 0] `|` + [set t | k t setT == +oo]); last first. + by apply/seteqP; split=> x /= /orP//. + by apply: measurableU; exact: kernel_measurable_eq_cst. +- apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel. + apply/EFin_measurable_fun; rewrite setTI. + apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]). + + exact: open_measurable. + + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey. + + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0. + exact: inv_continuous. + + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel. +Qed. + Section kcomp_def. Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2) (Z : measurableType d3) (R : realType). diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 488b4b005..f59201b04 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -1969,15 +1969,30 @@ move=> fs mh; under eq_fun do rewrite fsbig_finite//. exact: emeasurable_fun_sum. Qed. -Lemma ge0_emeasurable_fun_sum D (h : nat -> (T -> \bar R)) : - (forall k x, 0 <= h k x) -> (forall k, measurable_fun D (h k)) -> - measurable_fun D (fun x => \sum_(i h0 mh; rewrite [X in measurable_fun _ X](_ : _ = - (fun x => limn_esup (fun n => \sum_(0 <= i < n) h i x))); last first. +Lemma ge0_emeasurable_fun_sum D (h : nat -> (T -> \bar R)) (P : pred nat) : + (forall k x, D x -> P k -> 0 <= h k x) -> (forall k, P k -> measurable_fun D (h k)) -> + measurable_fun D (fun x => \sum_(i h0 mh. +move=> mD; move: (mD). +apply/(@measurable_restrict _ _ _ _ _ setT) => //. +rewrite [X in measurable_fun _ X](_ : _ = + (fun x => \sum_(0 <= i x/=; rewrite /patch; case: ifPn => // xD. + by rewrite eseries0. +rewrite [X in measurable_fun _ X](_ : _ = + (fun x => limn_esup (fun n => \sum_(0 <= i < n | P i) (h i) \_ D x))); last first. apply/funext=> x; rewrite is_cvg_limn_esupE//. - exact: is_cvg_ereal_nneg_natsum. -by apply: measurable_fun_limn_esup => k; exact: emeasurable_fun_sum. + apply: is_cvg_nneseries_cond => n Pn; rewrite patchE. + by case: ifPn => // xD; rewrite h0//; exact/set_mem. +apply: measurable_fun_limn_esup => k. +under eq_fun do rewrite big_mkcond. +apply: emeasurable_fun_sum => n. +have [|] := boolP (n \in P). + rewrite /in_mem/= => Pn; rewrite Pn. + by apply/(measurable_restrict (h n)) => //; exact: mh. +by rewrite /in_mem/= => /negbTE ->. Qed. Lemma emeasurable_funB D f g : @@ -5262,7 +5277,7 @@ rewrite ge0_integralZl//; last by rewrite lee_fin. - by move=> y _; rewrite lee_fin. Qed. -Lemma sfun_measurable_fun_fubini_tonelli_F : measurable_fun setT F. +Lemma sfun_measurable_fun_fubini_tonelli_F : measurable_fun [set: T1] F. Proof. rewrite sfun_fubini_tonelli_FE//; apply: emeasurable_fun_fsum => // r. exact/measurable_funeM/measurable_fun_xsection. @@ -5703,8 +5718,8 @@ transitivity (\sum_(n \sum_(n x. by rewrite ge0_integral_measure_series//; exact/measurableT_comp. - apply: ge0_emeasurable_fun_sum; first by move=> k x; exact: integral_ge0. - by move=> k; apply: measurable_fun_fubini_tonelli_F. + apply: ge0_emeasurable_fun_sum; first by move=> k x *; exact: integral_ge0. + by move=> k _; exact: measurable_fun_fubini_tonelli_F. apply: eq_eseriesr => n _; apply: eq_integral => x _. by rewrite ge0_integral_measure_series//; exact/measurableT_comp. transitivity (\sum_(n mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. - by rewrite preimage_setT setIT. Qed. +Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x <= g x). +Proof. +move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. +- under eq_fun do rewrite -subr_ge0. + rewrite preimage_true -preimage_itv_c_infty. + by apply: (measurable_funB mg mf) => //; exact: measurable_itv. +- under eq_fun do rewrite leNgt -subr_gt0. + rewrite preimage_false set_predC setCK -preimage_itv_o_infty. + by apply: (measurable_funB mf mg) => //; exact: measurable_itv. +- by rewrite preimage_set0 setI0. +- by rewrite preimage_setT setIT. +Qed. + Lemma measurable_maxr D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \max g). Proof. diff --git a/theories/measure.v b/theories/measure.v index 259b796dc..0b5b9d509 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1177,6 +1177,36 @@ have [-> _|-> _|-> _ |-> _] := subset_set2 YT. - by rewrite -setT_bool preimage_setT setIT. Qed. +Lemma measurable_fun_TF D (f : T1 -> bool) : + measurable (D `&` f @^-1` [set true]) -> + measurable (D `&` f @^-1` [set false]) -> + measurable_fun D f. +Proof. +move=> mT mF mD /= Y mY. +have := @subsetT _ Y; rewrite setT_bool => YT. +move: mY; have [-> _|-> _|-> _ |-> _] := subset_set2 YT. +- by rewrite preimage0 ?setI0. +- exact: mT. +- exact: mF. +- by rewrite -setT_bool preimage_setT setIT. +Qed. + +Lemma measurable_and D (f : T1 -> bool) (g : T1 -> bool) : + measurable_fun D f -> measurable_fun D g -> + measurable_fun D (fun x => f x && g x). +Proof. +move=> mf mg mD; apply: measurable_fun_TF => //. +- rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `&` + (D `&` g @^-1` [set true])); last first. + by rewrite setIACA setIid; congr (_ `&` _); apply/seteqP; split => x /andP. + by apply: measurableI; [exact: mf|exact: mg]. +- rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set false] `|` + (D `&` g @^-1` [set false])); last first. + rewrite -setIUr; congr (_ `&` _). + by apply/seteqP; split => x /=; case: (f x); case: (g x); tauto. +- by apply: measurableU; [exact: mf|exact: mg]. +Qed. + End measurable_fun. #[global] Hint Extern 0 (measurable_fun _ (fun=> _)) => solve [apply: measurable_cst] : core. diff --git a/theories/probability.v b/theories/probability.v index b1acd306f..b7d24ce98 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -838,191 +838,267 @@ Definition onem_nonneg (R : numDomainType) (p : {nonneg R}) (p1 : (p%:num <= 1)%R) := NngNum (onem_nonneg_proof p1). +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 = \sum_(0 <= i 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 measurable_fun_pow {R : realType} D (f : R -> R) n : measurable_fun D f -> + measurable_fun D (fun x => f x ^+ n). +Proof. +move=> mf. +apply: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f) => //. +Qed. + +Lemma measurable_natmul {R : realType} D n : + measurable_fun D ((@GRing.natmul R)^~ n). +Proof. +under eq_fun do rewrite -mulr_natr. +by do 2 apply: measurable_funM => //. +Qed. +(* /TODO: move *) + +Section bernoulli_pmf. +Context {R : realType} (p : R). +Local Open Scope ring_scope. + +Definition bernoulli_pmf b := if b then p else 1 - p. + +Lemma bernoulli_pmf_ge0 (p01 : 0 <= p <= 1) b : 0 <= bernoulli_pmf b. +Proof. +rewrite /bernoulli_pmf. +by move: p01 => /andP[p0 p1]; case: ifPn => // _; rewrite subr_ge0. +Qed. + +Lemma bernoulli_pmf1 (p01 : 0 <= p <= 1) : + \sum_(i \in [set: bool]) (bernoulli_pmf i)%:E = 1%E. +Proof. +rewrite setT_bool fsbigU//=; last by move=> x [/= ->]. +by rewrite !fsbig_set1/= -EFinD addrCA subrr addr0. +Qed. + +End bernoulli_pmf. + +Lemma measurable_bernoulli_pmf {R : realType} D n : + measurable_fun D (@bernoulli_pmf R ^~ n). +Proof. +by apply/measurable_funTS/measurable_fun_if => //=; exact: measurable_funB. +Qed. + +Definition bernoulli {R : realType} (p : R) : set bool -> \bar R := fun A => + if (0 <= p <= 1)%R then \sum_(b \in A) (bernoulli_pmf p b)%:E else \d_false A. + Section bernoulli. -Local Open Scope ereal_scope. -Variables (R : realType) (p : {nonneg R}) (p1 : (p%:num <= 1)%R). +Context {R : realType} (p : R). + +Local Notation bernoulli := (bernoulli p). -Definition bernoulli : set bool -> \bar R := measure_add - (mscale p (dirac true)) (mscale (onem_nonneg p1) (dirac false)). +Let bernoulli0 : bernoulli set0 = 0. +Proof. +by rewrite /bernoulli; case: ifPn => // p01; rewrite fsbig_set0. +Qed. -HB.instance Definition _ := Measure.on bernoulli. +Let bernoulli_ge0 U : (0 <= bernoulli U)%E. +Proof. +rewrite /bernoulli; case: ifPn => // p01. +rewrite fsbig_finite//= sumEFin lee_fin. +by apply: sumr_ge0 => /= b _; exact: bernoulli_pmf_ge0. +Qed. -Let bernoulli_setT : bernoulli [set: _] = 1. +Let bernoulli_sigma_additive : semi_sigma_additive bernoulli. Proof. -rewrite /bernoulli/= measure_addE/= /mscale/= !diracT !mule1. -by rewrite -EFinD add_onemK. +move=> F mF tF mUF; rewrite /bernoulli; case: ifPn => p01; last first. + exact: measure_semi_sigma_additive. +apply: cvg_toP. + apply: ereal_nondecreasing_is_cvgn => m n mn. + apply: lee_sum_nneg_natr => // k _ _. + rewrite fsbig_finite//= sumEFin lee_fin. + by apply: sumr_ge0 => /= b _; exact: bernoulli_pmf_ge0. +transitivity (\sum_(0 <= i k _; rewrite esum_fset//= => b _. + by 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. + +HB.instance Definition _ := isMeasure.Build _ _ _ bernoulli + bernoulli0 bernoulli_ge0 bernoulli_sigma_additive. + +Let bernoulli_setT : bernoulli [set: _] = 1%E. +Proof. +rewrite /bernoulli/=; case: ifPn => p01; last by rewrite probability_setT. +by rewrite bernoulli_pmf1. Qed. HB.instance Definition _ := @Measure_isProbability.Build _ _ R bernoulli bernoulli_setT. +End bernoulli. + +Section bernoulli_measure. +Context {R : realType}. +Variables (p : R) (p0 : (0 <= p)%R) (p1 : ((NngNum p0)%:num <= 1)%R). + +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. +rewrite measure_addE/= /mscale/=. +have := @subsetT _ U; rewrite setT_bool => UT. +have [->|->|->|->] /= := subset_set2 UT. +- rewrite -esum_fset//=; last by move=> b; rewrite lee_fin bernoulli_pmf_ge0. + by rewrite esum_set0 2!measure0 2!mule0 adde0. +- rewrite -esum_fset//=; last by move=> b; rewrite lee_fin bernoulli_pmf_ge0. + rewrite esum_set1/= ?lee_fin// 2!diracE mem_set//= memNset//= mule0 adde0. + by rewrite mule1. +- rewrite -esum_fset//=; last by move=> b; rewrite lee_fin bernoulli_pmf_ge0. + rewrite esum_set1/= ?lee_fin ?subr_ge0// 2!diracE memNset//= mem_set//=. + by rewrite mule0 add0e mule1. +- rewrite fsbigU//=; last by move=> x [->]. + by rewrite 2!fsbig_set1/= -setT_bool 2!diracT !mule1. +Qed. + +End bernoulli_measure. +Arguments bernoulli {R}. + +Section integral_bernoulli. +Context {R : realType}. +Variables (p : R) (p01 : (0 <= p <= 1)%R). +Local Open Scope ereal_scope. + +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]_y (f y) = p%:num%:E * f true + (`1-(p%:num))%:E * f false. + \int[bernoulli p]_y (f y) = p%:E * f true + (`1-p)%:E * f false. Proof. -move=> f0. +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. -End bernoulli. +End integral_bernoulli. -(* TODO: move *) -Lemma sumbool_ler {R : realDomainType} (x y : R) : (x <= y)%R + (x > y)%R. -Proof. by have [_|_] := leP x y; [exact: inl|exact: inr]. Qed. - -Lemma measurable_fun_TF d1 (T1 : measurableType d1) (D : set T1) (f : T1 -> bool) : - measurable (D `&` f @^-1` [set true]) -> - measurable (D `&` f @^-1` [set false]) -> measurable_fun D f. -Proof. -move=> mT mF mD /= Y mY. -have := @subsetT _ Y; rewrite setT_bool => YT. -move: mY; have [-> _|-> _|-> _ |-> _] := subset_set2 YT. -- by rewrite preimage0 ?setI0. -- exact: mT. -- exact: mF. -- by rewrite -setT_bool preimage_setT setIT. -Qed. - -Lemma measurable_and d1 (T1 : measurableType d1) (D : set T1) - (f : T1 -> bool) (g : T1 -> bool) : - measurable_fun D f -> measurable_fun D g -> - measurable_fun D (fun x => f x && g x). -Proof. -move=> mf mg mD; apply: measurable_fun_TF => //. -- rewrite [X in measurable X](_ : _ = - D `&` f @^-1` [set true] `&` (D `&` g @^-1` [set true])); last first. - rewrite setICA !setIA setIid -setIA; congr (_ `&` _). - by apply/seteqP; split => x /andP. - by apply: measurableI; [exact: mf|exact: mg]. -- rewrite [X in measurable X](_ : _ = - D `&` f @^-1` [set false] `|` (D `&` g @^-1` [set false])); last first. - rewrite -setIUr; congr (_ `&` _). - apply/seteqP; split => x /=. - by case: (f x); case: (g x); [|right|left|left]. - by case: (f x); case: (g x) => //= -[]. - by apply: measurableU; [exact: mf|exact: mg]. -Qed. - -Lemma measurable_fun_pow d (T : measurableType d) (R : realType) (D : set T) - (f : T -> R) n : measurable_fun D f -> - measurable_fun D (fun x => f x ^+ n). +Section measurable_bernoulli. +Local Open Scope ring_scope. +Variable R : realType. +Implicit Type p : R. + +Lemma measurable_bernoulli : + measurable_fun setT (bernoulli : R -> pprobability bool R). Proof. -move=> mf. -exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). +apply: (@measurability _ _ _ _ _ _ + (@pset _ _ _ : set (set (pprobability _ R)))) => //. +move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=. +apply: measurable_fun_if => //=. + 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]. + by rewrite fsbig_finite//=. +apply: emeasurable_fun_sum => n. +move=> k Ysk; apply/measurableT_comp => //. +exact: measurable_bernoulli_pmf. +Qed. + +Lemma measurable_bernoulli2 U : measurable U -> + measurable_fun setT (bernoulli ^~ U : R -> \bar R). +Proof. +by move=> ?; exact: (measurable_kernel (kprobability measurable_bernoulli)). Qed. -Section bernoulli_total. +End measurable_bernoulli. +Arguments measurable_bernoulli {R}. + +Section binomial_pmf. Local Open Scope ring_scope. -Variable R : realType. -Implicit Type p : R. +Context {R : realType} (n : nat) (p : R). -Definition bernoulli0 := @bernoulli R 0%:nng ler01. +Definition binomial_pmf k := p ^+ k * (`1-p) ^+ (n - k) *+ 'C(n, k). -HB.instance Definition _ := Probability.on bernoulli0. +Lemma binomial_pmf_ge0 k (p01 : (0 <= p <= 1)%R) : 0 <= binomial_pmf k. +Proof. +move: p01 => /andP[p0 p1]; rewrite mulrn_wge0// mulr_ge0// ?exprn_ge0//. +exact: onem_ge0. +Qed. -Definition bernoulliT p : probability bool R := - if sumbool_ler 0 p is inl l0p then - if sumbool_ler (NngNum l0p)%:num 1%R is inl lp1 then - bernoulli lp1 - else bernoulli0 - else bernoulli0. +End binomial_pmf. -Lemma bernoulliTE p U : 0 <= p <= 1 -> - (bernoulliT p U = p%:E * \d_true U + (`1-p)%:E * \d_false U)%E. +Lemma measurable_binomial_pmf {R : realType} D n k : + measurable_fun D (@binomial_pmf R n ^~ k). Proof. -move=> /andP[p0 p1]. -rewrite /bernoulliT; case: sumbool_ler => [{}p0/=|]; last first. - by rewrite ltNge p0. -case: sumbool_ler => [{}p1/=|]; last by rewrite ltNge p1. -by rewrite /bernoulli/= measure_addE. +apply: (@measurableT_comp _ _ _ _ _ _ (fun x : R => x *+ 'C(n, k))%R) => /=. + exact: measurable_natmul. +apply: measurable_funM => //=; apply: measurable_fun_pow. +exact: measurable_funB. Qed. -Lemma bernoulliT_le1 p U : (bernoulliT p U <= 1)%E. +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_0%N U. + +Section binomial. +Context {R : realType} (n : nat) (p : R). +Local Open Scope ereal_scope. + +Local Notation binomial := (binomial_prob n p). + +Let binomial0 : binomial set0 = 0. +Proof. by rewrite /binomial measure0; case: ifPn => //; rewrite esum_set0. Qed. + +Let binomial_ge0 U : 0 <= binomial U. Proof. -rewrite /bernoulliT; case: sumbool_ler => //= p0; last first. - by rewrite probability_le1. -by case: sumbool_ler => //= p1; rewrite probability_le1. +rewrite /binomial; case: ifPn => // p01; apply: esum_ge0 => /= k Uk. +by rewrite lee_fin binomial_pmf_ge0. Qed. -Lemma measurable_bernoulliT : - measurable_fun setT (bernoulliT : R -> pprobability bool R). +Let binomial_sigma_additive : semi_sigma_additive binomial. Proof. -apply: (@measurability _ _ _ _ _ _ - (@pset _ _ _ : set (set (pprobability _ R)))) => //. -move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=. -rewrite /bernoulliT. -have := @subsetT _ Ys; rewrite setT_bool => UT. -have [->|->|->|->] /= := subset_set2 UT. -- rewrite [X in measurable_fun _ X](_ : _ = cst 0%E)//. - by apply/funext => x/=; case: sumbool_ler. -- rewrite [X in measurable_fun _ X](_ : _ = - (fun x => if 0 <= x <= 1 then x%:E else 0%E))//. - apply: measurable_fun_ifT => //=; 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). - apply/funext => x/=; case: sumbool_ler => /= x0. - case: sumbool_ler => /= x1. - rewrite x0 x1/= /bernoulli/= measure_addE/= /mscale/= !diracE. - by rewrite mem_set//= memNset//= mule0 adde0 mule1. - rewrite x0/= leNgt x1/= /bernoulli0 /bernoulli /= measure_addE/= /mscale/=. - by rewrite mul0e add0e diracE memNset//= mule0. - rewrite leNgt x0/= /bernoulli0 /bernoulli /= measure_addE/= /mscale/=. - by rewrite mul0e add0e diracE memNset//= mule0. -- rewrite [X in measurable_fun _ X](_ : _ = - (fun x => if 0 <= x <= 1 then (`1-x)%:E else 1%E))//. - apply: measurable_fun_ifT => //=. - 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). - exact/EFin_measurable_fun/measurable_funB. - apply/funext => x/=; case: sumbool_ler => /= x0. - case: sumbool_ler => /= x1. - rewrite /bernoulli/= measure_addE/= /mscale/=. - by rewrite !diracE memNset//= mule0 add0e mem_set//= mule1 x0 x1. - rewrite /bernoulli0 /bernoulli /= measure_addE/= /mscale/=. - by rewrite mul0e add0e onem0 mul1e diracE mem_set//= x0/= leNgt x1. - rewrite /bernoulli0 /bernoulli /= measure_addE/= /mscale/=. - by rewrite mul0e add0e onem0 mul1e diracE mem_set//= leNgt x0. -- rewrite [X in measurable_fun _ X](_ : _ = cst 1%E)//; apply/funext => x/=. - case: sumbool_ler => /= x0. - case: sumbool_ler => /= x1. - rewrite /bernoulli/= measure_addE/=. - by rewrite /mscale/= -setT_bool !diracT !mule1 -EFinD add_onemK. - rewrite /bernoulli0 /bernoulli/= measure_addE/=. - by rewrite /mscale/= -setT_bool !diracT mul0e mule1 add0e onem0. - rewrite /bernoulli0 /bernoulli/= measure_addE/=. - by rewrite /mscale/= -setT_bool !diracT mul0e add0e mule1 onem0. -Qed. - -Lemma measurable_bernoulliT2 U : measurable U -> - measurable_fun setT (bernoulliT ^~ U : R -> \bar R). -Proof. -by move=> ?; exact: (measurable_kernel (kprobability measurable_bernoulliT)). -Qed. - -Lemma integral_bernoulliT p (f : bool -> \bar R) : - 0 <= p <= 1 -> (forall x, 0 <= f x)%E -> - (\int[bernoulliT p]_y (f y) = p%:E * f true + (`1-p)%:E * f false)%E. -Proof. -move=> /andP[p0 p1] f0; rewrite /bernoulliT; case: sumbool_ler => [? /=|]. - case: (sumbool_ler p 1) => [? /=|]; last by rewrite ltNge p1. - by rewrite integral_bernoulli. -by rewrite ltNge p0. -Qed. - -End bernoulli_total. -Arguments bernoulliT {R}. -Arguments measurable_bernoulliT {R}. +move=> F mF tF mUF; rewrite /binomial; case: ifPn => p01; last first. + exact: measure_semi_sigma_additive. +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. +by rewrite nneseries_sum_bigcup// => i; rewrite lee_fin binomial_pmf_ge0. +Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ binomial + binomial0 binomial_ge0 binomial_sigma_additive. + +Let binomial_setT : binomial [set: _] = 1. +Proof. +rewrite /binomial; case: ifPn; last by move=> _; rewrite probability_setT. +move=> p01; rewrite /binomial_pmf. +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. + 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 addrC add_onemK expr1n. +Qed. + +HB.instance Definition _ := + @Measure_isProbability.Build _ _ R binomial binomial_setT. + +End binomial. Section binomial_probability. Local Open Scope ring_scope. -Context {R : realType} (n : nat) (p : {nonneg R}) (p1 : p%:num <= 1). +Context {R : realType} (n : nat) (p : R) + (p0 : (0 <= p)%R) (p1 : ((NngNum p0)%:num <= 1)%R). Definition bin_prob (k : nat) : {nonneg R} := - (p%: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. @@ -1030,102 +1106,88 @@ rewrite /bin_prob bin0 subn0/=; apply/val_inj => /=. by rewrite expr0 mul1r mulr1n. Qed. -Lemma bin_prob1 : - bin_prob 1 = (p%:num * (NngNum (onem_ge0 p1))%:num^+(n-1)%N *+ n)%:nng. -Proof. by rewrite /bin_prob bin1/=; apply/val_inj => /=; rewrite expr1. Qed. - -Definition binomial_prob : set nat -> \bar R := - msum (fun k => mscale (bin_prob k) \d_k) n.+1. - -HB.instance Definition _ := Measure.on binomial_prob. +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. -Let binomial_setT : binomial_prob [set: _] = 1%:E. +Lemma binomial_msum : + binomial_prob n p = msum (fun k => mscale (bin_prob k) \d_k) n.+1. Proof. -rewrite /binomial_prob /msum /mscale /bin_prob/= /mscale/=. -under eq_bigr do rewrite diracT mule1. -rewrite sumEFin. -under eq_bigr do rewrite mulrC. -by rewrite -exprDn_comm ?subrK ?expr1n//; exact: mulrC. +apply/funext => U. +rewrite /binomial_prob; case: ifPn => [_|]; last by rewrite p1 p0. +rewrite /msum/= /mscale/= /binomial_pmf. +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. + 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. -HB.instance Definition _ := - Measure_isProbability.Build _ _ R binomial_prob binomial_setT. +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 binomial_msum. Qed. Lemma integral_binomial (f : nat -> \bar R) : (forall x, 0 <= f x)%E -> - (\int[binomial_prob]_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 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. -Section binomial_total. -Local Open Scope ring_scope. -Variables (R : realType) (n : nat). -Implicit Type p : R. - -Definition binomial_prob0 := @binomial_prob R 0 0%:nng ler01. - -Definition binomial_probT p : probability nat R := - if sumbool_ler 0 p is inl l0p then - if sumbool_ler (NngNum l0p)%:num 1 is inl lp1 then - @binomial_prob R n (NngNum l0p) lp1 - else binomial_prob0 - else binomial_prob0. - -Lemma measurable_binomial_probT : - measurable_fun setT (binomial_probT : R -> pprobability _ _). +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)%E. +Proof. +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))//. +rewrite !big_ord_recl/=. +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)%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. + +Lemma measurable_binomial_prob (R : realType) (n : nat) : + measurable_fun setT (binomial_prob n : R -> pprobability _ _). Proof. apply: (@measurability _ _ _ _ _ _ (@pset _ _ _ : set (set (pprobability _ R)))) => //. move=> _ -[_ [r r01] [Ys mYs <-]] <-; apply: emeasurable_fun_infty_o => //=. -rewrite /binomial_probT/=. +rewrite /binomial_prob/=. set f := (X in measurable_fun _ X). -rewrite (_ : f = fun x => if 0 <= x <= 1 then (\sum_(m < n.+1) - if sumbool_ler 0 x is inl l0p then - if sumbool_ler x 1 is inl lp1 then - mscale (@bin_prob _ n (NngNum l0p) lp1 m) (\d_(nat_of_ord m)) Ys - else - (x ^+ m * `1-x ^+ (n - m) *+ 'C(n, m))%:E * \d_(nat_of_ord m) Ys - else (x ^+ m * `1-x ^+ (n - m) *+ 'C(n, m))%:E * \d_(nat_of_ord m) Ys)%E - else \d_0%N Ys)//. - move=> _; apply: measurable_fun_ifT => //=. - 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). - apply: emeasurable_fun_sum => m /=. - rewrite /mscale/= [X in measurable_fun _ X](_ : _ = (fun x => - (x ^+ m * `1-x ^+ (n - m) *+ 'C(n, m))%:E * \d_(nat_of_ord m) Ys)%E); last first. - by apply:funext => x; case: sumbool_ler => // x0; case: sumbool_ler. - apply: emeasurable_funM => //; apply/EFin_measurable_fun => //. - under eq_fun do rewrite -mulr_natr. - do 2 apply: measurable_funM => //. - exact/measurable_fun_pow/measurable_funB. -rewrite {}/f; apply/funext => x. -case: sumbool_ler => /= x0; last first. - rewrite leNgt x0/= /binomial_prob /= /msum big_ord_recl/= big_ord0 /mscale. - by rewrite bin_prob0/= expr0 mul1e adde0. -rewrite x0/=; case: sumbool_ler => /= x1; last first. - rewrite (leNgt x) x1/= /binomial_prob /msum big_ord_recl/=/=. - by rewrite bin_prob0/= big_ord0 adde0 /mscale/= expr0 mul1e. -by rewrite x1. -Qed. - -Lemma integral_binomial_probT p (p0 : 0 <= p) (p1 : (NngNum p0)%:num <= 1) - (f : nat -> \bar R) : (forall x, 0 <= f x)%E -> - (\int[binomial_probT p]_y (f y) = \sum_(k < n.+1) (bin_prob n p1 k)%:num%:E * f k)%E. -Proof. -move=> f0; rewrite /binomial_probT/=; case: sumbool_ler => [? /=|]; last first. - by rewrite ltNge p0. -case: sumbool_ler => [?/=|]; last by rewrite ltNge p1. -by rewrite integral_binomial. -Qed. - -End binomial_total. -Arguments binomial_probT {R}. -Arguments measurable_binomial_probT {R}. +apply: measurable_fun_if => //=. + by apply: measurable_and => //; exact: measurable_fun_ler. +apply: (eq_measurable_fun (fun t => + \sum_(k x /set_mem[_/= x01]. + rewrite nneseries_esum// -1?[in RHS](set_mem_set Ys)// => k kYs. + by rewrite lee_fin binomial_pmf_ge0. +apply: ge0_emeasurable_fun_sum. + by move=> k x/= [_ x01] _; rewrite lee_fin binomial_pmf_ge0. +move=> k Ysk; apply/measurableT_comp => //. +exact: measurable_binomial_pmf. +Qed. Section uniform_probability. Local Open Scope ring_scope. @@ -1142,12 +1204,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. @@ -1158,7 +1215,7 @@ Lemma integral_uniform_pdf U : Proof. rewrite [RHS]integral_mkcondr/=; apply: eq_integral => x xU. rewrite patchE; case: ifPn => //. -rewrite notin_set/= in_itv/= => /negP/negbTE xab. +rewrite notin_setE/= in_itv/= => /negP/negbTE xab. by rewrite /uniform_pdf xab. Qed. @@ -1191,8 +1248,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. @@ -1204,7 +1260,8 @@ move=> /= F mF tF mUF; rewrite /uniform_prob; apply: cvg_toP. apply: lee_sum_nneg_natr => // k _ _. by apply: integral_ge0 => /= x Fkx; rewrite lee_fin uniform_pdf_ge0. rewrite ge0_integral_bigcup//=. -- by apply: integrableS; [| | | exact: integrable_uniform_pdf]. +- apply: measurable_funTS; apply: measurableT_comp => //. + exact: measurable_uniform_pdf. - by move=> x _; rewrite lee_fin uniform_pdf_ge0. Qed. @@ -1246,7 +1303,7 @@ move=> mE; rewrite integral_indic//= /uniform_prob setIT -ge0_integralZl//=. case: ifPn. rewrite inE/= in_itv/= => xab. by rewrite /uniform_pdf xab indicE xE mule1. - by rewrite notin_set/= in_itv/= => /negP/negbTE; rewrite /uniform_pdf => ->. + by rewrite notin_setE/= in_itv/= => /negP/negbTE; rewrite /uniform_pdf => ->. case: ifPn => //. by rewrite inE/= in_itv/= => axb; rewrite indicE (negbTE xE) mule0. - exact/EFin_measurable_fun/measurable_indic. From 029d3caad64c41311754fa9eca4222c28db6c02c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 16 May 2024 07:27:45 +0900 Subject: [PATCH 3/4] changelog & doc --- CHANGELOG_UNRELEASED.md | 34 +++++++++++++++ theories/esum.v | 9 ++++ theories/lebesgue_measure.v | 14 +++++++ theories/probability.v | 84 +++++++++++++++---------------------- theories/signed.v | 6 +++ 5 files changed, 96 insertions(+), 51 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8acf8ff94..1330b6e5d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -34,6 +34,37 @@ - in `normedtype.v`: + lemma `not_near_at_leftP` +- in `lebesgue_measure.v`: + + lemma `measurable_fun_ler` + +- in `measure.v`: + + lemmas `measurable_fun_TF`, `measurable_and` + +- in `signed.v`: + + lemma `onem_nonneg_proof`, definition `onem_nonneg` + +- in `esum.v`: + + lemma `nneseries_sum_bigcup` + +- in `lebesgue_measurable.v`: + + lemmas `measurable_natmul`, `measurable_fun_pow` + +- in `probability.v`: + + definition `bernoulli_pmf` + + lemmas `bernoulli_pmf_ge0`, `bernoulli_pmf1`, `measurable_bernoulli_pmf` + + definition `bernoulli` (equipped with the `probability` structure) + + lemmas `bernoulli_dirac`, `bernoulliE`, `integral_bernoulli`, `measurable_bernoulli`, + `measurable_bernoulli2` + + definition `binomial_pmf` + + lemmas `binomial_pmf_ge0`, `measurable_binomial_pmf` + + definitions `binomial_prob` (equipped with the `probability` structure), `bin_prob` + + lemmas `bin_prob0`, `bin_prob1`, `binomial_msum`, `binomial_probE`, `integral_binomial`, + `integral_binomial_prob`, `measurable_binomial_prob` + + definition `uniform_pdf` + + lemmas `measurable_uniform_pdf`, `integral_uniform_pdf`, `integral_uniform_pdf1` + + definition `uniform_prob` (equipped with the `probability` structure) + + lemmas `dominates_uniform_prob`, `integral_uniform` + ### Changed - in `forms.v`: @@ -110,6 +141,9 @@ (from `measurableType` to `semiRingOfSetsType`) + lemmas ` measurable_prod_measurableType`, `measurable_prod_g_measurableTypeR` (from `measurableType` to `algebraOfSetsType`) +- in `lebesgue_integral.v`: + + lemma `ge0_emeasurable_fun_sum` + ### Deprecated - in `classical_sets.v`: diff --git a/theories/esum.v b/theories/esum.v index 63250f50f..95e7d038e 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -451,6 +451,15 @@ End esum_bigcup. Arguments esum_bigcupT {R T K} J a. Arguments esum_bigcup {R T K} J a. +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 = \sum_(0 <= i tF f0; rewrite esum_bigcupT// nneseries_esum//; last first. + by move=> k _; exact: esum_ge0. +by rewrite fun_true; apply: eq_esum => /= i _. +Qed. + Definition summable (T : choiceType) (R : realType) (D : set T) (f : T -> \bar R) := (\esum_(x in D) `| f x | < +oo)%E. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index eb0269857..2b1018f6e 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1686,6 +1686,20 @@ Proof. by apply: continuous_measurable_fun; exact: continuous_expR. Qed. #[global] Hint Extern 0 (measurable_fun _ expR) => solve [apply: measurable_expR] : core. +Lemma measurable_natmul {R : realType} D n : + measurable_fun D ((@GRing.natmul R)^~ n). +Proof. +under eq_fun do rewrite -mulr_natr. +by do 2 apply: measurable_funM => //. +Qed. + +Lemma measurable_fun_pow {R : realType} D (f : R -> R) n : measurable_fun D f -> + measurable_fun D (fun x => f x ^+ n). +Proof. +move=> mf. +exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f). +Qed. + Lemma measurable_powR (R : realType) p : measurable_fun [set: R] (@powR R ^~ p). Proof. diff --git a/theories/probability.v b/theories/probability.v index b7d24ce98..0ab1ddf26 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -15,24 +15,39 @@ Require Import exp numfun lebesgue_measure lebesgue_integral kernel. (* the type probability T R (a measure that sums to 1). *) (* *) (* ``` *) -(* {RV P >-> R} == real random variable: a measurable function from *) -(* the measurableType of the probability P to R *) -(* distribution P X == measure image of the probability measure P by the *) -(* random variable X : {RV P -> R} *) -(* P as type probability T R with T of type *) -(* measurableType. *) -(* Declared as an instance of probability measure. *) -(* 'E_P[X] == expectation of the real measurable function X *) -(* covariance X Y == covariance between real random variable X and Y *) -(* 'V_P[X] == variance of the real random variable X *) -(* mmt_gen_fun X == moment generating function of the random variable *) -(* X *) -(* {dmfun T >-> R} == type of discrete real-valued measurable functions *) -(* {dRV P >-> R} == real-valued discrete random variable *) -(* dRV_dom X == domain of the discrete random variable X *) -(* dRV_enum X == bijection between the domain and the range of X *) -(* pmf X r := fine (P (X @^-1` [set r])) *) -(* enum_prob X k == probability of the kth value in the range of X *) +(* {RV P >-> R} == real random variable: a measurable function from *) +(* the measurableType of the probability P to R *) +(* distribution P X == measure image of the probability measure P by the *) +(* random variable X : {RV P -> R} *) +(* P as type probability T R with T of type *) +(* measurableType. *) +(* Declared as an instance of probability measure. *) +(* 'E_P[X] == expectation of the real measurable function X *) +(* covariance X Y == covariance between real random variable X and Y *) +(* 'V_P[X] == variance of the real random variable X *) +(* mmt_gen_fun X == moment generating function of the random variable *) +(* X *) +(* {dmfun T >-> R} == type of discrete real-valued measurable functions *) +(* {dRV P >-> R} == real-valued discrete random variable *) +(* dRV_dom X == domain of the discrete random variable X *) +(* dRV_enum X == bijection between the domain and the range of X *) +(* pmf X r := fine (P (X @^-1` [set r])) *) +(* enum_prob X k == probability of the kth value in the range of X *) +(* ``` *) +(* *) +(* ``` *) +(* 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 ab == uniform probability over the interval [a,b] *) +(* with ab0 a proof that 0 < b - a *) (* ``` *) (* *) (******************************************************************************) @@ -829,39 +844,6 @@ Qed. End discrete_distribution. -(* TODO: move *) -Lemma onem_nonneg_proof (R : numDomainType) (p : {nonneg R}) : - (p%:num <= 1 -> 0 <= `1-(p%:num))%R. -Proof. by rewrite /onem/= subr_ge0. Qed. - -Definition onem_nonneg (R : numDomainType) (p : {nonneg R}) - (p1 : (p%:num <= 1)%R) := - NngNum (onem_nonneg_proof p1). - -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 = \sum_(0 <= i 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 measurable_fun_pow {R : realType} D (f : R -> R) n : measurable_fun D f -> - measurable_fun D (fun x => f x ^+ n). -Proof. -move=> mf. -apply: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f) => //. -Qed. - -Lemma measurable_natmul {R : realType} D n : - measurable_fun D ((@GRing.natmul R)^~ n). -Proof. -under eq_fun do rewrite -mulr_natr. -by do 2 apply: measurable_funM => //. -Qed. -(* /TODO: move *) - Section bernoulli_pmf. Context {R : realType} (p : R). Local Open Scope ring_scope. diff --git a/theories/signed.v b/theories/signed.v index de3932d30..84fc0d8db 100644 --- a/theories/signed.v +++ b/theories/signed.v @@ -1225,4 +1225,10 @@ Lemma onemX_NngNum r (r1 : r <= 1) (r0 : 0 <= r) n : `1-(r ^+ n) = (NngNum (onemX_ge0 n r0 r1))%:num. Proof. by []. Qed. +Lemma onem_nonneg_proof (p : {nonneg R}) : p%:num <= 1 -> 0 <= `1-(p%:num). +Proof. by rewrite /onem/= subr_ge0. Qed. + +Definition onem_nonneg (p : {nonneg R}) (p1 : p%:num <= 1) := + NngNum (onem_nonneg_proof p1). + End onem_signed. From 860e0f915374671aefa14dfcbbdde4ea71c372b6 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 20 May 2024 20:19:55 +0900 Subject: [PATCH 4/4] adressing comments by t6s Co-authored-by: Takafumi Saikawa --- CHANGELOG_UNRELEASED.md | 8 ++++++- theories/charge.v | 4 ++-- theories/kernel.v | 4 ++-- theories/lebesgue_measure.v | 33 ++++++++------------------ theories/measure.v | 46 ++++++++++++++++++------------------- 5 files changed, 44 insertions(+), 51 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1330b6e5d..b8287296e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -38,7 +38,7 @@ + lemma `measurable_fun_ler` - in `measure.v`: - + lemmas `measurable_fun_TF`, `measurable_and` + + lemma `measurable_and` - in `signed.v`: + lemma `onem_nonneg_proof`, definition `onem_nonneg` @@ -65,6 +65,9 @@ + definition `uniform_prob` (equipped with the `probability` structure) + lemmas `dominates_uniform_prob`, `integral_uniform` +- in `measure.v`: + + lemma `measurableID` + ### Changed - in `forms.v`: @@ -75,6 +78,9 @@ - in `sequences.v`: + definition `expR` is now HB.locked +- in `measure.v`: + + change the hypothesis of `measurable_fun_bool` + ### Renamed - in `constructive_ereal.v`: diff --git a/theories/charge.v b/theories/charge.v index 6c6fb76f5..780a4e063 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1467,7 +1467,7 @@ have muAP_gt0 : 0 < mu AP. pose h x := if x \in AP then f x + (epsRN mA abs)%:num%:E else f x. have mh : measurable_fun setT h. apply: measurable_fun_if => //. - - by apply: (measurable_fun_bool true); rewrite preimage_mem_true. + - by apply: (measurable_fun_bool true); rewrite setTI preimage_mem_true. - by apply: measurable_funTS; apply: emeasurable_funD => //; exact: mf. - by apply: measurable_funTS; exact: mf. have hge0 x : 0 <= h x. @@ -1559,7 +1559,7 @@ pose f_ j x := if x \in E j then g_ j x else 0. have f_ge0 k x : 0 <= f_ k x by rewrite /f_; case: ifP. have mf_ k : measurable_fun setT (f_ k). apply: measurable_fun_if => //. - - by apply: (measurable_fun_bool true); rewrite preimage_mem_true. + - by apply: (measurable_fun_bool true); rewrite setTI preimage_mem_true. - rewrite preimage_mem_true. by apply: measurable_funTS => //; have /integrableP[] := ig_ k. have if_T k : integrable mu setT (f_ k). diff --git a/theories/kernel.v b/theories/kernel.v index 821974a20..88b70b7b7 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -784,8 +784,8 @@ apply: measurable_fun_if => //. - apply: (measurable_fun_bool true) => //. rewrite (_ : _ @^-1` _ = [set t | k t setT == 0] `|` [set t | k t setT == +oo]); last first. - by apply/seteqP; split=> x /= /orP//. - by apply: measurableU; exact: kernel_measurable_eq_cst. + by apply/seteqP; split=> x /= /orP. + by rewrite setTI; apply: measurableU; exact: kernel_measurable_eq_cst. - apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel. apply/EFin_measurable_fun; rewrite setTI. apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]). diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 2b1018f6e..f8e1c5b86 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1566,29 +1566,17 @@ Qed. Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (fun x => f x < g x). Proof. -move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. -- under eq_fun do rewrite -subr_gt0. - rewrite preimage_true -preimage_itv_o_infty. - by apply: (measurable_funB mg mf) => //; exact: measurable_itv. -- under eq_fun do rewrite ltNge -subr_ge0. - rewrite preimage_false set_predC setCK -preimage_itv_c_infty. - by apply: (measurable_funB mf mg) => //; exact: measurable_itv. -- by rewrite preimage_set0 setI0. -- by rewrite preimage_setT setIT. +move=> mf mg mD; apply: (measurable_fun_bool true) => //. +under eq_fun do rewrite -subr_gt0. +by rewrite preimage_true -preimage_itv_o_infty; exact: measurable_funB. Qed. Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g -> measurable_fun D (fun x => f x <= g x). Proof. -move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->. -- under eq_fun do rewrite -subr_ge0. - rewrite preimage_true -preimage_itv_c_infty. - by apply: (measurable_funB mg mf) => //; exact: measurable_itv. -- under eq_fun do rewrite leNgt -subr_gt0. - rewrite preimage_false set_predC setCK -preimage_itv_o_infty. - by apply: (measurable_funB mf mg) => //; exact: measurable_itv. -- by rewrite preimage_set0 setI0. -- by rewrite preimage_setT setIT. +move=> mf mg mD; apply: (measurable_fun_bool true) => //. +under eq_fun do rewrite -subr_ge0. +by rewrite preimage_true -preimage_itv_c_infty; exact: measurable_funB. Qed. Lemma measurable_maxr D f g : @@ -1704,7 +1692,8 @@ Lemma measurable_powR (R : realType) p : measurable_fun [set: R] (@powR R ^~ p). Proof. apply: measurable_fun_if => //. -- apply: (measurable_fun_bool true); rewrite (_ : _ @^-1` _ = [set 0])//. +- apply: (measurable_fun_bool true). + rewrite (_ : _ @^-1` _ = [set 0]) ?setTI//. by apply/seteqP; split => [_ /eqP ->//|_ -> /=]; rewrite eqxx. - rewrite setTI; apply: measurableT_comp => //. rewrite (_ : _ @^-1` _ = [set~ 0]); first exact: measurableT_comp. @@ -1788,9 +1777,7 @@ move=> mf;rewrite (_ : er_map _ = fun x => if x \is a fin_num then (f (fine x))%:E else x); last first. by apply: funext=> -[]. apply: measurable_fun_ifT => //=. -+ apply: (measurable_fun_bool true). - rewrite /preimage/= -[X in measurable X]setTI. - exact/emeasurable_fin_num. ++ by apply: (measurable_fun_bool true); exact/emeasurable_fin_num. + exact/EFin_measurable_fun/measurableT_comp. Qed. #[deprecated(since="mathcomp-analysis 0.6.3", note="renamed `measurable_er_map`")] @@ -1807,7 +1794,7 @@ Lemma measurable_fun_einfs D (f : (T -> \bar R)^nat) : Proof. move=> mf n mD. apply: (measurability (ErealGenCInfty.measurableE R)) => //. -move=> _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n => /=. +move=> _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n =>/=. by apply: bigcap_measurable => ? ?; exact/mf/emeasurable_itv. Qed. diff --git a/theories/measure.v b/theories/measure.v index 0b5b9d509..3865b1354 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -920,6 +920,13 @@ rewrite -bigsetI_fset_set// big_seq; apply: bigsetI_measurable => i. by rewrite in_fset_set ?inE// => *; apply: Fm. Qed. +Lemma measurableID A B : measurable A -> measurable (A `&` B) -> + measurable (A `\` B). +Proof. +move=> mA /measurableC; rewrite setCI => /(measurableI A) => /(_ mA). +by rewrite setIUr setICr set0U. +Qed. + End algebraofsets_lemmas. Section measurable_lemmas. @@ -1160,24 +1167,9 @@ by move=> mx my; apply: measurable_fun_if => //; [exact: measurable_funS mx|exact: measurable_funS my]. Qed. -Lemma measurable_fun_bool D (f : T1 -> bool) b : - measurable (f @^-1` [set b]) -> measurable_fun D f. -Proof. -have FNT : [set false] = [set~ true] by apply/seteqP; split => -[]//=. -wlog {b}-> : b / b = true. - case: b => [|h]; first exact. - by rewrite FNT -preimage_setC => /measurableC; rewrite setCK; exact: h. -move=> mfT mD /= Y; have := @subsetT _ Y; rewrite setT_bool => YT. -have [-> _|-> _|-> _ |-> _] := subset_set2 YT. -- by rewrite preimage0 ?setI0. -- by apply: measurableI => //; exact: mfT. -- rewrite -[X in measurable X]setCK; apply: measurableC; rewrite setCI. - apply: measurableU; first exact: measurableC. - by rewrite FNT preimage_setC setCK; exact: mfT. -- by rewrite -setT_bool preimage_setT setIT. -Qed. +Section measurable_fun_bool. -Lemma measurable_fun_TF D (f : T1 -> bool) : +Let measurable_fun_TF D (f : T1 -> bool) : measurable (D `&` f @^-1` [set true]) -> measurable (D `&` f @^-1` [set false]) -> measurable_fun D f. @@ -1191,20 +1183,28 @@ move: mY; have [-> _|-> _|-> _ |-> _] := subset_set2 YT. - by rewrite -setT_bool preimage_setT setIT. Qed. +Lemma measurable_fun_bool D (f : T1 -> bool) b : + measurable (D `&` f @^-1` [set b]) -> measurable_fun D f. +Proof. +move=> mb mD; have mDb : measurable (D `&` f @^-1` [set ~~ b]). + rewrite (_ : [set ~~ b] = [set~ b]); last first. + by apply/seteqP; split=> -[] /=; case: b {mb}. + by rewrite -preimage_setC; exact: measurableID. +by case: b => /= in mb mDb *; exact: measurable_fun_TF. +Qed. + +End measurable_fun_bool. +Arguments measurable_fun_bool {D f} _. + Lemma measurable_and D (f : T1 -> bool) (g : T1 -> bool) : measurable_fun D f -> measurable_fun D g -> measurable_fun D (fun x => f x && g x). Proof. -move=> mf mg mD; apply: measurable_fun_TF => //. +move=> mf mg mD; apply: (measurable_fun_bool true) => //. - rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `&` (D `&` g @^-1` [set true])); last first. by rewrite setIACA setIid; congr (_ `&` _); apply/seteqP; split => x /andP. by apply: measurableI; [exact: mf|exact: mg]. -- rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set false] `|` - (D `&` g @^-1` [set false])); last first. - rewrite -setIUr; congr (_ `&` _). - by apply/seteqP; split => x /=; case: (f x); case: (g x); tauto. -- by apply: measurableU; [exact: mf|exact: mg]. Qed. End measurable_fun.