diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9d260b055..1eb68223b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -24,6 +24,9 @@ - in `constructive_ereal.v`: + notations `\prod` in scope ereal_scope + lemmas `prode_ge0`, `prode_fin_num` +- in `probability.v`: + + lemma `expectation_def` + + notation `'M_` ### Changed @@ -37,6 +40,8 @@ + `emeasurable_fun_sum` -> `emeasurable_sum` + `emeasurable_fun_fsum` -> `emeasurable_fsum` + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum` +- in `probability.v`: + + `expectationM` -> `expectationZl` - in `classical_sets.v`: + `preimage_itv_o_infty` -> `preimage_itvoy` @@ -52,6 +57,18 @@ ### 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 - in file `lebesgue_integral.v`: diff --git a/theories/probability.v b/theories/probability.v index 0dfa28de6..d66943139 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -16,23 +16,24 @@ From mathcomp Require Import 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 *) +(* {RV P >-> T'} == random variable: a measurable function to the *) +(* measurableType T' from the measured space *) +(* characterized by the probability P *) (* distribution P X == measure image of the probability measure P by the *) -(* random variable X : {RV P -> R} *) +(* random variable X : {RV P -> T'} *) (* 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 *) +(* 'M_ 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])) *) +(* pmf X r := fine (P (X @^-1` [set r])) *) (* enum_prob X k == probability of the kth value in the range of X *) (* ``` *) (* *) @@ -57,6 +58,8 @@ Reserved Notation "'{' 'RV' P >-> R '}'" (at level 0, format "'{' 'RV' P '>->' R '}'"). Reserved Notation "''E_' P [ X ]" (format "''E_' P [ X ]", at level 5). Reserved Notation "''V_' P [ X ]" (format "''V_' P [ X ]", at level 5). +Reserved Notation "'M_ X t" (format "''M_' X t", + at level 5, t, X at next level). Reserved Notation "{ 'dmfun' aT >-> T }" (at level 0, format "{ 'dmfun' aT >-> T }"). Reserved Notation "'{' 'dRV' P >-> R '}'" @@ -72,27 +75,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 +108,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 +116,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 +147,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 +167,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 expectationZl (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 +217,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 `expectationZl`")] +Notation expectationM := expectationZl (only parsing). HB.lock Definition covariance {d} {T : measurableType d} {R : realType} (P : probability T R) (X Y : T -> R) := @@ -238,7 +249,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?expectationZl//= ?finite_measure_integrable_cst//. by rewrite expectation_cst mule1 fineM// EFinM !fineK// muleC subeK ?fin_numM. Qed. @@ -278,7 +289,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 !expectationZl//. by rewrite -muleA -muleBr// fin_num_adde_defr// expectation_fin_num. Qed. @@ -548,13 +559,14 @@ apply: (le_trans (@le_integral_comp_abse _ _ _ P _ measurableT (EFin \o X) Qed. Definition mmt_gen_fun (X : {RV P >-> R}) (t : R) := 'E_P[expR \o t \o* X]. +Local Notation "'M_ X t" := (mmt_gen_fun X t). Lemma chernoff (X : {RV P >-> R}) (r a : R) : (0 < r)%R -> - P [set x | X x >= a]%R <= mmt_gen_fun X r * (expR (- (r * a)))%:E. + P [set x | X x >= a]%R <= 'M_X r * (expR (- (r * a)))%:E. 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 +691,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 +745,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 +763,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.