proposition: Lemma summable_sum (F : I -> T -> R) (P : pred I) r : (forall i, P i -> summable (F i)) -> summable (fun x => \sum_(i <- r | P i) F i x).
proof: Proof. move=> sm_F; elim: r => [|i r ih]. by apply/(eq_summable _ summable0) => x; rewrite big_nil. pose G x := (F i x) * (P i)%:R + \sum_(i <- r | P i) F i x. apply/(eq_summable (S1 := G)) => [x|]. by rewrite {}/G big_cons; case: ifP=> Pi; rewrite !Monoid.simpm. apply/summableD => //; case/boolP: (P i) => [|_]. by move/sm_F; apply/eq_summable => x; rewrite mulr1. by apply/(eq_summable _ summable0) => x; rewrite mulr0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology