let f be PartFunc of REAL,REAL; for a being Real
for A being non empty Subset of REAL st right_closed_halfline a c= dom f & A = right_closed_halfline a & f is_+infty_improper_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a holds
( f | A is_integrable_on L-Meas & improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) )
let a be Real; for A being non empty Subset of REAL st right_closed_halfline a c= dom f & A = right_closed_halfline a & f is_+infty_improper_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a holds
( f | A is_integrable_on L-Meas & improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) )
let A be non empty Subset of REAL; ( right_closed_halfline a c= dom f & A = right_closed_halfline a & f is_+infty_improper_integrable_on a & abs f is_+infty_ext_Riemann_integrable_on a implies ( f | A is_integrable_on L-Meas & improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) ) )
assume that
A1:
right_closed_halfline a c= dom f
and
A2:
A = right_closed_halfline a
and
A3:
f is_+infty_improper_integrable_on a
and
A4:
abs f is_+infty_ext_Riemann_integrable_on a
; ( f | A is_integrable_on L-Meas & improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) )
A5:
dom (max+ f) = dom f
by RFUNCT_3:def 10;
A6:
f is_+infty_ext_Riemann_integrable_on a
by A1, A3, A4, Th61;
then A7:
max+ f is_+infty_ext_Riemann_integrable_on a
by A1, A4, Th66;
A8:
max+ f is_+infty_improper_integrable_on a
by A1, A4, A6, Th66, INTEGR25:21;
A9:
max+ f is nonnegative
by MESFUNC6:61;
A10:
abs (max+ f) is_+infty_ext_Riemann_integrable_on a
by A7, MESFUNC6:61, LPSPACE2:14;
then
(max+ f) | A is_integrable_on L-Meas
by A1, A5, A2, A8, A9, Th78;
then A11:
max+ (f | A) is_integrable_on L-Meas
by MESFUNC6:66;
max+ (R_EAL (f | A)) = max+ (f | A)
by MESFUNC6:30;
then A12:
max+ (R_EAL (f | A)) = R_EAL (max+ (f | A))
by MESFUNC5:def 7;
then A13:
max+ (R_EAL (f | A)) is_integrable_on L-Meas
by A11, MESFUNC6:def 4;
A14:
dom (max- f) = dom f
by RFUNCT_3:def 11;
A15:
max- f is_+infty_ext_Riemann_integrable_on a
by A1, A4, A6, Th70;
A16:
max- f is_+infty_improper_integrable_on a
by A1, A4, A6, Th70, INTEGR25:21;
A17:
max- f is nonnegative
by MESFUNC6:61;
A18:
abs (max- f) is_+infty_ext_Riemann_integrable_on a
by A15, MESFUNC6:61, LPSPACE2:14;
then
(max- f) | A is_integrable_on L-Meas
by A1, A14, A2, A16, A17, Th78;
then A19:
max- (f | A) is_integrable_on L-Meas
by MESFUNC6:66;
max- (R_EAL (f | A)) = max- (f | A)
by MESFUNC6:30;
then A20:
max- (R_EAL (f | A)) = R_EAL (max- (f | A))
by MESFUNC5:def 7;
then
max- (R_EAL (f | A)) is_integrable_on L-Meas
by A19, MESFUNC6:def 4;
hence
f | A is_integrable_on L-Meas
by A13, MESFUN13:18, MESFUNC6:def 4; improper_integral_+infty (f,a) = Integral (L-Meas,(f | A))
A = [.a,+infty.[
by A2, LIMFUNC1:def 2;
then reconsider A1 = A as Element of L-Field by MEASUR12:72, MEASUR12:75;
R_EAL (f | A) is_integrable_on L-Meas
by A20, A13, A19, MESFUNC6:def 4, MESFUN13:18;
then consider E being Element of L-Field such that
A21:
( E = dom (R_EAL (f | A)) & R_EAL (f | A) is E -measurable )
by MESFUNC5:def 17;
A22:
improper_integral_+infty (f,a) = (improper_integral_+infty ((max+ f),a)) - (improper_integral_+infty ((max- f),a))
by A1, A7, A15, Th74;
A23: improper_integral_+infty ((max+ f),a) =
Integral (L-Meas,((max+ f) | A))
by A1, A5, A2, A8, A10, A9, Th78
.=
Integral (L-Meas,(max+ (f | A)))
by MESFUNC6:66
.=
Integral (L-Meas,(max+ (R_EAL (f | A))))
by A12, MESFUNC6:def 3
;
improper_integral_+infty ((max- f),a) =
Integral (L-Meas,((max- f) | A))
by A1, A14, A2, A16, A18, A17, Th78
.=
Integral (L-Meas,(max- (f | A)))
by MESFUNC6:66
.=
Integral (L-Meas,(max- (R_EAL (f | A))))
by A20, MESFUNC6:def 3
;
then
improper_integral_+infty (f,a) = Integral (L-Meas,(R_EAL (f | A)))
by A21, A22, A23, MESFUN11:54;
hence
improper_integral_+infty (f,a) = Integral (L-Meas,(f | A))
by MESFUNC6:def 3; verum