proposition: Lemma integral_kseries d d' (X : measurableType d) (Y : measurableType d') (R : realType) (k : (R.-ker X ~> Y)^nat) (f : Y -> \bar R) x : (forall y, 0 <= f y) -> measurable_fun [set: Y] f -> \int[kseries k x]_y (f y) = \sum_(i <oo) \int[k i x]_y (f y).
proof: Proof. by move=> f0 mf; rewrite /kseries/= ge0_integral_measure_series. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology normedtype sequences esum measure numfun lebesgue_measure lebesgue_integral