independence, expectation of product

CHANGELOG_UNRELEASED.md

@@ -110,6 +110,59 @@
   + structures `POrderedNbhs`, `POrderedTopological`, `POrderedUniform`, `POrderedPseudoMetric`,
     `POrderedPointedTopological`
 
+- in `measurable_function.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`, `funrposDneg`, `funrposBneg`,
+    `funrD_posD`, `funrpos_le`, `funrneg_le`
+  + lemmas `funerpos`, `funerneg`
+
+- in `measurable_structure.v`:
+  + definitions `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`:
+  + definition `independent_events`
+  + definition `mutual_independence`
+  + lemma `eq_mutual_independence`
+  + definition `independence2`, `independence2P`
+  + lemmas `setI_closed_setT`, `setI_closed_set0`
+  + lemma `g_sigma_algebra_finite_measure_unique`
+  + lemma `mutual_independence_fset`
+  + lemma `mutual_independence_finiteS`
+  + theorem `mutual_independence_finite_g_sigma`
+  + lemma `mutual_dependence_bigcup`
+  + lemmas `g_sigma_algebra_preimage_comp`, `g_sigma_algebra_preimage_funrpos`,
+    `g_sigma_algebra_preimage_funrneg`
+  + definition `independent_RVs`
+  + lemma `independent_RVsD1`
+  + theorem `independent_generators`
+  + definition `independent_RVs2`
+  + lemmas `independent_RVs2_comp`, `independent_RVs2_funrposneg`,
+    `independent_RVs2_funrnegpos`, `independent_RVs2_funrnegneg`,
+    `independent_RVs2_funrpospos`
+  + definition `pairRV`, lemma `measurable_pairRV`
+  + lemmas `independent_RVs2_product_measure1`
+  + lemmas `independent_RVs2_setI_preimage`,
+    `independent_Lfun1_expectation_product_measure_lty`
+  + lemmas `expectationM_nnsfun`, `expectationM_ge0`,
+    `ge0_independent_expectationM`, `independent_Lfun1_expectationM_lty`,
+    `independent_Lfun1M`, `independent_expectationM`
+
+- in `functions.v`:
+  + lemma `addBrfctE`
+
+- in `ereal.v`:
+  + lemma `ge0_addBefctE`
+
 ### Changed
 
 - in `charge.v`:
@@ -163,6 +216,11 @@
       `bounded_variationN`, `bounded_variationl`, `bounded_variationr`,
       `variations_opp`, `nondecreasing_bounded_variation`
 
+- in `numfun.v`:
+  + `fune_abse` renamed to `funeposDneg` and direction of the equality changed
+  + `funeposneg` renamed to `funeposBneg` and direction of the equality changed
+  + `funeD_posD` renamed to `funeDB` and direction of the equality changed
+
 ### Renamed
 
 - in `probability.v`:

_CoqProject

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

classical/functions.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From HB Require Import structures.
 From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.
@@ -2700,6 +2700,10 @@ Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed.
 Lemma opprfctE (T : Type) (K : zmodType) (f : T -> K) : - f = (fun x => - f x).
 Proof. by []. Qed.
 
+Lemma addBrfctE (U : Type) (K : zmodType) :
+  @interchange (U -> K) (fun a b => a - b) (fun a b => a + b).
+Proof. by move=> a b c d; apply/funext => x; rewrite addrACA -opprD. Qed.
+
 Lemma mulrfctE (T : Type) (K : pzRingType) (f g : T -> K) :
   f * g = (fun x => f x * g x).
 Proof. by []. Qed.

classical/unstable.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint.
 From mathcomp Require Import archimedean interval mathcomp_extra.
 

reals/constructive_ereal.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 (* -------------------------------------------------------------------- *)
 (* Copyright (c) - 2015--2016 - IMDEA Software Institute                *)
 (* Copyright (c) - 2015--2018 - Inria                                   *)

theories/Make

@@ -91,6 +91,7 @@ lebesgue_integral_theory/giry.v
 ftc.v
 hoelder.v
 probability.v
+independence.v
 convex.v
 charge.v
 kernel.v

theories/charge.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat.
@@ -2174,7 +2174,7 @@ Lemma Radon_Nikodym_change_of_variables f E : measurable E ->
   \int[mu]_(x in E) (f x * ('d (charge_of_finite_measure nu) '/d mu) x) =
   \int[nu]_(x in E) f x.
 Proof.
-move=> mE mf; rewrite [in RHS](funeposneg f) integralB //; last 2 first.
+move=> mE mf; rewrite -[in RHS](funeposBneg f) integralB //; last 2 first.
   - exact: integrable_funepos.
   - exact: integrable_funeneg.
 transitivity (\int[mu]_(x in E) (f x * Radon_Nikodym_SigmaFinite.f nu mu x)).
@@ -2186,7 +2186,7 @@ transitivity (\int[mu]_(x in E) (f x * Radon_Nikodym_SigmaFinite.f nu mu x)).
     exact: measurable_int (Radon_Nikodym_SigmaFinite.f_integrable _).
   - apply: ae_eqe_mul2l.
     exact/ae_eq_sym/ae_eq_Radon_Nikodym_SigmaFinite.
-rewrite [in LHS](funeposneg f).
+rewrite -[in LHS](funeposBneg f).
 under [in LHS]eq_integral => x xE. rewrite muleBl; last 2 first.
   - exact: Radon_Nikodym_SigmaFinite.f_fin_num.
   - exact: add_def_funeposneg.

theories/ereal.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 (* -------------------------------------------------------------------- *)
 (* Copyright (c) - 2015--2016 - IMDEA Software Institute                *)
 (* Copyright (c) - 2015--2018 - Inria                                   *)
@@ -58,11 +58,16 @@ Import numFieldTopology.Exports.
 From mathcomp Require Import mathcomp_extra unstable.
 
 Local Open Scope ring_scope.
-
 Local Open Scope ereal_scope.
-
 Local Open Scope classical_set_scope.
 
+Lemma ge0_addBefctE (T : Type) (R : realDomainType) (a b c d : T -> \bar R) :
+  (forall x, 0 <= c x) -> (forall x, 0 <= d x) ->
+  a + b \- (c + d) = a \- c + (b \- d).
+Proof.
+by move=> ? ?; apply/funext=> x; rewrite !fctE addeACA oppeD ?ge0_adde_def ?inE.
+Qed.
+
 Lemma EFin_bigcup T (F : nat -> set T) :
   EFin @` (\bigcup_i F i) = \bigcup_i (EFin @` F i).
 Proof.

theories/esum.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop reals ereal interval_inference.
@@ -507,14 +507,14 @@ Proof. by move=> Df; rewrite summableN; exact: summableD. Qed.
 
 Lemma summable_funepos D f : summable D f -> summable D f^\+.
 Proof.
-apply: le_lt_trans; apply le_esum => t Dt.
-by rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDl.
+apply: le_lt_trans; apply: le_esum => t Dt.
+by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDl.
 Qed.
 
 Lemma summable_funeneg D f : summable D f -> summable D f^\-.
 Proof.
-apply: le_lt_trans; apply le_esum => t Dt.
-by rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDr.
+apply: le_lt_trans; apply: le_esum => t Dt.
+by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDr.
 Qed.
 
 End summable_lemmas.
@@ -596,7 +596,7 @@ have -> : (C_ = A_ \- B_)%R.
   apply/funext => k.
   rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -summable_fine_sum//.
   apply eq_bigr => i Pi; rewrite -fineB//.
-  - by rewrite [in LHS](funeposneg f).
+  - by rewrite -[in LHS](funeposBneg f).
   - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funepos.
   - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funeneg.
 by rewrite distrC; apply: hN; near: n; exists N.
@@ -653,14 +653,14 @@ rewrite [X in _ == X -> _]addeC -sube_eq; last 2 first.
   - rewrite fin_num_adde_defr// ge0_esum_posneg//.
     rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di.
     by rewrite /= gee0_abs// f0.
-rewrite -addeA addeCA eq_sym [X in _ == X -> _]addeC -sube_eq; last 2 first.
-  - rewrite ge0_esum_posneg//.
-    rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di.
-    by rewrite /= gee0_abs// f0.
-  - rewrite fin_num_adde_defl// ge0_esum_posneg//.
-    rewrite (@eq_esum _ _ _ _ (abse \o g))// -?summableE// => i Di.
-    by rewrite /= gee0_abs// g0.
-by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->.
+rewrite -addeA addeCA eq_sym [X in _ == X -> _]addeC -sube_eq.
+- by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->.
+- rewrite ge0_esum_posneg//.
+  rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di.
+  by rewrite /= gee0_abs// f0.
+- rewrite fin_num_adde_defl// ge0_esum_posneg//.
+  rewrite (@eq_esum _ _ _ _ (abse \o g))// -?summableE// => i Di.
+  by rewrite /= gee0_abs// g0.
 Qed.
 
 End esumB.