From 5ecf0215ba2f5c6a614d7dfef9500cf7f401ff80 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 12 Apr 2023 17:31:00 +0900 Subject: [PATCH] a hierarchy and a theory of kernels Co-authored-by: Cyril Cohen Co-authored-by: @AyumuSaito --- CHANGELOG_UNRELEASED.md | 20 + theories/kernel.v | 1137 ++++++++++++++++++++++++++++++++++ theories/lebesgue_integral.v | 8 +- 3 files changed, 1163 insertions(+), 2 deletions(-) create mode 100644 theories/kernel.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ee86a4389c..ed2a03b953 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,8 +4,28 @@ ### Added +- in file `kernel.v`, + + new definitions `kseries`, `measure_fam_uub`, `kzero`, `kdirac`, + `prob_pointed`, `mset`, `pset`, `pprobability`, `kprobability`, `kadd`, + `mnormalize`, `knormalize`, `kcomp`, and `mkcomp`. + + new lemmas `eq_kernel`, `measurable_fun_kseries`, `integral_kseries`, + `measure_fam_uubP`, `eq_sfkernel`, `kzero_uub`, `sfinite_finite`, + `sfinite`, `sfinite_kernel_measure`, `finite_kernel_measure`, + `measurable_prod_subset_xsection_kernel`, + `measurable_fun_xsection_finite_kernel`, + `measurable_fun_xsection_integral`, + `measurable_fun_integral_finite_kernel`, + `measurable_fun_integral_sfinite_kernel`, `lt0_mset`, `gt1_mset`, + `kernel_measurable_eq_cst`, `kernel_measurable_neq_cst`, `kernel_measurable_fun_eq_cst`, + `measurable_fun_kcomp_finite`, `mkcomp_sfinite`, + `measurable_fun_mkcomp_sfinite`, `measurable_fun_preimage_integral`, + `measurable_fun_integral_kernel`, and `integral_kcomp`. + ### Changed +- in `lebesgue_integral.v`: + + lemma `xsection_ndseq_closed` generalized from a measure to a family of measures + ### Renamed - in `derive.v`: diff --git a/theories/kernel.v b/theories/kernel.v new file mode 100644 index 0000000000..36cc91f472 --- /dev/null +++ b/theories/kernel.v @@ -0,0 +1,1137 @@ +(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. +Require Import mathcomp_extra boolp classical_sets signed functions cardinality. +Require Import reals ereal topology normedtype sequences esum measure. +Require Import lebesgue_measure fsbigop numfun lebesgue_integral. + +(******************************************************************************) +(* Kernels *) +(* *) +(* This file provides a formation of kernels and extends the theory of *) +(* measures with, e.g., Tonelli-Fubini's theorem for s-finite measures. *) +(* The main result is the fact that s-finite kernels are stable by *) +(* composition. *) +(* *) +(* finite_measure mu == the measure mu is finite *) +(* sfinite_measure mu == the measure mu is s-finite *) +(* R.-ker X ~> Y == kernel *) +(* kseries == countable sum of kernels *) +(* R.-sfker X ~> Y == s-finite kernel *) +(* R.-fker X ~> Y == finite kernel *) +(* R.-spker X ~> Y == subprobability kernel *) +(* R.-pker X ~> Y == probability kernel *) +(* mset U r == the set probability measures mu such that mu U < r *) +(* pset == the sets mset U r with U measurable and r \in [0,1] *) +(* pprobability == the measurable type generated by pset *) +(* kprobability m == kernel defined by a probability measure *) +(* kdirac mf == kernel defined by a measurable function *) +(* kadd k1 k2 == lifting of the addition of measures to kernels *) +(* mnormalize f == normalization of a kernel to a probability *) +(* l \; k == composition of kernels *) +(* *) +(* ref: R. Affeldt, C. Cohen, A. Saito, Semantics of probabilistic programs *) +(* using s-finite kernels in Coq. CPP 2023 *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope ereal_scope. + +Reserved Notation "R .-ker X ~> Y" + (at level 42, format "R .-ker X ~> Y"). +Reserved Notation "R .-sfker X ~> Y" + (at level 42, format "R .-sfker X ~> Y"). +Reserved Notation "R .-fker X ~> Y" + (at level 42, format "R .-fker X ~> Y"). +Reserved Notation "R .-spker X ~> Y" + (at level 42, format "R .-spker X ~> Y"). +Reserved Notation "R .-pker X ~> Y" + (at level 42, format "R .-pker X ~> Y"). + +HB.mixin Record isKernel d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := + {measurable_kernel : forall U, measurable U -> measurable_fun setT (k ^~ U)}. + +#[short(type=kernel)] +HB.structure Definition Kernel + d d' (X : measurableType d) (Y : measurableType d') (R : realType) := + { k & isKernel _ _ X Y R k }. +Notation "R .-ker X ~> Y" := (kernel X Y R). + +Arguments measurable_kernel {_ _ _ _ _} _. + +Lemma kernel_measurable_eq_cst d d' (T : measurableType d) + (T' : measurableType d') (R : realType) (f : R.-ker T ~> T') k : + measurable [set t | f t setT == k]. +Proof. +rewrite [X in measurable X](_ : _ = (f ^~ setT) @^-1` [set k]); last first. + by apply/seteqP; split => t/= /eqP. +have /(_ measurableT [set k]) := measurable_kernel f setT measurableT. +by rewrite setTI; exact. +Qed. + +Lemma kernel_measurable_neq_cst d d' (T : measurableType d) + (T' : measurableType d') (R : realType) (f : R.-ker T ~> T') k : + measurable [set t | f t setT != k]. +Proof. +rewrite [X in measurable X](_ : _ = (f ^~ setT) @^-1` [set~ k]); last first. + by apply/seteqP; split => t /eqP. +have /(_ measurableT [set~ k]) := measurable_kernel f setT measurableT. +by rewrite setTI; apply => //; exact: measurableC. +Qed. + +Lemma kernel_measurable_fun_eq_cst d d' (T : measurableType d) + (T' : measurableType d') (R : realType) (f : R.-ker T ~> T') k : + measurable_fun setT (fun t => f t setT == k). +Proof. +move=> _ /= B mB; rewrite setTI. +have [/eqP->|/eqP->|/eqP->|/eqP->] := set_bool B. +- exact: kernel_measurable_eq_cst. +- rewrite (_ : _ @^-1` _ = [set b | f b setT != k]); last first. + by apply/seteqP; split => [t /negbT//|t /negbTE]. + exact: kernel_measurable_neq_cst. +- by rewrite preimage_set0. +- by rewrite preimage_setT. +Qed. + +Lemma eq_kernel d d' (T : measurableType d) (T' : measurableType d') + (R : realType) (k1 k2 : R.-ker T ~> T') : + (forall x U, k1 x U = k2 x U) -> k1 = k2. +Proof. +move: k1 k2 => [m1 [[?]]] [m2 [[?]]] /= k12. +have ? : m1 = m2. + by apply/funext => t; apply/eq_measure; apply/funext => U; rewrite k12. +by subst m1; f_equal; f_equal; f_equal; apply/Prop_irrelevance. +Qed. + +Section kseries. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variable k : (R.-ker X ~> Y)^nat. + +Definition kseries : X -> {measure set Y -> \bar R} := + fun x => [the measure _ _ of mseries (k ^~ x) 0]. + +Lemma measurable_fun_kseries (U : set Y) : + measurable U -> + measurable_fun setT (kseries ^~ U). +Proof. +move=> mU. +by apply: ge0_emeasurable_fun_sum => // n; exact/measurable_kernel. +Qed. + +HB.instance Definition _ := + isKernel.Build _ _ _ _ _ kseries measurable_fun_kseries. + +End kseries. + +Lemma integral_kseries d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : (R.-ker X ~> Y)^nat) (f : Y -> \bar R) x : + (forall y, 0 <= f y) -> + measurable_fun setT f -> + \int[kseries k x]_y (f y) = \sum_(i f0 mf; rewrite /kseries/= ge0_integral_measure_series. +Qed. + +Section measure_fam_uub. +Context d d' (X : measurableType d) (Y : measurableType d') (R : numFieldType). +Variable k : X -> {measure set Y -> \bar R}. + +Definition measure_fam_uub := exists r, forall x, k x [set: Y] < r%:E. + +Lemma measure_fam_uubP : measure_fam_uub <-> + exists r : {posnum R}, forall x, k x [set: Y] < r%:num%:E. +Proof. +split => [|] [r kr]; last by exists r%:num. +suff r_gt0 : (0 < r)%R by exists (PosNum r_gt0). +by rewrite -lte_fin; apply: (le_lt_trans _ (kr point)). +Qed. + +End measure_fam_uub. + +HB.mixin Record Kernel_isSFinite_subdef + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := { + sfinite_subdef : exists2 s : (R.-ker X ~> Y)^nat, + forall n, measure_fam_uub (s n) & + forall x U, measurable U -> k x U = kseries s x U }. + +#[short(type=sfinite_kernel)] +HB.structure Definition SFiniteKernel + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) := + {k of @Kernel _ _ _ _ R k & Kernel_isSFinite_subdef _ _ X Y R k }. +Notation "R .-sfker X ~> Y" := (sfinite_kernel X Y R). + +Arguments sfinite_subdef {_ _ _ _ _} _. + +Lemma eq_sfkernel d d' (T : measurableType d) (T' : measurableType d') + (R : realType) (k1 k2 : R.-sfker T ~> T') : + (forall x U, k1 x U = k2 x U) -> k1 = k2. +Proof. +move: k1 k2 => [m1 [[?] [?]]] [m2 [[?] [?]]] /= k12. +have ? : m1 = m2. + by apply/funext => t; apply/eq_measure; apply/funext => U; rewrite k12. +by subst m1; f_equal; f_equal; f_equal; apply/Prop_irrelevance. +Qed. + +HB.mixin Record SFiniteKernel_isFinite + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := + { measure_uub : measure_fam_uub k }. + +#[short(type=finite_kernel)] +HB.structure Definition FiniteKernel + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) := + {k of @SFiniteKernel _ _ _ _ _ k & + SFiniteKernel_isFinite _ _ X Y R k }. +Notation "R .-fker X ~> Y" := (finite_kernel X Y R). + +Arguments measure_uub {_ _ _ _ _} _. + +HB.factory Record Kernel_isFinite d d' (X : measurableType d) + (Y : measurableType d') (R : realType) (k : X -> {measure set Y -> \bar R}) + of isKernel _ _ _ _ _ k := { + measure_uub : measure_fam_uub k }. + +Section kzero. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). + +Definition kzero : X -> {measure set Y -> \bar R} := + fun _ : X => [the measure _ _ of mzero]. + +Let measurable_fun_kzero U : measurable U -> + measurable_fun setT (kzero ^~ U). +Proof. by move=> ?/=; exact: measurable_fun_cst. Qed. + +HB.instance Definition _ := + @isKernel.Build _ _ X Y R kzero measurable_fun_kzero. + +Lemma kzero_uub : measure_fam_uub kzero. +Proof. by exists 1%R => /= t; rewrite /mzero/=. Qed. + +End kzero. + +HB.builders Context d d' (X : measurableType d) (Y : measurableType d') + (R : realType) k of Kernel_isFinite d d' X Y R k. + +Lemma sfinite_finite : + exists2 k_ : (R.-ker _ ~> _)^nat, forall n, measure_fam_uub (k_ n) & + forall x U, measurable U -> k x U = mseries (k_ ^~ x) 0 U. +Proof. +exists (fun n => if n is O then [the _.-ker _ ~> _ of k] else + [the _.-ker _ ~> _ of @kzero _ _ X Y R]). + by case => [|_]; [exact: measure_uub|exact: kzero_uub]. +move=> t U mU/=; rewrite /mseries. +rewrite (nneseries_split 1%N)// big_ord_recl/= big_ord0 adde0. +rewrite ereal_series (@eq_eseriesr _ _ (fun=> 0%E)); last by case. +by rewrite eseries0// adde0. +Qed. + +HB.instance Definition _ := + @Kernel_isSFinite_subdef.Build d d' X Y R k sfinite_finite. + +HB.instance Definition _ := + @SFiniteKernel_isFinite.Build d d' X Y R k measure_uub. + +HB.end. + +Section sfinite. +Context d d' (X : measurableType d) (Y : measurableType d'). +Variables (R : realType) (k : R.-sfker X ~> Y). + +Let s : (X -> {measure set Y -> \bar R})^nat := + let: exist2 x _ _ := cid2 (sfinite_subdef k) in x. + +Let ms n : @isKernel d d' X Y R (s n). +Proof. +split; rewrite /s; case: cid2 => /= s' s'_uub kE. +exact: measurable_kernel. +Qed. + +HB.instance Definition _ n := ms n. + +Let s_uub n : measure_fam_uub (s n). +Proof. by rewrite /s; case: cid2. Qed. + +HB.instance Definition _ n := + @Kernel_isFinite.Build d d' X Y R (s n) (s_uub n). + +Lemma sfinite : exists s : (R.-fker X ~> Y)^nat, + forall x U, measurable U -> k x U = kseries s x U. +Proof. +exists (fun n => [the _.-fker _ ~> _ of s n]) => x U mU. +by rewrite /s /= /s; by case: cid2 => ? ? ->. +Qed. + +End sfinite. + +Lemma sfinite_kernel_measure d d' (Z : measurableType d) (X : measurableType d') + (R : realType) (k : R.-sfker Z ~> X) (z : Z) : + sfinite_measure (k z). +Proof. +have [s ks] := sfinite k. +exists (s ^~ z). + move=> n; have [r snr] := measure_uub (s n). + by apply: lty_fin_num_fun; rewrite (lt_le_trans (snr _))// leey. +by move=> U mU; rewrite ks. +Qed. + +HB.instance Definition _ d d' (X : measurableType d) + (Y : measurableType d') (R : realType) := + @Kernel_isFinite.Build _ _ _ _ R (@kzero _ _ X Y R) + (@kzero_uub _ _ X Y R). + +HB.factory Record Kernel_isSFinite d d' (X : measurableType d) + (Y : measurableType d') (R : realType) (k : X -> {measure set Y -> \bar R}) + of isKernel _ _ _ _ _ k := { + sfinite : exists s : (R.-fker X ~> Y)^nat, + forall x U, measurable U -> k x U = kseries s x U }. + +HB.builders Context d d' (X : measurableType d) (Y : measurableType d') + (R : realType) k of Kernel_isSFinite d d' X Y R k. + +Lemma sfinite_subdef : Kernel_isSFinite_subdef d d' X Y R k. +Proof. +split; have [s sE] := sfinite; exists s => //. +by move=> n; exact: measure_uub. +Qed. + +HB.instance Definition _ := (*@isSFinite0.Build d d' X Y R k*) sfinite_subdef. + +HB.end. + +HB.mixin Record FiniteKernel_isSubProbability + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := + { sprob_kernel : ereal_sup [set k x [set: Y] | x in setT] <= 1}. + +#[short(type=sprobability_kernel)] +HB.structure Definition SubProbabilityKernel + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) := + {k of @FiniteKernel _ _ _ _ _ k & + FiniteKernel_isSubProbability _ _ X Y R k }. +Notation "R .-spker X ~> Y" := (sprobability_kernel X Y R). + +HB.factory Record Kernel_isSubProbability + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) of isKernel _ _ X Y R k + := { sprob_kernel : ereal_sup [set k x [set: Y] | x in setT] <= 1}. + +HB.builders Context d d' (X : measurableType d) (Y : measurableType d') + (R : realType) k of Kernel_isSubProbability d d' X Y R k. + +Let finite : @Kernel_isFinite d d' X Y R k. +Proof. +split; exists 2%R => /= ?; rewrite (@le_lt_trans _ _ 1%:E) ?lte_fin ?ltr1n//. +by rewrite (le_trans _ sprob_kernel)//; exact: ereal_sup_ub. +Qed. + +HB.instance Definition _ := finite. + +HB.instance Definition _ := + @FiniteKernel_isSubProbability.Build _ _ _ _ _ k sprob_kernel. + +HB.end. + +HB.mixin Record SubProbability_isProbability + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) := + { prob_kernel : forall x, k x [set: Y] = 1}. + +#[short(type=probability_kernel)] +HB.structure Definition ProbabilityKernel + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) := + {k of @SubProbabilityKernel _ _ _ _ _ k & + SubProbability_isProbability _ _ X Y R k }. +Notation "R .-pker X ~> Y" := (probability_kernel X Y R). + +HB.factory Record Kernel_isProbability + d d' (X : measurableType d) (Y : measurableType d') + (R : realType) (k : X -> {measure set Y -> \bar R}) of isKernel _ _ X Y R k + := { prob_kernel : forall x, k x setT = 1 }. + +HB.builders Context d d' (X : measurableType d) (Y : measurableType d') + (R : realType) k of Kernel_isProbability d d' X Y R k. + +Let sprob_kernel : @Kernel_isSubProbability d d' X Y R k. +Proof. +by split; apply: ub_ereal_sup => x [y _ <-{x}]; rewrite prob_kernel. +Qed. + +HB.instance Definition _ := sprob_kernel. + +HB.instance Definition _ := + @SubProbability_isProbability.Build _ _ _ _ _ k prob_kernel. + +HB.end. + +Lemma finite_kernel_measure d d' (X : measurableType d) + (Y : measurableType d') (R : realType) (k : R.-fker X ~> Y) (x : X) : + fin_num_fun (k x). +Proof. +have [r k_r] := measure_uub k. +by apply: lty_fin_num_fun; rewrite (@lt_trans _ _ r%:E) ?ltey. +Qed. + +(* see measurable_prod_subset in lebesgue_integral.v; + the differences between the two are: + - m2 is a kernel instead of a measure (the proof uses the + measurability of each measure of the family) + - as a consequence, m2D_bounded holds for all x *) +Section measurable_prod_subset_kernel. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Implicit Types A : set (X * Y). + +Section xsection_kernel. +Variable (k : R.-ker X ~> Y) (D : set Y) (mD : measurable D). +Let kD x := mrestr (k x) mD. +HB.instance Definition _ x := Measure.on (kD x). +Let phi A := fun x => kD x (xsection A x). +Let XY := [set A | measurable A /\ measurable_fun setT (phi A)]. + +Let phiM (A : set X) B : phi (A `*` B) = (fun x => kD x B * (\1_A x)%:E). +Proof. +rewrite funeqE => x; rewrite indicE /phi/=. +have [xA|xA] := boolP (x \in A); first by rewrite mule1 in_xsectionM. +by rewrite mule0 notin_xsectionM// set0I measure0. +Qed. + +Lemma measurable_prod_subset_xsection_kernel : + (forall x, exists M, forall X, measurable X -> kD x X < M%:E) -> + measurable `<=` XY. +Proof. +move=> kD_ub; rewrite measurable_prod_measurableType. +set C := [set A `*` B | A in measurable & B in measurable]. +have CI : setI_closed C. + move=> _ _ [X1 mX1 [X2 mX2 <-]] [Y1 mY1 [Y2 mY2 <-]]. + exists (X1 `&` Y1); first exact: measurableI. + by exists (X2 `&` Y2); [exact: measurableI|rewrite setMI]. +have CT : C setT by exists setT => //; exists setT => //; rewrite setMTT. +have CXY : C `<=` XY. + move=> _ [A mA [B mB <-]]; split; first exact: measurableM. + rewrite phiM. + apply: emeasurable_funM => //; first exact/measurable_kernel/measurableI. + by apply/EFin_measurable_fun; rewrite (_ : \1_ _ = mindic R mA). +suff monoB : monotone_class setT XY by exact: monotone_class_subset. +split => //; [exact: CXY| |exact: xsection_ndseq_closed]. +move=> A B BA [mA mphiA] [mB mphiB]; split; first exact: measurableD. +suff : phi (A `\` B) = (fun x => phi A x - phi B x). + by move=> ->; exact: emeasurable_funB. +rewrite funeqE => x; rewrite /phi/= xsectionD// measureD. +- by rewrite setIidr//; exact: le_xsection. +- exact: measurable_xsection. +- exact: measurable_xsection. +- have [M kM] := kD_ub x. + rewrite (lt_le_trans (kM (xsection A x) _)) ?leey//. + exact: measurable_xsection. +Qed. + +End xsection_kernel. + +End measurable_prod_subset_kernel. + +(* see measurable_fun_xsection in lebesgue_integral.v + the difference is that this section uses a finite kernel m2 + instead of a sigma-finite measure m2 *) +Section measurable_fun_xsection_finite_kernel. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variable k : R.-fker X ~> Y. +Implicit Types A : set (X * Y). + +Let phi A := fun x => k x (xsection A x). +Let XY := [set A | measurable A /\ measurable_fun setT (phi A)]. + +Lemma measurable_fun_xsection_finite_kernel A : + A \in measurable -> measurable_fun setT (phi A). +Proof. +move: A; suff : measurable `<=` XY by move=> + A; rewrite inE => /[apply] -[]. +move=> /= A mA; rewrite /XY/=; split => //; rewrite (_ : phi _ = + (fun x => mrestr (k x) measurableT (xsection A x))); last first. + by apply/funext => x//=; rewrite /mrestr setIT. +apply measurable_prod_subset_xsection_kernel => // x. +have [r hr] := measure_uub k; exists r => B mB. +by rewrite (le_lt_trans _ (hr x)) // /mrestr /= setIT le_measure// inE. +Qed. + +End measurable_fun_xsection_finite_kernel. + +Section measurable_fun_integral_finite_sfinite. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variable k : X * Y -> \bar R. + +Lemma measurable_fun_xsection_integral + (l : X -> {measure set Y -> \bar R}) + (k_ : ({nnsfun [the measurableType _ of (X * Y)%type] >-> R})^nat) + (ndk_ : nondecreasing_seq (k_ : (X * Y -> R)^nat)) + (k_k : forall z, EFin \o (k_ ^~ z) --> k z) : + (forall n r, + measurable_fun setT (fun x => l x (xsection (k_ n @^-1` [set r]) x))) -> + measurable_fun setT (fun x => \int[l x]_y k (x, y)). +Proof. +move=> h. +rewrite (_ : (fun x => _) = + (fun x => lim_esup (fun n => \int[l x]_y (k_ n (x, y))%:E))); last first. + apply/funext => x. + transitivity (lim (fun n => \int[l x]_y (k_ n (x, y))%:E)); last first. + rewrite is_cvg_lim_esupE//. + apply: ereal_nondecreasing_is_cvg => m n mn. + apply: ge0_le_integral => //. + - by move=> y _; rewrite lee_fin. + - exact/EFin_measurable_fun/measurable_fun_prod1. + - by move=> y _; rewrite lee_fin. + - exact/EFin_measurable_fun/measurable_fun_prod1. + - by move=> y _; rewrite lee_fin; exact/lefP/ndk_. + rewrite -monotone_convergence//. + - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: k_k. + - by move=> n; exact/EFin_measurable_fun/measurable_fun_prod1. + - by move=> n y _; rewrite lee_fin. + - by move=> y _ m n mn; rewrite lee_fin; exact/lefP/ndk_. +apply: measurable_fun_lim_esup => n. +rewrite [X in measurable_fun _ X](_ : _ = (fun x => \int[l x]_y + (\sum_(r \in range (k_ n)) + r * \1_(k_ n @^-1` [set r]) (x, y))%:E)); last first. + by apply/funext => x; apply: eq_integral => y _; rewrite fimfunE. +rewrite [X in measurable_fun _ X](_ : _ = (fun x => \sum_(r \in range (k_ n)) + (\int[l x]_y (r * \1_(k_ n @^-1` [set r]) (x, y))%:E))); last first. + apply/funext => x; rewrite -ge0_integral_fsum//. + - by apply: eq_integral => y _; rewrite -fsumEFin. + - move=> r. + apply/EFin_measurable_fun/measurable_funrM/measurable_fun_prod1 => /=. + rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) (measurable_set1 r)))//. + exact/measurable_funP. + - by move=> m y _; rewrite nnfun_muleindic_ge0. +apply: emeasurable_fun_fsum => // r. +rewrite [X in measurable_fun _ X](_ : _ = (fun x => r%:E * + \int[l x]_y (\1_(k_ n @^-1` [set r]) (x, y))%:E)); last first. + apply/funext => x; under eq_integral do rewrite EFinM. + have [r0|r0] := leP 0%R r. + rewrite ge0_integralM//; last by move=> y _; rewrite lee_fin. + apply/EFin_measurable_fun/measurable_fun_prod1 => /=. + rewrite (_ : \1_ _ = mindic R (measurable_sfunP (k_ n) (measurable_set1 r)))//. + exact/measurable_funP. + rewrite integral0_eq; last first. + by move=> y _; rewrite preimage_nnfun0// indic0 mule0. + by rewrite integral0_eq ?mule0// => y _; rewrite preimage_nnfun0// indic0. +apply/measurable_funeM. +rewrite (_ : (fun x => _) = (fun x => l x (xsection (k_ n @^-1` [set r]) x))). + exact/h. +apply/funext => x; rewrite integral_indic//; last first. + rewrite (_ : (fun x => _) = xsection (k_ n @^-1` [set r]) x). + exact: measurable_xsection. + by rewrite /xsection; apply/seteqP; split=> y/= /[!inE]. +congr (l x _); apply/funext => y1/=; rewrite /xsection/= inE. +by apply/propext; tauto. +Qed. + +Lemma measurable_fun_integral_finite_kernel (l : R.-fker X ~> Y) + (k0 : forall z, 0 <= k z) (mk : measurable_fun setT k) : + measurable_fun setT (fun x => \int[l x]_y k (x, y)). +Proof. +have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x). +apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r. +have [l_ hl_] := measure_uub l. +by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. +Qed. + +Lemma measurable_fun_integral_sfinite_kernel (l : R.-sfker X ~> Y) + (k0 : forall t, 0 <= k t) (mk : measurable_fun setT k) : + measurable_fun setT (fun x => \int[l x]_y k (x, y)). +Proof. +have [k_ [ndk_ k_k]] := approximation measurableT mk (fun xy _ => k0 xy). +apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r. +have [l_ hl_] := sfinite l. +rewrite (_ : (fun x => _) = (fun x => + mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first. + by apply/funext => x; rewrite hl_//; exact/measurable_xsection. +apply: ge0_emeasurable_fun_sum => // m. +by apply: measurable_fun_xsection_finite_kernel => // /[!inE]. +Qed. + +End measurable_fun_integral_finite_sfinite. +Arguments measurable_fun_xsection_integral {_ _ _ _ _} k l. +Arguments measurable_fun_integral_finite_kernel {_ _ _ _ _} k l. +Arguments measurable_fun_integral_sfinite_kernel {_ _ _ _ _} k l. + +Section kdirac. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variable f : X -> Y. + +Definition kdirac (mf : measurable_fun setT f) + : X -> {measure set Y -> \bar R} := + fun x => [the measure _ _ of dirac (f x)]. + +Hypothesis mf : measurable_fun setT f. + +Let measurable_fun_kdirac U : measurable U -> + measurable_fun setT (kdirac mf ^~ U). +Proof. +move=> mU; apply/EFin_measurable_fun. +by rewrite (_ : (fun x => _) = mindic R mU \o f)//; exact/measurable_funT_comp. +Qed. + +HB.instance Definition _ := isKernel.Build _ _ _ _ _ (kdirac mf) + measurable_fun_kdirac. + +Let kdirac_prob x : kdirac mf x setT = 1. +Proof. by rewrite /kdirac/= diracT. Qed. + +HB.instance Definition _ := Kernel_isProbability.Build _ _ _ _ _ + (kdirac mf) kdirac_prob. + +End kdirac. +Arguments kdirac {d d' X Y R f}. + +Section dist_salgebra_instance. +Context d (T : measurableType d) (R : realType). + +Let p0 : probability T R := [the probability _ _ of dirac point]. + +Definition prob_pointed := Pointed.Class + (Choice.Class gen_eqMixin (Choice.Class gen_eqMixin gen_choiceMixin)) p0. + +Canonical probability_eqType := EqType (probability T R) prob_pointed. +Canonical probability_choiceType := ChoiceType (probability T R) prob_pointed. +Canonical probability_ptType := PointedType (probability T R) prob_pointed. + +Definition mset (U : set T) (r : R) := [set mu : probability T R | mu U < r%:E]. + +Lemma lt0_mset (U : set T) (r : R) : (r < 0)%R -> mset U r = set0. +Proof. +move=> r0; apply/seteqP; split => // x/=. +by apply/negP; rewrite -leNgt (@le_trans _ _ 0)// lee_fin ltW. +Qed. + +Lemma gt1_mset (U : set T) (r : R) : + measurable U -> (1 < r)%R -> mset U r = setT. +Proof. +move=> mU r1; apply/seteqP; split => // x/= _. +by rewrite /mset/= (le_lt_trans (probability_le1 _ _)). +Qed. + +Definition pset : set (set (probability T R)) := + [set mset U r | r in `[0%R,1%R] & U in measurable]. + +Definition pprobability : measurableType pset.-sigma := + [the measurableType _ of salgebraType pset]. + +End dist_salgebra_instance. + +Section kprobability. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variable P : X -> pprobability Y R. + +Definition kprobability (mP : measurable_fun setT P) + : X -> {measure set Y -> \bar R} := P. + +Hypothesis mP : measurable_fun setT P. + +Let measurable_fun_kprobability U : measurable U -> + measurable_fun setT (kprobability mP ^~ U). +Proof. +move=> mU. +apply: (measurability (ErealGenInftyO.measurableE R)) => _ /= -[_ [r ->] <-]. +rewrite setTI preimage_itv_infty_o -/(P @^-1` mset U r). +have [r0|r0] := leP 0%R r; last by rewrite lt0_mset// preimage_set0. +have [r1|r1] := leP r 1%R; last by rewrite gt1_mset// preimage_setT. +move: mP => /(_ measurableT (mset U r)); rewrite setTI; apply. +by apply: sub_sigma_algebra; exists r => /=; [rewrite in_itv/= r0|exists U]. +Qed. + +HB.instance Definition _ := + @isKernel.Build _ _ X Y R (kprobability mP) measurable_fun_kprobability. + +Let kprobability_prob x : kprobability mP x setT = 1. +Proof. by rewrite /kprobability/= probability_setT. Qed. + +HB.instance Definition _ := + @Kernel_isProbability.Build _ _ X Y R (kprobability mP) kprobability_prob. + +End kprobability. + +Section kadd. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variables k1 k2 : R.-ker X ~> Y. + +Definition kadd : X -> {measure set Y -> \bar R} := + fun x => [the measure _ _ of measure_add (k1 x) (k2 x)]. + +Let measurable_fun_kadd U : measurable U -> + measurable_fun setT (kadd ^~ U). +Proof. +move=> mU; rewrite /kadd. +rewrite (_ : (fun _ => _) = (fun x => k1 x U + k2 x U)); last first. + by apply/funext => x; rewrite -measure_addE. +by apply: emeasurable_funD; exact/measurable_kernel. +Qed. + +HB.instance Definition _ := + @isKernel.Build _ _ _ _ _ kadd measurable_fun_kadd. +End kadd. + +Section sfkadd. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variables k1 k2 : R.-sfker X ~> Y. + +Let sfinite_kadd : exists2 k_ : (R.-ker _ ~> _)^nat, + forall n, measure_fam_uub (k_ n) & + forall x U, measurable U -> + kadd k1 k2 x U = mseries (k_ ^~ x) 0 U. +Proof. +have [f1 hk1] := sfinite k1; have [f2 hk2] := sfinite k2. +exists (fun n => [the _.-ker _ ~> _ of kadd (f1 n) (f2 n)]). + move=> n. + have [r1 f1r1] := measure_uub (f1 n). + have [r2 f2r2] := measure_uub (f2 n). + exists (r1 + r2)%R => x/=. + by rewrite /msum !big_ord_recr/= big_ord0 add0e EFinD lte_add. +move=> x U mU. +rewrite /kadd/= -/(measure_add (k1 x) (k2 x)) measure_addE hk1//= hk2//=. +rewrite /mseries -nneseriesD//; apply: eq_eseriesr => n _ /=. +by rewrite -/(measure_add (f1 n x) (f2 n x)) measure_addE. +Qed. + +HB.instance Definition _ t := + Kernel_isSFinite_subdef.Build _ _ _ _ R (kadd k1 k2) sfinite_kadd. +End sfkadd. + +Section fkadd. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variables k1 k2 : R.-fker X ~> Y. + +Let kadd_finite_uub : measure_fam_uub (kadd k1 k2). +Proof. +have [f1 hk1] := measure_uub k1; have [f2 hk2] := measure_uub k2. +exists (f1 + f2)%R => x; rewrite /kadd /=. +rewrite -/(measure_add (k1 x) (k2 x)). +by rewrite measure_addE EFinD; exact: lte_add. +Qed. + +HB.instance Definition _ t := + Kernel_isFinite.Build _ _ _ _ R (kadd k1 k2) kadd_finite_uub. +End fkadd. + +Section mnormalize. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variables (f : X -> {measure set Y -> \bar R}) (P : probability Y R). + +Definition mnormalize x U := + let evidence := f x [set: Y] in + if (evidence == 0) || (evidence == +oo) then P U + else f x U * (fine evidence)^-1%:E. + +Let mnormalize0 x : mnormalize x set0 = 0. +Proof. +by rewrite /mnormalize; case: ifPn => // _; rewrite measure0 mul0e. +Qed. + +Let mnormalize_ge0 x U : 0 <= mnormalize x U. +Proof. by rewrite /mnormalize; case: ifPn => //; case: ifPn. Qed. + +Let mnormalize_sigma_additive x : semi_sigma_additive (mnormalize x). +Proof. +move=> F mF tF mUF; rewrite /mnormalize/=. +case: ifPn => [_|_]; first exact: measure_semi_sigma_additive. +rewrite (_ : (fun _ => _) = ((fun n => \sum_(0 <= i < n) f x (F i)) \* + cst ((fine (f x setT))^-1)%:E)); last first. + by apply/funext => n; rewrite -ge0_sume_distrl. +by apply: cvgeMr => //; exact: measure_semi_sigma_additive. +Qed. + +HB.instance Definition _ x := isMeasure.Build _ _ _ (mnormalize x) + (mnormalize0 x) (mnormalize_ge0 x) (@mnormalize_sigma_additive x). + +Let mnormalize1 x : mnormalize x setT = 1. +Proof. +rewrite /mnormalize; case: ifPn; first by rewrite probability_setT. +rewrite negb_or => /andP[ft0 ftoo]. +have ? : f x setT \is a fin_num. + by rewrite ge0_fin_numE// lt_neqAle ftoo/= leey. +by rewrite -{1}(@fineK _ (f x setT))// -EFinM divrr// ?unitfE fine_eq0. +Qed. + +HB.instance Definition _ x := + Measure_isProbability.Build _ _ _ (mnormalize x) (mnormalize1 x). + +End mnormalize. + +Section knormalize. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variable f : R.-ker X ~> Y. + +Definition knormalize (P : probability Y R) : X -> {measure set Y -> \bar R} := + fun x => [the measure _ _ of mnormalize f P x]. + +Variable P : probability Y R. + +Let measurable_fun_knormalize U : + measurable U -> measurable_fun setT (knormalize P ^~ U). +Proof. +move=> mU; rewrite /knormalize/= /mnormalize /=. +rewrite (_ : (fun _ => _) = (fun x => + if f x setT == 0 then P U else if f x setT == +oo then P U + else f x U * (fine (f x setT))^-1%:E)); last first. + apply/funext => x; case: ifPn => [/orP[->//|->]|]; first by case: ifPn. + by rewrite negb_or=> /andP[/negbTE -> /negbTE ->]. +apply: measurable_fun_if => //; + [exact: kernel_measurable_fun_eq_cst|exact: measurable_fun_cst|]. +apply: measurable_fun_if => //. +- rewrite setTI [X in measurable X](_ : _ = [set t | f t setT != 0]). + exact: kernel_measurable_neq_cst. + by apply/seteqP; split => [x /negbT//|x /negbTE]. +- apply: (@measurable_funS _ _ _ _ setT) => //. + exact: kernel_measurable_fun_eq_cst. +- exact: measurable_fun_cst. +- apply: emeasurable_funM. + by have := measurable_kernel f U mU; exact: measurable_funS. + apply/EFin_measurable_fun. + apply: (@measurable_fun_comp _ _ _ _ _ _ [set r : R | r != 0%R]) => //. + + exact: open_measurable. + + move=> /= r [t] [] [_ ft0] ftoo ftr; apply/eqP => r0. + move: (ftr); rewrite r0 => /eqP; rewrite fine_eq0 ?ft0//. + by rewrite ge0_fin_numE// lt_neqAle leey ftoo. + + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0. + exact: inv_continuous. + + apply: measurable_funT_comp => /=; first exact: measurable_fun_fine. + by have := measurable_kernel f _ measurableT; exact: measurable_funS. +Qed. + +HB.instance Definition _ := isKernel.Build _ _ _ _ R (knormalize P) + measurable_fun_knormalize. + +Let knormalize1 x : knormalize P x setT = 1. +Proof. +rewrite /knormalize/= /mnormalize. +case: ifPn => [_|]; first by rewrite probability_setT. +rewrite negb_or => /andP[fx0 fxoo]. +have ? : f x setT \is a fin_num by rewrite ge0_fin_numE// lt_neqAle fxoo/= leey. +rewrite -{1}(@fineK _ (f x setT))//=. +by rewrite -EFinM divrr// ?lte_fin ?ltr1n// ?unitfE fine_eq0. +Qed. + +HB.instance Definition _ := + @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) knormalize1. + +End knormalize. + +Section kcomp_def. +Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2) + (Z : measurableType d3) (R : realType). +Variable l : X -> {measure set Y -> \bar R}. +Variable k : (X * Y)%type -> {measure set Z -> \bar R}. + +Definition kcomp x U := \int[l x]_y k (x, y) U. + +End kcomp_def. + +Section kcomp_is_measure. +Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2) + (Z : measurableType d3) (R : realType). +Variable l : R.-ker X ~> Y. +Variable k : R.-ker [the measurableType _ of (X * Y)%type] ~> Z. + +Local Notation "l \; k" := (kcomp l k). + +Let kcomp0 x : (l \; k) x set0 = 0. +Proof. +by rewrite /kcomp (eq_integral (cst 0)) ?integral0// => y _; rewrite measure0. +Qed. + +Let kcomp_ge0 x U : 0 <= (l \; k) x U. Proof. exact: integral_ge0. Qed. + +Let kcomp_sigma_additive x : semi_sigma_additive ((l \; k) x). +Proof. +move=> U mU tU mUU; rewrite [X in _ --> X](_ : _ = + \int[l x]_y (\sum_(n V _. + by apply/esym/cvg_lim => //; exact/measure_semi_sigma_additive. +apply/cvg_closeP; split. + by apply: is_cvg_nneseries => n _; exact: integral_ge0. +rewrite closeE// integral_nneseries// => n. +by have /measurable_fun_prod1 := measurable_kernel k _ (mU n). +Qed. + +HB.instance Definition _ x := isMeasure.Build _ R _ + ((l \; k) x) (kcomp0 x) (kcomp_ge0 x) (@kcomp_sigma_additive x). + +Definition mkcomp : X -> {measure set Z -> \bar R} := fun x => + [the measure _ _ of (l \; k) x]. + +End kcomp_is_measure. + +Notation "l \; k" := (mkcomp l k) : ereal_scope. + +Module KCOMP_FINITE_KERNEL. + +Section kcomp_finite_kernel_kernel. +Context d d' d3 (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType) (l : R.-fker X ~> Y) + (k : R.-ker [the measurableType _ of (X * Y)%type] ~> Z). + +Lemma measurable_fun_kcomp_finite U : + measurable U -> measurable_fun setT ((l \; k) ^~ U). +Proof. +move=> mU; apply: (measurable_fun_integral_finite_kernel (k ^~ U)) => //=. +exact/measurable_kernel. +Qed. + +HB.instance Definition _ := + isKernel.Build _ _ X Z R (l \; k) measurable_fun_kcomp_finite. + +End kcomp_finite_kernel_kernel. + +Section kcomp_finite_kernel_finite. +Context d d' d3 (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). +Variable l : R.-fker X ~> Y. +Variable k : R.-fker [the measurableType _ of (X * Y)%type] ~> Z. + +Let mkcomp_finite : measure_fam_uub (l \; k). +Proof. +have /measure_fam_uubP[r hr] := measure_uub k. +have /measure_fam_uubP[s hs] := measure_uub l. +apply/measure_fam_uubP; exists (PosNum [gt0 of (r%:num * s%:num)%R]) => x /=. +apply: (@le_lt_trans _ _ (\int[l x]__ r%:num%:E)). + apply: ge0_le_integral => //. + - have /measurable_fun_prod1 := measurable_kernel k _ measurableT. + exact. + - exact/measurable_fun_cst. + - by move=> y _; exact/ltW/hr. +by rewrite integral_cst//= EFinM lte_pmul2l. +Qed. + +HB.instance Definition _ := + Kernel_isFinite.Build _ _ X Z R (l \; k) mkcomp_finite. + +End kcomp_finite_kernel_finite. +End KCOMP_FINITE_KERNEL. + +Section kcomp_sfinite_kernel. +Context d d' d3 (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). +Variable l : R.-sfker X ~> Y. +Variable k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z. + +Import KCOMP_FINITE_KERNEL. + +Lemma mkcomp_sfinite : exists k_ : (R.-fker X ~> Z)^nat, + forall x U, measurable U -> (l \; k) x U = kseries k_ x U. +Proof. +have [k_ hk_] := sfinite k; have [l_ hl_] := sfinite l. +have [kl hkl] : exists kl : (R.-fker X ~> Z) ^nat, forall x U, + \esum_(i in setT) (l_ i.2 \; k_ i.1) x U = \sum_(i [the _.-fker _ ~> _ of l_ (f i).2 \; k_ (f i).1]) => x U. + by rewrite (reindex_esum [set: nat] _ f)// nneseries_esum// fun_true. +exists kl => x U mU. +transitivity (([the _.-ker _ ~> _ of kseries l_] \; + [the _.-ker _ ~> _ of kseries k_]) x U). + rewrite /= /kcomp [in RHS](eq_measure_integral (l x)); last first. + by move=> *; rewrite hl_. + by apply: eq_integral => y _; rewrite hk_. +rewrite /= /kcomp/= integral_nneseries//=; last first. + move=> n; have /measurable_fun_prod1 := measurable_kernel (k_ n) _ mU. + exact. +transitivity (\sum_(i i _; rewrite integral_kseries//. + by have /measurable_fun_prod1 := measurable_kernel (k_ i) _ mU; exact. +rewrite /mseries -hkl/=. +rewrite (_ : setT = setT `*`` (fun=> setT)); last by apply/seteqP; split. +rewrite -(@esum_esum _ _ _ _ _ (fun i j => (l_ j \; k_ i) x U))//. +rewrite nneseries_esum; last by move=> n _; exact: nneseries_ge0. +by rewrite fun_true; apply: eq_esum => /= i _; rewrite nneseries_esum// fun_true. +Qed. + +Lemma measurable_fun_mkcomp_sfinite U : measurable U -> + measurable_fun setT ((l \; k) ^~ U). +Proof. +move=> mU; apply: (measurable_fun_integral_sfinite_kernel (k ^~ U)) => //. +exact/measurable_kernel. +Qed. + +End kcomp_sfinite_kernel. + +Module KCOMP_SFINITE_KERNEL. +Section kcomp_sfinite_kernel. +Context d d' d3 (X : measurableType d) (Y : measurableType d') + (Z : measurableType d3) (R : realType). +Variable l : R.-sfker X ~> Y. +Variable k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z. + +HB.instance Definition _ := + isKernel.Build _ _ X Z R (l \; k) (measurable_fun_mkcomp_sfinite l k). + +#[export] +HB.instance Definition _ := + Kernel_isSFinite.Build _ _ X Z R (l \; k) (mkcomp_sfinite l k). + +End kcomp_sfinite_kernel. +End KCOMP_SFINITE_KERNEL. +HB.export KCOMP_SFINITE_KERNEL. + +Section measurable_fun_preimage_integral. +Context d d' (X : measurableType d) (Y : measurableType d') (R : realType). +Variables (k : Y -> \bar R) + (k_ : ({nnsfun Y >-> R}) ^nat) + (ndk_ : nondecreasing_seq (k_ : (Y -> R)^nat)) + (k_k : forall z, setT z -> EFin \o (k_ ^~ z) --> k z). + +Let k_2 : (X * Y -> R)^nat := fun n => k_ n \o snd. + +Let k_2_ge0 n x : (0 <= k_2 n x)%R. Proof. by []. Qed. + +HB.instance Definition _ n := @isNonNegFun.Build _ _ _ (k_2_ge0 n). + +Let mk_2 n : measurable_fun setT (k_2 n). +Proof. by apply: measurable_funT_comp => //; exact: measurable_fun_snd. Qed. + +HB.instance Definition _ n := @isMeasurableFun.Build _ _ _ _ (mk_2 n). + +Let fk_2 n : finite_set (range (k_2 n)). +Proof. +have := @fimfunP _ _ (k_ n). +suff : range (k_ n) = range (k_2 n) by move=> <-. +by apply/seteqP; split => r [y ?] <-; [exists (point, y)|exists y.2]. +Qed. + +HB.instance Definition _ n := @FiniteImage.Build _ _ _ (fk_2 n). + +Lemma measurable_fun_preimage_integral (l : X -> {measure set Y -> \bar R}) : + (forall n r, measurable_fun setT (l ^~ (k_ n @^-1` [set r]))) -> + measurable_fun setT (fun x => \int[l x]_z k z). +Proof. +move=> h; apply: (measurable_fun_xsection_integral (k \o snd) l + (fun n => [the {nnsfun _ >-> _} of k_2 n])) => /=. +- by rewrite /k_2 => m n mn; apply/lefP => -[x y] /=; exact/lefP/ndk_. +- by move=> [x y]; exact: k_k. +- move=> n r _ /= B mB. + have := h n r measurableT B mB; rewrite !setTI. + suff : (l ^~ (k_ n @^-1` [set r])) @^-1` B = + (fun x => l x (xsection (k_2 n @^-1` [set r]) x)) @^-1` B by move=> ->. + by apply/seteqP; split => x/=; + rewrite (comp_preimage _ snd (k_ n)) xsection_preimage_snd. +Qed. + +End measurable_fun_preimage_integral. + +Lemma measurable_fun_integral_kernel + d d' (X : measurableType d) (Y : measurableType d') (R : realType) + (l : X -> {measure set Y -> \bar R}) + (ml : forall U, measurable U -> measurable_fun setT (l ^~ U)) + (* NB: l is really just a kernel *) + (k : Y -> \bar R) (k0 : forall z, 0 <= k z) (mk : measurable_fun setT k) : + measurable_fun setT (fun x => \int[l x]_y k y). +Proof. +have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x). +by apply: (measurable_fun_preimage_integral ndk_ k_k) => n r; exact/ml. +Qed. + +Section integral_kcomp. +Context d d2 d3 (X : measurableType d) (Y : measurableType d2) + (Z : measurableType d3) (R : realType). +Variables (l : R.-sfker X ~> Y) + (k : R.-sfker [the measurableType _ of (X * Y)%type] ~> Z). + +Let integral_kcomp_indic x E (mE : measurable E) : + \int[(l \; k) x]_z (\1_E z)%:E = \int[l x]_y (\int[k (x, y)]_z (\1_E z)%:E). +Proof. +rewrite integral_indic//= /kcomp. +by apply: eq_integral => y _; rewrite integral_indic. +Qed. + +Let integral_kcomp_nnsfun x (f : {nnsfun Z >-> R}) : + \int[(l \; k) x]_z (f z)%:E = \int[l x]_y (\int[k (x, y)]_z (f z)%:E). +Proof. +under [in LHS]eq_integral do rewrite fimfunE -fsumEFin//. +rewrite ge0_integral_fsum//; last 2 first. + - move=> r; apply/EFin_measurable_fun/measurable_funrM. + have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. + by rewrite (_ : \1__ = mindic R fr). + - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. +under [in RHS]eq_integral. + move=> y _. + under eq_integral. + by move=> z _; rewrite fimfunE -fsumEFin//; over. + rewrite /= ge0_integral_fsum//; last 2 first. + - move=> r; apply/EFin_measurable_fun/measurable_funrM. + have fr : measurable (f @^-1` [set r]) by exact/measurable_sfunP. + by rewrite (_ : \1__ = mindic R fr). + - by move=> r z _; rewrite EFinM nnfun_muleindic_ge0. + under eq_fsbigr. + move=> r _. + rewrite (integralM_indic _ (fun r => f @^-1` [set r]))//; last first. + by move=> r0; rewrite preimage_nnfun0. + rewrite integral_indic// setIT. + over. + over. +rewrite /= ge0_integral_fsum//; last 2 first. + - move=> r; apply: measurable_funeM. + have := measurable_kernel k (f @^-1` [set r]) + (measurable_sfunP f (measurable_set1 r)). + by move=> /measurable_fun_prod1; exact. + - move=> n y _. + have := mulemu_ge0 (fun n => f @^-1` [set n]). + by apply; exact: preimage_nnfun0. +apply: eq_fsbigr => r _. +rewrite (integralM_indic _ (fun r => f @^-1` [set r]))//; last first. + exact: preimage_nnfun0. +rewrite /= integral_kcomp_indic; last exact/measurable_sfunP. +have [r0|r0] := leP 0%R r. + rewrite ge0_integralM//; last first. + have := measurable_kernel k (f @^-1` [set r]) + (measurable_sfunP f (measurable_set1 r)). + by move/measurable_fun_prod1; exact. + by congr (_ * _); apply: eq_integral => y _; rewrite integral_indic// setIT. +rewrite integral0_eq ?mule0; last first. + move=> y _; rewrite integral0_eq// => z _. + by rewrite preimage_nnfun0// indic0. +by rewrite integral0_eq// => y _; rewrite preimage_nnfun0// measure0 mule0. +Qed. + +Lemma integral_kcomp x f : (forall z, 0 <= f z) -> measurable_fun setT f -> + \int[(l \; k) x]_z f z = \int[l x]_y (\int[k (x, y)]_z f z). +Proof. +move=> f0 mf. +have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z). +transitivity (\int[(l \; k) x]_z (lim (EFin \o f_^~ z))). + by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: f_f. +rewrite monotone_convergence//; last 3 first. + by move=> n; exact/EFin_measurable_fun. + by move=> n z _; rewrite lee_fin. + by move=> z _ a b /ndf_ /lefP ab; rewrite lee_fin. +rewrite (_ : (fun _ => _) = + (fun n => \int[l x]_y (\int[k (x, y)]_z (f_ n z)%:E)))//; last first. + by apply/funext => n; rewrite integral_kcomp_nnsfun. +transitivity (\int[l x]_y lim (fun n => \int[k (x, y)]_z (f_ n z)%:E)). + rewrite -monotone_convergence//; last 3 first. + - move=> n; apply: measurable_fun_integral_kernel => //. + + move=> U mU; have := measurable_kernel k _ mU. + by move=> /measurable_fun_prod1; exact. + + by move=> z; rewrite lee_fin. + + exact/EFin_measurable_fun. + - by move=> n y _; apply: integral_ge0 => // z _; rewrite lee_fin. + - move=> y _ a b ab; apply: ge0_le_integral => //. + + by move=> z _; rewrite lee_fin. + + exact/EFin_measurable_fun. + + by move=> z _; rewrite lee_fin. + + exact/EFin_measurable_fun. + + by move: ab => /ndf_ /lefP ab z _; rewrite lee_fin. +apply: eq_integral => y _; rewrite -monotone_convergence//; last 3 first. + - by move=> n; exact/EFin_measurable_fun. + - by move=> n z _; rewrite lee_fin. + - by move=> z _ a b /ndf_ /lefP; rewrite lee_fin. +by apply: eq_integral => z _; apply/cvg_lim => //; exact: f_f. +Qed. + +End integral_kcomp. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 7a7fd10854..e9b430901a 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -4066,8 +4066,12 @@ Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (R : realType). Implicit Types A : set (T1 * T2). Section xsection. -Variables (pt2 : T2) (m2 : {measure set T2 -> \bar R}). -Let phi A := m2 \o xsection A. +Variables (pt2 : T2) (m2 : T1 -> {measure set T2 -> \bar R}). +(* the generalization from m2 : {measure set T2 -> \bar R}t to + T1 -> {measure set T2 -> \bar R} is needed to develop the theory + of kernels; the original type was sufficient for the development + of the theory of integration *) +Let phi A x := m2 x (xsection A x). Let B := [set A | measurable A /\ measurable_fun setT (phi A)]. Lemma xsection_ndseq_closed : ndseq_closed B.