proposition: Lemma measurable_fun_integral_sfinite_kernel (l : R.-sfker X ~> Y) (k0 : forall t, 0 <= k t) (mk : measurable_fun [set: X * Y] k) : measurable_fun [set: X] (fun x => \int[l x]_y k (x, y)).
proof: 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_kernel 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.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology normedtype sequences esum measure numfun lebesgue_measure lebesgue_integral