proposition: Lemma summable_pr E mu : summable (fun x => (E x)%:R * mu x).
proof: Proof. apply/(le_summable (F2 := mu)) => [x|]; last by apply/summable_mu. by rewrite mulr_ge0 ?ler0n //= ler_piMl // lern1 leq_b1. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum