proposition: Lemma change_of_variables f E : (forall x, 0 <= f x) -> measurable E -> measurable_fun E f -> \int[mu]_(x in E) (f x * ('d nu '/d mu) x) = \int[nu]_(x in E) f x.
proof: Proof. move=> f0 mE mf; set g := 'd nu '/d mu. have [h [ndh hf]] := approximation mE mf (fun x _ => f0 x). have -> : \int[nu]_(x in E) f x = lim (\int[nu]_(x in E) (EFin \o h n) x @[n --> \oo]). have fE x : E x -> f x = lim ((EFin \o h n) x @[n --> \oo]). by move=> Ex; apply/esym/cvg_lim => //; exact: hf. under eq_integral => x /[!inE] /fE -> //. apply: monotone_convergence => //. - move=> n; apply/EFin_measurable_fun. by apply: (measurable_funS measurableT) => //; exact/measurable_funP. - by move=> n x Ex //=; rewrite lee_fin. - by move=> x Ex a b /ndh /=; rewrite lee_fin => /lefP. have -> : \int[mu]_(x in E) (f \* g) x = lim (\int[mu]_(x in E) ((EFin \o h n) \* g) x @[n --> \oo]). have fg x :E x -> f x * g x = lim (((EFin \o h n) \* g) x @[n --> \oo]). by move=> Ex; apply/esym/cvg_lim => //; apply: cvgeMr; [exact: f_fin_num|exact: hf]. under eq_integral => x /[!inE] /fg -> //. apply: monotone_convergence => [//| | |]. - move=> n; apply/emeasurable_funM; apply/measurable_funTS. exact/EFin_measurable_fun. exact: measurable_int (f_integrable _). - by move=> n x Ex //=; rewrite mule_ge0 ?lee_fin//=; exact: f_ge0. - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin// f_ge0. suff suf n : \int[mu]_(x in E) ((EFin \o h n) x * g x) = \int[nu]_(x in E) (EFin \o h n) x. by under eq_fun do rewrite suf. transitivity (\int[nu]_(x in E) (\sum_(y \in range (h n)) (y * \1_(h n @^-1` [set y]) x)%:E)); last first. by apply: eq_integral => t tE; rewrite /= fimfunE -fsumEFin. have indich m r : measurable_fun E (fun x => (r * \1_(h m @^-1` [set r]) x)%:E). by apply: (measurable_comp measurableT) => //; exact: measurable_funM. rewrite ge0_integral_fsum//; last by move=> m y Ey; exact: nnfun_muleindic_ge0. transitivity (\int[mu]_(x in E) (\sum_(y \in range (h n)) (y * \1_(h n @^-1` [set y]) x)%:E * g x)). under [RHS]eq_integral => x xE. rewrite -ge0_mule_fsuml => [|y]; last exact: nnfun_muleindic_ge0. rewrite fsumEFin // -(fimfunE _ x); over. by []. rewrite ge0_integral_fsum//; last 2 first. - move=> y; apply: emeasurable_funM => //; apply: measurable_funTS. exact: measurable_int (f_integrable _). - by move=> m y Ey; rewrite mule_ge0 ?f_ge0// nnfun_muleindic_ge0. apply: eq_fsbigr => r rhn. under [RHS]eq_integral do rewrite EFinM. rewrite integralZl_indic_nnsfun => //. under eq_integral do rewrite EFinM -muleA. rewrite ge0_integralZl//. - under eq_integral do rewrite muleC. by rewrite -integral_setI_indic// -f_integral// integral_indic// setIC. - apply: emeasurable_funM; first exact/EFin_measurable_fun. exact/measurable_funTS/(measurable_int (f_integrable _)). - by move=> t Et; rewrite mule_ge0// ?lee_fin//; exact: f_ge0. - by move: rhn; rewrite inE => -[t _ <-]; rewrite lee_fin. 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