diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e3728effa2..86a37fdfec 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -112,6 +112,14 @@ - in `lebesgue_integral_definition.v`: + lemmas `le_measure_sintegral`, `ge0_le_measure_integral` +- in `probability.v`: + + lemma `cdf_lebesgue_stieltjes_id` + +- in `real_interval.v`: + + lemma `itvNybndEbigcup` + +- in `lebesgue_stieltjes_measure.v`: + + mixin `isCumulativeBounded`, structure `CumulativeBounded` with type `cumulative_bounded` ### Changed @@ -238,6 +246,9 @@ `LspaceType` to `ae_eq_op`, `ae_eq_op_refl`, `ae_eq_op_sym`, `ae_eq_op_trans`, `aeEqMfun` * renamed lemma `LequivP` to `ae_eqP` +- moved from `measurable_realfun.v` to `lebesgue_stieltjes_measure.v`: + + definitions `measurableTypeR`, `measurableR` + + lemmas `measurable_set1`, `measurable_itv` ### Renamed diff --git a/reals/real_interval.v b/reals/real_interval.v index 7beee977ba..2343f4190f 100644 --- a/reals/real_interval.v +++ b/reals/real_interval.v @@ -167,6 +167,15 @@ rewrite in_itv /= andbT => xy; exists (trunc y).+1 => //=. by rewrite in_itv /= xy /= truncnS_gt. Qed. +Lemma itvNybndEbigcup b x : [set` Interval -oo%O (BSide b x)] = + \bigcup_k [set` Interval (BRight (- k%:R)) (BSide b x)]. +Proof. +rewrite predeqE => y; split=> /=; last first. + by move=> [n _]/=; rewrite in_itv => /andP[ny yx]; rewrite in_itv. +rewrite in_itv /= => yx; exists (trunc `|y|).+1 => //=; rewrite in_itv/=. +by rewrite yx /= andbT ltrNl (le_lt_trans (ler_norm _))// normrN truncnS_gt. +Qed. + Lemma itvoyEbigcup x : `]x, +oo[%classic = \bigcup_k `[x + k.+1%:R^-1, +oo[%classic. Proof. diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index ba7ac313d5..ab5cbb4671 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -36,6 +36,9 @@ From mathcomp Require Import realfun. (* f is a cumulative function. *) (* completed_lebesgue_stieltjes_measure f == the completed Lebesgue-Stieltjes *) (* measure *) +(* cumulative_bounded R l r == type of cumulative functions f such that *) +(* f @ -oo --> l and f @ +oo --> r *) +(* The HB class is CumulativeBounded. *) (* ``` *) (* *) (******************************************************************************) @@ -541,3 +544,102 @@ HB.instance Definition _ (f : cumulative R) := End completed_lebesgue_stieltjes_measure. Arguments completed_lebesgue_stieltjes_measure {R}. + +Section salgebra_R_ssets. +Variable R : realType. + +Definition measurableTypeR := g_sigma_algebraType (R.-ocitv.-measurable). +Definition measurableR : set (set R) := + (R.-ocitv.-measurable).-sigma.-measurable. + +HB.instance Definition _ := Pointed.on R. +HB.instance Definition R_isMeasurable : + isMeasurable default_measure_display R := + @isMeasurable.Build _ measurableTypeR measurableR + measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). +(*HB.instance (Real.sort R) R_isMeasurable.*) + +Lemma measurable_set1 (r : R) : measurable [set r]. +Proof. +rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. +by apply: sub_sigma_algebra; exact/is_ocitv. +Qed. +#[local] Hint Resolve measurable_set1 : core. + +Lemma measurable_itv (i : interval R) : measurable [set` i]. +Proof. +have moc (a b : R) : measurable `]a, b]. + by apply: sub_sigma_algebra; apply: is_ocitv. +have mopoo (x : R) : measurable `]x, +oo[. + by rewrite itv_bndy_bigcup_BRight; exact: bigcup_measurable. +have mnooc (x : R) : measurable `]-oo, x]. + by rewrite -setCitvr; exact/measurableC. +have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b. + case: (boolP (a < b)) => ab; last by rewrite !set_itv_ge ?set0D. + by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF. +have moo (a b : R) : measurable `]a, b[. + by rewrite ooE; exact: measurableD. +have mcc (a b : R) : measurable `[a, b]. + case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge. + by rewrite -setU1itv//; apply/measurableU. +have mco (a b : R) : measurable `[a, b[. + case: (boolP (a < b)) => ab; last by rewrite set_itv_ge. + by rewrite -setU1itv//; apply/measurableU. +have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b. + by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx. +case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge. +- by rewrite -setU1itv//; exact/measurableU. +- by rewrite oooE; exact/measurableD. +- by rewrite set_itvNyy. +Qed. +#[local] Hint Resolve measurable_itv : core. + +End salgebra_R_ssets. +#[global] +Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. +#[global] +Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. + +HB.mixin Record isCumulativeBounded (R : numFieldType) (l r : R) (f : R -> R) := { + cumulativeNy0 : f @ -oo --> l ; + cumulativey1 : f @ +oo --> r }. + +#[short(type=cumulativeBounded)] +HB.structure Definition CumulativeBounded (R : numFieldType) (l r : R) := + { f of isCumulativeBounded R l r f & Cumulative R f}. + +Arguments cumulativeNy0 {R l r} s. +Arguments cumulativey1 {R l r} s. + +Section probability_measure_of_lebesgue_stieltjes_mesure. +Context {R : realType} (f : cumulativeBounded (0:R) (1:R)). +Local Open Scope measure_display_scope. + +Let T := g_sigma_algebraType R.-ocitv.-measurable. +Let lsf := lebesgue_stieltjes_measure f. + +Let lebesgue_stieltjes_setT : lsf setT = 1%E. +Proof. +rewrite -(bigcup_itvT false false). +pose I n : set R := `]- (n%:R), n%:R]%classic. +have : (lsf \o I) n @[n --> \oo] --> 1%E. + have -> : lsf \o I = (fun n => (f n%:R)%:E - (f (- n%:R))%:E)%E. + apply/funext=> n; rewrite /= /lsf/= /lebesgue_stieltjes_measure. + rewrite /measure_extension measurable_mu_extE/=; last exact: is_ocitv. + by rewrite wlength_itv_bnd// ge0_cp. + rewrite -(sube0 1); apply: cvgeB => //. + - by apply/cvg_EFin; [near=> F + |exact/(cvg_comp _ _ (@cvgr_idn R))/cumulativey1]. + - apply/cvg_EFin; [by near=> F|apply: (cvg_ninftyP _ _).1 => //]. + exact: cumulativeNy0. + by apply: (cvg_comp _ _ (@cvgr_idn R)); rewrite ninfty. +have : (lsf \o I) n @[n --> \oo] --> lsf (\bigcup_n I n). + apply: nondecreasing_cvg_mu; rewrite /I//; first exact: bigcup_measurable. + by move=> *; apply/subsetPset/subset_itv; rewrite leBSide/= ?lerN2 ler_nat. +exact: cvg_unique. +Unshelve. all: end_near. Qed. + +HB.instance Definition _ := @Measure_isProbability.Build _ _ _ + (lebesgue_stieltjes_measure f) lebesgue_stieltjes_setT. + +End probability_measure_of_lebesgue_stieltjes_mesure. diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 56f724edba..53af2179c0 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -183,52 +183,6 @@ End puncture_ereal_itv. Section salgebra_R_ssets. Variable R : realType. -Definition measurableTypeR := g_sigma_algebraType (R.-ocitv.-measurable). -Definition measurableR : set (set R) := - (R.-ocitv.-measurable).-sigma.-measurable. - -HB.instance Definition _ := Pointed.on R. -HB.instance Definition R_isMeasurable : - isMeasurable default_measure_display R := - @isMeasurable.Build _ measurableTypeR measurableR - measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). -(*HB.instance (Real.sort R) R_isMeasurable.*) - -Lemma measurable_set1 (r : R) : measurable [set r]. -Proof. -rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _. -by apply: sub_sigma_algebra; exact/is_ocitv. -Qed. -#[local] Hint Resolve measurable_set1 : core. - -Lemma measurable_itv (i : interval R) : measurable [set` i]. -Proof. -have moc (a b : R) : measurable `]a, b]. - by apply: sub_sigma_algebra; apply: is_ocitv. -have mopoo (x : R) : measurable `]x, +oo[. - by rewrite itv_bndy_bigcup_BRight; exact: bigcup_measurable. -have mnooc (x : R) : measurable `]-oo, x]. - by rewrite -setCitvr; exact/measurableC. -have ooE (a b : R) : `]a, b[%classic = `]a, b] `\ b. - case: (boolP (a < b)) => ab; last by rewrite !set_itv_ge ?set0D. - by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx andbF. -have moo (a b : R) : measurable `]a, b[. - by rewrite ooE; exact: measurableD. -have mcc (a b : R) : measurable `[a, b]. - case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge. - by rewrite -setU1itv//; apply/measurableU. -have mco (a b : R) : measurable `[a, b[. - case: (boolP (a < b)) => ab; last by rewrite set_itv_ge. - by rewrite -setU1itv//; apply/measurableU. -have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b. - by rewrite -setUitv1// setUDK// => x [->]; rewrite /= in_itv/= ltxx. -case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge. -- by rewrite -setU1itv//; exact/measurableU. -- by rewrite oooE; exact/measurableD. -- by rewrite set_itvNyy. -Qed. -#[local] Hint Resolve measurable_itv : core. - Lemma measurable_fun_itv_bndo_bndc (a : itv_bound R) (b : R) (f : R -> R) : measurable_fun [set` Interval a (BLeft b)] f -> @@ -387,8 +341,7 @@ Qed. End salgebra_R_ssets. #[global] -Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1| - apply: emeasurable_set1] : core. +Hint Extern 0 (measurable [set _]) => solve [apply: emeasurable_set1] : core. #[global] Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. diff --git a/theories/probability.v b/theories/probability.v index f165d970f4..45dab4df6a 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -247,6 +247,38 @@ Unshelve. all: by end_near. Qed. End cumulative_distribution_function. +Section cdf_of_lebesgue_stieltjes_mesure. +Context {R : realType} (f : cumulativeBounded (0:R) (1:R)). +Local Open Scope measure_display_scope. + +Let T := g_sigma_algebraType R.-ocitv.-measurable. +Let lsf := lebesgue_stieltjes_measure f. + +Let idTR : T -> R := idfun. + +#[local] HB.instance Definition _ := + @isMeasurableFun.Build _ _ T R idTR (@measurable_id _ _ setT). + +Lemma cdf_lebesgue_stieltjes_id r : cdf (idTR : {RV lsf >-> R}) r = (f r)%:E. +Proof. +rewrite /= preimage_id itvNybndEbigcup. +have : lsf `]-n%:R, r] @[n --> \oo] --> (f r)%:E. + suff : ((f r)%:E - (f (-n%:R))%:E)%E @[n --> \oo] --> (f r)%:E. + apply: cvg_trans; apply: near_eq_cvg; near=> n. + rewrite /lsf /lebesgue_stieltjes_measure /measure_extension/=. + rewrite measurable_mu_extE/= ?wlength_itv_bnd//; last exact: is_ocitv. + by rewrite lerNl; near: n; exact: nbhs_infty_ger. + rewrite -[X in _ --> X](sube0 (f r)%:E); apply: (cvgeB _ (cvg_cst _ )) => //. + apply: (cvg_comp _ _ (cvg_comp _ _ _ (cumulativeNy0 f))) => //. + by apply: (cvg_comp _ _ cvgr_idn); rewrite ninfty. +have : lsf `]- n%:R, r] @[n --> \oo] --> lsf (\bigcup_n `]-n%:R, r]%classic). + apply: nondecreasing_cvg_mu; rewrite /I//; first exact: bigcup_measurable. + by move=> *; apply/subsetPset/subset_itv; rewrite leBSide//= lerN2 ler_nat. +exact: cvg_unique. +Unshelve. all: by end_near. Qed. + +End cdf_of_lebesgue_stieltjes_mesure. + HB.lock Definition expectation {d} {T : measurableType d} {R : realType} (P : probability T R) (X : T -> R) := (\int[P]_w (X w)%:E)%E. Canonical expectation_unlockable := Unlockable expectation.unlock.