proposition: Lemma integral_funepos_lt_pinfty f : mu_int f -> \int[mu]_(x in D) f^\+ x < +oo.
proof: Proof. move=> /integrableP[mf]; apply: le_lt_trans; apply: ge0_le_integral => //. - exact: measurable_funepos. - exact: measurableT_comp. - move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0. rewrite lee0_abs// /funepos. by move: (fx0) => /max_idPr ->; rewrite -leeNr oppe0. by rewrite gee0_abs// /funepos; move: (fx0) => /max_idPl ->. 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