proposition: Lemma summable_mu_wgtd (f : T -> R) mu : (forall x, 0 <= f x <= 1) -> summable (fun x => mu x * f x).
proof: Proof. move=> in01_f; apply/summableMr=> //. exists 1 => x; case/andP: (in01_f x) => ge0_fx le1_fx. by rewrite ger0_norm. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum