proposition: Lemma eq_exp mu (f1 f2 : T -> R): {in dinsupp mu, f1 =1 f2} -> \E_[mu] f1 = \E_[mu] f2.
proof: Proof. move=> eq_f; apply/eq_sum => x; case/boolP: (x \in dinsupp mu). by move/eq_f=> ->. by move/dinsuppPn=> ->; rewrite !mulr0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum