expectation of product

CHANGELOG_UNRELEASED.md

@@ -92,6 +92,46 @@
   + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and
     `max_fun_continuous`.
 
+- in `constructive_ereal.v`:
+  + notation `\prod_( i <- r | P ) F` for extended real numbers and its variants
+
+- 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`:
+  + lemma `measurable_indicP`
+  + lemmas `measurable_funrpos`, `measurable_funrneg`
+
+- in `lebesgue_integral.v`:
+  + definition `approx_A` (was `Let A`)
+  + definition `approx_B` (was `Let B`)
+  + lemma `measurable_fun_sum`
+  + lemma `integrable_indic`
+
+- in `probability.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`
+
 ### Changed
 
 - in file `normedtype.v`,
@@ -143,10 +183,19 @@
     `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`,
     `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`.
 
+- in `lebesgue_integrale.v`
+  + change implicits of `measurable_funP`
+
 ### Changed
 
 ### Renamed
 
+- in `lebesgue_measure.v`:
+  + `measurable_fun_indic` -> `measurable_indic`
+
+- in `probability.v`:
+  + `expectationM` -> `expectationMl`
+
 ### Generalized
 
 - in `lebesgue_integral.v`:
@@ -161,6 +210,9 @@
 - in `topology_structure.v`:
   + lemma `closureC`
 
+- in file `lebesgue_integral.v`:
+  + lemma `approximation`
+
 ### Removed
 
 - in `lebesgue_integral.v`:
@@ -175,6 +227,10 @@
   + lemma `cst_nnfun_subproof` (turned into a `Let`)
   + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead)
 
+- 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)
+
 ### Infrastructure
 
 ### Misc

reals/constructive_ereal.v

@@ -551,6 +551,31 @@ Notation "\sum_ ( i 'in' A ) F" :=
 Notation "\sum_ ( i 'in' A ) F" :=
   (\big[+%E/0%E]_(i in A) F%E) : ereal_scope.
 
+Notation "\prod_ ( i <- r | P ) F" :=
+  (\big[*%E/1%:E]_(i <- r | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( i <- r ) F" :=
+  (\big[*%E/1%:E]_(i <- r) F%E) : ereal_scope.
+Notation "\prod_ ( m <= i < n | P ) F" :=
+  (\big[*%E/1%:E]_(m <= i < n | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( m <= i < n ) F" :=
+  (\big[*%E/1%:E]_(m <= i < n) F%E) : ereal_scope.
+Notation "\prod_ ( i | P ) F" :=
+  (\big[*%E/1%:E]_(i | P%B) F%E) : ereal_scope.
+Notation "\prod_ i F" :=
+  (\big[*%E/1%:E]_i F%E) : ereal_scope.
+Notation "\prod_ ( i : t | P ) F" :=
+  (\big[*%E/1%:E]_(i : t | P%B) F%E) (only parsing) : ereal_scope.
+Notation "\prod_ ( i : t ) F" :=
+  (\big[*%E/1%:E]_(i : t) F%E) (only parsing) : ereal_scope.
+Notation "\prod_ ( i < n | P ) F" :=
+  (\big[*%E/1%:E]_(i < n | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( i < n ) F" :=
+  (\big[*%E/1%:E]_(i < n) F%E) : ereal_scope.
+Notation "\prod_ ( i 'in' A | P ) F" :=
+  (\big[*%E/1%:E]_(i in A | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( i 'in' A ) F" :=
+  (\big[*%E/1%:E]_(i in A) F%E) : ereal_scope.
+
 Section ERealOrderTheory.
 Context {R : numDomainType}.
 Implicit Types x y z : \bar R.

theories/charge.v

@@ -1921,29 +1921,29 @@ Lemma change_of_variables f E : (forall x, 0 <= f x) ->
   \int[mu]_(x in E) (f x * ('d nu '/d mu) x) = \int[nu]_(x in E) f x.
 Proof.
 move=> f0 mE mf; set g := 'd nu '/d mu.
-have [h [ndh hf]] := approximation mE mf (fun x _ => f0 x).
+pose h := nnsfun_approx mE mf.
 have -> : \int[nu]_(x in E) f x =
     lim (\int[nu]_(x in E) (EFin \o h n) x @[n --> \oo]).
   have fE x : E x -> f x = lim ((EFin \o h n) x @[n --> \oo]).
-    by move=> Ex; apply/esym/cvg_lim => //; exact: hf.
+    by move=> Ex; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
   under eq_integral => x /[!inE] /fE -> //.
   apply: monotone_convergence => //.
   - move=> n; apply/measurable_EFinP.
     by apply: (measurable_funS measurableT) => //; exact/measurable_funP.
   - by move=> n x Ex //=; rewrite lee_fin.
-  - by move=> x Ex a b /ndh /=; rewrite lee_fin => /lefP.
+  - by move=> x Ex a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 have -> : \int[mu]_(x in E) (f \* g) x =
     lim (\int[mu]_(x in E) ((EFin \o h n) \* g) x @[n --> \oo]).
   have fg x :E x -> f x * g x = lim (((EFin \o h n) \* g) x @[n --> \oo]).
     by move=> Ex; apply/esym/cvg_lim => //; apply: cvgeMr;
-      [exact: f_fin_num|exact: hf].
+      [exact: f_fin_num|exact: cvg_nnsfun_approx].
   under eq_integral => x /[!inE] /fg -> //.
   apply: monotone_convergence => [//| | |].
   - move=> n; apply/emeasurable_funM; apply/measurable_funTS.
       exact/measurable_EFinP.
     exact: measurable_int (f_integrable _).
   - by move=> n x Ex //=; rewrite mule_ge0 ?lee_fin//=; exact: f_ge0.
-  - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin// f_ge0.
+  - by move=> x Ex a b ab/=; rewrite lee_wpmul2r ?lee_fin ?f_ge0//; exact/lefP/nd_nnsfun_approx.
 suff suf n : \int[mu]_(x in E) ((EFin \o h n) x * g x) =
     \int[nu]_(x in E) (EFin \o h n) x.
   by under eq_fun do rewrite suf.
@@ -2008,7 +2008,7 @@ Proof.
 move=> numu mula mE; have nula := measure_dominates_trans numu mula.
 have mf : measurable_fun E ('d nu '/d mu).
   exact/measurable_funTS/(measurable_int _ (f_integrable _)).
-have [h [ndh hf]] := approximation mE mf (fun x _ => f_ge0 numu x).
+pose h := approximation mE mf.
 apply: integral_ae_eq => //.
 - apply: (integrableS measurableT) => //.
   apply: f_integrable.
@@ -2018,7 +2018,7 @@ apply: integral_ae_eq => //.
 - move=> A AE mA; rewrite change_of_variables//.
   + by rewrite -!f_integral.
   + exact: f_ge0.
-  + exact: measurable_funS mf.
+  + by move: (mf); exact: measurable_funS.
 Qed.
 
 End chain_rule.

theories/kernel.v

@@ -571,24 +571,30 @@ Lemma measurable_fun_integral_finite_kernel (l : R.-fker X ~> Y)
     (k0 : forall z, 0 <= k z) (mk : measurable_fun [set: X * Y] k) :
   measurable_fun [set: X] (fun x => \int[l x]_y k (x, y)).
 Proof.
-have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x).
-apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r.
-have [l_ hl_] := measure_uub l.
-by apply: measurable_fun_xsection_finite_kernel => // /[!inE].
+pose k_ := nnsfun_approx measurableT mk.
+apply: (@measurable_fun_xsection_integral _ k_).
+- by move=> a b ab; exact/nd_nnsfun_approx.
+- by move=> z; exact/cvg_nnsfun_approx.
+- move => n r.
+  have [l_ hl_] := measure_uub l.
+  by apply: measurable_fun_xsection_finite_kernel => // /[!inE].
 Qed.
 
 Lemma measurable_fun_integral_sfinite_kernel (l : R.-sfker X ~> Y)
     (k0 : forall t, 0 <= k t) (mk : measurable_fun [set: X * Y] k) :
   measurable_fun [set: X] (fun x => \int[l x]_y k (x, y)).
 Proof.
-have [k_ [ndk_ k_k]] := approximation measurableT mk (fun xy _ => k0 xy).
-apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r.
-have [l_ hl_] := sfinite_kernel l.
-rewrite (_ : (fun x => _) = (fun x =>
-    mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first.
-  by apply/funext => x; rewrite hl_//; exact/measurable_xsection.
-apply: ge0_emeasurable_fun_sum => // m _.
-by apply: measurable_fun_xsection_finite_kernel => // /[!inE].
+pose k_ := nnsfun_approx measurableT mk.
+apply: (@measurable_fun_xsection_integral _ k_).
+- by move=> a b ab; exact/nd_nnsfun_approx.
+- by move=> z; exact/cvg_nnsfun_approx.
+- move => n r.
+  have [l_ hl_] := sfinite_kernel l.
+  rewrite (_ : (fun x => _) = (fun x =>
+      mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first.
+    by apply/funext => x; rewrite hl_//; exact/measurable_xsection.
+  apply: ge0_emeasurable_fun_sum => // m _.
+  by apply: measurable_fun_xsection_finite_kernel => // /[!inE].
 Qed.
 
 End measurable_fun_integral_finite_sfinite.
@@ -1007,8 +1013,11 @@ Lemma measurable_fun_integral_kernel
     (k : Y -> \bar R) (k0 : forall z, 0 <= k z) (mk : measurable_fun [set: Y] k) :
   measurable_fun [set: X] (fun x => \int[l x]_y k y).
 Proof.
-have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x).
-by apply: (measurable_fun_preimage_integral ndk_ k_k) => n r; exact/ml.
+pose k_ := nnsfun_approx measurableT mk.
+apply: (@measurable_fun_preimage_integral _ _ _ _ _ _ k_) => //.
+- by move=> a b ab; exact/nd_nnsfun_approx.
+- by move=> z _; exact/cvg_nnsfun_approx.
+- by move=> n r; exact/ml.
 Qed.
 
 End measurable_fun_integral_kernel.
@@ -1077,13 +1086,13 @@ Lemma integral_kcomp x f : (forall z, 0 <= f z) -> measurable_fun [set: Z] f ->
   \int[kcomp l k x]_z f z = \int[l x]_y (\int[k (x, y)]_z f z).
 Proof.
 move=> f0 mf.
-have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z).
+pose f_ := nnsfun_approx measurableT mf.
 transitivity (\int[kcomp l k x]_z (lim ((f_ n z)%:E @[n --> \oo]))).
-  by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: f_f.
+  by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: cvg_nnsfun_approx.
 rewrite monotone_convergence//; last 3 first.
   by move=> n; exact/measurable_EFinP.
   by move=> n z _; rewrite lee_fin.
-  by move=> z _ a b /ndf_ /lefP ab; rewrite lee_fin.
+  by move=> z _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 rewrite (_ : (fun _ => _) =
     (fun n => \int[l x]_y (\int[k (x, y)]_z (f_ n z)%:E)))//; last first.
   by apply/funext => n; rewrite integral_kcomp_nnsfun.
@@ -1099,12 +1108,12 @@ transitivity (\int[l x]_y lim ((\int[k (x, y)]_z (f_ n z)%:E) @[n --> \oo])).
     + exact/measurable_EFinP.
     + by move=> z _; rewrite lee_fin.
     + exact/measurable_EFinP.
-    + by move: ab => /ndf_ /lefP ab z _; rewrite lee_fin.
+    + by move=> z _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 apply: eq_integral => y _; rewrite -monotone_convergence//; last 3 first.
   - by move=> n; exact/measurable_EFinP.
   - by move=> n z _; rewrite lee_fin.
-  - by move=> z _ a b /ndf_ /lefP; rewrite lee_fin.
-by apply: eq_integral => z _; apply/cvg_lim => //; exact: f_f.
+  - by move=> z _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
+by apply: eq_integral => z _; apply/cvg_lim => //; exact: cvg_nnsfun_approx.
 Qed.
 
 End integral_kcomp.