proposition: Lemma partition_psum_cond (S : T -> R) : summable S -> psum S = psum (fun y => (C y)%:R * psum (fun x => S x * (f x == y)%:R)).
proof: Proof. move=> smS; apply/(eq_trans (partition_psum smS)). apply/eq_psum => y; case/boolP: (C y); rewrite !simpm //. move=> NCy; rewrite psum_eq0 // => x; case: (_ =P y). by move/eqP=> fxE; move/asboolP: NCy; case; exists x. by 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