From 80429b775223f4b58846428228bce74fabeac587 Mon Sep 17 00:00:00 2001
From: Alessandro Bruni <brun@itu.dk>
Date: Thu, 14 Nov 2024 08:59:43 +0100
Subject: [PATCH] fixes after merge

---
 theories/probability.v | 34 ++--------------------------------
 1 file changed, 2 insertions(+), 32 deletions(-)

diff --git a/theories/probability.v b/theories/probability.v
index e07651a05..9b6548fc2 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -2761,17 +2761,6 @@ apply: bigcup_measurable => n _.
 apply: ma.
 Qed.
 
-Section independent_events.
-Context {R : realType} d {T : measurableType d}.
-Variable P : probability T R.
-Local Open Scope ereal_scope.
-
-Definition independent_events (I0 : choiceType) (I : set I0) (A : I0 -> set T) :=
-  forall J : {fset I0}, [set` J] `<=` I ->
-    P (\bigcap_(i in [set` J]) A i) = \prod_(i <- J) P (A i).
-
-End independent_events.
-
 Section independent_classes.
 Context {R : realType} d {T : measurableType d}.
 Variable P : probability T R.
@@ -2834,25 +2823,6 @@ HB.instance Definition _ := @isMeasurable.Build default_measure_display
 
 End generated_sigma_algebra.
 
-Section generated_sigma_algebra_RV.
-Context {R : realType} d d' (T : measurableType d) (T' : measurableType d').
-Variable P : probability T R.
-
-Definition independent_RVs (I0 : choiceType) (I : set I0) (X : I0 -> {mfun T >-> T'}) : Prop :=
-  independent_classes P I (fun i => g_sigma_algebra_mapping (X i)).
-
-End generated_sigma_algebra_RV.
-
-Section independent_RVs2.
-Context {R : realType} d d' (T : measurableType d) (T' : measurableType d').
-Variable P : probability T R.
-
-Definition independent_RVs2 (X Y : {mfun T >-> T'}) :=
-  independent_RVs P [set 0%N; 1%N] [eta (fun=> cst point) with 0%N |-> X, 1%N |-> Y].
-
-End independent_RVs2.
-
-
 Section bool_to_real.
 Context d (T : measurableType d) (R : realType) (P : probability T R) (f : {mfun T >-> bool}).
 Definition bool_to_real : T -> R := (fun x => x%:R) \o (f : T -> bool).
@@ -2916,7 +2886,7 @@ rewrite /mscale/=.
 rewrite diracE/= mem_set// mule1// diracE/= memNset//.
 rewrite mule0 adde0.
 rewrite /distribution /= => <-.
-apply/eqP; congr (P _).
+congr (P _).
 rewrite /preimage/=.
 by apply/seteqP; split => [x /eqP H//|x /eqP].
 Qed.
@@ -2930,7 +2900,7 @@ rewrite /mscale/=.
 rewrite diracE/= memNset//.
 rewrite mule0// diracE/= mem_set// add0e mule1.
 rewrite /distribution /= => <-.
-apply/eqP; congr (P _).
+congr (P _).
 rewrite /preimage/=.
 by apply/seteqP; split => [x /eqP H//|x /eqP].
 Qed.