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_improper_integrable_on a,b & f | A is nonnegative holds
( improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ) implies Integral (L-Meas,(f | A)) = +infty ) )
let a, b be Real; for A being non empty Subset of REAL st ].a,b.[ c= dom f & A = ].a,b.[ & f is_improper_integrable_on a,b & f | A is nonnegative holds
( improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ) implies Integral (L-Meas,(f | A)) = +infty ) )
let A be non empty Subset of REAL; ( ].a,b.[ c= dom f & A = ].a,b.[ & f is_improper_integrable_on a,b & f | A is nonnegative implies ( improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ) implies Integral (L-Meas,(f | A)) = +infty ) ) )
assume that
A1:
].a,b.[ c= dom f
and
A2:
A = ].a,b.[
and
A3:
f is_improper_integrable_on a,b
and
A4:
f | A is nonnegative
; ( improper_integral (f,a,b) = Integral (L-Meas,(f | A)) & ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ) implies Integral (L-Meas,(f | A)) = +infty ) )
consider c being Real such that
A5:
( a < c & c < b )
and
A6:
f is_left_improper_integrable_on a,c
and
A7:
f is_right_improper_integrable_on c,b
and
A8:
( not left_improper_integral (f,a,c) = -infty or not right_improper_integral (f,c,b) = +infty )
and
A9:
( not left_improper_integral (f,a,c) = +infty or not right_improper_integral (f,c,b) = -infty )
by A3, INTEGR24:def 5;
reconsider L = ].a,c.] as non empty Subset of REAL by A5, XXREAL_1:32;
reconsider L1 = L as Element of L-Field by MEASUR10:5, MEASUR12:75;
reconsider R = [.c,b.[ as non empty Subset of REAL by A5, XXREAL_1:31;
reconsider R1 = R as Element of L-Field by MEASUR10:5, MEASUR12:75;
( L c= ].a,b.[ & R c= ].a,b.[ )
by A5, XXREAL_1:48, XXREAL_1:49;
then A10:
( L c= dom f & R c= dom f )
by A1;
then A11:
( f is L1 -measurable & f is R1 -measurable )
by A6, A7, Th33, Th34;
then A12:
f is L1 \/ R1 -measurable
by MESFUNC6:17;
(f | A) | L is nonnegative
by A4, MESFUNC6:55;
then A13:
f | L is nonnegative
by A2, A5, XXREAL_1:49, RELAT_1:74;
then A14:
left_improper_integral (f,a,c) = Integral (L-Meas,(f | L))
by A6, A10, Th43;
(f | A) | R is nonnegative
by A4, MESFUNC6:55;
then A15:
f | R is nonnegative
by A2, A5, XXREAL_1:48, RELAT_1:74;
then A16:
right_improper_integral (f,c,b) = Integral (L-Meas,(f | R))
by A7, A10, Th41;
reconsider R2 = ].c,b.[ as Element of L-Field by MEASUR10:5, MEASUR12:75;
reconsider C = {c} as Element of L-Field by Th28;
C = [.c,c.]
by XXREAL_1:17;
then A17:
L-Meas . C = c - c
by MESFUN14:5;
set fLR = f | (L1 \/ R1);
A18:
( L1 \/ R1 = ].a,b.[ & L1 \/ R2 = ].a,b.[ )
by A5, XXREAL_1:172, XXREAL_1:171;
then A19:
L1 \/ R1 = dom (f | (L1 \/ R1))
by A1, RELAT_1:62;
then
L1 \/ R1 = (dom f) /\ (L1 \/ R1)
by RELAT_1:61;
then A20:
f | (L1 \/ R1) is L1 \/ R1 -measurable
by A12, MESFUNC6:76;
A21:
( L1 c= L1 \/ R1 & R1 c= L1 \/ R1 )
by XBOOLE_1:7;
R2 c= R1
by XXREAL_1:45;
then A22:
R2 c= L1 \/ R1
by A21;
A23:
f | (L1 \/ R1) is nonnegative
by A2, A4, A5, XXREAL_1:172;
R2 = R1 \ C
by A5, XXREAL_1:136;
then A24:
(f | R1) | (R1 \ C) = f | R2
by XXREAL_1:45, RELAT_1:74;
A25:
R1 = dom (f | R1)
by A10, RELAT_1:62;
then
R1 = (dom f) /\ R1
by RELAT_1:61;
then A26:
Integral (L-Meas,(f | R2)) = Integral (L-Meas,(f | R1))
by A24, A17, A25, A11, MESFUNC6:76, MESFUNC6:89;
Integral (L-Meas,((f | (L1 \/ R1)) | (L1 \/ R2))) = (Integral (L-Meas,((f | (L1 \/ R1)) | L1))) + (Integral (L-Meas,((f | (L1 \/ R1)) | R2)))
by A19, A20, A23, XXREAL_1:91, MESFUNC6:85;
then A27: Integral (L-Meas,(f | (L1 \/ R1))) =
(Integral (L-Meas,(f | L1))) + (Integral (L-Meas,((f | (L1 \/ R1)) | R2)))
by A18, XBOOLE_1:7, RELAT_1:74
.=
(Integral (L-Meas,(f | L1))) + (Integral (L-Meas,(f | R2)))
by A22, RELAT_1:74
;
hence
improper_integral (f,a,b) = Integral (L-Meas,(f | A))
by A1, A3, A5, A14, A16, A26, A18, A2, INTEGR24:48; ( ( ex c being Real st
( a < c & c < b & f is_left_ext_Riemann_integrable_on a,c & f is_right_ext_Riemann_integrable_on c,b ) implies f | A is_integrable_on L-Meas ) & ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ) implies Integral (L-Meas,(f | A)) = +infty ) )
hereby ( ( for c being Real st a < c & c < b & f is_left_ext_Riemann_integrable_on a,c holds
not f is_right_ext_Riemann_integrable_on c,b ) implies Integral (L-Meas,(f | A)) = +infty )
assume
ex
c being
Real st
(
a < c &
c < b &
f is_left_ext_Riemann_integrable_on a,
c &
f is_right_ext_Riemann_integrable_on c,
b )
;
f | A is_integrable_on L-Meas then consider c being
Real such that A28:
(
a < c &
c < b )
and A29:
f is_left_ext_Riemann_integrable_on a,
c
and A30:
f is_right_ext_Riemann_integrable_on c,
b
;
A31:
f is_left_improper_integrable_on a,
c
by A29, INTEGR24:32;
A32:
f is_right_improper_integrable_on c,
b
by A30, INTEGR24:33;
reconsider L1 =
].a,c.] as
Element of
L-Field by MEASUR10:5, MEASUR12:75;
reconsider R1 =
[.c,b.[ as
Element of
L-Field by MEASUR10:5, MEASUR12:75;
A33:
L1 \/ R1 = A
by A2, A28, XXREAL_1:172;
A34:
dom (f | A) = A
by A1, A2, RELAT_1:62;
then A35:
dom (R_EAL (f | A)) = L1 \/ R1
by A33, MESFUNC5:def 7;
A36:
L1 \/ R1 = (dom f) /\ (L1 \/ R1)
by A33, A34, RELAT_1:61;
A37:
f | A is
L1 \/ R1 -measurable
by A1, A3, A33, A2, Th35, A36, MESFUNC6:76;
then A38:
R_EAL (f | A) is
L1 \/ R1 -measurable
by MESFUNC6:def 1;
A39:
not
L1 is
empty
by A28, XXREAL_1:32;
L1 c= ].a,b.[
by A28, XXREAL_1:49;
then A40:
L1 c= dom f
by A1;
then A41:
L1 = dom (f | L1)
by RELAT_1:62;
then A42:
L1 = (dom f) /\ L1
by RELAT_1:61;
A43:
dom (R_EAL (f | L1)) = L1
by A41, MESFUNC5:def 7;
f is
L1 -measurable
by A40, Th34, A29, INTEGR24:32;
then A44:
R_EAL (f | L1) is
L1 -measurable
by A42, MESFUNC6:def 1, MESFUNC6:76;
(f | A) | L1 is
nonnegative
by A4, MESFUNC6:55;
then
f | L1 is
nonnegative
by A2, A28, XXREAL_1:49, RELAT_1:74;
then
f | L1 is_integrable_on L-Meas
by A39, A40, A29, A31, Th43;
then
R_EAL (f | L1) is_integrable_on L-Meas
by MESFUNC6:def 4;
then A45:
(
integral+ (
L-Meas,
(max+ (R_EAL (f | L1))))
< +infty &
integral+ (
L-Meas,
(max- (R_EAL (f | L1))))
< +infty )
by MESFUNC5:def 17;
A46:
not
R1 is
empty
by A28, XXREAL_1:31;
R1 c= ].a,b.[
by A28, XXREAL_1:48;
then A47:
R1 c= dom f
by A1;
then A48:
R1 = dom (f | R1)
by RELAT_1:62;
then A49:
R1 = (dom f) /\ R1
by RELAT_1:61;
A50:
dom (R_EAL (f | R1)) = R1
by A48, MESFUNC5:def 7;
f is
R1 -measurable
by A47, Th33, A30, INTEGR24:33;
then A51:
R_EAL (f | R1) is
R1 -measurable
by A49, MESFUNC6:def 1, MESFUNC6:76;
(f | A) | R1 is
nonnegative
by A4, MESFUNC6:55;
then
f | R1 is
nonnegative
by A2, A28, XXREAL_1:48, RELAT_1:74;
then
f | R1 is_integrable_on L-Meas
by A46, A47, A30, A32, Th41;
then A52:
R_EAL (f | R1) is_integrable_on L-Meas
by MESFUNC6:def 4;
then A53:
(
integral+ (
L-Meas,
(max+ (R_EAL (f | R1))))
< +infty &
integral+ (
L-Meas,
(max- (R_EAL (f | R1))))
< +infty )
by MESFUNC5:def 17;
set R2 =
].c,b.[;
reconsider R2 =
].c,b.[ as
Element of
L-Field by MEASUR10:5, MEASUR12:75;
set C =
{c};
A54:
{c} = [.c,c.]
by XXREAL_1:17;
reconsider C =
{c} as
Element of
L-Field by Th28;
A55:
L-Meas . C =
c - c
by A54, MESFUN14:5
.=
0
;
A56:
dom (f | R1) = R1
by A47, RELAT_1:62;
then A57:
dom (R_EAL (f | R1)) = R1
by MESFUNC5:def 7;
ex
E being
Element of
L-Field st
(
E = dom (R_EAL (f | R1)) &
R_EAL (f | R1) is
E -measurable )
by A52, MESFUNC5:def 17;
then A58:
(
max+ (f | R1) is
R1 -measurable &
max- (f | R1) is
R1 -measurable )
by A56, A57, MESFUNC6:def 1, MESFUNC6:46, MESFUNC6:47;
A59:
(
dom (max+ (f | R1)) = R1 &
dom (max- (f | R1)) = R1 )
by A56, RFUNCT_3:def 10, RFUNCT_3:def 11;
A60:
R2 = R1 \ C
by A28, XXREAL_1:136;
(f | R1) | (R1 \ C) = f | R2
by A60, XBOOLE_1:36, RELAT_1:74;
then A61:
(
(max+ (f | R1)) | (R1 \ C) = max+ (f | R2) &
(max- (f | R1)) | (R1 \ C) = max- (f | R2) )
by RFUNCT_3:44, RFUNCT_3:45;
A62:
(
max+ (R_EAL (f | A)) = max+ (f | A) &
max- (R_EAL (f | A)) = max- (f | A) &
max+ (R_EAL (f | L1)) = max+ (f | L1) &
max- (R_EAL (f | L1)) = max- (f | L1) &
max+ (R_EAL (f | R1)) = max+ (f | R1) &
max- (R_EAL (f | R1)) = max- (f | R1) )
by MESFUNC6:30;
A63:
(
dom (max+ (R_EAL (f | A))) = L1 \/ R1 &
dom (max- (R_EAL (f | A))) = L1 \/ R1 )
by A35, MESFUNC2:def 2, MESFUNC2:def 3;
A64:
(
max+ (R_EAL (f | A)) is
L1 \/ R1 -measurable &
max- (R_EAL (f | A)) is
L1 \/ R1 -measurable )
by A35, A37, MESFUNC2:25, MESFUNC2:26, MESFUNC6:def 1;
A65:
integral+ (
L-Meas,
(max+ (R_EAL (f | A)))) =
Integral (
L-Meas,
(max+ (R_EAL (f | A))))
by A63, A64, MESFUNC5:88, MESFUN11:5
.=
Integral (
L-Meas,
(R_EAL (max+ (f | A))))
by A62, MESFUNC5:def 7
.=
Integral (
L-Meas,
(max+ (f | A)))
by MESFUNC6:def 3
;
A66:
integral+ (
L-Meas,
(max- (R_EAL (f | A)))) =
Integral (
L-Meas,
(max- (R_EAL (f | A))))
by A63, A64, MESFUNC5:88, MESFUN11:5
.=
Integral (
L-Meas,
(R_EAL (max- (f | A))))
by A62, MESFUNC5:def 7
.=
Integral (
L-Meas,
(max- (f | A)))
by MESFUNC6:def 3
;
A67:
(
dom (max+ (R_EAL (f | L1))) = L1 &
dom (max- (R_EAL (f | L1))) = L1 )
by A43, MESFUNC2:def 2, MESFUNC2:def 3;
A68:
(
max+ (R_EAL (f | L1)) is
L1 -measurable &
max- (R_EAL (f | L1)) is
L1 -measurable )
by A43, A44, MESFUNC2:25, MESFUNC2:26;
A69:
integral+ (
L-Meas,
(max+ (R_EAL (f | L1)))) =
Integral (
L-Meas,
(max+ (R_EAL (f | L1))))
by A67, A68, MESFUNC5:88, MESFUN11:5
.=
Integral (
L-Meas,
(R_EAL (max+ (f | L1))))
by A62, MESFUNC5:def 7
.=
Integral (
L-Meas,
(max+ (f | L1)))
by MESFUNC6:def 3
;
A70:
integral+ (
L-Meas,
(max- (R_EAL (f | L1)))) =
Integral (
L-Meas,
(max- (R_EAL (f | L1))))
by A67, A68, MESFUNC5:88, MESFUN11:5
.=
Integral (
L-Meas,
(R_EAL (max- (f | L1))))
by A62, MESFUNC5:def 7
.=
Integral (
L-Meas,
(max- (f | L1)))
by MESFUNC6:def 3
;
A71:
(
dom (max+ (R_EAL (f | R1))) = R1 &
dom (max- (R_EAL (f | R1))) = R1 )
by A50, MESFUNC2:def 2, MESFUNC2:def 3;
A72:
(
max+ (R_EAL (f | R1)) is
R1 -measurable &
max- (R_EAL (f | R1)) is
R1 -measurable )
by A50, A51, MESFUNC2:25, MESFUNC2:26;
A73:
integral+ (
L-Meas,
(max+ (R_EAL (f | R1)))) =
Integral (
L-Meas,
(max+ (R_EAL (f | R1))))
by A71, A72, MESFUNC5:88, MESFUN11:5
.=
Integral (
L-Meas,
(R_EAL (max+ (f | R1))))
by A62, MESFUNC5:def 7
.=
Integral (
L-Meas,
(max+ (f | R1)))
by MESFUNC6:def 3
;
A74:
integral+ (
L-Meas,
(max- (R_EAL (f | R1)))) =
Integral (
L-Meas,
(max- (R_EAL (f | R1))))
by A71, A72, MESFUNC5:88, MESFUN11:5
.=
Integral (
L-Meas,
(R_EAL (max- (f | R1))))
by A62, MESFUNC5:def 7
.=
Integral (
L-Meas,
(max- (f | R1)))
by MESFUNC6:def 3
;
A75:
(
dom (max+ (f | A)) = A &
dom (max- (f | A)) = A )
by A34, RFUNCT_3:def 10, RFUNCT_3:def 11;
A76:
(
max+ (f | A) is
L1 \/ R1 -measurable &
max- (f | A) is
L1 \/ R1 -measurable )
by A33, A34, A37, MESFUNC6:46, MESFUNC6:47;
A77:
(
max+ (f | A) is
nonnegative &
max- (f | A) is
nonnegative )
by MESFUNC6:61;
A78:
(
A = L1 \/ R1 &
A = L1 \/ R2 )
by A2, A28, XXREAL_1:172, XXREAL_1:171;
A79:
(max+ (f | A)) | L1 =
max+ ((f | A) | L1)
by RFUNCT_3:44
.=
max+ (f | L1)
by A78, XBOOLE_1:7, RELAT_1:74
;
A80:
(max- (f | A)) | L1 =
max- ((f | A) | L1)
by RFUNCT_3:45
.=
max- (f | L1)
by A78, XBOOLE_1:7, RELAT_1:74
;
A81:
(max+ (f | A)) | R2 =
max+ ((f | A) | R2)
by RFUNCT_3:44
.=
max+ (f | R2)
by A78, XBOOLE_1:7, RELAT_1:74
;
A82:
(max- (f | A)) | R2 =
max- ((f | A) | R2)
by RFUNCT_3:45
.=
max- (f | R2)
by A78, XBOOLE_1:7, RELAT_1:74
;
Integral (
L-Meas,
(max+ (f | A))) =
Integral (
L-Meas,
((max+ (f | A)) | A))
by A75
.=
(Integral (L-Meas,((max+ (f | A)) | L1))) + (Integral (L-Meas,((max+ (f | A)) | R2)))
by A75, A76, A77, A78, XXREAL_1:91, MESFUNC6:85
.=
(Integral (L-Meas,(max+ (f | L1)))) + (Integral (L-Meas,(max+ (f | R1))))
by A79, A81, A61, A58, A59, A55, MESFUNC6:89
;
then A83:
integral+ (
L-Meas,
(max+ (R_EAL (f | A))))
< +infty
by A45, A53, A65, A69, A73, XXREAL_3:16, XXREAL_0:4;
Integral (
L-Meas,
(max- (f | A))) =
Integral (
L-Meas,
((max- (f | A)) | A))
by A75
.=
(Integral (L-Meas,((max- (f | A)) | L1))) + (Integral (L-Meas,((max- (f | A)) | R2)))
by A75, A76, A77, A78, XXREAL_1:91, MESFUNC6:85
.=
(Integral (L-Meas,(max- (f | L1)))) + (Integral (L-Meas,(max- (f | R1))))
by A80, A82, A61, A58, A59, A55, MESFUNC6:89
;
then
integral+ (
L-Meas,
(max- (R_EAL (f | A))))
< +infty
by A45, A53, A66, A70, A74, XXREAL_3:16, XXREAL_0:4;
hence
f | A is_integrable_on L-Meas
by A35, A38, A83, MESFUNC5:def 17, MESFUNC6:def 4;
verum
end;
hereby verum
assume A84:
for
c being
Real st
a < c &
c < b &
f is_left_ext_Riemann_integrable_on a,
c holds
not
f is_right_ext_Riemann_integrable_on c,
b
;
Integral (L-Meas,(f | A)) = +infty per cases
( not f is_left_ext_Riemann_integrable_on a,c or not f is_right_ext_Riemann_integrable_on c,b )
by A84, A5;
suppose
not
f is_left_ext_Riemann_integrable_on a,
c
;
Integral (L-Meas,(f | A)) = +infty then
Integral (
L-Meas,
(f | L))
= +infty
by A10, A6, A13, Th43;
hence
Integral (
L-Meas,
(f | A))
= +infty
by A9, A13, A6, A10, Th43, A16, A26, A27, A18, A2, XXREAL_3:def 2;
verum end; suppose
not
f is_right_ext_Riemann_integrable_on c,
b
;
Integral (L-Meas,(f | A)) = +infty then
Integral (
L-Meas,
(f | R))
= +infty
by A10, A7, A15, Th41;
hence
Integral (
L-Meas,
(f | A))
= +infty
by A8, A15, A7, A10, Th41, A14, A26, A27, A18, A2, XXREAL_3:def 2;
verum end;
end;