let f be PartFunc of REAL,REAL; for b being Real
for A being non empty Subset of REAL st left_closed_halfline b c= dom f & A = left_closed_halfline b & f is_-infty_improper_integrable_on b & abs f is_-infty_ext_Riemann_integrable_on b holds
( f | A is_integrable_on L-Meas & improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) )
let b be Real; for A being non empty Subset of REAL st left_closed_halfline b c= dom f & A = left_closed_halfline b & f is_-infty_improper_integrable_on b & abs f is_-infty_ext_Riemann_integrable_on b holds
( f | A is_integrable_on L-Meas & improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) )
let A be non empty Subset of REAL; ( left_closed_halfline b c= dom f & A = left_closed_halfline b & f is_-infty_improper_integrable_on b & abs f is_-infty_ext_Riemann_integrable_on b implies ( f | A is_integrable_on L-Meas & improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) ) )
assume that
A1:
left_closed_halfline b c= dom f
and
A2:
A = left_closed_halfline b
and
A3:
f is_-infty_improper_integrable_on b
and
A4:
abs f is_-infty_ext_Riemann_integrable_on b
; ( f | A is_integrable_on L-Meas & improper_integral_-infty (f,b) = Integral (L-Meas,(f | A)) )
A5:
dom (max+ f) = dom f
by RFUNCT_3:def 10;
A6:
f is_-infty_ext_Riemann_integrable_on b
by A1, A3, A4, Th60;
then A7:
max+ f is_-infty_improper_integrable_on b
by A1, A4, Th65, INTEGR25:20;
A8:
max+ f is_-infty_ext_Riemann_integrable_on b
by A6, A1, A4, Th65;
then A9:
abs (max+ f) is_-infty_ext_Riemann_integrable_on b
by MESFUNC6:61, LPSPACE2:14;
A10:
max+ f is nonnegative
by MESFUNC6:61;
then
(max+ f) | A is_integrable_on L-Meas
by A1, A5, A2, A7, A9, Th77;
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_improper_integrable_on b
by A1, A4, A6, Th69, INTEGR25:20;
A16:
max- f is_-infty_ext_Riemann_integrable_on b
by A1, A4, A6, Th69;
then A17:
abs (max- f) is_-infty_ext_Riemann_integrable_on b
by MESFUNC6:61, LPSPACE2:14;
A18:
max- f is nonnegative
by MESFUNC6:61;
then
(max- f) | A is_integrable_on L-Meas
by A1, A14, A2, A15, A17, Th77;
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 A21:
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,b) = Integral (L-Meas,(f | A))
A = ].-infty,b.]
by A2, LIMFUNC1:def 1;
then reconsider A1 = A as Element of L-Field by MEASUR12:72, MEASUR12:75;
R_EAL (f | A) is_integrable_on L-Meas
by A21, A12, A11, MESFUNC6:def 4, MESFUN13:18;
then consider E being Element of L-Field such that
A22:
( E = dom (R_EAL (f | A)) & R_EAL (f | A) is E -measurable )
by MESFUNC5:def 17;
A23:
improper_integral_-infty (f,b) = (improper_integral_-infty ((max+ f),b)) - (improper_integral_-infty ((max- f),b))
by A1, A8, A16, Th73;
A24: improper_integral_-infty ((max+ f),b) =
Integral (L-Meas,((max+ f) | A))
by A1, A5, A2, A7, A9, A10, Th77
.=
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),b) =
Integral (L-Meas,((max- f) | A))
by A1, A14, A2, A15, A17, A18, Th77
.=
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,b) = Integral (L-Meas,(R_EAL (f | A)))
by A22, A23, A24, MESFUN11:54;
hence
improper_integral_-infty (f,b) = Integral (L-Meas,(f | A))
by MESFUNC6:def 3; verum