proposition: Lemma measurable_fun_fubini_tonelli_G : measurable_fun setT G.
proof: Proof. have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). apply: (emeasurable_fun_cvg (G_ g)) => //. - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_G. - move=> y _; rewrite /G_ /G /fubini_G [in X in _ --> X](_ : (fun _ => _) = fun x => limn (EFin \o g ^~ (x, y))); last first. by rewrite funeqE => x; apply/esym/cvg_lim => //; exact: g_f. apply: cvg_monotone_convergence => //. - by move=> n; apply/EFin_measurable_fun => //; exact/measurableT_comp. - by move=> n x _; rewrite lee_fin; exact: fun_ge0. - by move=> x _ a b ab; rewrite lee_fin; exact/lefP/g_nd. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun