proposition: Lemma ge0_integral_sum (s : seq I) : \int[mu]_(x in D) (\sum_(k <- s) f k x) = \sum_(k <- s) \int[mu]_(x in D) (f k x).
proof: Proof. elim: s => [|h t ih]. by (under eq_fun do rewrite big_nil); rewrite big_nil integral0. rewrite big_cons /= -ih -ge0_integralD//. - by apply: eq_integral => x Dx; rewrite big_cons. - by move=> *; exact: f0. - by move=> *; apply: sume_ge0 => // k _; exact: f0. - exact: emeasurable_fun_sum. 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