proposition: Lemma integral_pushforward (f : Y -> \bar R) : measurable_fun setT f -> (forall y, 0 <= f y) -> \int[pushforward mu mphi]_y f y = \int[mu]_x (f \o phi) x.
proof: Proof. move=> mf f0. have [f_ [ndf_ f_f]] := approximation measurableT mf (fun t _ => f0 t). transitivity (limn (fun n => \int[pushforward mu mphi]_x (f_ n x)%:E)). rewrite -monotone_convergence//. - by apply: eq_integral => y _; apply/esym/cvg_lim => //; exact: f_f. - by move=> n; exact/EFin_measurable_fun. - by move=> n y _; rewrite lee_fin. - by move=> y _ m n mn; rewrite lee_fin; apply/lefP/ndf_. rewrite (_ : (fun _ => _) = (fun n => \int[mu]_x (EFin \o f_ n \o phi) x)). rewrite -monotone_convergence//; last 3 first. - by move=> n /=; apply: measurableT_comp => //; exact: measurableT_comp. - by move=> n x _ /=; rewrite lee_fin. - by move=> x _ m n mn; rewrite lee_fin; exact/lefP/ndf_. by apply: eq_integral => x _ /=; apply/cvg_lim => //; exact: f_f. apply/funext => n. have mfnphi r : measurable (f_ n @^-1` [set r] \o phi). rewrite -[_ \o _]/(phi @^-1` (f_ n @^-1` [set r])) -(setTI (_ @^-1` _)). exact/mphi. transitivity (\sum_(k \in range (f_ n)) \int[mu]_x (k * \1_((f_ n @^-1` [set k]) \o phi) x)%:E). under eq_integral do rewrite fimfunE -fsumEFin//. rewrite ge0_integral_fsum//; last 2 first. - by move=> y; apply/EFin_measurable_fun; exact: measurable_funM. - by move=> y x _; rewrite nnfun_muleindic_ge0. apply: eq_fsbigr => r _; rewrite integralZl_indic_nnsfun// integral_indic//=. rewrite (integralZl_indic _ (fun r => f_ n @^-1` [set r] \o phi))//. by congr (_ * _); rewrite [RHS](@integral_indic). by move=> r0; rewrite preimage_nnfun0. rewrite -ge0_integral_fsum//; last 2 first. - by move=> r; apply/EFin_measurable_fun; exact: measurable_funM. - by move=> r x _; rewrite nnfun_muleindic_ge0. by apply: eq_integral => x _; rewrite fsumEFin// -fimfunE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun