remark 2.15

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -23,6 +23,16 @@
 - file `lebesgue_integral.v`:
   + lemma `measurable_fun_le`
 
+- in `trigo.v`:
+  + lemma `integral0oo_atan`
+
+- in `measure.v`:
+  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_compS`
+  + lemma `preimage_set_system_id`
+
+- in `Rstruct_topology.v`:
+  + lemma `RexpE`
+
 - file `mathcomp_extra.v`:
   + lemma `mulr_funEcomp`
 
@@ -57,16 +67,6 @@
   + lemma `expectationM_ge0`, `integrable_expectationM`, `independent_integrableM`,
     ` expectation_mul`
 
-- in `trigo.v`:
-  + lemma `integral0oo_atan`
-
-- in `measure.v`:
-  + lemmas `preimage_set_system0`, `preimage_set_systemU`, `preimage_set_system_comp`
-  + lemma `preimage_set_system_id`
-
-- in `Rstruct_topology.v`:
-  + lemma `RexpE`
-
 ### Changed
 
 - file `nsatz_realtype.v` moved from `reals` to `reals-stdlib` package
@@ -89,43 +89,7 @@
   + `min_le_min` -> `le_min2`
   + `max_le_max` -> `le_max2`
   + `real_sqrtC` -> `sqrtC_real`
-- in `measure.v`
-  + `preimage_class` -> `preimage_set_system`
-  + `image_class` -> `image_set_system`
-  + `preimage_classes` -> `g_sigma_preimageU`
-  + `preimage_class_measurable_fun` -> `preimage_set_system_measurable_fun`
-  + `sigma_algebra_preimage_class` -> `sigma_algebra_preimage`
-  + `sigma_algebra_image_class` -> `sigma_algebra_image`
-  + `sigma_algebra_preimage_classE` -> `g_sigma_preimageE`
-  + `preimage_classes_comp` -> `g_sigma_preimageU_comp`
 
-### Renamed
-
-- in `lebesgue_measure.v`:
-  + `measurable_fun_indic` -> `measurable_indic`
-  + `emeasurable_fun_sum` -> `emeasurable_sum`
-  + `emeasurable_fun_fsum` -> `emeasurable_fsum`
-  + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum`
-- in `probability.v`:
-  + `expectationM` -> `expectationZl`
-
-- in `classical_sets.v`:
-  + `preimage_itv_o_infty` -> `preimage_itvoy`
-  + `preimage_itv_c_infty` -> `preimage_itvcy`
-  + `preimage_itv_infty_o` -> `preimage_itvNyo`
-  + `preimage_itv_infty_c` -> `preimage_itvNyc`
-
-- in `constructive_ereal.v`:
-  + `maxeMr` -> `maxe_pMr`
-  + `maxeMl` -> `maxe_pMl`
-  + `mineMr` -> `mine_pMr`
-  + `mineMl` -> `mine_pMl`
-
-- in `probability.v`:
-  + `integral_distribution` -> `ge0_integral_distribution`
-
-- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v`
-
 ### Generalized
 
 - in `constructive_ereal.v`:
@@ -143,16 +107,6 @@
   + lemma `Pos_to_natE` (moved to `Rstruct.v`)
   + lemma `deg_le2_ge0` (available as `deg_le2_poly_ge0` in `ssrnum.v`
     since MathComp 2.1.0)
-- in `sequences.v`:
-  + notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`,
-    `ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0)
-- in `topology_structure.v`:
-  + lemma `closureC`
-
-- in file `lebesgue_integral.v`:
-  + lemma `approximation`
-
-### Removed
 
 - in `lebesgue_integral.v`:
   + definition `cst_mfun`

experimental_reals/discrete.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From Coq Require Setoid.
+From Corelib Require Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.classical Require Import boolp.

reals/reals.v

@@ -38,7 +38,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
-From Coq Require Import Setoid.
+From Corelib Require Import Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp Require Import boolp classical_sets set_interval.

theories/independence.v

@@ -863,6 +863,58 @@ Qed.
 
 End independent_RVs_lemmas.
 
+Local Open Scope ereal_scope.
+(**md see Achim Klenke's Probability Theory, Ch.2, remark 2.15 *)
+Lemma independence_RVsP {R : realType} d (T : measurableType d)
+    {I0 : choiceType} {d'} (T' : measurableType d') (P : probability T R)
+    (I : set I0) (X : I0 -> {mfun T >-> T'}) :
+  independent_RVs (P := P) I X <->
+  forall J : {fset I0}, [set` J] `<=` I ->
+    forall A : I0  -> set T', (forall j, I j -> A j \in measurable) ->
+      P (\big[setI/setT]_(j <- J) (X j @^-1` A j))
+      = \prod_(j <- J) P (X j @^-1` A j).
+Proof.
+split.
+  move=> [H1 +] J JI A IA.
+  apply => // j jJ /=.
+  rewrite inE/=.
+  exists (A j).
+    exact/set_mem/IA/JI.
+  by rewrite setTI.
+move=> H; split.
+  move=> j Ij _ [B mB] <-.
+  rewrite setTI.
+  exact: measurable_sfunP.
+move=> J JI E JE.
+pose A : I0 -> set T' := fun i => match pselect (i \in J) with
+  left H => sval (cid2 (set_mem (JE i H))) | right _ => setT end.
+have H1 (j : I0) : I j -> A j \in d'.-measurable.
+  move=> Ij.
+  rewrite /A.
+  case: pselect => [|]; last by rewrite inE.
+  move=> jJ.
+  rewrite inE.
+  by case: cid2.
+have := H _ JI A H1 => {}H.
+apply: eq_trans.
+  apply: eq_trans; last exact: H.
+  congr (P _).
+  rewrite big_seq [RHS]big_seq.
+  apply: eq_bigr => j jJ.
+  rewrite /A.
+  case: pselect; last by [].
+  move=> jJ'.
+  case: cid2 => //= ? ?.
+  by rewrite setTI.
+rewrite big_seq [RHS]big_seq.
+apply: eq_bigr => j jJ.
+rewrite /A.
+case: pselect; last by [].
+move=> jJ'.
+case: cid2 => //= ?.
+by rewrite setTI => ? ->.
+Qed.
+
 Section independent_generators.
 Context {R : realType} d (T : measurableType d).
 Context {I0 : choiceType}.