expectation of product

Co-authored-by: @affeldt-aist
Co-authored-by: @t6s

CHANGELOG_UNRELEASED.md

@@ -31,6 +31,22 @@
 - in `lebesgue_measure.v`:
   + lemmas `measurable_funrpos`, `measurable_funrneg`
 
+- in `numfun.v`:
+  + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-`
+  + lemmas `funrpos_ge0`, `funrneg_ge0`, `funrposN`, `funrnegN`, `ge0_funrposE`,
+    `ge0_funrnegE`, `le0_funrposE`, `le0_funrnegE`, `ge0_funrposM`, `ge0_funrnegM`,
+    `le0_funrposM`, `le0_funrnegM`, `funr_normr`, `funrposneg`, `funrD_Dpos`,
+    `funrD_posD`, `funrpos_le`, `funrneg_le`
+  + lemmas `funerpos`, `funerneg`
+
+- in `measure.v`:
+  + lemma `preimage_class_comp`
+  + defintions `mapping_display`, `g_sigma_algebra_mappingType`, `g_sigma_algebra_mapping`,
+    notations `.-mapping`, `.-mapping.-measurable`
+
+- in `lebesgue_measure.v`:
+  + lemmas `measurable_funrpos`, `measurable_funrneg`
+
 - in `lebesgue_integral.v`:
   + definition `dyadic_approx` (was `Let A`)
   + definition `integer_approx` (was `Let B`)
@@ -44,6 +60,28 @@
   + lemma `expectation_def`
   + notation `'M_`
 
+- new file `independence.v`:
+  + lemma `expectationM_ge0`
+  + definition `independent_events`
+  + definition `mutual_independence`
+  + definition `independent_RVs`
+  + definition `independent_RVs2`
+  + lemmas `g_sigma_algebra_mapping_comp`, `g_sigma_algebra_mapping_funrpos`,
+    `g_sigma_algebra_mapping_funrneg`
+  + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`,
+    `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`,
+    `independent_RVs2_funrpospos`
+  + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`,
+    ` expectation_prod`
+- in `lebesgue_integral.v`:
+  + lemma `abse_integralP`
+- in `signed.v`:
+  + definition `onem_NngNum`
+- in `measure.v`:
+  + definition `bernoulli`, declared as a probability measure instance
+- in `itv.v`:
+  + canonical `onem_itv01`
+
 - new file `independence.v`:
   + lemma `expectationM_ge0`
   + definition `independent_events`
@@ -94,6 +132,7 @@
 
 - in `probability.v`:
   + `integral_distribution` -> `ge0_integral_distribution`
+  + `expectationM` -> `expectationMl`
 
 ### Generalized
 
@@ -119,6 +158,14 @@
 
 ### Removed
 
+- in `topology_structure.v`:
+  + lemma `closureC`
+
+- in file `lebesgue_integral.v`:
+  + lemma `approximation`
+
+### Removed
+
 - in `lebesgue_integral.v`:
   + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
   + notation `measurable_fun_indic` (deprecation since 0.6.3)

_CoqProject

@@ -87,6 +87,7 @@ theories/ftc.v
 theories/hoelder.v
 theories/probability.v
 theories/independence.v
+theories/sampling.v
 theories/convex.v
 theories/charge.v
 theories/kernel.v

reals/itv.v

@@ -850,6 +850,9 @@ Lemma inum_lt : {mono inum : x y / (x < y)%O}. Proof. by []. Qed.
 
 End Morph.
 
+Canonical onem_itv01 {R : realDomainType} (p : {i01 R}) : {i01 R} :=
+  @Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].
+
 Section Test1.
 
 Variable R : numDomainType.
@@ -890,8 +893,6 @@ Definition s_of_pq (p q : {i01 R}) : {i01 R} :=
 Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p.
 Proof. by apply/val_inj; rewrite /= subr0 mulr1 subKr. Qed.
 
