proposition: Lemma ae_eq_Radon_Nikodym_SigmaFinite E : measurable E -> ae_eq mu E (Radon_Nikodym_SigmaFinite.f nu mu) ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu).
proof: Proof. move=> mE; apply: integral_ae_eq => //. - apply: (integrableS measurableT) => //. exact: Radon_Nikodym_SigmaFinite.f_integrable. - exact: measurable_funTS. - move=> A AE mA; rewrite -Radon_Nikodym_integral//. by rewrite -Radon_Nikodym_SigmaFinite.f_integral. 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