Bernoulli sampling lemma

CHANGELOG_UNRELEASED.md

@@ -15,6 +15,38 @@
 - in `lebesgue_measure.v`:
   + lemma `measurable_indicP`
 
+- 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 `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`)
@@ -28,6 +60,42 @@
   + 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`
+  + 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`:
   + lemmas `integrable_pushforward`, `integral_pushforward`
   + lemma `integral_measure_add`
@@ -64,6 +132,7 @@
 
 - in `probability.v`:
   + `integral_distribution` -> `ge0_integral_distribution`
+  + `expectationM` -> `expectationMl`
 
 ### Generalized
 
@@ -89,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

@@ -86,6 +86,8 @@ theories/lebesgue_integral.v
 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

@@ -52,6 +52,8 @@ lebesgue_integral.v
 ftc.v
 hoelder.v
 probability.v
+independence.v
+sampling.v
 lebesgue_stieltjes_measure.v
 convex.v
 charge.v