let f be PartFunc of REAL,REAL; for a, b being Real
for A being non empty Subset of REAL st [.a,b.[ c= dom f & A = [.a,b.[ & f is_right_improper_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b holds
( f | A is_integrable_on L-Meas & right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )
let a, b be Real; for A being non empty Subset of REAL st [.a,b.[ c= dom f & A = [.a,b.[ & f is_right_improper_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b holds
( f | A is_integrable_on L-Meas & right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )
let A be non empty Subset of REAL; ( [.a,b.[ c= dom f & A = [.a,b.[ & f is_right_improper_integrable_on a,b & abs f is_right_ext_Riemann_integrable_on a,b implies ( f | A is_integrable_on L-Meas & right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) ) )
assume that
A1:
[.a,b.[ c= dom f
and
A2:
A = [.a,b.[
and
A3:
f is_right_improper_integrable_on a,b
and
A4:
abs f is_right_ext_Riemann_integrable_on a,b
; ( f | A is_integrable_on L-Meas & right_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )
A5:
dom (max+ f) = dom f
by RFUNCT_3:def 10;
a < b
by A2, XXREAL_1:27;
then A6:
f is_right_ext_Riemann_integrable_on a,b
by A1, A3, A4, Th57;
then A7:
max+ f is_right_ext_Riemann_integrable_on a,b
by A1, A2, A4, Th64, XXREAL_1:27;
then A8:
max+ f is_right_improper_integrable_on a,b
by INTEGR24:33;
A9:
abs (max+ f) is_right_ext_Riemann_integrable_on a,b
by A7, LPSPACE2:14, MESFUNC6:61;
A10:
(max+ f) | A is nonnegative
by MESFUNC6:61, MESFUNC6:55;
then
(max+ f) | A is_integrable_on L-Meas
by A1, A5, A2, A8, A9, Th76;
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_right_ext_Riemann_integrable_on a,b
by A1, A2, A4, A6, Th68, XXREAL_1:27;
then A16:
max- f is_right_improper_integrable_on a,b
by INTEGR24:33;
A17:
abs (max- f) is_right_ext_Riemann_integrable_on a,b
by A15, LPSPACE2:14, MESFUNC6:61;
A18:
(max- f) | A is nonnegative
by MESFUNC6:61, MESFUNC6:55;
then
(max- f) | A is_integrable_on L-Meas
by A1, A14, A2, A16, A17, Th76;
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; right_improper_integral (f,a,b) = Integral (L-Meas,(f | A))
reconsider A1 = A as Element of L-Field by A2, 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:
right_improper_integral (f,a,b) = (right_improper_integral ((max+ f),a,b)) - (right_improper_integral ((max- f),a,b))
by A1, A7, A15, Th72;
A23: right_improper_integral ((max+ f),a,b) =
Integral (L-Meas,((max+ f) | A))
by A1, A5, A2, A8, A9, A10, Th76
.=
Integral (L-Meas,(max+ (f | A)))
by MESFUNC6:66
.=
Integral (L-Meas,(max+ (R_EAL (f | A))))
by A12, MESFUNC6:def 3
;
right_improper_integral ((max- f),a,b) =
Integral (L-Meas,((max- f) | A))
by A1, A14, A2, A16, A17, A18, Th76
.=
Integral (L-Meas,(max- (f | A)))
by MESFUNC6:66
.=
Integral (L-Meas,(max- (R_EAL (f | A))))
by A20, MESFUNC6:def 3
;
then
right_improper_integral (f,a,b) = Integral (L-Meas,(R_EAL (f | A)))
by A21, A22, A23, MESFUN11:54;
hence
right_improper_integral (f,a,b) = Integral (L-Meas,(f | A))
by MESFUNC6:def 3; verum