proposition: Lemma approximation_sfun : exists g : {sfun T >-> R}^nat, (forall x, D x -> EFin \o g^~ x @ \oo --> f x).
proof: Proof. have [fp_ [fp_nd fp_cvg]] := approximation mD (measurable_funepos mf) (fun=> ltac:(by [])). have [fn_ [fn_nd fn_cvg]] := approximation mD (measurable_funeneg mf) (fun=> ltac:(by [])). exists (fun n => [the {sfun T >-> R} of fp_ n \+ cst (-1) \* fn_ n]) => x /=. rewrite [X in X @ \oo --> _](_ : _ = EFin \o fp_^~ x \+ (-%E \o EFin \o fn_^~ x))%E; last first. by apply/funext => n/=; rewrite EFinD mulN1r. by move=> Dx; rewrite (funeposneg f); apply: cvgeD; [exact: add_def_funeposneg|apply: fp_cvg|apply:cvgeN; exact: fn_cvg]. 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