proposition: Lemma ge0_integral_mscale (mf : measurable_fun D f) : (forall x, D x -> 0 <= f x) -> \int[mscale k m]_(x in D) f x = k%:num%:E * \int[m]_(x in D) f x.
proof: Proof. move=> f0; have [f_ [ndf_ f_f]] := approximation mD mf f0. transitivity (limn (fun n => \int[mscale k m]_(x in D) (f_ n x)%:E)). rewrite -monotone_convergence//=. - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //=; exact: f_f. - by move=> n; exact/EFin_measurable_fun/measurable_funTS. - by move=> n x _; rewrite lee_fin. - by move=> x _ a b /ndf_ /lefP; rewrite lee_fin. rewrite (_ : \int[m]_(x in D) _ = limn (fun n => \int[m]_(x in D) (f_ n x)%:E)); last first. rewrite -monotone_convergence//=. - by apply: eq_integral => x /[!inE] xD; apply/esym/cvg_lim => //; exact: f_f. - by move=> n; exact/EFin_measurable_fun/measurable_funTS. - by move=> n x _; rewrite lee_fin. - by move=> x _ a b /ndf_ /lefP; rewrite lee_fin. rewrite -limeMl//. by congr (limn _); apply/funext => n /=; rewrite integral_mscale_nnsfun. apply/ereal_nondecreasing_is_cvgn => a b ab; apply: ge0_le_integral => //. - by move=> x _; rewrite lee_fin. - exact/EFin_measurable_fun/measurable_funTS. - by move=> x _; rewrite lee_fin. - exact/EFin_measurable_fun/measurable_funTS. - by move=> x _; rewrite lee_fin; move/ndf_ : ab => /lefP. 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