diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f74d42437..60c4e915b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -7,6 +7,9 @@ - in `constructive_ereal.v`: + lemma `ltgte_fin_num` +- in `probability.v`: + + lemmas `cdf_fin_num`, `lebesgue_stieltjes_cdf_id` + - in `num_normedtype.v`: + lemma `nbhs_infty_gtr` diff --git a/theories/ftc.v b/theories/ftc.v index 4abdd3a67..8399560d6 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -348,7 +348,7 @@ Proof. by move=> xu locf F ax fx; exact: (@continuous_FTC1 _ _ _ u). Qed. End FTC. Definition parameterized_integral {R : realType} - (mu : {measure set (g_sigma_algebraType (R.-ocitv.-measurable)) -> \bar R}) + (mu : {measure set (measurableTypeR R) -> \bar R}) a x (f : R -> R) : R := (\int[mu]_(t in `[a, x]) f t)%R. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index f75da4bc9..a6d9a7356 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -335,7 +335,7 @@ End hlength_extension. End LebesgueMeasure. Definition lebesgue_measure {R : realType} : - set (g_sigma_algebraType R.-ocitv.-measurable) -> \bar R := + set (measurableTypeR R) -> \bar R := lebesgue_stieltjes_measure idfun. HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R). HB.instance Definition _ (R : realType) := @@ -399,7 +399,7 @@ have mF_ m : mu (F_ m) < completed_mu E + m.+1%:R^-1%:E. apply: lee_nneseries => // n _. by rewrite -((measurable_mu_extE hlength) (A m n))//; have [/(_ n)] := mA m. pose F := \bigcap_n (F_ n). -have FM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) F. +have FM : @measurable _ (measurableTypeR R) F. apply: bigcapT_measurable => k; apply: bigcupT_measurable => i. by apply: sub_sigma_algebra; have [/(_ i)] := mA k. have EF : E `<=` F by exact: sub_bigcap. @@ -434,7 +434,7 @@ have mG_ m : mu (G_ m) < completed_mu (F `\` E) + m.+1%:R^-1%:E. apply: lee_nneseries => // n _. by rewrite -((measurable_mu_extE hlength) (B m n))//; have [/(_ n)] := mB m. pose G := \bigcap_n (G_ n). -have GM : @measurable _ (g_sigma_algebraType R.-ocitv.-measurable) G. +have GM : @measurable _ (measurableTypeR R) G. apply: bigcapT_measurable => k; apply: bigcupT_measurable => i. by apply: sub_sigma_algebra; have [/(_ i)] := mB k. have FEG : F `\` E `<=` G by exact: sub_bigcap. diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index c099013a8..c6eb7627d 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -510,12 +510,14 @@ Arguments lebesgue_stieltjes_measure {R}. #[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `wlength_sigma_subadditive`")] Notation wlength_sigma_sub_additive := wlength_sigma_subadditive (only parsing). +Definition measurableTypeR (R : realType) := + g_sigma_algebraType R.-ocitv.-measurable. + Section lebesgue_stieltjes_measure. Variable R : realType. -Let gitvs : measurableType _ := g_sigma_algebraType (@ocitv R). Lemma lebesgue_stieltjes_measure_unique (f : cumulative R R) - (mu : {measure set gitvs -> \bar R}) : + (mu : {measure set (measurableTypeR R) -> \bar R}) : (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> forall X, measurable X -> lebesgue_stieltjes_measure f X = mu X. Proof. @@ -550,14 +552,13 @@ 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 + @isMeasurable.Build _ (measurableTypeR R) measurableR measurable0 (@measurableC _ _) (@bigcupT_measurable _ _). (*HB.instance (Real.sort R) R_isMeasurable.*) @@ -631,7 +632,6 @@ 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. diff --git a/theories/probability.v b/theories/probability.v index 06fed1326..6927b7e6e 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -169,6 +169,11 @@ Lemma cdf_ge0 r : 0 <= cdf X r. Proof. by []. Qed. Lemma cdf_le1 r : cdf X r <= 1. Proof. exact: probability_le1. Qed. +Lemma cdf_fin_num r : cdf X r \is a fin_num. +Proof. +by rewrite ge0_fin_numE ?cdf_ge0//; exact/(le_lt_trans (cdf_le1 r))/ltry. +Qed. + Lemma cdf_nondecreasing : nondecreasing_fun (cdf X). Proof. by move=> r s rs; rewrite le_measure ?inE//; exact: subitvPr. Qed. @@ -252,17 +257,16 @@ HB.instance Definition _ := isCumulative.Build R _ (\bar R) (cdf X) End cumulative_distribution_function. -Section cdf_of_lebesgue_stieltjes_mesure. +Section cdf_of_lebesgue_stieltjes_measure. 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. +Let idTR : measurableTypeR R -> R := idfun. #[local] HB.instance Definition _ := - @isMeasurableFun.Build _ _ T R idTR (@measurable_id _ _ setT). + @isMeasurableFun.Build _ _ _ _ idTR (@measurable_id _ _ setT). + +Let lsf := lebesgue_stieltjes_measure f. Lemma cdf_lebesgue_stieltjes_id r : cdf (idTR : {RV lsf >-> R}) r = (f r)%:E. Proof. @@ -277,12 +281,65 @@ have : lsf `]-n%:R, r] @[n --> \oo] --> (f r)%:E. apply: (cvg_comp _ _ (cvg_comp _ _ _ (cumulativeNy 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. + apply: nondecreasing_cvg_mu => //; 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. +End cdf_of_lebesgue_stieltjes_measure. + +Section lebesgue_stieltjes_measure_of_cdf. +Context {R : realType} (P : probability (measurableTypeR R) R). +Local Open Scope measure_display_scope. + +Let idTR : measurableTypeR R -> R := idfun. + +#[local] HB.instance Definition _ := + @isMeasurableFun.Build _ _ _ _ idTR (@measurable_id _ _ setT). + +Let fcdf r := fine (cdf (idTR : {RV P >-> R}) r). + +Let fcdf_nd : nondecreasing fcdf. +Proof. +by move=> *; apply: fine_le; [exact: cdf_fin_num.. | exact: cdf_nondecreasing]. +Qed. + +Let fcdf_rc : right_continuous fcdf. +Proof. +move=> a; apply: fine_cvg. +by rewrite fineK; [exact: cdf_right_continuous | exact: cdf_fin_num]. +Qed. + +#[local] HB.instance Definition _ := + isCumulative.Build R _ R fcdf fcdf_nd fcdf_rc. + +Let fcdf_Ny0 : fcdf @ -oo --> (0:R). +Proof. exact/fine_cvg/cvg_cdfNy0. Qed. + +Let fcdf_y1 : fcdf @ +oo --> (1:R). +Proof. exact/fine_cvg/cvg_cdfy1. Qed. + +#[local] HB.instance Definition _ := + isCumulativeBounded.Build R 0 1 fcdf fcdf_Ny0 fcdf_y1. + +Let lscdf := lebesgue_stieltjes_measure fcdf. + +Lemma lebesgue_stieltjes_cdf_id (A : set _) (mA : measurable A) : lscdf A = P A. +Proof. +apply: lebesgue_stieltjes_measure_unique => [I [[a b]]/= _ <- | //]. +rewrite /lebesgue_stieltjes_measure /measure_extension/=. +rewrite measurable_mu_extE/=; last exact: is_ocitv. +have [ab | ba] := leP a b; last first. + by rewrite set_itv_ge ?wlength0 ?measure0// bnd_simp -leNgt ltW. +rewrite wlength_itv_bnd// EFinB !fineK ?cdf_fin_num//. +rewrite /cdf /distribution /pushforward !preimage_id. +have : `]a, b]%classic = `]-oo, b] `\` `]-oo, a] => [|->]. + by rewrite -[RHS]setCK setCD setCitvl setUC -[LHS]setCK setCitv. +rewrite measureD ?setIidr//; first exact: subset_itvl. +by rewrite -ge0_fin_numE// fin_num_measure. +Qed. + +End lebesgue_stieltjes_measure_of_cdf. HB.lock Definition expectation {d} {T : measurableType d} {R : realType} (P : probability T R) (X : T -> R) := (\int[P]_w (X w)%:E)%E.