proposition: Lemma sfun_fubini_tonelli1 : \int[m1 \x m2]_z (f z)%:E = \int[m1]_x F x.
proof: Proof. under [LHS]eq_integral do rewrite EFinf; rewrite ge0_integral_fsum //; last 2 first. - move=> r. apply/EFin_measurable_fun/measurableT_comp => //=. - by move=> r /= z _; exact: nnfun_muleindic_ge0. transitivity (\sum_(k \in range f) \int[m1]_x (k%:E * fubini_F m2 (EFin \o \1_(f @^-1` [set k])) x)). apply: eq_fsbigr => i; rewrite inE => -[z _ <-{i}]. rewrite ge0_integralZl//; last 3 first. - exact/EFin_measurable_fun. - by move=> /= x _; rewrite lee_fin. - by rewrite lee_fin. rewrite indic_fubini_tonelli1// -ge0_integralZl//; last by rewrite lee_fin. - exact: indic_measurable_fun_fubini_tonelli_F. - by move=> /= x _; exact: indic_fubini_tonelli_F_ge0. rewrite -ge0_integral_fsum //; last 2 first. - by move=> r; apply/measurable_funeM/indic_measurable_fun_fubini_tonelli_F. - move=> r x _; rewrite /fubini_F. have [r0|r0] := leP 0%R r. by rewrite mule_ge0//; exact: indic_fubini_tonelli_F_ge0. rewrite integral0_eq ?mule0// => y _. by rewrite preimage_nnfun0//= indicE in_set0. apply: eq_integral => x _; rewrite sfun_fubini_tonelli_FE. by under eq_fsbigr do rewrite indic_fubini_tonelli_FE//. 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