proposition: Lemma Radon_Nikodym_change_of_variables f E : measurable E -> nu.-integrable E f -> \int[mu]_(x in E) (f x * ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu) x) = \int[nu]_(x in E) f x.
proof: Proof. move=> mE mf; rewrite [in RHS](funeposneg f) integralB //; last 2 first. - exact: integrable_funepos. - exact: integrable_funeneg. rewrite -(ae_eq_integral _ _ _ _ _ (ae_eq_mul2l f (ae_eq_Radon_Nikodym_SigmaFinite mE)))//; last 2 first. - apply: emeasurable_funM => //; first exact: measurable_int mf. apply: measurable_funTS. exact: measurable_int (Radon_Nikodym_SigmaFinite.f_integrable _). - apply: emeasurable_funM => //; first exact: measurable_int mf. exact: measurable_funTS. rewrite [in LHS](funeposneg f). under eq_integral => x xE. rewrite muleBl; last 2 first. - exact: Radon_Nikodym_SigmaFinite.f_fin_num. - exact: add_def_funeposneg. over. rewrite [in LHS]integralB //; last 2 first. - apply: Radon_Nikodym_SigmaFinite.integrableM => //. exact: integrable_funepos. - apply: Radon_Nikodym_SigmaFinite.integrableM => //. exact: integrable_funeneg. congr (_ - _) ; rewrite Radon_Nikodym_SigmaFinite.change_of_variables//; apply: measurable_int; first exact: integrable_funepos mf. exact: integrable_funeneg 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