proposition: Lemma Radon_Nikodym_cscale mu nu c E : measurable E -> nu `<< mu -> ae_eq mu E ('d [the charge _ _ of cscale c nu] '/d mu) (fun x => c%:E * 'd nu '/d mu x).
proof: Proof. move=> mE numu; apply: integral_ae_eq => [//| | |A AE mA]. - apply: (integrableS measurableT) => //. exact/Radon_Nikodym_integrable/dominates_cscalel. - exact/measurable_funTS/emeasurable_funM. - rewrite integralZl//; last first. by apply: (integrableS measurableT) => //; exact: Radon_Nikodym_integrable. rewrite -Radon_Nikodym_integral => //; last exact: dominates_cscalel. by rewrite -Radon_Nikodym_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