changelog

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

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                               *)

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.

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).

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).

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 <oo | n \in dRV_dom X) (pmf X (dRV_enum X n))%:E * (dRV_enum X n)%:E)%E.
+Local Open Scope ereal_scope.
+Lemma expectation_pmf (X : {dRV P >-> R}) :
+    P.-integrable [set: T] (EFin \o X) -> 'E_P[X] =
+  \sum_(n <oo | n \in dRV_dom X) (pmf X (dRV_enum X n))%:E * (dRV_enum X n)%:E.
 Proof.
 move=> 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.