proposition: Lemma measurable_fun_limn_sup D (h : (T -> R)^nat) : (forall t, D t -> has_ubound (range (h ^~ t))) -> (forall t, D t -> has_lbound (range (h ^~ t))) -> (forall n, measurable_fun D (h n)) -> measurable_fun D (fun x => limn_sup (h ^~ x)).
proof: Proof. move=> f_ub f_lb mf. have : {in D, (fun x => inf [set sups (h ^~ x) n | n in [set n | 0 <= n]%N]) =1 (fun x => limn_sup (h^~ x))}. move=> t; rewrite inE => Dt; apply/esym/cvg_lim => //. rewrite [X in _ --> X](_ : _ = inf (range (sups (h^~t)))). by apply: cvg_sups_inf; [exact: f_ub|exact: f_lb]. by congr (inf [set _ | _ in _]); rewrite predeqE. move/eq_measurable_fun; apply; apply: measurable_fun_infs => //. move=> t Dt; have [M hM] := f_lb _ Dt; exists M => _ [m /= nm <-]. rewrite (@le_trans _ _ (h m t)) //; first by apply hM => /=; exists m. by apply: sup_ub; [exact/has_ubound_sdrop/f_ub|exists m => /=]. by move=> k; exact: measurable_fun_sups. 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