minor fix

math-comp · Jan 3, 2025 · 8a5e466 · 8a5e466
1 parent c48e72f
commit 8a5e466
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 364 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/lang_syntax.v b/theories/lang_syntax.v
@@ -1337,7 +1337,8 @@ Lemma beta_pdf_uniq_ae (a b : nat) :
                (EFin \o (beta_pdf a b)).
 Proof.
 apply: integral_ae_eq => //.
-- apply: integrableS (Radon_Nikodym_integrable _) => //.
+- apply: (@integrableS _ _ _ _ setT) => //=.
+  apply: Radon_Nikodym_integrable => //=.
   exact: beta_prob_dom.
 - apply/measurable_funTS/measurableT_comp => //.
   exact: measurable_beta_pdf.
@@ -1366,9 +1367,9 @@ move=> mU mf finf.
 rewrite -(Radon_Nikodym_change_of_variables (beta_prob_dom a b)) //=; last first.
   by apply/integrableP; split.
 apply: ae_eq_integral => //.
-- apply: emeasurable_funM => //; apply: measurable_int.
-  apply: integrableS (Radon_Nikodym_integrable _) => //=.
-  exact: beta_prob_dom.
+- apply: emeasurable_funM => //; apply: (measurable_int mu).
+  apply: (integrableS _ _ (@subsetT _ _)) => //=.
+  by apply: Radon_Nikodym_integrable; exact: beta_prob_dom.
 - apply: emeasurable_funM => //=; apply/measurableT_comp => //=.
   by apply/measurable_funTS; exact: measurable_beta_pdf.
 - apply: ae_eq_mul2l => /=.

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).