proposition: Lemma psumID S (P : pred T) : summable S -> psum S = psum (fun x => (P x)%:R * S x) + psum (fun x => (~~P x)%:R * S x).
proof: Proof. have h x: `|S x| = (P x)%:R * `|S x| + (~~P x)%:R * `|S x|. by case: (P x); rewrite !Monoid.simpm. move=> smS; rewrite -[LHS]psum_abs (eq_psum h) psumD. by move=> x; rewrite mulr_ge0. by move=> x; rewrite mulr_ge0. by apply/summable_condl/summable_abs. by apply/summable_condl/summable_abs. congr (_ + _); apply/eq_psum_abs=> x /=. by rewrite !normrM normr_nat normr_id. by rewrite !normrM normr_nat normr_id. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology