proposition: Lemma Radon_Nikodym_chain_rule : nu `<< mu -> mu `<< la -> ae_eq la setT ('d nu '/d la) ('d nu '/d mu \* 'd [the charge _ _ of charge_of_finite_measure mu] '/d la).
proof: Proof. have [Pnu [Nnu nuPN]] := Hahn_decomposition nu. move=> numu mula; have nula := measure_dominates_trans numu mula. apply: integral_ae_eq; [exact: measurableT| |exact: emeasurable_funM|]. - exact: Radon_Nikodym_integrable. - move=> E _ mE. rewrite -Radon_Nikodym_integral// Radon_Nikodym_change_of_variables//. + exact: Radon_Nikodym_integral. + by apply: (integrableS measurableT) => //; exact: Radon_Nikodym_integrable. 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