proposition: Lemma integrableM f E : (forall x, 0 <= f x) -> measurable E -> nu.-integrable E f -> mu.-integrable E (f \* 'd nu '/d mu).
proof: Proof. move=> f0 mE intEf; apply/integrableP; split. apply: emeasurable_funM; first exact: (@measurable_int _ _ _ nu). exact/measurable_funTS/(measurable_int (f_integrable _)). under eq_integral. move=> x _; rewrite gee0_abs; last first. by apply: mule_ge0=> //; exact: f_ge0. over. rewrite change_of_variables//; last exact: (@measurable_int _ _ _ nu). by move/integrableP : intEf=> [mf +]; under eq_integral do rewrite gee0_abs//. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets cardinality) mathcomp(functions fsbigop set_interval) HB(structures) reals ereal signed topology numfun normedtype sequences esum measure realfun lebesgue_measure lebesgue_integral