proposition: Lemma chain_rule E : nu `<< mu -> mu `<< la -> measurable E -> ae_eq la E ('d nu '/d la) ('d nu '/d mu \* 'd mu '/d la).
proof: Proof. move=> numu mula mE; have nula := measure_dominates_trans numu mula. have mf : measurable_fun E ('d nu '/d mu). exact/measurable_funTS/(measurable_int (f_integrable _)). have [h [ndh hf]] := approximation mE mf (fun x _ => f_ge0 numu x). apply: integral_ae_eq => //. - apply: (integrableS measurableT) => //. apply: f_integrable. exact: (measure_dominates_trans numu mula). - apply: emeasurable_funM => //. exact/measurable_funTS/(measurable_int (f_integrable _)). - move=> A AE mA; rewrite change_of_variables//. + by rewrite -!f_integral. + exact: f_ge0. + exact: measurable_funS mf. 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