proposition: Lemma emeasurable_fun_cvg D (f_ : (T -> \bar R)^nat) (f : T -> \bar R) : (forall m, measurable_fun D (f_ m)) -> (forall x, D x -> f_ ^~ x @ \oo --> f x) -> measurable_fun D f.
proof: Proof. move=> mf_ f_f; have fE x : D x -> f x = limn_esup (f_^~ x). rewrite limn_esup_lim. by move=> Dx; have /cvg_lim <-// := @cvg_esups _ (f_^~x) (f x) (f_f x Dx). apply: (eq_measurable_fun (fun x => limn_esup (f_ ^~ x))) => //. by move=> x; rewrite inE => Dx; rewrite fE. exact: measurable_fun_limn_esup. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure