expectation of product

CHANGELOG_UNRELEASED.md

@@ -4,16 +4,185 @@
 
 ### Added
 
+- in `probability.v`:
+  + lemmas `eq_bernoulli`, `eq_bernoulliV2`
+- file `mathcomp_extra.v`
+  + lemmas `ge_trunc`, `lt_succ_trunc`, `trunc_ge_nat`, `trunc_lt_nat`
+
+- file `Rstruct.v`
+  + lemma `Pos_to_natE` (from `mathcomp_extra.v`)
+  + lemmas `RabsE`, `RdistE`, `sum_f_R0E`, `factE`
+
+- new file `internal_Eqdep_dec.v` (don't use, internal, to be removed)
+
+- in `measure.v`:
+  + lemmas `mnormalize_id`, `measurable_fun_eqP`
+
+- in `ftc.v`:
+  + lemma `integrable_locally`
+
+- in `constructive_ereal.v`:
+  + lemma `EFin_bigmax`
+
+- in `mathcomp_extra.v`:
+  + lemmas `inr_inj`, `inl_inj`
+
+- in `classical_sets.v`:
+  + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f`
+  + lemmas `inr_in_set_inl`, `inl_in_set_inl`
+
+- in `lebesgue_integral_approximation.v`:
+  + lemma `measurable_prod`
+
+- in `measure.v`:
+  + lemma `preimage_set_system_compS`
+
+- 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 `preimage_display`, `g_sigma_algebra_preimageType`, `g_sigma_algebra_preimage`,
+    notations `.-preimage`, `.-preimage.-measurable`
+
+- in `measurable_realfun.v`:
+  + lemmas `measurable_funrpos`, `measurable_funrneg`
+
+- new file `independence.v`:
+  + lemma `expectationM_ge0`
+  + definition `independent_events`
+  + definition `mutual_independence`
+  + definition `independent_RVs`
+  + definition `independent_RVs2`
+  + lemmas `g_sigma_algebra_preimage_comp`, `g_sigma_algebra_preimage_funrpos`,
+    `g_sigma_algebra_preimage_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 `numfun.v`
+  + lemmas `funeposE`, `funenegE`, `funepos_comp`, `funeneg_comp`
+
+- in `classical_sets.v`:
+  + lemmas `xsectionE`, `ysectionE`
+
+- file `constructive_ereal.v`:
+  + definition `iter_mule`
+  + lemma `prodEFin`
+
+- file `exp.v`:
+  + lemma `expR_sum`
+
+- file `lebesgue_integral.v`:
+  + lemma `measurable_fun_le`
+
 ### Changed
 
 ### Renamed
 
+- in `kernel.v`:
+  + `isFiniteTransition` -> `isFiniteTransitionKernel`
+- in `lebesgue_integral.v`:
+  + `fubini1a` -> `integrable12ltyP`
+  + `fubini1b` -> `integrable21ltyP`
+  + `measurable_funP` -> `measurable_funPT` (field of `isMeasurableFun` mixin)
+
+- in `mathcomp_extra.v`
+  + `comparable_min_le_min` -> `comparable_le_min2`
+  + `comparable_max_le_max` -> `comparable_le_max2`
+  + `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
 
 ### Deprecated
 
 ### Removed
 
+- file `mathcomp_extra.v`
+  + 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`
+  + lemma `mfun_cst`
+
+- in `cardinality.v`:
+  + lemma `cst_fimfun_subproof`
+
+- in `lebesgue_integral.v`:
+  + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead)
+  + 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)
+- in `constructive_ereal.v`
+  + notation `lee_opp` (deprecated since 0.6.5)
+  + notation `lte_opp` (deprecated since 0.6.5)
+- in `measure.v`:
+  + `dynkin_setI_bigsetI` (use `big_ind` instead)
+
+- in `lebesgue_measurable.v`:
+  + notation `measurable_fun_power_pos` (deprecated since 0.6.3)
+  + notation `measurable_power_pos` (deprecated since 0.6.4)
+
 ### Infrastructure
 
 ### Misc

_CoqProject

@@ -113,6 +113,7 @@ theories/lebesgue_integral_theory/lebesgue_integral.v
 theories/ftc.v
 theories/hoelder.v
 theories/probability.v
+theories/independence.v
 theories/convex.v
 theories/charge.v
 theories/kernel.v

experimental_reals/discrete.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From Corelib Require Setoid.
+From Coq 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 Corelib Require Import Setoid.
+From Coq 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/Make

@@ -77,6 +77,7 @@ lebesgue_integral_theory/lebesgue_integral.v
 ftc.v
 hoelder.v
 probability.v
+independence.v
 lebesgue_stieltjes_measure.v
 convex.v
 charge.v