From 9ca2dbb3dc94bbdb1af2659058fe8b22783e9458 Mon Sep 17 00:00:00 2001 From: Yosuke-Ito-345 Date: Wed, 4 Jun 2025 08:53:19 +0900 Subject: [PATCH 1/6] add section cdf_of_lebesgue_stieltjes_mesure --- theories/probability.v | 73 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 73 insertions(+) diff --git a/theories/probability.v b/theories/probability.v index f165d970f4..10d9a9879c 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -247,6 +247,79 @@ Unshelve. all: by end_near. Qed. End cumulative_distribution_function. +Section cdf_of_lebesgue_stieltjes_mesure. +Context {R : realType} (f : cumulative R) + (f_y1 : f @ +oo --> (1:R)) (f_Ny0 : f @ -oo --> (0: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. +pose I n := `]-(n%:R):R, n%:R]%classic. +have <- : \bigcup_n I n = setT. + rewrite -subTset=> x _; rewrite /bigcup/=; exists (truncn`|x|).+1=>//. + by rewrite /I/= subset_itv_oo_oc// in_itv/= -real_ltr_norml//= truncnS_gt. +have cvg_cup : (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. +have cvg_1 : (lsf \o I) n @[n --> \oo] --> 1%E. + rewrite /comp/I/lsf/lebesgue_stieltjes_measure/measure_extension/=. + suff : ((f n%:R)%:E - (f (1 *- n))%:E)%E @[n --> \oo] --> 1%E => ?. + under eq_cvg=> n. + rewrite measurable_mu_extE/=; last exact: is_ocitv. + rewrite wlength_itv_bnd; last exact: (le_trans _ (ler0n R n)). + over. + assumption. + rewrite -(sube0 1); apply: cvgeB=>//; apply: cvg_EFin; try by near=> F. + by rewrite /comp; apply/(cvg_comp _ _ (@cvgr_idn R))/f_y1. + rewrite /comp/=; apply: ((iffLR (cvg_ninftyP _ _)) f_Ny0). + by apply: (cvg_comp _ _ (@cvgr_idn R)); rewrite ninfty. +by rewrite -(cvg_unique _ cvg_cup cvg_1). +Unshelve. all: end_near. Qed. + +HB.instance Definition _ := @Measure_isProbability.Build _ _ _ + (lebesgue_stieltjes_measure f) lebesgue_stieltjes_setT. + +Let idTR : T -> R := (fun x => x). + +Lemma measurable_idTR : measurable_fun setT idTR. +Proof. by apply: measurable_id. Qed. + +#[local] HB.instance Definition _ := + @isMeasurableFun.Build _ _ T R idTR measurable_idTR. + +Let Xid : {RV lsf >-> R} := idTR. + +Lemma cdf_lebesgue_stieltjes_id r : cdf Xid r = EFin (f r). +Proof. +rewrite /= preimage_id. +have <- : (\bigcup_n `]-n%:R, r]%classic) = `]-oo, r]%classic. + apply/seteqP; split=> x/=; first by case=> n _/=; rewrite !in_itv/=; case/andP. + rewrite in_itv/= => xr; exists (truncn`|x|).+1=>//=; rewrite in_itv/=. + apply/andP; split=>//; rewrite ltrNl -normrN. + apply: le_lt_trans; [exact: ler_norm | exact: truncnS_gt]. +have cvg_cup : (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//. +have cvg_fr : (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. + near: n; exists (truncn`|r|).+1=>// n/=; rewrite truncn_lt_nat// lerNl. + by move/ltW; apply /le_trans; rewrite -normrN ler_norm. + rewrite -[X in _ --> X](sube0 (f r)%:E). + apply: cvgeB=>//; first exact: cvg_cst. + apply: cvg_comp; [apply: cvg_comp; last exact: f_Ny0 | by[]]. + by apply: cvg_comp; [exact: cvgr_idn | rewrite ninfty]. +by rewrite -(cvg_unique _ cvg_cup cvg_fr). +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. From 6d59e5f3ac2e7d658b43524fa29b144fa509c25b Mon Sep 17 00:00:00 2001 From: Yosuke-Ito-345 Date: Thu, 5 Jun 2025 20:06:49 +0900 Subject: [PATCH 2/6] update changelog --- CHANGELOG_UNRELEASED.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e3728effa2..f6daaa2807 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -112,6 +112,8 @@ - in `lebesgue_integral_definition.v`: + lemmas `le_measure_sintegral`, `ge0_le_measure_integral` +- in `probability.v`: + + lemmas `measurable_idTR`, `cdf_lebesgue_stieltjes_id` ### Changed From 4c33c1f77120f74ac21359ef20b134fb5fbce71e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 1 Jul 2025 11:39:05 +0900 Subject: [PATCH 3/6] nitpick --- CHANGELOG_UNRELEASED.md | 5 ++- reals/real_interval.v | 9 +++++ theories/probability.v | 74 ++++++++++++++++------------------------- 3 files changed, 41 insertions(+), 47 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f6daaa2807..c4109e81b6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -113,7 +113,10 @@ - in `lebesgue_integral_definition.v`: + lemmas `le_measure_sintegral`, `ge0_le_measure_integral` - in `probability.v`: - + lemmas `measurable_idTR`, `cdf_lebesgue_stieltjes_id` + + lemma `cdf_lebesgue_stieltjes_id` + +- in `real_interval.v`: + + lemma `itvNybndEbigcup` ### Changed 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/probability.v b/theories/probability.v index 10d9a9879c..4869a00688 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -257,65 +257,47 @@ Let lsf := lebesgue_stieltjes_measure f. Let lebesgue_stieltjes_setT : lsf setT = 1%E. Proof. -pose I n := `]-(n%:R):R, n%:R]%classic. -have <- : \bigcup_n I n = setT. - rewrite -subTset=> x _; rewrite /bigcup/=; exists (truncn`|x|).+1=>//. - by rewrite /I/= subset_itv_oo_oc// in_itv/= -real_ltr_norml//= truncnS_gt. -have cvg_cup : (lsf \o I) n @[n --> \oo] --> lsf (\bigcup_n I n). +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))/f_y1]. + - apply/cvg_EFin; [by near=> F|apply: (cvg_ninftyP _ _).1 => //]. + 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. -have cvg_1 : (lsf \o I) n @[n --> \oo] --> 1%E. - rewrite /comp/I/lsf/lebesgue_stieltjes_measure/measure_extension/=. - suff : ((f n%:R)%:E - (f (1 *- n))%:E)%E @[n --> \oo] --> 1%E => ?. - under eq_cvg=> n. - rewrite measurable_mu_extE/=; last exact: is_ocitv. - rewrite wlength_itv_bnd; last exact: (le_trans _ (ler0n R n)). - over. - assumption. - rewrite -(sube0 1); apply: cvgeB=>//; apply: cvg_EFin; try by near=> F. - by rewrite /comp; apply/(cvg_comp _ _ (@cvgr_idn R))/f_y1. - rewrite /comp/=; apply: ((iffLR (cvg_ninftyP _ _)) f_Ny0). - by apply: (cvg_comp _ _ (@cvgr_idn R)); rewrite ninfty. -by rewrite -(cvg_unique _ cvg_cup cvg_1). +exact: cvg_unique. Unshelve. all: end_near. Qed. HB.instance Definition _ := @Measure_isProbability.Build _ _ _ (lebesgue_stieltjes_measure f) lebesgue_stieltjes_setT. -Let idTR : T -> R := (fun x => x). - -Lemma measurable_idTR : measurable_fun setT idTR. -Proof. by apply: measurable_id. Qed. +Let idTR : T -> R := idfun. #[local] HB.instance Definition _ := - @isMeasurableFun.Build _ _ T R idTR measurable_idTR. - -Let Xid : {RV lsf >-> R} := idTR. + @isMeasurableFun.Build _ _ T R idTR (@measurable_id _ _ setT). -Lemma cdf_lebesgue_stieltjes_id r : cdf Xid r = EFin (f r). +Lemma cdf_lebesgue_stieltjes_id r : cdf (idTR : {RV lsf >-> R}) r = (f r)%:E. Proof. -rewrite /= preimage_id. -have <- : (\bigcup_n `]-n%:R, r]%classic) = `]-oo, r]%classic. - apply/seteqP; split=> x/=; first by case=> n _/=; rewrite !in_itv/=; case/andP. - rewrite in_itv/= => xr; exists (truncn`|x|).+1=>//=; rewrite in_itv/=. - apply/andP; split=>//; rewrite ltrNl -normrN. - apply: le_lt_trans; [exact: ler_norm | exact: truncnS_gt]. -have cvg_cup : (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//. -have cvg_fr : (lsf `]-n%:R, r])@[n --> \oo] --> (f r)%:E. - suff : ((f r)%:E - (f (-n%:R))%:E)%E@[n --> \oo] --> (f r)%:E. +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 /lsf /lebesgue_stieltjes_measure /measure_extension/=. rewrite measurable_mu_extE/= ?wlength_itv_bnd//; last exact: is_ocitv. - near: n; exists (truncn`|r|).+1=>// n/=; rewrite truncn_lt_nat// lerNl. - by move/ltW; apply /le_trans; rewrite -normrN ler_norm. - rewrite -[X in _ --> X](sube0 (f r)%:E). - apply: cvgeB=>//; first exact: cvg_cst. - apply: cvg_comp; [apply: cvg_comp; last exact: f_Ny0 | by[]]. - by apply: cvg_comp; [exact: cvgr_idn | rewrite ninfty]. -by rewrite -(cvg_unique _ cvg_cup cvg_fr). + 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 _ _ _ f_Ny0)) => //. + 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. From 88f8b30f57e7854c0008d92a3af3cfc12aee8e6a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 1 Jul 2025 16:49:35 +0900 Subject: [PATCH 4/6] structure cumulative01 --- CHANGELOG_UNRELEASED.md | 3 + theories/lebesgue_stieltjes_measure.v | 99 +++++++++++++++++++++++++++ theories/measurable_realfun.v | 49 +------------ theories/probability.v | 27 +------- 4 files changed, 105 insertions(+), 73 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c4109e81b6..f42e9324a9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -243,6 +243,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/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index ba7ac313d5..adfba190ca 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -541,3 +541,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 isCumulative01 (R : numFieldType) (f : R -> R) := { + cumulativeNy0 : f @ -oo --> (0:R) ; + cumulativey1 : f @ +oo --> (1:R) }. + +#[short(type=cumulative01)] +HB.structure Definition Cumulative01 (R : numFieldType) := + { f of isCumulative01 R f & Cumulative R f}. + +Arguments cumulativeNy0 {R} s. +Arguments cumulativey1 {R} s. + +Section probability_measure_of_lebesgue_stieltjes_mesure. +Context {R : realType} (f : cumulative01 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 4869a00688..f40e7ab373 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -248,35 +248,12 @@ Unshelve. all: by end_near. Qed. End cumulative_distribution_function. Section cdf_of_lebesgue_stieltjes_mesure. -Context {R : realType} (f : cumulative R) - (f_y1 : f @ +oo --> (1:R)) (f_Ny0 : f @ -oo --> (0:R)). +Context {R : realType} (f : cumulative01 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))/f_y1]. - - apply/cvg_EFin; [by near=> F|apply: (cvg_ninftyP _ _).1 => //]. - 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. - Let idTR : T -> R := idfun. #[local] HB.instance Definition _ := @@ -292,7 +269,7 @@ have : lsf `]-n%:R, r] @[n --> \oo] --> (f r)%:E. 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 _ _ _ f_Ny0)) => //. + 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. From 18c068b937e03bb147a020e8ae651ab049875720 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 1 Jul 2025 17:10:39 +0900 Subject: [PATCH 5/6] upd changlog and doc --- CHANGELOG_UNRELEASED.md | 3 +++ theories/lebesgue_stieltjes_measure.v | 3 +++ 2 files changed, 6 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f42e9324a9..18a1d9d821 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -118,6 +118,9 @@ - in `real_interval.v`: + lemma `itvNybndEbigcup` +- in `lebesgue_stieltjes_measure.v`: + + mixin `isCumulative01`, structure `Cumulative01` with type `cumulative01` + ### Changed - in `convex.v`: diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index adfba190ca..ce76d79cdd 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 *) +(* cumulative01 R == type of cumulative functions f such that *) +(* f @ -oo --> 0 and f @ +oo --> 1 *) +(* The HB class is Cumulative01. *) (* ``` *) (* *) (******************************************************************************) From ac40f39e71a6a0e17a6071536432feaa79b03ae0 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 2 Jul 2025 15:41:37 +0900 Subject: [PATCH 6/6] addressing comments --- CHANGELOG_UNRELEASED.md | 2 +- theories/lebesgue_stieltjes_measure.v | 24 ++++++++++++------------ theories/probability.v | 2 +- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 18a1d9d821..86a37fdfec 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -119,7 +119,7 @@ + lemma `itvNybndEbigcup` - in `lebesgue_stieltjes_measure.v`: - + mixin `isCumulative01`, structure `Cumulative01` with type `cumulative01` + + mixin `isCumulativeBounded`, structure `CumulativeBounded` with type `cumulative_bounded` ### Changed diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index ce76d79cdd..ab5cbb4671 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -36,9 +36,9 @@ From mathcomp Require Import realfun. (* f is a cumulative function. *) (* completed_lebesgue_stieltjes_measure f == the completed Lebesgue-Stieltjes *) (* measure *) -(* cumulative01 R == type of cumulative functions f such that *) -(* f @ -oo --> 0 and f @ +oo --> 1 *) -(* The HB class is Cumulative01. *) +(* cumulative_bounded R l r == type of cumulative functions f such that *) +(* f @ -oo --> l and f @ +oo --> r *) +(* The HB class is CumulativeBounded. *) (* ``` *) (* *) (******************************************************************************) @@ -600,19 +600,19 @@ Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core. #[global] Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core. -HB.mixin Record isCumulative01 (R : numFieldType) (f : R -> R) := { - cumulativeNy0 : f @ -oo --> (0:R) ; - cumulativey1 : f @ +oo --> (1:R) }. +HB.mixin Record isCumulativeBounded (R : numFieldType) (l r : R) (f : R -> R) := { + cumulativeNy0 : f @ -oo --> l ; + cumulativey1 : f @ +oo --> r }. -#[short(type=cumulative01)] -HB.structure Definition Cumulative01 (R : numFieldType) := - { f of isCumulative01 R f & Cumulative R f}. +#[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} s. -Arguments cumulativey1 {R} s. +Arguments cumulativeNy0 {R l r} s. +Arguments cumulativey1 {R l r} s. Section probability_measure_of_lebesgue_stieltjes_mesure. -Context {R : realType} (f : cumulative01 R). +Context {R : realType} (f : cumulativeBounded (0:R) (1:R)). Local Open Scope measure_display_scope. Let T := g_sigma_algebraType R.-ocitv.-measurable. diff --git a/theories/probability.v b/theories/probability.v index f40e7ab373..45dab4df6a 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -248,7 +248,7 @@ Unshelve. all: by end_near. Qed. End cumulative_distribution_function. Section cdf_of_lebesgue_stieltjes_mesure. -Context {R : realType} (f : cumulative01 R). +Context {R : realType} (f : cumulativeBounded (0:R) (1:R)). Local Open Scope measure_display_scope. Let T := g_sigma_algebraType R.-ocitv.-measurable.