proposition: Lemma integral_distribution (X : {RV P >-> R}) (f : R -> \bar R) : measurable_fun [set: R] f -> (forall y, 0 <= f y) -> \int[distribution P X]_y f y = \int[P]_x (f \o X) x.
proof: Proof. by move=> mf f0; rewrite integral_pushforward. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) HB(structures) exp numfun lebesgue_measure lebesgue_integral reals ereal signed topology normedtype sequences esum measure exp numfun lebesgue_measure lebesgue_integral