proposition: Lemma summable_mlet f mu y : summable (fun x : T => mu x * (f x) y).
proof: Proof. by apply/summable_mu_wgtd=> x; rewrite ge0_mu le1_mu1. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum