independence, expectation of product

CHANGELOG_UNRELEASED.md

@@ -40,6 +40,42 @@
 - in `tvs.v`:
   + lemmas `cvg_sum`, `sum_continuous`
 
+- in `classical_sets.v`:
+  + lemmas `setI_closed_setT`, `setI_closed_set0`
+
+- in `measurable_function.v`:
+  + lemma `g_sigma_algebra_preimage_comp`
+
+- in `measure_function.v`:
+  + lemma `g_sigma_algebra_finite_measure_unique`
+
+- new file `independence.v`:
+  + definition `independent_events`
+  + definition `mutual_independence`
+  + lemma `eq_mutual_independence`
+  + definition `independence2`, `independence2P`
+  + lemma `mutual_independence_fset`
+  + lemma `mutual_independence_finiteS`
+  + theorem `mutual_independence_finite_g_sigma`
+  + lemma `mutual_dependence_bigcup`
+  + 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`
+  + lemma `ge0_independent_expectationM`
+  + lemmas `independent_Lfun1_expectationM_lty`, `independent_Lfun1M`,
+    `independent_expectationM`
+
+- in `ereal.v`:
+  + lemma `ge0_addBefctE`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:
@@ -73,6 +109,11 @@
 - moved from `topology_structure.v` to `filter.v`:
   + lemma `continuous_comp` (and generalized)
 
+- 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 `tvs.v`:

_CoqProject

@@ -139,6 +139,8 @@ theories/probability_theory/poisson_distribution.v
 theories/probability_theory/beta_distribution.v
 theories/probability_theory/probability.v
 
+theories/independence.v
+
 theories/convex.v
 theories/charge.v
 theories/kernel.v

classical/classical_sets.v

@@ -1651,6 +1651,22 @@ Definition setU_closed := forall A B, G A -> G B -> G (A `|` B).
 
 End set_systems.
 
+Lemma setI_closed_setT T (F : set_system T) :
+  setI_closed F -> setI_closed (F `|` [set setT]).
+Proof.
+move=> IF=> C D [FC|/= ->{C}].
+- by move=> [FD|/= ->{D}]; [left; exact: IF|rewrite setIT; left].
+- by move=> [FD|->{D}]; [rewrite setTI; left|rewrite !setTI; right].
+Qed.
+
+Lemma setI_closed_set0 T (F : set_system T) :
+  setI_closed F -> setI_closed (F `|` [set set0]).
+Proof.
+move=> IF=> C D [FC|/= ->{C}].
+- by move=> [FD|/= ->{D}]; [left; exact: IF|rewrite setI0; right].
+- by move=> [FD|->{D}]; [rewrite set0I; right|rewrite !set0I; right].
+Qed.
+
 Section rectangle.
 Context {T1 T2 : Type}.
 Implicit Types (X : set_system T1) (Y : set_system T2).

classical/functions.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 mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint rat.
 From HB Require Import structures.
 #[warning="-warn-library-file-internal-analysis"]

theories/Make

@@ -105,6 +105,8 @@ probability_theory/poisson_distribution.v
 probability_theory/beta_distribution.v
 probability_theory/probability.v
 
+independence.v
+
 convex.v
 charge.v
 kernel.v

theories/charge.v

@@ -2175,7 +2175,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 //.
+move=> mE mf; rewrite -[in RHS](funeposBneg f) integralB //.
   - exact: integrable_funepos.
   - exact: integrable_funeneg.
 transitivity (\int[mu]_(x in E) (f x * Radon_Nikodym_SigmaFinite.f nu mu x)).
@@ -2187,7 +2187,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.
   - exact: Radon_Nikodym_SigmaFinite.f_fin_num.
   - exact: add_def_funeposneg.

theories/ereal.v

@@ -62,6 +62,13 @@ 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 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

@@ -508,14 +508,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.
@@ -597,9 +597,9 @@ 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 fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funepos.
-  - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funeneg.
-  - by rewrite [in LHS](funeposneg f).
+  - by rewrite fin_num_abs (@summable_pinfty _ _ P)// summable_funepos.
+  - by rewrite fin_num_abs (@summable_pinfty _ _ P)// summable_funeneg.
+  - by rewrite -[in LHS](funeposBneg f).
 by rewrite distrC; apply: hN; near: n; exists N.
 Unshelve. all: by end_near. Qed.
 

theories/hoelder.v

@@ -538,7 +538,7 @@ Lemma convex_powR p : 1 <= p ->
   convex_function (`[0, +oo[%classic : set R) (@powR R ^~ p).
 Proof.
 move=> p1 t x y /[!inE] /= /[!in_itv] /= /[!andbT] x_ge0 y_ge0.
-have p0 : 0 < p by rewrite (lt_le_trans _ p1).  
+have p0 : 0 < p by rewrite (lt_le_trans _ p1).
 rewrite convRE [X in X `^ _ <= _]convRE; set w1 := t%:num; set w2 := t%:inum.~.
 have [->|w20] := eqVneq w2 0.
   rewrite !mul0r !addr0; have [->|w10] := eqVneq w1 0.