use gauss_integral to complete another example

Author: affeldt-aist

theories/kernel.v

@@ -1565,14 +1565,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}

theories/lang_syntax.v

@@ -18,10 +18,13 @@ From mathcomp Require Import ring lra.
 (*   Probabilistic Programming Language in Coq using s-finite kernels in Coq. *)
 (*   APLAS 2023                                                               *)
 (*                                                                            *)
-(* beta distribution specialized to nat                                       *)
+(* beta distribution                                                          *)
+(* ```                                                                        *)
 (*            beta_pdf == probability density function for beta               *)
 (*           beta_prob == beta probability measure                            *)
+(* ```                                                                        *)
 (*                                                                            *)
+(* ```                                                                        *)
 (*                 typ == syntax for types of data structures                 *)
 (* measurable_of_typ t == the measurable type corresponding to type t         *)
 (*                        It is of type {d & measurableType d}                *)
@@ -58,6 +61,7 @@ From mathcomp Require Import ring lra.
 (*                        measurable                                          *)
 (*             execP e == a s-finite kernel corresponding to the evaluation   *)
 (*                        of the probabilistic expression e                   *)
+(* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
 
@@ -1337,7 +1341,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 +1371,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 => /=.

theories/lang_syntax_examples.v

@@ -1,3 +1,4 @@
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From Coq Require Import String.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.

theories/lang_syntax_table_game.v

@@ -1,3 +1,4 @@
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 Require Import String.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
@@ -554,7 +555,7 @@ under eq_integral.
   rewrite /XMonemX01 patchE x0 XMonemX0.
   over.
 rewrite /= => ->; congr bernoulli.
-by rewrite /div_betafun addn0 !betafunE/= !factE/= !factE; field.
+by rewrite /div_betafun addn0 !betafunE/= !factE/= ?factE; field.
 Qed.
 
 Lemma dirac_bool {R : realType} (U : set bool) :

theories/lang_syntax_toy.v

@@ -1,23 +1,26 @@
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From Coq Require Import String Classical.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg.
 From mathcomp Require Import mathcomp_extra boolp.
 From mathcomp Require Import signed reals topology normedtype.
 From mathcomp Require Import lang_syntax_util.
 
-(******************************************************************************)
-(*           Intrinsically-typed concrete syntax for a toy language           *)
+(**md**************************************************************************)
+(* # Intrinsically-typed concrete syntax for a toy language                   *)
 (*                                                                            *)
 (* The main module provided by this file is "lang_intrinsic_tysc" which       *)
 (* provides an example of intrinsically-typed concrete syntax for a toy       *)
 (* language (a simplification of the syntax/evaluation formalized in          *)
 (* lang_syntax.v). Other modules provide even more simplified language for    *)
 (* pedagogical purposes.                                                      *)
 (*                                                                            *)
+(* ```                                                                        *)
 (*      lang_extrinsic == non-intrinsic definition of expression              *)
 (*   lang_intrinsic_ty == intrinsically-typed syntax                          *)
 (*   lang_intrinsic_sc == intrinsically-scoped syntax                         *)
 (* lang_intrinsic_tysc == intrinsically-typed/scoped syntax                   *)
+(* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
 

theories/lang_syntax_util.v

@@ -1,11 +1,12 @@
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From Coq Require Import String.
 From HB Require Import structures.
 Require Import Classical_Prop. (* NB: to compile with Coq 8.17 *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import signed.
 
-(******************************************************************************)
-(*                  Shared by lang_syntax_*.v files                           *)
+(**md**************************************************************************)
+(* Shared by lang_syntax_*.v files                                            *)
 (******************************************************************************)
 
 HB.instance Definition _ := hasDecEq.Build string eqb_spec.