proposition: Lemma integral_kcomp x f : (forall z, 0 <= f z) -> measurable_fun [set: Z] f -> \int[kcomp l k x]_z f z = \int[l x]_y (\int[k (x, y)]_z f z).
proof: Proof. move=> f0 mf. have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z). transitivity (\int[kcomp l k x]_z (lim ((f_ n z)%:E @[n --> \oo]))). 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 ((\int[k (x, y)]_z (f_ n z)%:E) @[n --> \oo])). rewrite -monotone_convergence//; last 3 first. - move=> n; apply: measurable_fun_integral_kernel => //. + by move=> U mU; exact: measurableT_comp (measurable_kernel k _ mU) _. + 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.
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