Probability (#516)

* first take at probability theory

Co-authored-by: Takafumi Saikawa <[email protected]>
Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: Pierre Roux <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -77,6 +77,37 @@
     `powere_posNyr`, `fine_powere_pos`, `powere_pos_ge0`,
     `powere_pos_gt0`, `powere_pos_eq0`, `powere_posM`, `powere12_sqrt`
 
+- file `ereal.v`:
+  + lemmas `compreBr`, `compre_scale`
+  + lemma `le_er_map`
+- file `lebesgue_measure.v`
+  + lemma `measurable_fun_er_map`
+- file `lebesgue_integral.v`:
+  + instance of `isMeasurableFun` for `normr`
+  + lemma `finite_measure_integrable_cst`
+  + lemma `ae_ge0_le_integral`
+  + lemma `ae_eq_refl`
+- file `probability.v`:
+  + 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 `variance_ge0`, `variance_cst`
+  + 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`
+
 - in file `topology.v`,
   + new definitions `totally_disconnected`, and `zero_dimensional`.
   + new lemmas `component_closed`, `zero_dimension_prod`, 
@@ -185,6 +216,7 @@
 
 - in `lebesgue_measure.v`:
   + lemma `ae_eq_mul`
+  + `emeasurable_fun_bool` -> `measurable_fun_bool`
 
 ### Infrastructure
 

_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

theories/constructive_ereal.v

@@ -31,6 +31,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              *)
 (*                   sqrte == square root for extended reals                  *)
 (*                `| x |%E == the absolute value of x                         *)
 (*                  x ^+ n == iterated multiplication                         *)

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.

theories/lebesgue_integral.v

@@ -263,6 +263,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.
@@ -3057,6 +3060,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).
@@ -4101,6 +4119,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                                                          *)
 (******************************************************************************)

theories/lebesgue_measure.v

@@ -1789,29 +1789,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).