proposition: Lemma le_psum_condl (S : T -> R) (P : pred T) : summable S -> psum (fun x => (P x)%:R * S x) <= psum S.
proof: Proof. move=> smS; apply/le_psum_abs=> // x; rewrite normrM. by apply/ler_piMl => //; rewrite normr_nat lern1 leq_b1. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology