proposition: Lemma measurable_fun_einfs D (f : (T -> \bar R)^nat) : (forall n, measurable_fun D (f n)) -> forall n, measurable_fun D (fun x => einfs (f ^~ x) n).
proof: Proof. move=> mf n mD. apply: (measurability (ErealGenCInfty.measurableE R)) => //. move=> _ [_ [x ->] <-]; rewrite einfs_preimage -bigcapIr; last by exists n => /=. by apply: bigcap_measurable => ? ?; exact/mf/emeasurable_itv. 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