Probabilistic convergence

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
 

_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

@@ -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,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

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

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