proposition: Lemma Radon_Nikodym_cadd mu nu0 nu1 E : measurable E -> nu0 `<< mu -> nu1 `<< mu -> ae_eq mu E ('d [the charge _ _ of cadd nu0 nu1] '/d mu) ('d nu0 '/d mu \+ 'd nu1 '/d mu).
proof: Proof. move=> mE nu0mu nu1mu; apply: integral_ae_eq => [//| | |A AE mA]. - apply: (integrableS measurableT) => //. by apply: Radon_Nikodym_integrable => /=; exact: dominates_cadd. - by apply: measurable_funTS => //; exact: emeasurable_funD. - rewrite integralD //; [|exact: integrableS (Radon_Nikodym_integrable _)..]. rewrite -Radon_Nikodym_integral //=; last exact: dominates_cadd. by rewrite -Radon_Nikodym_integral // -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