From 4854dad1d305c879dac020e337c913ec9d9ed906 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 3 Dec 2024 11:26:24 +0900 Subject: [PATCH] generalize the return type of RVs Co-authored-by: Alessandro Bruni --- CHANGELOG_UNRELEASED.md | 18 +++++++ theories/probability.v | 107 ++++++++++++++++++++++------------------ 2 files changed, 77 insertions(+), 48 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index acacf8db1..a7d5070d0 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,12 +10,30 @@ - in `normedtype.v`: + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP` +- in `probability.v`: + + lemma `expectation_def` + ### Changed ### Renamed +- in `probability.v`: + + `expectationM` -> `expectationMl` + ### Generalized +- in `probability.v`: + + definition `random_variable` + + lemmas `notin_range_measure`, `probability_range` + + definition `distribution` + + lemma `probability_distribution`, `integral_distribution` + + mixin `MeasurableFun_isDiscrete` + + structure `discreteMeasurableFun` + + definition `discrete_random_variable` + + lemma `dRV_dom_enum` + + definitions `dRV_dom`, `dRV_enum`, `enum_prob` + + lemmas `distribution_dRV`, `sum_enum_prob` + ### Deprecated ### Removed diff --git a/theories/probability.v b/theories/probability.v index c57cac324..cc6787ae8 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -72,27 +72,29 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Definition random_variable (d : _) (T : measurableType d) (R : realType) - (P : probability T R) := {mfun T >-> R}. +Definition random_variable d d' (T : measurableType d) (T' : measurableType d') + (R : realType) (P : probability T R) := {mfun T >-> T'}. -Notation "{ 'RV' P >-> R }" := (@random_variable _ _ R P) : form_scope. +Notation "{ 'RV' P >-> T' }" := (@random_variable _ _ _ T' _ P) : form_scope. -Lemma notin_range_measure d (T : measurableType d) (R : realType) - (P : {measure set T -> \bar R}) (X : T -> R) r : +Lemma notin_range_measure d d' (T : measurableType d) (T' : measurableType d') + (R : realType) (P : {measure set T -> \bar R}) (X : T -> R) r : r \notin range X -> P (X @^-1` [set r]) = 0%E. Proof. by rewrite notin_setE => hr; rewrite preimage10. Qed. -Lemma probability_range d (T : measurableType d) (R : realType) - (P : probability T R) (X : {RV P >-> R}) : P (X @^-1` range X) = 1%E. +Lemma probability_range d d' (T : measurableType d) (T' : measurableType d') + (R : realType) (P : probability T R) (X : {RV P >-> R}) : + P (X @^-1` range X) = 1%E. Proof. by rewrite preimage_range probability_setT. Qed. -Definition distribution d (T : measurableType d) (R : realType) - (P : probability T R) (X : {mfun T >-> R}) := +Definition distribution d d' (T : measurableType d) (T' : measurableType d') + (R : realType) (P : probability T R) (X : {mfun T >-> T'}) := pushforward P (@measurable_funP _ _ _ _ X). Section distribution_is_probability. -Context d (T : measurableType d) (R : realType) (P : probability T R) - (X : {mfun T >-> R}). +Context d d' {T : measurableType d} {T' : measurableType d'} {R : realType} + {P : probability T R}. +Variable X : {mfun T >-> T'}. Let distribution0 : distribution P X set0 = 0%E. Proof. exact: measure0. Qed. @@ -103,7 +105,7 @@ Proof. exact: measure_ge0. Qed. Let distribution_sigma_additive : semi_sigma_additive (distribution P X). Proof. exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ := isMeasure.Build _ _ R (distribution P X) +HB.instance Definition _ := isMeasure.Build _ _ _ (distribution P X) distribution0 distribution_ge0 distribution_sigma_additive. Let distribution_is_probability : distribution P X [set: _] = 1%:E. @@ -111,21 +113,22 @@ Proof. by rewrite /distribution /= /pushforward /= preimage_setT probability_setT. Qed. -HB.instance Definition _ := Measure_isProbability.Build _ _ R +HB.instance Definition _ := Measure_isProbability.Build _ _ _ (distribution P X) distribution_is_probability. End distribution_is_probability. Section transfer_probability. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) (P : probability T R). +Context d d' {T : measurableType d} {T' : measurableType d'} {R : realType} + (P : probability T R). -Lemma probability_distribution (X : {RV P >-> R}) r : +Lemma probability_distribution (X : {RV P >-> T'}) r : P [set x | X x = r] = distribution P X [set r]. Proof. by []. Qed. -Lemma integral_distribution (X : {RV P >-> R}) (f : R -> \bar R) : - measurable_fun [set: R] f -> (forall y, 0 <= f y) -> +Lemma integral_distribution (X : {RV P >-> T'}) (f : T' -> \bar R) : + measurable_fun [set: T'] f -> (forall y, 0 <= f y) -> \int[distribution P X]_y f y = \int[P]_x (f \o X) x. Proof. by move=> mf f0; rewrite ge0_integral_pushforward. Qed. @@ -141,6 +144,9 @@ Section expectation_lemmas. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). +Lemma expectation_def (X : {RV P >-> R}) : 'E_P[X] = (\int[P]_w (X w)%:E)%E. +Proof. by rewrite unlock. Qed. + Lemma expectation_fin_num (X : {RV P >-> R}) : P.-integrable setT (EFin \o X) -> 'E_P[X] \is a fin_num. Proof. by move=> ?; rewrite unlock integral_fune_fin_num. Qed. @@ -158,7 +164,7 @@ move: iX => /integrableP[? Xoo]; rewrite (le_lt_trans _ Xoo)// unlock. exact: le_trans (le_abse_integral _ _ _). Qed. -Lemma expectationM (X : {RV P >-> R}) (iX : P.-integrable [set: T] (EFin \o X)) +Lemma expectationMl (X : {RV P >-> R}) (iX : P.-integrable [set: T] (EFin \o X)) (k : R) : 'E_P[k \o* X] = k%:E * 'E_P [X]. Proof. by rewrite unlock muleC -integralZr. Qed. @@ -208,6 +214,8 @@ by apply/funext => t/=; rewrite big_map sumEFin mfun_sum. Qed. End expectation_lemmas. +#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to `expectationMl`")] +Notation expectationM := expectationMl (only parsing). HB.lock Definition covariance {d} {T : measurableType d} {R : realType} (P : probability T R) (X Y : T -> R) := @@ -238,7 +246,7 @@ rewrite expectationD/=; last 2 first. - by rewrite compreBr// integrableB// compre_scale ?integrableZl. - by rewrite compre_scale// integrableZl// finite_measure_integrable_cst. rewrite 2?expectationB//= ?compre_scale// ?integrableZl//. -rewrite 3?expectationM//= ?finite_measure_integrable_cst//. +rewrite 3?expectationMl//= ?finite_measure_integrable_cst//. by rewrite expectation_cst mule1 fineM// EFinM !fineK// muleC subeK ?fin_numM. Qed. @@ -278,7 +286,7 @@ have aXY : (a \o* X * Y = a \o* (X * Y))%R. rewrite [LHS]covarianceE => [||//|] /=; last 2 first. - by rewrite compre_scale ?integrableZl. - by rewrite aXY compre_scale ?integrableZl. -rewrite covarianceE// aXY !expectationM//. +rewrite covarianceE// aXY !expectationMl//. by rewrite -muleA -muleBr// fin_num_adde_defr// expectation_fin_num. Qed. @@ -554,7 +562,7 @@ Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R -> Proof. move=> t0. rewrite /mmt_gen_fun; have -> : expR \o r \o* X = - (normr \o normr) \o [the {mfun T >-> R} of expR \o r \o* X]. + (normr \o normr) \o [the {mfun _ >-> _} of expR \o r \o* X]. by apply: funext => t /=; rewrite normr_id ger0_norm ?expR_ge0. rewrite expRN lee_pdivlMr ?expR_gt0//. rewrite (le_trans _ (markov _ (expR_gt0 (r * a)) _ _ _))//; last first. @@ -679,50 +687,53 @@ Qed. End markov_chebyshev_cantelli. -HB.mixin Record MeasurableFun_isDiscrete d (T : measurableType d) (R : realType) - (X : T -> R) of @MeasurableFun d _ T R X := { +HB.mixin Record MeasurableFun_isDiscrete d d' (T : measurableType d) + (T' : measurableType d') (X : T -> T') of @MeasurableFun d d' T T' X := { countable_range : countable (range X) }. -HB.structure Definition discreteMeasurableFun d (T : measurableType d) - (R : realType) := { - X of isMeasurableFun d _ T R X & MeasurableFun_isDiscrete d T R X +HB.structure Definition discreteMeasurableFun d d' (T : measurableType d) + (T' : measurableType d') := { + X of isMeasurableFun d d' T T' X & MeasurableFun_isDiscrete d d' T T' X }. Notation "{ 'dmfun' aT >-> T }" := - (@discreteMeasurableFun.type _ aT T) : form_scope. + (@discreteMeasurableFun.type _ _ aT T) : form_scope. -Definition discrete_random_variable (d : _) (T : measurableType d) - (R : realType) (P : probability T R) := {dmfun T >-> R}. +Definition discrete_random_variable d d' (T : measurableType d) + (T' : measurableType d') (R : realType) (P : probability T R) := + {dmfun T >-> T'}. -Notation "{ 'dRV' P >-> R }" := - (@discrete_random_variable _ _ R P) : form_scope. +Notation "{ 'dRV' P >-> T }" := + (@discrete_random_variable _ _ _ T _ P) : form_scope. Section dRV_definitions. -Context d (T : measurableType d) (R : realType) (P : probability T R). +Context {d} {d'} {T : measurableType d} {T' : measurableType d'} {R : realType} + (P : probability T R). -Definition dRV_dom_enum (X : {dRV P >-> R}) : +Lemma dRV_dom_enum (X : {dRV P >-> T'}) : { B : set nat & {splitbij B >-> range X}}. Proof. -have /countable_bijP/cid[B] := @countable_range _ _ _ X. +have /countable_bijP/cid[B] := @countable_range _ _ _ _ X. move/card_esym/ppcard_eqP/unsquash => f. exists B; exact: f. Qed. -Definition dRV_dom (X : {dRV P >-> R}) : set nat := projT1 (dRV_dom_enum X). +Definition dRV_dom (X : {dRV P >-> T'}) : set nat := projT1 (dRV_dom_enum X). -Definition dRV_enum (X : {dRV P >-> R}) : {splitbij (dRV_dom X) >-> range X} := +Definition dRV_enum (X : {dRV P >-> T'}) : {splitbij (dRV_dom X) >-> range X} := projT2 (dRV_dom_enum X). -Definition enum_prob (X : {dRV P >-> R}) := +Definition enum_prob (X : {dRV P >-> T'}) := (fun k => P (X @^-1` [set dRV_enum X k])) \_ (dRV_dom X). End dRV_definitions. Section distribution_dRV. Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType) (P : probability T R). -Variable X : {dRV P >-> R}. +Context d d' (T : measurableType d) (T' : measurableType d') (R : realType) + (P : probability T R). +Variable X : {dRV P >-> T'}. Lemma distribution_dRV_enum (n : nat) : n \in dRV_dom X -> distribution P X [set dRV_enum X n] = enum_prob X n. @@ -730,13 +741,15 @@ Proof. by move=> nX; rewrite /distribution/= /enum_prob/= patchE nX. Qed. +Hypothesis measurable_set1T' : forall x : T', measurable [set x]. + Lemma distribution_dRV A : measurable A -> distribution P X A = \sum_(k mA; rewrite /distribution /pushforward. have mAX i : dRV_dom X i -> measurable (X @^-1` (A `&` [set dRV_enum X i])). - move=> _; rewrite preimage_setI; apply: measurableI => //. - exact/measurable_sfunP. + move=> domXi; rewrite preimage_setI. + by apply: measurableI; rewrite //-[X in _ X]setTI; exact/measurable_funP. have tAX : trivIset (dRV_dom X) (fun k => X @^-1` (A `&` [set dRV_enum X k])). under eq_fun do rewrite preimage_setI; rewrite -/(trivIset _ _). apply: trivIset_setIl; apply/trivIsetP => i j iX jX /eqP ij. @@ -746,13 +759,11 @@ have := measure_bigcup P _ (fun k => X @^-1` (A `&` [set dRV_enum X k])) mAX tAX rewrite -preimage_bigcup => {mAX tAX}PXU. rewrite -{1}(setIT A) -(setUv (\bigcup_(i in dRV_dom X) [set dRV_enum X i])). rewrite setIUr preimage_setU measureU; last 3 first. - - rewrite preimage_setI; apply: measurableI => //. - exact: measurable_sfunP. - by apply: measurable_sfunP; exact: bigcup_measurable. - - apply: measurable_sfunP; apply: measurableI => //. - by apply: measurableC; exact: bigcup_measurable. - - rewrite 2!preimage_setI setIACA -!setIA -preimage_setI. - by rewrite setICr preimage_set0 2!setI0. + - by rewrite preimage_setI; apply: measurableI; rewrite //-[X in _ X]setTI; + apply/measurable_funP => //; exact: bigcup_measurable. + - by rewrite preimage_setI; apply: measurableI; rewrite //-[X in _ X]setTI; + apply/measurable_funP => //; apply: measurableC; exact: bigcup_measurable. + - by rewrite -preimage_setI -setIIr setIA setICK preimage_set0. rewrite [X in _ + X = _](_ : _ = 0) ?adde0; last first. rewrite (_ : _ @^-1` _ = set0) ?measure0//; apply/disjoints_subset => x AXx. rewrite setCK /bigcup /=; exists ((dRV_enum X)^-1 (X x))%function.