From 9f5064f70e787e995d1310db359d6c3d65d51d69 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 3 Jan 2025 11:08:40 +0900
Subject: [PATCH] minor fix

---
 theories/kernel.v            | 4 ++--
 theories/lebesgue_integral.v | 2 +-
 theories/prob_lang.v         | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/kernel.v b/theories/kernel.v
index 8b9d428a8..86fa740c6 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -1566,14 +1566,14 @@ Definition mkproduct :=
 
 End kproduct_measure.
 
-(* [Theorem 14.22, Klenke 2014] (3/3): the composition of finite transition
-  kernels is sigma-finite *)
 HB.instance Definition _ d0 d1 d2 (T0 : measurableType d0)
     (T1 : measurableType d1) (T2 : measurableType d2) {R : realType}
     (k1 : R.-ftker T0 ~> T1) (k2 : R.-ftker (T0 * T1) ~> T2) :=
   @isKernel.Build _ _ T0 (T1 * T2)%type R
     (mkproduct k1 k2) (measurable_kproduct k1 k2).
 
+(* [Theorem 14.22, Klenke 2014] (3/3): the composition of finite transition
+  kernels is sigma-finite *)
 Section sigma_finite_kproduct.
 Context d0 d1 d2 (T0 : measurableType d0)
   (T1 : measurableType d1) (T2 : measurableType d2) {R : realType}
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 284f18536..d02164a02 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -5950,7 +5950,7 @@ Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variables (m1 : {sfinite_measure set X -> \bar R}).
 Variables (m2 : {sfinite_measure set Y -> \bar R}).
 Variables (f : X * Y -> \bar R) (f0 : forall xy, 0 <= f xy).
-Hypothesis mf : measurable_fun setT f.
+Hypothesis mf : measurable_fun [set: X * Y] f.
 
 Lemma sfinite_Fubini :
   \int[m1]_x \int[m2]_y f (x, y) = \int[m2]_y \int[m1]_x f (x, y).
diff --git a/theories/prob_lang.v b/theories/prob_lang.v
index 24ae6a524..efa884970 100644
--- a/theories/prob_lang.v
+++ b/theories/prob_lang.v
@@ -1466,8 +1466,8 @@ by rewrite /score/= /mscale/= ger0_norm//= f0.
 Qed.
 
 Lemma score_score (f : R -> R) (g : R * unit -> R)
-    (mf : measurable_fun setT f)
-    (mg : measurable_fun setT g) :
+    (mf : measurable_fun [set: R] f)
+    (mg : measurable_fun [set: R * unit] g) :
   letin (score mf) (score mg) =
   score (measurable_funM mf (measurableT_comp mg (measurable_pair2 tt))).
 Proof.