proposition: Lemma integral_measure_series_nnsfun (D : set T) (mD : measurable D) (f : {nnsfun T >-> R}) : \int[m]_x (f x)%:E = \sum_(n <oo) \int[m_ n]_x (f x)%:E.
proof: Proof. under eq_integral do rewrite fimfunE -fsumEFin//. rewrite ge0_integral_fsum//; last 2 first. - by move=> r /=; apply: measurableT_comp => //; exact: measurableT_comp. - by move=> r t _; rewrite EFinM nnfun_muleindic_ge0. transitivity (\sum_(i \in range f) (\sum_(n <oo) i%:E * \int[m_ n]_x (\1_(f @^-1` [set i]) x)%:E)). apply: eq_fsbigr => r _. rewrite integralZl_indic_nnsfun// integral_measure_series_indic// nneseriesZl//. by move=> n _; apply: integral_ge0 => t _; rewrite lee_fin. rewrite fsbig_finite//= -nneseries_sum; last first. move=> r j _. have [r0|r0] := leP 0%R r. by rewrite mule_ge0//; apply: integral_ge0 => // t _; rewrite lee_fin. rewrite integral0_eq ?mule0// => x _. by rewrite preimage_nnfun0// indicE in_set0. apply: eq_eseriesr => k _. rewrite integralT_nnsfun sintegralE fsbig_finite//=; apply: eq_bigr => r _. by congr (_ * _); rewrite integral_indic// setIT. 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