proposition: Lemma measurable_fun_cvg D (h : (T -> R)^nat) f : (forall m, measurable_fun D (h m)) -> (forall x, D x -> h ^~ x @ \oo --> f x) -> measurable_fun D f.
proof: Proof. move=> mf_ f_f; have fE x : D x -> f x = limn_sup (h ^~ x). move=> Dx; have /cvg_lim <-// := @cvg_sups _ (h ^~ x) (f x) (f_f _ Dx). apply: (@eq_measurable_fun _ _ _ _ D (fun x => limn_sup (h ^~ x))). by move=> x; rewrite inE => Dx; rewrite -fE. apply: (@measurable_fun_limn_sup _ h) => // t Dt. - by apply/bounded_fun_has_ubound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f. - by apply/bounded_fun_has_lbound/cvg_seq_bounded/cvg_ex; eexists; exact: f_f. 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