let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )
let f be PartFunc of X,ExtREAL; ( f is_integrable_on M implies ( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 ) )
A1:
max+ f is nonnegative
by Lm1;
assume A2:
f is_integrable_on M
; ( f " {+infty} in S & f " {-infty} in S & M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )
then A3:
integral+ (M,(max+ f)) < +infty
;
consider A being Element of S such that
A4:
A = dom f
and
A5:
f is A -measurable
by A2;
A6:
for x being object holds
( ( x in eq_dom (f,+infty) implies x in A ) & ( x in eq_dom (f,-infty) implies x in A ) )
by A4, MESFUNC1:def 15;
then A7:
eq_dom (f,+infty) c= A
;
then A8:
A /\ (eq_dom (f,+infty)) = eq_dom (f,+infty)
by XBOOLE_1:28;
A9:
eq_dom (f,-infty) c= A
by A6;
then A10:
A /\ (eq_dom (f,-infty)) = eq_dom (f,-infty)
by XBOOLE_1:28;
A11:
A /\ (eq_dom (f,+infty)) in S
by A4, A5, MESFUNC1:33;
then A12:
f " {+infty} in S
by A8, Th30;
A13:
A /\ (eq_dom (f,-infty)) in S
by A5, MESFUNC1:34;
then reconsider B2 = f " {-infty} as Element of S by A10, Th30;
A14:
f " {-infty} in S
by A13, A10, Th30;
thus
( f " {+infty} in S & f " {-infty} in S )
by A11, A13, A8, A10, Th30; ( M . (f " {+infty}) = 0 & M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )
set C2 = A \ B2;
A15:
integral+ (M,(max- f)) < +infty
by A2;
reconsider B1 = f " {+infty} as Element of S by A11, A8, Th30;
A16:
A = dom (max+ f)
by A4, MESFUNC2:def 2;
then A17:
B1 c= dom (max+ f)
by A7, Th30;
then A18:
B1 = (dom (max+ f)) /\ B1
by XBOOLE_1:28;
A19:
max+ f is A -measurable
by A5, MESFUNC2:25;
then
max+ f is B1 -measurable
by A16, A17, MESFUNC1:30;
then A20:
(max+ f) | B1 is B1 -measurable
by A18, Th42;
set C1 = A \ B1;
A21:
for x being Element of X holds
( ( x in dom ((max+ f) | (B1 \/ (A \ B1))) implies ((max+ f) | (B1 \/ (A \ B1))) . x = (max+ f) . x ) & ( x in dom ((max- f) | (B2 \/ (A \ B2))) implies ((max- f) | (B2 \/ (A \ B2))) . x = (max- f) . x ) )
by FUNCT_1:47;
B1 \/ (A \ B1) = A
by A16, A17, XBOOLE_1:45;
then
dom ((max+ f) | (B1 \/ (A \ B1))) = (dom (max+ f)) /\ (dom (max+ f))
by A16, RELAT_1:61;
then
(max+ f) | (B1 \/ (A \ B1)) = max+ f
by A21, PARTFUN1:5;
then
integral+ (M,(max+ f)) = (integral+ (M,((max+ f) | B1))) + (integral+ (M,((max+ f) | (A \ B1))))
by A1, A16, A19, Th81, XBOOLE_1:106;
then A22:
integral+ (M,((max+ f) | B1)) <= integral+ (M,(max+ f))
by A1, A16, A19, Th80, XXREAL_3:65;
hereby ( M . (f " {-infty}) = 0 & (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )
A23:
for
r being
Real st
0 < r holds
r * (M . B1) <= integral+ (
M,
(max+ f))
proof
defpred S1[
object ]
means $1
in dom ((max+ f) | B1);
let r be
Real;
( 0 < r implies r * (M . B1) <= integral+ (M,(max+ f)) )
deffunc H1(
object )
-> Element of
ExtREAL =
In (
r,
ExtREAL);
A24:
for
x being
object st
S1[
x] holds
H1(
x)
in ExtREAL
;
consider g being
PartFunc of
X,
ExtREAL such that A25:
( ( for
x being
object holds
(
x in dom g iff (
x in X &
S1[
x] ) ) ) & ( for
x being
object st
x in dom g holds
g . x = H1(
x) ) )
from PARTFUN1:sch 3(A24);
assume A26:
0 < r
;
r * (M . B1) <= integral+ (M,(max+ f))
then
for
x being
object st
x in dom g holds
0 <= g . x
by A25;
then A27:
g is
nonnegative
by SUPINF_2:52;
dom ((max+ f) | B1) = (dom (max+ f)) /\ B1
by RELAT_1:61;
then A28:
dom ((max+ f) | B1) = B1
by A17, XBOOLE_1:28;
for
x being
object holds
(
x in dom g iff (
x in X &
x in dom ((max+ f) | B1) ) )
by A25;
then
dom g = X /\ (dom ((max+ f) | B1))
by XBOOLE_0:def 4;
then A29:
dom g = dom ((max+ f) | B1)
by XBOOLE_1:28;
then A30:
integral' (
M,
g)
= r * (M . (dom g))
by A26, A25, A28, Th104;
A31:
for
x being
Element of
X st
x in dom g holds
g . x <= ((max+ f) | B1) . x
proof
let x be
Element of
X;
( x in dom g implies g . x <= ((max+ f) | B1) . x )
assume A32:
x in dom g
;
g . x <= ((max+ f) | B1) . x
then
x in dom f
by A29, A28, FUNCT_1:def 7;
then A33:
x in dom (max+ f)
by MESFUNC2:def 2;
f . x in {+infty}
by A29, A28, A32, FUNCT_1:def 7;
then A34:
f . x = +infty
by TARSKI:def 1;
then
max (
(f . x),
0)
= f . x
by XXREAL_0:def 10;
then
(max+ f) . x = +infty
by A34, A33, MESFUNC2:def 2;
then
((max+ f) | B1) . x = +infty
by A29, A28, A32, FUNCT_1:49;
hence
g . x <= ((max+ f) | B1) . x
by XXREAL_0:4;
verum
end;
dom (chi (B1,X)) = X
by FUNCT_3:def 3;
then A35:
B1 = (dom (chi (B1,X))) /\ B1
by XBOOLE_1:28;
then A36:
(chi (B1,X)) | B1 is
B1 -measurable
by Th42, MESFUNC2:29;
A37:
B1 = dom ((chi (B1,X)) | B1)
by A35, RELAT_1:61;
A38:
for
x being
Element of
X st
x in dom g holds
g . x = (r (#) ((chi (B1,X)) | B1)) . x
proof
let x be
Element of
X;
( x in dom g implies g . x = (r (#) ((chi (B1,X)) | B1)) . x )
assume A39:
x in dom g
;
g . x = (r (#) ((chi (B1,X)) | B1)) . x
then
x in dom ((chi (B1,X)) | B1)
by A29, A28, A35, RELAT_1:61;
then
x in dom (r (#) ((chi (B1,X)) | B1))
by MESFUNC1:def 6;
then A40:
(r (#) ((chi (B1,X)) | B1)) . x =
r * (((chi (B1,X)) | B1) . x)
by MESFUNC1:def 6
.=
r * ((chi (B1,X)) . x)
by A29, A28, A37, A39, FUNCT_1:47
;
(chi (B1,X)) . x = 1
by A29, A28, A39, FUNCT_3:def 3;
then
(r (#) ((chi (B1,X)) | B1)) . x = r
by A40, XXREAL_3:81;
hence
g . x = (r (#) ((chi (B1,X)) | B1)) . x
by A25, A39;
verum
end;
dom g = dom (r (#) ((chi (B1,X)) | B1))
by A29, A28, A37, MESFUNC1:def 6;
then
g = r (#) ((chi (B1,X)) | B1)
by A38, PARTFUN1:5;
then A41:
g is
B1 -measurable
by A37, A36, MESFUNC1:37;
(max+ f) | B1 is
nonnegative
by Lm1, Th15;
then
integral+ (
M,
g)
<= integral+ (
M,
((max+ f) | B1))
by A20, A29, A28, A41, A27, A31, Th85;
then
integral+ (
M,
g)
<= integral+ (
M,
(max+ f))
by A22, XXREAL_0:2;
hence
r * (M . B1) <= integral+ (
M,
(max+ f))
by A25, A29, A28, A27, A30, Lm4, Th77;
verum
end; assume A42:
M . (f " {+infty}) <> 0
;
contradictionthen A43:
0 < M . (f " {+infty})
by A12, Th45;
per cases
( M . B1 = +infty or M . B1 <> +infty )
;
suppose
M . B1 <> +infty
;
contradictionthen reconsider MB =
M . B1 as
Element of
REAL by A43, XXREAL_0:14;
jj * (M . B1) <= integral+ (
M,
(max+ f))
by A23;
then A45:
0 < integral+ (
M,
(max+ f))
by A43;
then reconsider I =
integral+ (
M,
(max+ f)) as
Element of
REAL by A3, XXREAL_0:14;
A46:
((2 * I) / MB) * (M . B1) = ((2 * I) / MB) * MB
;
((2 * I) / MB) * (M . B1) <= integral+ (
M,
(max+ f))
by A43, A23, A45;
then
2
* I <= I
by A42, A46, XCMPLX_1:87;
hence
contradiction
by A45, XREAL_1:155;
verum end;
end;
then reconsider B1 = B1 as measure_zero of M by MEASURE1:def 7;
A47:
max- f is nonnegative
by Lm1;
A48:
A = dom (max- f)
by A4, MESFUNC2:def 3;
then A49:
B2 c= dom (max- f)
by A9, Th30;
then A50:
B2 = (dom (max- f)) /\ B2
by XBOOLE_1:28;
A51:
max- f is A -measurable
by A4, A5, MESFUNC2:26;
then
max- f is B2 -measurable
by A48, A49, MESFUNC1:30;
then A52:
(max- f) | B2 is B2 -measurable
by A50, Th42;
B2 \/ (A \ B2) = A
by A48, A49, XBOOLE_1:45;
then
dom ((max- f) | (B2 \/ (A \ B2))) = (dom (max- f)) /\ (dom (max- f))
by A48, RELAT_1:61;
then
(max- f) | (B2 \/ (A \ B2)) = max- f
by A21, PARTFUN1:5;
then
integral+ (M,(max- f)) = (integral+ (M,((max- f) | B2))) + (integral+ (M,((max- f) | (A \ B2))))
by A47, A48, A51, Th81, XBOOLE_1:106;
then A53:
integral+ (M,((max- f) | B2)) <= integral+ (M,(max- f))
by A47, A48, A51, Th80, XXREAL_3:65;
hereby ( (f " {+infty}) \/ (f " {-infty}) in S & M . ((f " {+infty}) \/ (f " {-infty})) = 0 )
A55:
for
r being
Real st
0 < r holds
r * (M . B2) <= integral+ (
M,
(max- f))
proof
defpred S1[
object ]
means $1
in dom ((max- f) | B2);
let r be
Real;
( 0 < r implies r * (M . B2) <= integral+ (M,(max- f)) )
deffunc H1(
object )
-> Element of
ExtREAL =
In (
r,
ExtREAL);
A56:
for
x being
object st
S1[
x] holds
H1(
x)
in ExtREAL
;
consider g being
PartFunc of
X,
ExtREAL such that A57:
( ( for
x being
object holds
(
x in dom g iff (
x in X &
S1[
x] ) ) ) & ( for
x being
object st
x in dom g holds
g . x = H1(
x) ) )
from PARTFUN1:sch 3(A56);
assume A58:
0 < r
;
r * (M . B2) <= integral+ (M,(max- f))
then
for
x being
object st
x in dom g holds
0 <= g . x
by A57;
then A59:
g is
nonnegative
by SUPINF_2:52;
dom ((max- f) | B2) = (dom (max- f)) /\ B2
by RELAT_1:61;
then A60:
dom ((max- f) | B2) = B2
by A49, XBOOLE_1:28;
for
x being
object holds
(
x in dom g iff (
x in X &
x in dom ((max- f) | B2) ) )
by A57;
then
dom g = X /\ (dom ((max- f) | B2))
by XBOOLE_0:def 4;
then A61:
dom g = dom ((max- f) | B2)
by XBOOLE_1:28;
then A62:
integral' (
M,
g)
= r * (M . (dom g))
by A58, A57, A60, Th104;
dom (chi (B2,X)) = X
by FUNCT_3:def 3;
then A63:
B2 = (dom (chi (B2,X))) /\ B2
by XBOOLE_1:28;
then A64:
B2 = dom ((chi (B2,X)) | B2)
by RELAT_1:61;
A65:
for
x being
Element of
X st
x in dom g holds
g . x = (r (#) ((chi (B2,X)) | B2)) . x
proof
let x be
Element of
X;
( x in dom g implies g . x = (r (#) ((chi (B2,X)) | B2)) . x )
assume A66:
x in dom g
;
g . x = (r (#) ((chi (B2,X)) | B2)) . x
then
x in dom (r (#) ((chi (B2,X)) | B2))
by A61, A60, A64, MESFUNC1:def 6;
then A67:
(r (#) ((chi (B2,X)) | B2)) . x =
r * (((chi (B2,X)) | B2) . x)
by MESFUNC1:def 6
.=
r * ((chi (B2,X)) . x)
by A61, A60, A64, A66, FUNCT_1:47
;
(chi (B2,X)) . x = 1
by A61, A60, A66, FUNCT_3:def 3;
then
(r (#) ((chi (B2,X)) | B2)) . x = r
by A67, XXREAL_3:81;
hence
g . x = (r (#) ((chi (B2,X)) | B2)) . x
by A57, A66;
verum
end;
A68:
for
x being
Element of
X st
x in dom g holds
g . x <= ((max- f) | B2) . x
proof
let x be
Element of
X;
( x in dom g implies g . x <= ((max- f) | B2) . x )
assume A69:
x in dom g
;
g . x <= ((max- f) | B2) . x
then
x in dom f
by A61, A60, FUNCT_1:def 7;
then A70:
x in dom (max- f)
by MESFUNC2:def 3;
f . x in {-infty}
by A61, A60, A69, FUNCT_1:def 7;
then A71:
- (f . x) = +infty
by TARSKI:def 1, XXREAL_3:5;
then
max (
(- (f . x)),
0)
= - (f . x)
by XXREAL_0:def 10;
then
(max- f) . x = +infty
by A71, A70, MESFUNC2:def 3;
then
((max- f) | B2) . x = +infty
by A61, A60, A69, FUNCT_1:49;
hence
g . x <= ((max- f) | B2) . x
by XXREAL_0:4;
verum
end;
A72:
(chi (B2,X)) | B2 is
B2 -measurable
by A63, Th42, MESFUNC2:29;
dom g = dom (r (#) ((chi (B2,X)) | B2))
by A61, A60, A64, MESFUNC1:def 6;
then
g = r (#) ((chi (B2,X)) | B2)
by A65, PARTFUN1:5;
then A73:
g is
B2 -measurable
by A64, A72, MESFUNC1:37;
(max- f) | B2 is
nonnegative
by Lm1, Th15;
then
integral+ (
M,
g)
<= integral+ (
M,
((max- f) | B2))
by A52, A61, A60, A73, A59, A68, Th85;
then
integral+ (
M,
g)
<= integral+ (
M,
(max- f))
by A53, XXREAL_0:2;
hence
r * (M . B2) <= integral+ (
M,
(max- f))
by A57, A61, A60, A59, A62, Lm4, Th77;
verum
end; assume A74:
M . (f " {-infty}) <> 0
;
contradictionA75:
0 <= M . (f " {-infty})
by A14, Th45;
per cases
( M . B2 = +infty or M . B2 <> +infty )
;
suppose
M . B2 <> +infty
;
contradictionthen reconsider MB =
M . B2 as
Element of
REAL by A75, XXREAL_0:14;
jj * (M . B2) <= integral+ (
M,
(max- f))
by A55;
then A77:
0 < integral+ (
M,
(max- f))
by A74, A75;
then reconsider I =
integral+ (
M,
(max- f)) as
Element of
REAL by A15, XXREAL_0:14;
A78:
((2 * I) / MB) * (M . B2) = ((2 * I) / MB) * MB
;
((2 * I) / MB) * (M . B2) <= integral+ (
M,
(max- f))
by A74, A75, A55, A77;
then
2
* I <= I
by A74, A78, XCMPLX_1:87;
hence
contradiction
by A77, XREAL_1:155;
verum end;
end;
thus
(f " {+infty}) \/ (f " {-infty}) in S
by A12, A14, PROB_1:3; M . ((f " {+infty}) \/ (f " {-infty})) = 0
thus M . ((f " {+infty}) \/ (f " {-infty})) =
M . (B1 \/ B2)
.=
0
by A54, MEASURE1:38
; verum