proposition: Lemma exp_dunit (f : T -> R) (x : T) : \E_[dunit x] f = f x.
proof: Proof. rewrite /esp (sum_seq1 x) => [y|]; rewrite dunit1E. by case: (x == y) => //; rewrite mulr0 eqxx. by rewrite eqxx mulr1. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum