minor fix

math-comp · Jan 3, 2025 · 9f5064f · 9f5064f
1 parent c48e72f
commit 9f5064f
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git 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
@@ -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
@@ -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.