proposition: Lemma measurable_fun_fubini_tonelli_F : measurable_fun setT F.
proof: Proof. have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). apply: (emeasurable_fun_cvg (F_ g)) => //. - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_F. - move=> x _. rewrite /F_ /F /fubini_F [in X in _ --> X](_ : (fun _ => _) = fun y => limn (EFin \o g ^~ (x, y))); last first. by rewrite funeqE => y; apply/esym/cvg_lim => //; exact: g_f. apply: cvg_monotone_convergence => //. - by move=> n; apply/EFin_measurable_fun => //; exact/measurableT_comp. - by move=> n y _; rewrite lee_fin//; exact: fun_ge0. - by move=> y _ 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