diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 022e7edce..8ea86f0d2 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -52,38 +52,33 @@ - in `lebesgue_integral.v`: + notations `\x`, `\x^` for `product_measure1` and `product_measure2` +- file `ereal.v`: + + lemmas `compreBr`, `compre_scale` + + lemma `le_er_map` +- file `lebesgue_integral.v`: + + instance of `isMeasurableFun` for `normr` + + lemma `finite_measure_integrable_cst` + + lemma `measurable_fun_er_map` - file `probability.v`: - + mixin `isConvn`, structure `Convn`, notation `convn` - + lemmas `probability_fin_num`, `probability_integrable_cst`, - + definition `mexp`, instance of `isMeasurableFun` - + definition `subr`, instance of `isMeasurableFun` - + definition `mabs`, instance of `isMeasurableFun` - + `\*` instance of `isMeasurableFun` - + `\o` instance of `isMeasurableFun` + + definition `Lspace`, notation `.-Lspace` + + lemmas `Lspace1`, `Lspace2` + definition `random_variable`, notation `{RV _ >-> _}` - + lemmas `notin_range_probability`, `probability_range` - + definition `comp_RV`, notation ``` `o ````, - definition `exp_RV`, notation ``` `^+ ```, - definition `add_RV`, notation ``` `+ ```, - definition `sub_RV`, notation ``` `- ```, - definition `mul_RV`, notation ``` `* ```, - definition `scale_RV`, notation ``` `\o* ``` - + lemma `mul_cst` - + definition `expectation`, notation `'E` + + lemmas `notin_range_measure`, `probability_range` + + definition `distribution`, instance of `isProbability` + + lemma `probability_distribution`, `integral_distribution` + + definition `expectation`, notation `'E_P[X]` + lemmas `expectation_cst`, `expectation_indic`, `integrable_expectation`, `expectationM`, `expectation_ge0`, `expectation_le`, `expectationD`, `expectationB` - + definition `Lspace`, notation `.-Lspace` - + lemmas `Lspace1`, `Lspace2` - + definition `variance`, `'V` + + definition `variance`, `'V_P[X]` + lemma `varianceE` - + definition `distribution`, instance of `isProbability` - + lemmas `integral_distribution`, `markov`, `chebyshev`, - + mixin `isDiscreteRV`, structure `DiscreteRV`, type `discrete_random_variable`, - notation `{dRV _ >-> _}` + + lemmas `markov`, `chebyshev`, + + mixin `MeasurableFun_isDiscrete`, structure `discreteMeasurableFun`, + notation `{dmfun aT >-> T}` + + definition `discrete_random_variable`, notation `{dRV _ >-> _}` + definitions `dRV_dom_enum`, `dRV_dom`, `dRV_enum`, `enum_prob` - + lemmas `distribution_dRV_enum`, `distribution_dRV`, `convn_enum_prob`, - `probability_distribution`, `dRV_expectation` + + lemmas `distribution_dRV_enum`, `distribution_dRV`, `sum_enum_prob`, + `dRV_expectation` + definion `pmf`, lemma `expectation_pmf` ### Changed @@ -96,6 +91,10 @@ ### Removed +- in `lebesgue_measure.v`: + + `emeasurable_fun_bool` -> `measurable_fun_bool` + + ### Infrastructure ### Misc diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 1432af622..6ad81de4e 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -30,6 +30,7 @@ Require Import signed. (* r%:E == injects real numbers into \bar R *) (* +%E, -%E, *%E == addition/opposite/multiplication for extended *) (* reals *) +(* er_map (f : T -> T') == the \bar T -> \bar T' lifting of f *) (* `| x |%E == the absolute value of x *) (* x ^+ n == iterated multiplication *) (* x *+ n == iterated addition *) diff --git a/theories/ereal.v b/theories/ereal.v index db25e52e8..8de828de1 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -99,6 +99,16 @@ rewrite predeqE => t; split => //=; apply/eqP. by rewrite gt_eqF// (lt_le_trans _ (abse_ge0 t)). Qed. +Lemma compreBr T (h : R -> \bar R) (f g : T -> R) : + {morph h : x y / (x - y)%R >-> (x - y)%E} -> + h \o (f \- g)%R = ((h \o f) \- (h \o g))%E. +Proof. by move=> mh; apply/funext => t /=; rewrite mh. Qed. + +Lemma compre_scale T (h : R -> \bar R) (f : T -> R) k : + {morph h : x y / (x * y)%R >-> (x * y)%E} -> + h \o (k \o* f) = (fun t => h k * h (f t))%E. +Proof. by move=> mf; apply/funext => t /=; rewrite mf; rewrite muleC. Qed. + Local Close Scope classical_set_scope. End ERealArith. @@ -139,6 +149,15 @@ Section ERealArithTh_realDomainType. Context {R : realDomainType}. Implicit Types (x y z u a b : \bar R) (r : R). +Lemma le_er_map (f : R -> R) : + {in `[0, +oo[%classic%R &, {homo f : x y / (x <= y)%O}} -> + {in `[0, +oo[%classic%E &, {homo er_map f : x y / (x <= y)%E}}. +Proof. +move=> f_nd x y; rewrite !inE/= !in_itv/= !andbT. +move: x y => [x| |] [y| |] x0 y0 xy//=; last by rewrite leey. +by rewrite lee_fin f_nd// inE /= in_itv/= andbT -lee_fin. +Qed. + Lemma fsume_gt0 (I : choiceType) (P : set I) (F : I -> \bar R) : 0 < \sum_(i \in P) F i -> exists2 i, P i & 0 < F i. Proof. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 96bb978d3..220f66f7a 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -152,6 +152,9 @@ Definition cst_mfun x := [the {mfun aT >-> rT} of cst x]. Lemma mfun_cst x : @cst_mfun x =1 cst x. Proof. by []. Qed. +HB.instance Definition _ := @isMeasurableFun.Build _ _ rT + (@normr rT rT) (@measurable_fun_normr rT setT). + End mfun. Section ring. @@ -2960,6 +2963,21 @@ Qed. End integrable_lemmas. Arguments integrable_mkcond {d T R mu D} f. +Lemma finite_measure_integrable_cst d (T : measurableType d) (R : realType) + (mu : {finite_measure set T -> \bar R}) k : + mu.-integrable [set: T] (EFin \o cst k). +Proof. +split; first exact/EFin_measurable_fun/measurable_fun_cst. +have [k0|k0] := leP 0 k. +- under eq_integral do rewrite /= ger0_norm//. + rewrite integral_cstr//= lte_mul_pinfty// fin_num_fun_lty//. + exact: fin_num_measure. +- under eq_integral do rewrite /= ltr0_norm//. + rewrite integral_cstr//= lte_mul_pinfty//. + by rewrite lee_fin ler_oppr oppr0 ltW. + by rewrite fin_num_fun_lty//; exact: fin_num_measure. +Qed. + Section integrable_ae. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 64e5d5d34..418fb5dfe 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1756,29 +1756,26 @@ congr (_ `&` _);rewrite eqEsubset; split=> [|? []/= _ /[swap] -[->//]]. by move=> ? ?; exact: preimage_image. Qed. +Lemma measurable_fun_er_map d (T : measurableType d) (R : realType) (f : R -> R) + : measurable_fun setT f -> measurable_fun [set: \bar R] (er_map f). +Proof. +move=> mf;rewrite (_ : er_map _ = + fun x => if x \is a fin_num then (f (fine x))%:E else x); last first. + by apply: funext=> -[]. +apply: measurable_fun_ifT => /=. ++ apply: (measurable_fun_bool true). + rewrite /preimage/= -[X in measurable X]setTI. + by apply/emeasurable_fin_num => //; exact: measurable_fun_id. ++ apply/EFin_measurable_fun/measurable_funT_comp => //. + exact/measurable_fun_fine. ++ exact: measurable_fun_id. +Qed. + Section emeasurable_fun. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType). Implicit Types (D : set T). -Lemma emeasurable_fun_bool (D : set T) (f : T -> bool) b : - measurable (f @^-1` [set b]) -> measurable_fun D f. -Proof. -have FNT : [set false] = [set~ true] by apply/seteqP; split => -[]//=. -wlog {b}-> : b / b = true. - case: b => [|h]; first exact. - by rewrite FNT -preimage_setC => /measurableC; rewrite setCK; exact: h. -move=> mfT mD /= Y; have := @subsetT _ Y; rewrite setT_bool => YT. -have [-> _|-> _|-> _ |-> _] := subset_set2 YT. -- by rewrite preimage0 ?setI0. -- by apply: measurableI => //; exact: mfT. -- rewrite -[X in measurable X]setCK; apply: measurableC; rewrite setCI. - apply: measurableU; first exact: measurableC. - by rewrite FNT preimage_setC setCK; exact: mfT. -- by rewrite -setT_bool preimage_setT setIT. -Qed. -Arguments emeasurable_fun_bool {D f} b. - Lemma measurable_fun_einfs D (f : (T -> \bar R)^nat) : (forall n, measurable_fun D (f n)) -> forall n, measurable_fun D (fun x => einfs (f ^~ x) n). diff --git a/theories/probability.v b/theories/probability.v index ddf80de77..67928481a 100644 --- a/theories/probability.v +++ b/theories/probability.v @@ -12,12 +12,12 @@ Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral. (* This file provides basic notions of probability theory. See measure.v for *) (* the type probability T R (a measure that sums to 1). *) (* *) +(* mu.-Lspace p := [set f : T -> R | measurable_fun setT f /\ *) +(* \int[mu]_(x in D) (`|f x| ^+ p)%:E < +oo] *) (* {RV P >-> R} == real random variable: a measurable function from *) (* the measurableType of the probability P to R *) (* distribution X == measure image of P by X : {RV P -> R}, declared *) (* as an instance of probability measure *) -(* mu.-Lspace p := [set f : T -> R | measurable_fun setT f /\ *) -(* \int[mu]_(x in D) (`|f x| ^+ p)%:E < +oo] *) (* 'E_P[X] == expectation of the real measurable function X *) (* 'V_P[X] == variance of the real random variable X *) (* {dmfun T >-> R} == type of discrete real-valued measurable functions *) @@ -49,57 +49,6 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -(* TODO: move *) -Definition funEFin {R : numDomainType} (f : R -> R) : \bar R -> \bar R := - fun x => if x is r%:E then (f r)%:E else x. - -Lemma measurable_fun_funEFin (R : realType) (f : R -> R) : - measurable_fun setT f -> - measurable_fun [set: \bar R] (@funEFin R f). -Proof. -move=> mf;rewrite (_ : funEFin _ = - fun x => if x \is a fin_num then (f (fine x))%:E else x); last first. - by apply: funext=> -[]. -apply: measurable_fun_ifT => /=. -+ apply: (@emeasurable_fun_bool _ _ _ _ true). - rewrite /preimage/= -[X in measurable X]setTI. - by apply/emeasurable_fin_num => //; exact: measurable_fun_id. -+ apply/EFin_measurable_fun/measurable_funT_comp => //. - exact/measurable_fun_fine. -+ exact: measurable_fun_id. -Qed. - -Lemma le_funEFin (R : realType) (f : R -> R) : - {in `[0, +oo[%classic%R &, {homo f : x y / (x <= y)}} -> - {in `[0, +oo[%classic%E &, {homo funEFin f : x y / (x <= y)%E}}. -Proof. -move=> f_nd x y; rewrite !inE/= !in_itv/= !andbT. -move: x y => [x| |] [y| |] x0 y0 xy//=; last by rewrite leey. -by rewrite lee_fin f_nd// inE /= in_itv/= andbT -lee_fin. -Qed. - -Section finite_measure_lemma. -Context d (T : measurableType d) (R : realType). - -Lemma finite_measure_integrable_cst (P : {finite_measure set T -> \bar R}) k : - P.-integrable [set: T] (EFin \o cst k). -Proof. -split; first exact/EFin_measurable_fun/measurable_fun_cst. -have [k0|k0] := leP 0 k. -- under eq_integral do rewrite /= ger0_norm//. - rewrite integral_cst//= lte_mul_pinfty// fin_num_fun_lty//. - exact: fin_num_measure. -- under eq_integral do rewrite /= ltr0_norm//. - rewrite integral_cst//= lte_mul_pinfty//. - by rewrite lee_fin ler_oppr oppr0 ltW. - by rewrite fin_num_fun_lty//; exact: fin_num_measure. -Qed. - -End finite_measure_lemma. - -HB.instance Definition _ (R : realType) := @isMeasurableFun.Build _ _ R - (@normr R R) (@measurable_fun_normr R setT). - Section Lspace. Context d (T : measurableType d) (R : realType). Variable mu : {measure set T -> \bar R}. @@ -135,8 +84,8 @@ Definition random_variable (d : _) (T : measurableType d) (R : realType) Notation "{ 'RV' P >-> R }" := (@random_variable _ _ R P) : form_scope. -Lemma notin_range_probability d (T : measurableType d) (R : realType) - (P : probability T R) (X : {RV P >-> R}) r : +Lemma notin_range_measure 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_set => hr; rewrite preimage10. Qed. @@ -256,17 +205,6 @@ Proof. by move=> ? ?; rewrite /expectation integralB_EFin. Qed. End expectation_lemmas. -(* TODO: move *) -Lemma compreBr (R : numDomainType) T (h : R -> \bar R) (f g : T -> R) : - {morph h : x y / (x - y)%R >-> (x - y)%E} -> - h \o (f \- g)%R = ((h \o f) \- (h \o g))%E. -Proof. by move=> mh; apply/funext => t /=; rewrite mh. Qed. - -Lemma compre_scale (R : numDomainType) T (h : R -> \bar R) (f : T -> R) k : - {morph h : x y / (x * y)%R >-> (x * y)%E} -> - h \o (k \o* f) = (fun x => h k * h (f x))%E. -Proof. by move=> mf; apply/funext => t /=; rewrite mf; rewrite muleC. Qed. - Section variance. Local Open Scope ereal_scope. Context d (T : measurableType d) (R : realType) (P : probability T R). @@ -282,16 +220,16 @@ have ? : P.-integrable [set: T] (EFin \o X) by rewrite Lspace1 in X1. have ? : P.-integrable [set: T] (EFin \o (X ^+ 2)%R) by apply: Lspace2. have ? : 'E_P[X] \is a fin_num by rewrite fin_num_abs// integrable_expectation. rewrite /variance. -rewrite [X in 'E_P[X]](_ : _ = - (X ^+ 2 \- (2 * fine 'E_P[X]) \o* X \+ fine ('E_P[X] ^+ 2) \o* cst 1)%R); last first. - apply/funeqP => x /=. - by rewrite -expr2 sqrrB mulr_natl -mulrnAr mul1r fineM. +rewrite [X in 'E_P[X]](_ : _ = (X ^+ 2 \- (2 * fine 'E_P[X]) \o* X \+ + fine ('E_P[X] ^+ 2) \o* cst 1)%R); last first. + by apply/funeqP => x /=; rewrite -expr2 sqrrB mulr_natl -mulrnAr mul1r fineM. rewrite expectationD/=; last 2 first. - rewrite compreBr; last by []. apply: integrableB; [exact: measurableT|assumption|]. by rewrite compre_scale; [exact: integrablerM|by []]. - rewrite compre_scale; last by []. - by apply: integrablerM; [exact: measurableT|exact: finite_measure_integrable_cst]. + apply: integrablerM; first exact: measurableT. + exact: finite_measure_integrable_cst. rewrite expectationB/=; [|assumption|]; last first. by rewrite compre_scale; [exact: integrablerM|by []]. rewrite expectationM// expectationM; last exact: finite_measure_integrable_cst. @@ -316,10 +254,10 @@ Lemma markov (X : {RV P >-> R}) (f : R -> R) (eps : R) : Proof. move=> e0 mf f0 f_nd; rewrite -(setTI [set _ | _]). apply: (le_trans (@le_integral_comp_abse d T R P setT measurableT (EFin \o X) - eps (funEFin f) _ _ _ _ e0)) => //=. -- exact: measurable_fun_funEFin. + eps (er_map f) _ _ _ _ e0)) => //=. +- exact: measurable_fun_er_map. - by case => //= r _; exact: f0. -- exact: le_funEFin. +- exact: le_er_map. - exact/EFin_measurable_fun. Qed. @@ -496,14 +434,16 @@ Qed. Definition pmf (X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])). -Lemma expectation_pmf (X : {dRV P >-> R}) : P.-integrable [set: T] (EFin \o X) -> - 'E_P[X] = - (\sum_(n -> R}) : + P.-integrable [set: T] (EFin \o X) -> 'E_P[X] = + \sum_(n iX; rewrite dRV_expectation// [in RHS]eseries_mkcond. apply: eq_eseriesr => k _. rewrite /enum_prob patchE; case: ifPn => kX; last by rewrite mul0e. by rewrite /pmf fineK// fin_num_measure. Qed. +Local Close Scope ereal_scope. End discrete_distribution.