-Canonical onem_itv01 (p : {i01 R}) : {i01 R} :=
-  @Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].
 
 Definition s_of_pq' (p q : {i01 R}) : {i01 R} :=
   (`1- (`1-(p%:inum) * `1-(q%:inum)))%:i01.

reals/signed.v

@@ -123,6 +123,7 @@ From mathcomp Require Import mathcomp_extra.
 (* Canonical instances are also provided according to types, as a             *)
 (* fallback when no known operator appears in the expression. Look to         *)
 (* nat_snum below for an example on how to add your favorite type.            *)
+(*                                                                            *)
 (******************************************************************************)
 
 Reserved Notation "{ 'compare' x0 & nz & cond }"

theories/Make

@@ -53,6 +53,7 @@ ftc.v
 hoelder.v
 probability.v
 independence.v
+sampling.v
 lebesgue_stieltjes_measure.v
 convex.v
 charge.v

theories/independence.v

@@ -766,24 +766,15 @@ HB.instance Definition _ := @Measure_isProbability.Build _ _ R (P \x P) PP.
 Lemma integrable_expectationM (X Y : {RV P >-> R}) :
   independent_RVs2 P X Y ->
   P.-integrable setT (EFin \o X) -> P.-integrable setT (EFin \o Y) ->
-  'E_(P \x P) [(fun x => `|X x.1 * Y x.2|)%R] < +oo
-(*  `|'E_(P) [(fun x => X x * Y x)%R]| < +oo *) .
+  'E_(P \x P) [(fun x => `|X x.1 * Y x.2|)%R] < +oo.
 Proof.
 move=> indeXY iX iY.
-(*apply: (@le_lt_trans _ _ 'E_(P \x P)[(fun x => `|(X x.1 * Y x.2)|%R)]
-   (* 'E_(P)[(fun x => `|(X x * Y x)|%R)] *)  ).
-  rewrite unlock/=.
-  rewrite (le_trans (le_abse_integral _ _ _))//.
-  apply/measurable_EFinP/measurable_funM.
-    by apply/measurableT_comp => //.
-  by apply/measurableT_comp => //.*)
 rewrite unlock.
 rewrite [ltLHS](_ : _ =
     \int[distribution (P \x P) (pairRV X Y)%R]_x `|x.1 * x.2|%:E); last first.
-  rewrite integral_distribution//=; last first.
+  rewrite ge0_integral_distribution//=; last first.
     apply/measurable_EFinP => //=.
-    by apply/measurableT_comp => //=.
-(*  admit. (* NG *)*)
+    exact/measurableT_comp.
 rewrite [ltLHS](_ : _ =
     \int[distribution P X \x distribution P Y]_x `|x.1 * x.2|%:E); last first.
   apply: eq_measure_integral => // A mA _.
@@ -804,14 +795,14 @@ rewrite [ltLHS](_ : _ = \int[distribution P X]_x `|x|%:E *
   rewrite -ge0_integralZl//=.
     by under eq_integral do rewrite normrM.
   exact/measurable_EFinP.
-rewrite integral_distribution//=; last exact/measurable_EFinP.
-rewrite integral_distribution//=; last exact/measurable_EFinP.
+rewrite ge0_integral_distribution//=; last exact/measurable_EFinP.
+rewrite ge0_integral_distribution//=; last exact/measurable_EFinP.
 rewrite lte_mul_pinfty//.
-  by apply: integral_ge0 => //.
-  apply: integral_fune_fin_num => //=.
-  by move/integrable_abse : iX => //.
-apply: integral_fune_lt_pinfty => //.
-by move/integrable_abse : iY => //.
+- exact: integral_ge0.
+- apply: integral_fune_fin_num => //=.
+  by move/integrable_abse : iX.
+- apply: integral_fune_lt_pinfty => //.
+  by move/integrable_abse : iY.
 Qed.
 
 End product_expectation.