proposition: Lemma sfun_fubini_tonelli_FE : F = fun x => \sum_(k \in range f) k%:E * m2 (xsection (f @^-1` [set k]) x).
proof: Proof. rewrite funeqE => x; rewrite /F /fubini_F [in LHS]/=. under eq_fun do rewrite fimfunE -fsumEFin//. rewrite ge0_integral_fsum //; last 2 first. - move=> i; apply/EFin_measurable_fun/measurableT_comp => //=. exact: measurableT_comp. - by move=> r y _; rewrite EFinM nnfun_muleindic_ge0. apply: eq_fsbigr => i; rewrite inE => -[/= t _ <-{i}]. under eq_fun do rewrite EFinM. rewrite ge0_integralZl//; last by rewrite lee_fin. - by rewrite -/((m2 \o xsection _) x) -indic_fubini_tonelli_FE. - exact/EFin_measurable_fun/measurableT_comp. - by move=> y _; rewrite lee_fin. 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