proposition: Lemma dmargin_psumE (mu : {distr T / R}) (f : T -> U) y : (dmargin f mu) y = psum (fun x => (f x == y)%:R * mu x).
proof: Proof. rewrite dmarginE dletE; apply/eq_psum => x //=. by rewrite mulrC dunit1E. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum