diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fbc855f68b..63d78e75d1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -61,6 +61,84 @@ + lemmas `inum_eq`, `inum_le`, `inum_lt` - in `measure.v`: + lemmas `ae_imply`, `ae_imply2` +- in `classical_sets.v`: + + canonical `unit_pointedType` +- in `measure.v`: + + definition `finite_measure` + + mixin `isProbability`, structure `Probability`, type `probability` + + lemma `probability_le1` + + definition `discrete_measurable_unit` + + structures `sigma_finite_additive_measure` and `sigma_finite_measure` + +- in file `topology.v`, + + new definition `perfect_set`. + + new lemmas `perfectTP`, `perfect_prod`, and `perfect_diagonal`. + +- in `constructive_ereal.v`: + + lemma `oppe_inj` + +- in `mathcomp_extra.v`: + + lemma `add_onemK` + + function `swap` +- in `classical_sets.v`: + + lemmas `setT0`, `set_unit`, `set_bool` + + lemmas `xsection_preimage_snd`, `ysection_preimage_fst` +- in `exp.v`: + + lemma `expR_ge0` +- in `measure.v` + + lemmas `measurable_curry`, `measurable_fun_fst`, `measurable_fun_snd`, + `measurable_fun_swap`, `measurable_fun_pair`, `measurable_fun_if_pair` + + lemmas `dirac0`, `diracT` + + lemma `finite_measure_sigma_finite` +- in `lebesgue_measure.v`: + + lemma `measurable_fun_opp` +- in `lebesgue_integral.v` + + lemmas `integral0_eq`, `fubini_tonelli` + + product measures now take `{measure _ -> _}` arguments and their + theory quantifies over a `{sigma_finite_measure _ -> _}`. + +- in `classical_sets.v`: + + lemma `trivIset_mkcond` +- in `numfun.v`: + + lemmas `xsection_indic`, `ysection_indic` +- in `classical_sets.v`: + + lemmas `xsectionI`, `ysectionI` +- 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` + + lemma `ae_ge0_le_integral` + + lemma `ae_eq_refl` +- file `probability.v`: + + mixin `isLfun`, structure `Lfun`, notation `LfunType` + + canonicals `Lfun_eqType`, `Lfun_choiceType`, `Lequiv_canonical` + + definition `LType` + + definition `Lspace`, notation `.-Lspace` + + lemmas `LequivP`, `Lspace1`, `Lspace2` + + definition `random_variable`, notation `{RV _ >-> _}` + + 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 `variance`, `'V_P[X]` + + lemma `varianceE` + + 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`, `sum_enum_prob`, + `dRV_expectation` + + definion `pmf`, lemma `expectation_pmf` ### Changed @@ -93,6 +171,7 @@ - in `lebesgue_measure.v`: + lemma `ae_eq_mul` + + `emeasurable_fun_bool` -> `measurable_fun_bool` ### Infrastructure diff --git a/_CoqProject b/_CoqProject index 594eaceef7..0db94c8411 100644 --- a/_CoqProject +++ b/_CoqProject @@ -36,6 +36,7 @@ theories/derive.v theories/measure.v theories/numfun.v theories/lebesgue_integral.v +theories/probability.v theories/summability.v theories/signed.v theories/itv.v diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 1432af622d..6ad81de4e1 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 db25e52e8f..d2a65e0191 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,14 @@ Section ERealArithTh_realDomainType. Context {R : realDomainType}. Implicit Types (x y z u a b : \bar R) (r : R). +Lemma le_er_map (A : set R) (f : R -> R) : + {in A &, {homo f : x y / (x <= y)%O}} -> + {in (EFin @` A)%classic &, {homo er_map f : x y / (x <= y)%E}}. +Proof. +move=> h x y; rewrite !inE/= => -[r Ar <-{x}] [s As <-{y}]. +by rewrite !lee_fin/= => /h; apply; rewrite inE. +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 458003bb87..f1df7cfb51 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). @@ -4002,6 +4020,31 @@ Qed. End dominated_convergence_theorem. +Section ae_ge0_le_integral. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType). +Variable mu : {measure set T -> \bar R}. +Variables (D : set T) (mD : measurable D) (f1 f2 : T -> \bar R). +Hypothesis f10 : forall x, D x -> 0 <= f1 x. +Hypothesis mf1 : measurable_fun D f1. +Hypothesis f20 : forall x, D x -> 0 <= f2 x. +Hypothesis mf2 : measurable_fun D f2. + +Lemma ae_ge0_le_integral : {ae mu, forall x, D x -> f1 x <= f2 x} -> + \int[mu]_(x in D) f1 x <= \int[mu]_(x in D) f2 x. +Proof. +move=> [N [mN muN f1f2N]]; rewrite (negligible_integral _ _ _ _ muN)//. +rewrite [leRHS](negligible_integral _ _ _ _ muN)//. +apply: ge0_le_integral; first exact: measurableD. +- by move=> t [Dt _]; exact: f10. +- exact: measurable_funS mf1. +- by move=> t [Dt _]; exact: f20. +- exact: measurable_funS mf2. +- by move=> t [Dt Nt]; move/subsetCl : f1f2N; apply. +Qed. + +End ae_ge0_le_integral. + (******************************************************************************) (* * product measure *) (******************************************************************************) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 94a5f5e7d8..44cd730afa 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1754,29 +1754,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 new file mode 100644 index 0000000000..a496037916 --- /dev/null +++ b/theories/probability.v @@ -0,0 +1,647 @@ +(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import all_ssreflect. +From mathcomp Require Import ssralg ssrnum ssrint interval finmap. +Require Import boolp reals ereal. +From HB Require Import structures. +Require Import classical_sets signed functions topology normedtype cardinality. +Require Import sequences esum measure numfun lebesgue_measure lebesgue_integral. + +(******************************************************************************) +(* Probability (experimental) *) +(* *) +(* This file provides basic notions of probability theory. See measure.v for *) +(* the type probability T R (a measure that sums to 1). *) +(* *) +(* LfunType mu p == type of measurable functions f such that the *) +(* integral of |f| ^ p is finite *) +(* LType mu p == type of the elements of the Lp space *) +(* mu.-Lspace p == Lp space *) +(* {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 *) +(* '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 *) +(* {dRV P >-> R} == real-valued discrete random variable *) +(* dRV_dom X == domain of the discrete random variable X *) +(* dRV_eunm X == bijection between the domain and the range of X *) +(* pmf X r := fine (P (X @^-1` [set r])) *) +(* enum_prob X k == probability of the kth value in the range of X *) +(* *) +(******************************************************************************) + +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 "mu .-Lspace p" (at level 4, format "mu .-Lspace p"). +Reserved Notation "''V_' P [ X ]" (format "''V_' P [ X ]", at level 5). +Reserved Notation "{ 'dmfun' aT >-> T }" + (at level 0, format "{ 'dmfun' aT >-> T }"). +Reserved Notation "'{' 'dRV' P >-> R '}'" + (at level 0, format "'{' 'dRV' P '>->' R '}'"). + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +HB.mixin Record isLfun d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (p : nat) (f : T -> R) := { + measurable_lfun : measurable_fun [set: T] f ; + lfuny : (\int[mu]_x (`|f x| ^+ p)%:E < +oo)%E +}. + +#[short(type=LfunType)] +HB.structure Definition LFun d (T : measurableType d) (R : realType) + (mu : {measure set T -> \bar R}) (p : nat) := + {f : T -> R & isLfun d T R mu p f}. + +#[global] Hint Resolve measurable_lfun : core. +Arguments lfuny {d} {T} {R} {mu} {p} _. +#[global] Hint Resolve lfuny : core. + +Section Lfun_canonical. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : nat). + +Canonical Lfun_eqType := EqType (LfunType mu p) gen_eqMixin. +Canonical Lfun_choiceType := ChoiceType (LfunType mu p) gen_choiceMixin. +End Lfun_canonical. + +Section Lequiv. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (p : nat). + +Definition Lequiv (f g : LfunType mu p) := `[< {ae mu, forall x, f x = g x} >]. + +Let Lequiv_refl : reflexive Lequiv. +Proof. +by move=> f; exact/asboolP/(ae_imply _ (ae_eq_refl mu setT (EFin \o f))). +Qed. + +Let Lequiv_sym : symmetric Lequiv. +Proof. +by move=> f g; apply/idP/idP => /asboolP h; apply/asboolP; exact: ae_imply h. +Qed. + +Let Lequiv_trans : transitive Lequiv. +Proof. +move=> f g h /asboolP gf /asboolP fh; apply/asboolP/(ae_imply2 _ gf fh). +by move=> x ->. +Qed. + +Canonical Lequiv_canonical := + EquivRel Lequiv Lequiv_refl Lequiv_sym Lequiv_trans. + +Local Open Scope quotient_scope. + +Let Ltype := {eq_quot Lequiv}. +Canonical Ltype_quotType := [quotType of Ltype]. +Canonical Ltype_eqType := [eqType of Ltype]. +Canonical Ltype_choiceType := [choiceType of Ltype]. +Canonical Ltype_eqQuotType := [eqQuotType Lequiv of Ltype]. + +Record LType := MemLType { Lfun_class : Ltype }. +Coercion LfunType_of_LType (f : LType) : LfunType mu p := repr (Lfun_class f). + +Canonical LType_subType' := [newType for Lfun_class]. +Canonical LType_subType := [subType Ltype of LfunType mu p by %/]. +Definition LType_eqMixin := Eval hnf in [eqMixin of LType by <:]. +Canonical LType_eqType := Eval hnf in EqType LType LType_eqMixin. +Definition LType_choiceMixin := Eval hnf in [choiceMixin of LType by <:]. +Canonical LType_choiceType := Eval hnf in ChoiceType LType LType_choiceMixin. + +Lemma LequivP (f g : LfunType mu p) : + reflect {ae mu, forall x, f x = g x} (f == g %[mod Ltype]). +Proof. by apply/(iffP idP); rewrite eqmodE// => /asboolP. Qed. + +End Lequiv. + +Section Lspace. +Context d (T : measurableType d) (R : realType). +Variable mu : {measure set T -> \bar R}. + +Definition Lspace p := [set: LType mu p]. +Arguments Lspace : clear implicits. + +Lemma Lspace1 (f : LType mu 1) : mu.-integrable setT (EFin \o f). +Proof. by split; [exact/EFin_measurable_fun|exact: lfuny f]. Qed. + +Lemma Lspace2 (f : LType mu 2%N) : + mu.-integrable [set: T] (EFin \o (fun x => f x ^+ 2)). +Proof. +split. +- exact/EFin_measurable_fun/measurable_fun_exprn. +- rewrite (le_lt_trans _ (lfuny f))// ge0_le_integral//. + + apply: measurable_funT_comp => //. + exact/EFin_measurable_fun/measurable_fun_exprn. + + apply/EFin_measurable_fun/measurable_fun_exprn. + exact: measurable_funT_comp. + + by move=> t _/=; rewrite lee_fin normrX. +Qed. + +End Lspace. +Notation "mu .-Lspace p" := (@Lspace _ _ _ mu p) : type_scope. + +Definition random_variable (d : _) (T : measurableType d) (R : realType) + (P : probability T R) := {mfun T >-> R}. + +Notation "{ 'RV' P >-> R }" := (@random_variable _ _ R P) : form_scope. + +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. + +Lemma probability_range 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}) := + pushforward P (@measurable_funP _ _ _ X). + +Section distribution_is_probability. +Context d (T : measurableType d) (R : realType) (P : probability T R) + (X : {mfun T >-> R}). + +Let distribution0 : distribution P X set0 = 0%E. +Proof. exact: measure0. Qed. + +Let distribution_ge0 A : (0 <= distribution P X A)%E. +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) + distribution0 distribution_ge0 distribution_sigma_additive. + +Let distribution_is_probability : distribution P X [set: _] = 1%:E. +Proof. +by rewrite /distribution /= /pushforward /= preimage_setT probability_setT. +Qed. + +HB.instance Definition _ := Measure_isProbability.Build _ _ R + (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). + +Lemma probability_distribution (X : {RV P >-> R}) 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) -> + \int[distribution P X]_y f y = \int[P]_x (f \o X) x. +Proof. by move=> mf f0; rewrite integral_pushforward. Qed. + +End transfer_probability. + +Section expectation. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +Definition expectation (X : T -> R) := \int[P]_w (X w)%:E. + +End expectation. +Arguments expectation {d T R} P _%R. +Notation "''E_' P [ X ]" := (@expectation _ _ _ P X). + +Section expectation_lemmas. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +Lemma expectation_cst r : 'E_P[cst r] = r%:E. +Proof. by rewrite /expectation /= integral_cst//= probability_setT mule1. Qed. + +Lemma expectation_indic (A : set T) (mA : measurable A) : 'E_P[\1_A] = P A. +Proof. by rewrite /expectation integral_indic// setIT. Qed. + +Lemma integrable_expectation (X : {RV P >-> R}) + (iX : P.-integrable [set: T] (EFin \o X)) : `| 'E_P[X] | < +oo. +Proof. +move: iX => [? Xoo]; rewrite (le_lt_trans _ Xoo)//. +exact: le_trans (le_abse_integral _ _ _). +Qed. + +Lemma expectationM (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. +rewrite /expectation. +under eq_integral do rewrite EFinM. +rewrite -integralM//. +by under eq_integral do rewrite muleC. +Qed. + +Lemma expectation_ge0 (X : {RV P >-> R}) : + (forall x, 0 <= X x)%R -> 0 <= 'E_P[X]. +Proof. +by move=> ?; rewrite /expectation integral_ge0// => x _; rewrite lee_fin. +Qed. + +Lemma expectation_le (X Y : T -> R) : + measurable_fun [set: T] X -> measurable_fun [set: T] Y -> + (forall x, 0 <= X x)%R -> (forall x, 0 <= Y x)%R -> + {ae P, (forall x, X x <= Y x)%R} -> 'E_P[X] <= 'E_P[Y]. +Proof. +move=> mX mY X0 Y0 XY; rewrite /expectation ae_ge0_le_integral => //. +- by move=> t _; apply: X0. +- by apply EFin_measurable_fun. +- by move=> t _; apply: Y0. +- by apply EFin_measurable_fun. +- move: XY => [N [mN PN XYN]]; exists N; split => // t /= h. + by apply: XYN => /=; apply: contra_not h; rewrite lee_fin. +Qed. + +Lemma expectationD (X Y : {RV P >-> R}) : + P.-integrable [set: T] (EFin \o X) -> P.-integrable [set: T] (EFin \o Y) -> + 'E_P[X \+ Y] = 'E_P[X] + 'E_P[Y]. +Proof. by move=> ? ?; rewrite /expectation integralD_EFin. Qed. + +Lemma expectationB (X Y : {RV P >-> R}) : + P.-integrable [set: T] (EFin \o X) -> P.-integrable [set: T] (EFin \o Y) -> + 'E_P[X \- Y] = 'E_P[X] - 'E_P[Y]. +Proof. by move=> ? ?; rewrite /expectation integralB_EFin. Qed. + +End expectation_lemmas. + +Section variance. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +Definition variance (X : T -> R) := 'E_P[(X \- cst (fine 'E_P[X])) ^+ 2]%R. +Local Notation "''V_' P [ X ]" := (variance X). + +(* TODO: since for finite measures L^1 <= L^2, the first hypo is redundant, + the proof of this fact is the purpose of an on-going PR*) +Lemma varianceE (X : {RV P >-> R}) : + (* TODO: check what happens when X is not integrable *) + P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o (X ^+ 2)%R) -> + 'V_P[X] = 'E_P[X ^+ 2] - ('E_P[X]) ^+ 2. +Proof. +move=> X1 X2. +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. + 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 []. + 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. +rewrite expectation_cst mule1 EFinM fineK// fineK ?fin_numM// -muleA -expe2. +rewrite mule_natl mule2n oppeD; last by rewrite fin_num_adde_defl// fin_numX. +by rewrite addeA subeK// fin_numX. +Qed. + +End variance. +Notation "'V_ P [ X ]" := (variance P X). + +Section markov_chebyshev. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +Lemma markov (X : {RV P >-> R}) (f : R -> R) (eps : R) : + (0 < eps)%R -> + measurable_fun [set: R] f -> (forall r, 0 <= f r)%R -> + {in `[0, +oo[%classic &, {homo f : x y / x <= y}}%R -> + (f eps)%:E * P [set x | eps%:E <= `| (X x)%:E | ] <= + 'E_P[f \o (fun x => `| x |%R) \o X]. +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 (er_map f) _ _ _ _ e0)) => //=. +- exact: measurable_fun_er_map. +- by case => //= r _; exact: f0. +- by move=> [x| |] [y| |] xP yP xy//=; rewrite ?leey ?leNye// lee_fin f_nd. +- exact/EFin_measurable_fun. +Qed. + +Lemma chebyshev (X : {RV P >-> R}) (eps : R) : (0 < eps)%R -> + P [set x | (eps <= `| X x - fine ('E_P[X])|)%R ] <= (eps ^- 2)%:E * 'V_P[X]. +Proof. +move => heps; have [->|hv] := eqVneq ('V_P[X])%E +oo%E. + by rewrite mulr_infty gtr0_sg ?mul1e// ?leey// invr_gt0// exprn_gt0. +have h (Y : {RV P >-> R}) : + P [set x | (eps <= `|Y x|)%R] <= (eps ^- 2)%:E * 'E_P[Y ^+ 2]. + rewrite -lee_pdivr_mull; last by rewrite invr_gt0// exprn_gt0. + rewrite exprnN expfV exprz_inv opprK -exprnP. + apply: (@le_trans _ _ ('E_P[(@GRing.exp R ^~ 2%N \o normr) \o Y])). + apply: (@markov Y (@GRing.exp R ^~ 2%N)) => //. + - exact/measurable_fun_exprn/measurable_fun_id. + - by move=> r; apply: sqr_ge0. + - move=> x y; rewrite !inE !mksetE !in_itv/= !andbT => x0 y0. + by rewrite ler_sqr. + apply: expectation_le => //. + - apply: measurable_funT_comp => //; apply: measurable_funT_comp => //. + exact/measurable_fun_exprn/measurable_fun_id. + - by move=> x /=; apply: sqr_ge0. + - by move=> x /=; apply: sqr_ge0. +simpl. + + + - by apply/aeW => t /=; rewrite real_normK// num_real. +have := h [the {mfun T >-> R} of (X \- cst (fine ('E_P[X])))%R]. +by move=> /le_trans; apply; rewrite lee_pmul2l// lte_fin invr_gt0 exprn_gt0. +Qed. + +End markov_chebyshev. + +HB.mixin Record MeasurableFun_isDiscrete d (T : measurableType d) (R : realType) + (X : T -> R) of @MeasurableFun d T R 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 +}. + +Notation "{ 'dmfun' aT >-> T }" := + (@discreteMeasurableFun.type _ aT T) : form_scope. + +Definition discrete_random_variable (d : _) (T : measurableType d) + (R : realType) (P : probability T R) := {dmfun T >-> R}. + +Notation "{ 'dRV' P >-> R }" := + (@discrete_random_variable _ _ R P) : form_scope. + +Section dRV_definitions. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +Definition dRV_dom_enum (X : {dRV P >-> R}) : + { B : set nat & {splitbij B >-> 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_enum (X : {dRV P >-> R}) : {splitbij (dRV_dom X) >-> range X} := + projT2 (dRV_dom_enum X). + +Definition enum_prob (X : {dRV P >-> R}) := + (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}. + +Lemma distribution_dRV_enum (n : nat) : n \in dRV_dom X -> + distribution P X [set dRV_enum X n] = enum_prob X n. +Proof. +by move=> nX; rewrite /distribution/= /enum_prob/= patchE nX. +Qed. + +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. +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. + rewrite -preimage_setI (_ : _ `&` _ = set0)//. + by apply/seteqP; split => //= x [] -> {x} /inj; rewrite inE inE => /(_ iX jX). +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. +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. + exact: funS. + by rewrite invK// inE. +rewrite setI_bigcupr; etransitivity; first exact: PXU. +rewrite eseries_mkcond; apply: eq_eseriesr => k _. +rewrite /enum_prob patchE; case: ifPn => nX; rewrite ?mul0e//. +rewrite diracE; have [kA|] := boolP (_ \in A). + by rewrite mule1 setIidr// => _ /= ->; exact: set_mem. +rewrite notin_set => kA. +rewrite mule0 (disjoints_subset _ _).2 ?preimage_set0 ?measure0//. +by apply: subsetCr; rewrite sub1set inE. +Qed. + +Lemma sum_enum_prob : (\sum_(n /esym; apply: eq_trans. +by rewrite [RHS]eseries_mkcond; apply: eq_eseriesr => k _; rewrite diracT mule1. +Qed. + +End distribution_dRV. + +Section discrete_distribution. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +Lemma dRV_expectation (X : {dRV P >-> R}) : P.-integrable [set: T] (EFin \o X) -> + 'E_P[X] = (\sum_(n ix; rewrite /expectation. +rewrite -[in LHS](_ : \bigcup_k (if k \in dRV_dom X then + X @^-1` [set dRV_enum X k] else set0) = setT); last first. + apply/seteqP; split => // t _. + exists ((dRV_enum X)^-1%function (X t)) => //. + case: ifPn=> [_|]. + by rewrite invK// inE. + by rewrite notin_set/=; apply; apply: funS. +have tA : trivIset (dRV_dom X) (fun k => [set dRV_enum X k]). + by move=> i j iX jX [r [/= ->{r}]] /inj; rewrite !inE; exact. +have {tA}/trivIset_mkcond tXA : + trivIset (dRV_dom X) (fun k => X @^-1` [set dRV_enum X k]). + apply/trivIsetP => /= i j iX jX ij. + move/trivIsetP : tA => /(_ i j iX jX) Aij. + by rewrite -preimage_setI Aij ?preimage_set0. +rewrite integral_bigcup //; last 2 first. + - by move=> k; case: ifPn. + - apply: (integrableS measurableT) => //. + by rewrite -bigcup_mkcond; exact: bigcup_measurable. +transitivity (\sum_(i i _; case: ifPn => iX. + by apply: eq_integral => t; rewrite in_setE/= => ->. + by rewrite !integral_set0. +transitivity (\sum_(i i _; rewrite -integralM//; last 2 first. + - by case: ifPn. + - split; first exact: measurable_fun_cst. + rewrite (eq_integral (cst 1%E)); last by move=> x _; rewrite abse1. + rewrite integral_cst//; last by case: ifPn. + rewrite mul1e (@le_lt_trans _ _ 1%E) ?ltey//. + by case: ifPn => // _; exact: probability_le1. + by apply: eq_integral => y _; rewrite mule1. +apply: eq_eseriesr => k _; case: ifPn => kX. + rewrite /= integral_cst//= mul1e probability_distribution muleC. + by rewrite distribution_dRV_enum. +by rewrite integral_set0 mule0 /enum_prob patchE (negbTE kX) mul0e. +Qed. + +Definition pmf (X : {RV P >-> R}) (r : R) : R := fine (P (X @^-1` [set r])). + +Local Open Scope ereal_scope. +Lemma expectation_pmf (X : {dRV P >-> 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. + +(* borrowed from cauchy-schwarz branch *) +Require Import exp. +Section from_cauchy_schwarz_branch. +Definition powere_pos (R : realType) (a : \bar R) (x : R) := + if x == 0 then 1%E else if a is a'%:E then if a' == 0 then 0%E else (exp_fun a' x)%:E else +oo%E. +Local Notation "a `^ x" := (powere_pos a x) : ereal_scope. + +Lemma powere_funr1 (R : realType) (a : \bar R) : (0 <= a)%E -> (a `^ 1)%E = a. +Proof. +move: a; case => a //. + move=> a0; rewrite /powere_pos oner_eq0 /exp_fun mul1r. case: ifPn => [/eqP -> // | h]. + by rewrite lnK// posrE lt_neqAle eq_sym h -lee_fin a0. +by rewrite /powere_pos oner_eq0. +Qed. + +Lemma powere_pos_ge0 (R : realType) (a : \bar R) (x : R) : (0 <= a `^ x)%E. +Proof. +rewrite /powere_pos; case: ifPn => // x0. +move: a => [a| |] //; case: ifPn => // a0. +by rewrite ltW// lte_fin exp_fun_gt0. +Qed. + +Context d (T : measurableType d) (R : realType). +Variable mu : {finite_measure set T -> \bar R}. + +Definition Lp_norm (p : nat) (f : T -> R) : \bar R := + ((\int[mu]_x (`|f x| ^+ p)%:E) `^ (p%:R^-1))%E. + +Local Notation "`|| f ||_ p" := (Lp_norm p f) (at level 0). + +Lemma Lp_norm_ge0 (p : nat) (f : T -> R) : (0 <= `|| f ||_(p%R))%E. +Proof. by rewrite /Lp_norm powere_pos_ge0. Qed. +End from_cauchy_schwarz_branch. + +Section other_norms. +Context d (T : measurableType d) (R : realType). +Variable mu : {finite_measure set T -> \bar R}. + +Definition esup (X : set R) : \bar R := ereal_sup (EFin @` X). + +Lemma esupT : esup [set: R] = +oo%E. +Abort. + +Definition uniform_norm (f : T -> R) : \bar R := esup (range (normr \o f)). +(*Local Notation "`|| X ||_unif" := (uniform_norm X) (at level 0).*) + +(* essential supremum *) +Definition ess_sup : set R -> \bar R. +Admitted. + +Definition Linfty_norm (f : T -> R) : \bar R := ess_sup (range (normr \o f)). +End other_norms. + +Section cvg_random_variable. +Variables (d : _) (T : measurableType d) (R : realType) (P : probability T R). + +Definition cvg_in_probability (X : {RV P >-> R}^nat) (Y : {RV P >-> R}) + := forall a : {posnum R}, + [sequence P [set x | a%:num <= `| X n x - Y x | ] ]_n --> 0%E. + +Definition cvg_in_Lp_norm (p : nat) (X : {RV P >-> R}^nat) (Y : {RV P >-> R}) := + Lp_norm P p (X n - Y) @[n --> \oo] --> 0%E. + +Definition cvg_in_uniform_norm (X : {RV P >-> R}^nat) (Y : {RV P >-> R}) := + uniform_norm (X n - Y) @[n --> \oo] --> 0%E. + +Definition cvg_in_Linfty_norm (p : nat) (X : {RV P >-> R}^nat) (Y : {RV P >-> R}) := + Linfty_norm P (X n - Y) @[n --> \oo] --> 0%E. + +Lemma prop_23_1 (X : {RV P >-> R}^nat) (Y : {RV P >-> R}) + : cvg_in_Lp_norm 1 X Y -> cvg_in_probability X Y. +Proof. +move => h a /=. +(* +apply/(@cvg_distP _ [pseudoMetricNormedZmodType R of R^o]). +move => eps heps. +rewrite near_map /=. +move /(@cvgr0Pnorm_lt _ [pseudoMetricNormedZmodType R of R^o]) : h. +have a0: 0 < a%:num by []. +move /(_ (a%:num) a0) => h1. +case: h1 => m _ h1 . +near=> n. +rewrite sub0r. +rewrite normrN. +rewrite ger0_norm; last first. + apply: fine_ge0; apply: probability_ge0. +change eps with (fine eps%:E). +rewrite fine_lt => //; first apply probability_fin. + admit. +*) +(* have -> : P [set x | (a%:num <= `|X n x - Y x|)%R] = 0%E. + have mn : (m <= n)%N. + near: n. + exists m => //. + have := h1 _ mn. + unfold norm1. + rewrite /=. + have := (@markov _ T R P (X n - Y) [the {mfun R >-> R} of (@mid R)] (a%:num) a0). + move => /=. *) + (* apply: le_lt_trans. *) + (* move: x. + near: n. + by []. + have := h x. + move => [m] _. + have mn : (m <= n)%N. + move /(_ m) => /=. + move /(_ (leqnn m)). + rewrite normr_id. + rewrite ltNge. *) + (* admit. +apply: le_lt_trans. + rewrite le_eqVlt. + apply /orP. left. + apply /eqP. + apply probability0. +apply heps. *) +Abort. + +End cvg_random_variable.