proposition: Lemma fubini_tonelli1 : \int[m1 \x m2]_z f z = \int[m1]_x F x.
proof: Proof. have [g [g_nd /= g_f]] := approximation measurableT mf (fun x _ => f0 x). have F_F x : F x = limn (F_ g ^~ x). rewrite [RHS](_ : _ = limn (fun n => \int[m2]_y (EFin \o g n) (x, y)))//. rewrite -monotone_convergence//; last 3 first. - by move=> n; exact/EFin_measurable_fun/measurableT_comp. - by move=> n /= y _; rewrite lee_fin; exact: fun_ge0. - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: g_f. rewrite [RHS](_ : _ = limn (fun n => \int[m1 \x m2]_z (EFin \o g n) z)). rewrite -monotone_convergence //; last 3 first. - by move=> n; exact/EFin_measurable_fun. - by move=> n /= x _; rewrite lee_fin; exact: fun_ge0. - by move=> y /= _ a b; rewrite lee_fin => /g_nd/lefP; exact. by apply: eq_integral => /= x _; apply/esym/cvg_lim => //; exact: g_f. rewrite [LHS](_ : _ = limn (fun n => \int[m1]_x (\int[m2]_y (EFin \o g n) (x, y)))). set r := fun _ => _; set l := fun _ => _; have -> // : l = r. by apply/funext => n; rewrite /l /r sfun_fubini_tonelli1. rewrite [RHS](_ : _ = limn (fun n => \int[m1]_x F_ g n x))//. rewrite -monotone_convergence //; first exact: eq_integral. - by move=> n; exact: sfun_measurable_fun_fubini_tonelli_F. - move=> n x _; apply: integral_ge0 => // y _ /=; rewrite lee_fin. exact: fun_ge0. - move=> x /= _ a b ab; apply: ge0_le_integral => //. + by move=> y _; rewrite lee_fin; exact: fun_ge0. + exact/EFin_measurable_fun/measurableT_comp. + by move=> *; rewrite lee_fin; exact: fun_ge0. + exact/EFin_measurable_fun/measurableT_comp. + by move=> y _; rewrite lee_fin; move/g_nd : ab => /lefP; exact. 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