proposition: Lemma measurable_abse (D : set (\bar R)) : measurable_fun D abse.
proof: Proof. move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //. move=> /= _ [_ [x ->] <-]. rewrite [X in _ @^-1` X](punct_eitv_bndy _ x) preimage_setU setIUr. apply: measurableU; last first. by rewrite preimage_abse_pinfty; apply: measurableI => //; exact: measurableU. apply: measurableI => //; exists (normr @^-1` `]x, +oo[%classic). rewrite -[X in measurable X]setTI. by apply: measurable_normr => //; exact: measurable_itv. exists set0; first by constructor. rewrite setU0 predeqE => -[y| |]; split => /= => -[r]; rewrite ?/= /= ?in_itv /= ?andbT => xr//. + by move=> [ry]; exists `|y| => //=; rewrite in_itv/= andbT -ry. + by move=> [ry]; exists y => //=; rewrite /= in_itv/= andbT -ry. 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