let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being Element of S st f is_simple_func_in S & f is nonnegative & A misses B holds
integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being Element of S st f is_simple_func_in S & f is nonnegative & A misses B holds
integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for A, B being Element of S st f is_simple_func_in S & f is nonnegative & A misses B holds
integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))
let f be PartFunc of X,ExtREAL ; :: thesis: for A, B being Element of S st f is_simple_func_in S & f is nonnegative & A misses B holds
integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))
let A, B be Element of S; :: thesis: ( f is_simple_func_in S & f is nonnegative & A misses B implies integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B)) )
assume that
A1:
f is_simple_func_in S
and
A2:
f is nonnegative
and
A3:
A misses B
; :: thesis: integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))
set g = f | (A \/ B);
set g1 = f | A;
set g2 = f | B;
A4:
f | (A \/ B) is_simple_func_in S
by A1, Th40;
f | (A \/ B) is nonnegative
by A2, Th21;
then A5:
for x being set st x in dom (f | (A \/ B)) holds
0 <= (f | (A \/ B)) . x
by SUPINF_2:70;
then consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that
A6:
( G,b are_Re-presentation_of f | (A \/ B) & b . 1 = 0 & ( for n being Nat st 2 <= n & n in dom b holds
( 0 < b . n & b . n < +infty ) ) )
by A1, Th40, MESFUNC3:14;
deffunc H1( Nat) -> Element of ExtREAL = (b . $1) * ((M * G) . $1);
consider y being FinSequence of ExtREAL such that
A7:
( len y = len G & ( for j being Nat st j in dom y holds
y . j = H1(j) ) )
from FINSEQ_2:sch 1();
A8: dom y =
Seg (len y)
by FINSEQ_1:def 3
.=
dom G
by A7, FINSEQ_1:def 3
;
deffunc H2( Nat) -> Element of bool X = (G . $1) /\ A;
consider G1 being FinSequence such that
A11:
( len G1 = len G & ( for k being Nat st k in dom G1 holds
G1 . k = H2(k) ) )
from FINSEQ_1:sch 2();
A12:
dom G1 = Seg (len G)
by A11, FINSEQ_1:def 3;
A13: dom G =
Seg (len G1)
by A11, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
A14:
for k being Nat st k in dom G holds
G1 . k = (G . k) /\ A
then reconsider G1 = G1 as Finite_Sep_Sequence of S by A13, Th41;
A15: dom ((f | (A \/ B)) | A) =
(dom (f | (A \/ B))) /\ A
by RELAT_1:90
.=
((dom f) /\ (A \/ B)) /\ A
by RELAT_1:90
.=
(dom f) /\ ((A \/ B) /\ A)
by XBOOLE_1:16
.=
(dom f) /\ A
by XBOOLE_1:21
.=
dom (f | A)
by RELAT_1:90
;
for x being set st x in dom ((f | (A \/ B)) | A) holds
((f | (A \/ B)) | A) . x = (f | A) . x
then
(f | (A \/ B)) | A = f | A
by A15, FUNCT_1:9;
then A18:
G1,b are_Re-presentation_of f | A
by A6, A13, A14, Th42;
deffunc H3( Nat) -> Element of bool X = (G . $1) /\ B;
consider G2 being FinSequence such that
A19:
( len G2 = len G & ( for k being Nat st k in dom G2 holds
G2 . k = H3(k) ) )
from FINSEQ_1:sch 2();
A20:
dom G2 = Seg (len G)
by A19, FINSEQ_1:def 3;
A21: dom G =
Seg (len G2)
by A19, FINSEQ_1:def 3
.=
dom G2
by FINSEQ_1:def 3
;
A22:
for k being Nat st k in dom G holds
G2 . k = (G . k) /\ B
then reconsider G2 = G2 as Finite_Sep_Sequence of S by A21, Th41;
A23: dom ((f | (A \/ B)) | B) =
(dom (f | (A \/ B))) /\ B
by RELAT_1:90
.=
((dom f) /\ (A \/ B)) /\ B
by RELAT_1:90
.=
(dom f) /\ ((A \/ B) /\ B)
by XBOOLE_1:16
.=
(dom f) /\ B
by XBOOLE_1:21
.=
dom (f | B)
by RELAT_1:90
;
for x being set st x in dom ((f | (A \/ B)) | B) holds
((f | (A \/ B)) | B) . x = (f | B) . x
then
(f | (A \/ B)) | B = f | B
by A23, FUNCT_1:9;
then A26:
G2,b are_Re-presentation_of f | B
by A6, A21, A22, Th42;
per cases
( dom (f | (A \/ B)) = {} or dom (f | (A \/ B)) <> {} )
;
suppose A30:
dom (f | (A \/ B)) <> {}
;
:: thesis: integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))
integral X,
S,
M,
(f | (A \/ B)) = Sum y
by A4, A5, A6, A8, A30, A7, MESFUNC4:3;
then A31:
integral' M,
(f | (A \/ B)) = Sum y
by A30, Def14;
per cases
( dom (f | A) = {} or dom (f | A) <> {} )
;
suppose A36:
dom (f | A) <> {}
;
:: thesis: integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))per cases
( dom (f | B) = {} or dom (f | B) <> {} )
;
suppose A41:
dom (f | B) <> {}
;
:: thesis: integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))
f | A is
nonnegative
by A2, Th21;
then A42:
for
x being
set st
x in dom (f | A) holds
0 <= (f | A) . x
by SUPINF_2:70;
f | B is
nonnegative
by A2, Th21;
then A43:
for
x being
set st
x in dom (f | B) holds
0 <= (f | B) . x
by SUPINF_2:70;
deffunc H4(
Nat)
-> Element of
ExtREAL =
(b . $1) * ((M * G1) . $1);
consider y1 being
FinSequence of
ExtREAL such that A44:
(
len y1 = len G1 & ( for
j being
Nat st
j in dom y1 holds
y1 . j = H4(
j) ) )
from FINSEQ_2:sch 1();
A45:
dom y1 =
Seg (len G1)
by A44, FINSEQ_1:def 3
.=
dom G1
by FINSEQ_1:def 3
;
integral X,
S,
M,
(f | A) = Sum y1
by A1, Th40, A18, A36, A42, A45, A44, MESFUNC4:3;
then A46:
integral' M,
(f | A) = Sum y1
by A36, Def14;
deffunc H5(
Nat)
-> Element of
ExtREAL =
(b . $1) * ((M * G2) . $1);
consider y2 being
FinSequence of
ExtREAL such that A47:
(
len y2 = len G2 & ( for
j being
Nat st
j in dom y2 holds
y2 . j = H5(
j) ) )
from FINSEQ_2:sch 1();
A48:
dom y2 =
Seg (len G2)
by A47, FINSEQ_1:def 3
.=
dom G2
by FINSEQ_1:def 3
;
integral X,
S,
M,
(f | B) = Sum y2
by A1, Th40, A26, A41, A43, A48, A47, MESFUNC4:3;
then A49:
integral' M,
(f | B) = Sum y2
by A41, Def14;
A50:
for
k being
Nat st
k in dom y1 holds
0 <= y1 . k
proof
let k be
Nat;
:: thesis: ( k in dom y1 implies 0 <= y1 . k )
assume A51:
k in dom y1
;
:: thesis: 0 <= y1 . k
A52:
y1 . k = (b . k) * ((M * G1) . k)
by A44, A51;
A53:
dom b =
dom G
by A6, MESFUNC3:def 1
.=
Seg (len y1)
by A11, A44, FINSEQ_1:def 3
.=
dom y1
by FINSEQ_1:def 3
;
k in Seg (len y1)
by A51, FINSEQ_1:def 3;
then A54:
( 1
<= k &
k <= len y1 )
by FINSEQ_1:3;
k in Seg (len G1)
by A44, A51, FINSEQ_1:def 3;
then A56:
k in dom G1
by FINSEQ_1:def 3;
then A57:
(M * G1) . k = M . (G1 . k)
by FUNCT_1:23;
(
G1 . k in rng G1 &
rng G1 c= S )
by A56, FUNCT_1:12;
then reconsider G1k =
G1 . k as
Element of
S ;
0 <= M . G1k
by SUPINF_2:58;
hence
0 <= y1 . k
by A52, A55, A57;
:: thesis: verum
end; A58:
for
k being
Nat st
k in dom y2 holds
0 <= y2 . k
proof
let k be
Nat;
:: thesis: ( k in dom y2 implies 0 <= y2 . k )
assume A59:
k in dom y2
;
:: thesis: 0 <= y2 . k
A60:
y2 . k = (b . k) * ((M * G2) . k)
by A47, A59;
A61:
dom b =
dom G
by A6, MESFUNC3:def 1
.=
Seg (len y2)
by A19, A47, FINSEQ_1:def 3
.=
dom y2
by FINSEQ_1:def 3
;
k in Seg (len y2)
by A59, FINSEQ_1:def 3;
then A62:
( 1
<= k &
k <= len y2 )
by FINSEQ_1:3;
k in Seg (len G2)
by A47, A59, FINSEQ_1:def 3;
then A64:
k in dom G2
by FINSEQ_1:def 3;
then A65:
(M * G2) . k = M . (G2 . k)
by FUNCT_1:23;
(
G2 . k in rng G2 &
rng G2 c= S )
by A64, FUNCT_1:12;
then reconsider G2k =
G2 . k as
Element of
S ;
0 <= M . G2k
by SUPINF_2:58;
hence
0 <= y2 . k
by A60, A63, A65;
:: thesis: verum
end; A66:
dom y1 =
Seg (len y2)
by A11, A19, A44, A47, FINSEQ_1:def 3
.=
dom y2
by FINSEQ_1:def 3
;
y = y1 + y2
proof
A67:
for
x being
set st
x in dom y1 holds
not
y1 . x in {-infty }
for
x being
set holds not
x in y1 " {-infty }
then A69:
y1 " {-infty } = {}
by XBOOLE_0:def 1;
A70:
for
x being
set st
x in dom y2 holds
not
y2 . x in {-infty }
for
x being
set holds not
x in y2 " {-infty }
then A72:
y2 " {-infty } = {}
by XBOOLE_0:def 1;
A73:
dom y =
(Seg (len G)) /\ (Seg (len G))
by A8, FINSEQ_1:def 3
.=
(dom y1) /\ (Seg (len G2))
by A11, A19, A44, FINSEQ_1:def 3
.=
(dom y1) /\ (dom y2)
by A47, FINSEQ_1:def 3
;
then A74:
dom y = ((dom y1) /\ (dom y2)) \ (((y1 " {-infty }) /\ (y2 " {+infty })) \/ ((y1 " {+infty }) /\ (y2 " {-infty })))
by A69, A72;
for
n being
Element of
NAT st
n in dom y holds
y . n = (y1 . n) + (y2 . n)
proof
let n be
Element of
NAT ;
:: thesis: ( n in dom y implies y . n = (y1 . n) + (y2 . n) )
assume A75:
n in dom y
;
:: thesis: y . n = (y1 . n) + (y2 . n)
then
n in Seg (len G)
by A7, FINSEQ_1:def 3;
then A76:
n in dom G
by FINSEQ_1:def 3;
A77:
(
n in dom y1 &
n in dom y2 )
by A73, A75, XBOOLE_0:def 4;
then
(
n in Seg (len G1) &
n in Seg (len G2) )
by A44, A47, FINSEQ_1:def 3;
then A78:
(
n in dom G1 &
n in dom G2 )
by FINSEQ_1:def 3;
A79:
G2 . n = (G . n) /\ B
by A22, A76;
then
G . n c= A \/ B
by TARSKI:def 3;
then A81:
G . n =
(G . n) /\ (A \/ B)
by XBOOLE_1:28
.=
((G . n) /\ A) \/ ((G . n) /\ B)
by XBOOLE_1:23
.=
(G1 . n) \/ (G2 . n)
by A14, A76, A79
;
(
G1 . n in rng G1 &
rng G1 c= S )
by A78, FUNCT_1:12;
then reconsider G1n =
G1 . n as
Element of
S ;
(
G2 . n in rng G2 &
rng G2 c= S )
by A78, FUNCT_1:12;
then reconsider G2n =
G2 . n as
Element of
S ;
A84:
(M * G) . n =
M . (G . n)
by A76, FUNCT_1:23
.=
(M . G1n) + (M . G2n)
by A81, A82, MEASURE1:61
.=
((M * G1) . n) + (M . (G2 . n))
by A78, FUNCT_1:23
.=
((M * G1) . n) + ((M * G2) . n)
by A78, FUNCT_1:23
;
(
0 <= M . G1n &
0 <= M . G2n )
by MEASURE1:def 4;
then
( (
0 = (M * G1) . n or
0 < (M * G1) . n ) & (
0 = (M * G2) . n or
0 < (M * G2) . n ) )
by A78, FUNCT_1:23;
then
(b . n) * ((M * G) . n) = ((b . n) * ((M * G1) . n)) + ((b . n) * ((M * G2) . n))
by A84, XXREAL_3:107;
then
y . n = ((b . n) * ((M * G1) . n)) + ((b . n) * ((M * G2) . n))
by A7, A75;
then
y . n = (y1 . n) + ((b . n) * ((M * G2) . n))
by A44, A77;
hence
y . n = (y1 . n) + (y2 . n)
by A47, A77;
:: thesis: verum
end;
hence
y = y1 + y2
by A74, MESFUNC1:def 3;
:: thesis: verum
end; hence
integral' M,
(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))
by A31, A46, A49, A50, A58, A66, MESFUNC4:1;
:: thesis: verum end; end;