let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) holds
Integral (M,f) = Sum x
let S be SigmaField of X; for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) holds
Integral (M,f) = Sum x
let M be sigma_Measure of S; for E being Element of S
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) holds
Integral (M,f) = Sum x
let E be Element of S; for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) holds
Integral (M,f) = Sum x
let f be PartFunc of X,ExtREAL; for F being Finite_Sep_Sequence of S
for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) holds
Integral (M,f) = Sum x
let F be Finite_Sep_Sequence of S; for a, x being FinSequence of ExtREAL st f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) holds
Integral (M,f) = Sum x
let a, x be FinSequence of ExtREAL ; ( f is_simple_func_in S & E = dom f & M . E < +infty & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i) ) implies Integral (M,f) = Sum x )
assume that
A1:
f is_simple_func_in S
and
A2:
E = dom f
and
A3:
M . E < +infty
and
A4:
F,a are_Re-presentation_of f
and
A5:
dom x = dom F
and
A6:
for i being Nat st i in dom x holds
x . i = (a . i) * ((M * F) . i)
; Integral (M,f) = Sum x
A7:
( max+ f is_simple_func_in S & max- f is_simple_func_in S )
by A1, Th4;
A8:
( max+ f is nonnegative & max- f is nonnegative )
by MESFUN11:5;
defpred S1[ Nat, ExtReal] means for x being object st x in F . $1 holds
$2 = max ((f . x),0);
A9:
dom a = dom F
by A4, MESFUNC3:def 1;
( dom (max+ f) = dom f & dom (max- f) = dom f )
by MESFUNC2:def 2, MESFUNC2:def 3;
then A10:
( dom (max+ f) = union (rng F) & dom (max- f) = union (rng F) )
by A4, MESFUNC3:def 1;
A11:
for k being Nat st k in Seg (len a) holds
ex y being Element of ExtREAL st S1[k,y]
proof
let k be
Nat;
( k in Seg (len a) implies ex y being Element of ExtREAL st S1[k,y] )
assume
k in Seg (len a)
;
ex y being Element of ExtREAL st S1[k,y]
then A12:
k in dom a
by FINSEQ_1:def 3;
per cases
( F . k = {} or F . k <> {} )
;
suppose
F . k <> {}
;
ex y being Element of ExtREAL st S1[k,y]then consider p being
object such that A15:
p in F . k
by XBOOLE_0:def 1;
A16:
max (
(f . p),
0) is
Element of
ExtREAL
by XXREAL_0:def 1;
for
x being
object st
x in F . k holds
max (
(f . p),
0)
= max (
(f . x),
0)
proof
let x be
object ;
( x in F . k implies max ((f . p),0) = max ((f . x),0) )
assume
x in F . k
;
max ((f . p),0) = max ((f . x),0)
then
(
f . x = a . k &
f . p = a . k )
by A4, A15, A9, A12, MESFUNC3:def 1;
hence
max (
(f . p),
0)
= max (
(f . x),
0)
;
verum
end; hence
ex
y being
Element of
ExtREAL st
S1[
k,
y]
by A16;
verum end; end;
end;
consider a1 being FinSequence of ExtREAL such that
A17:
dom a1 = Seg (len a)
and
A18:
for k being Nat st k in Seg (len a) holds
S1[k,a1 . k]
from FINSEQ_1:sch 5(A11);
A19:
dom a1 = dom a
by A17, FINSEQ_1:def 3;
A20:
for k being Nat st k in dom F holds
for x being object st x in F . k holds
(max+ f) . x = a1 . k
proof
let k be
Nat;
( k in dom F implies for x being object st x in F . k holds
(max+ f) . x = a1 . k )
assume A21:
k in dom F
;
for x being object st x in F . k holds
(max+ f) . x = a1 . k
let x be
object ;
( x in F . k implies (max+ f) . x = a1 . k )
assume A22:
x in F . k
;
(max+ f) . x = a1 . k
F . k in rng F
by A21, FUNCT_1:3;
then
x in union (rng F)
by A22, TARSKI:def 4;
then
x in dom f
by A4, MESFUNC3:def 1;
then A23:
x in dom (max+ f)
by MESFUNC2:def 2;
a1 . k = max (
(f . x),
0)
by A22, A21, A9, A19, A17, A18;
hence
(max+ f) . x = a1 . k
by A23, MESFUNC2:def 2;
verum
end;
then A24:
F,a1 are_Re-presentation_of max+ f
by A10, A9, A19, MESFUNC3:def 1;
defpred S2[ Nat, ExtReal] means $2 = (a1 . $1) * ((M * F) . $1);
A25:
for k being Nat st k in Seg (len F) holds
ex y being Element of ExtREAL st S2[k,y]
;
consider x1 being FinSequence of ExtREAL such that
A26:
( dom x1 = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S2[k,x1 . k] ) )
from FINSEQ_1:sch 5(A25);
A27:
dom x1 = dom F
by A26, FINSEQ_1:def 3;
A28:
dom F = Seg (len F)
by FINSEQ_1:def 3;
now for q being object st q in rng x1 holds
q in REAL let q be
object ;
( q in rng x1 implies b1 in REAL )assume
q in rng x1
;
b1 in REAL then consider p being
Element of
NAT such that A29:
(
p in dom x1 &
q = x1 . p )
by PARTFUN1:3;
A30:
q = (a1 . p) * ((M * F) . p)
by A26, A29;
per cases
( a1 . p is Real or F . p = {} )
by A1, A24, A29, A27, Th4, Th12;
suppose A31:
a1 . p is
Real
;
b1 in REAL
F . p c= union (rng F)
by A29, A27, FUNCT_1:3, ZFMISC_1:74;
then
F . p c= E
by A2, A4, MESFUNC3:def 1;
then
(
0 <= M . (F . p) &
M . (F . p) <= M . E )
by SUPINF_2:51, MEASURE1:31;
then
(
0 <= (M * F) . p &
(M * F) . p <= M . E )
by A29, A27, FUNCT_1:13;
then
(M * F) . p in REAL
by A3, XXREAL_0:14;
hence
q in REAL
by A30, A31, XREAL_0:def 1;
verum end; end; end;
then
rng x1 c= REAL
;
then reconsider rx1 = x1 as FinSequence of REAL by FINSEQ_1:def 4;
A32:
Sum rx1 = Sum x1
by MESFUNC3:2;
integral' (M,(max+ f)) = Sum x1
proof
per cases
( dom (max+ f) = {} or dom (max+ f) <> {} )
;
suppose A35:
dom (max+ f) <> {}
;
integral' (M,(max+ f)) = Sum x1then
integral (
M,
(max+ f))
= Sum x1
by A7, A10, A9, A19, A20, A26, A28, A8, MESFUNC3:def 1, MESFUNC4:3;
hence
integral' (
M,
(max+ f))
= Sum x1
by A35, MESFUNC5:def 14;
verum end; end;
end;
then A36:
Integral (M,(max+ f)) = Sum rx1
by A7, A8, A32, MESFUNC5:89;
defpred S3[ Nat, ExtReal] means for x being object st x in F . $1 holds
$2 = max ((- (f . x)),0);
A37:
for k being Nat st k in Seg (len a) holds
ex y being Element of ExtREAL st S3[k,y]
proof
let k be
Nat;
( k in Seg (len a) implies ex y being Element of ExtREAL st S3[k,y] )
assume
k in Seg (len a)
;
ex y being Element of ExtREAL st S3[k,y]
then A38:
k in dom a
by FINSEQ_1:def 3;
per cases
( F . k = {} or F . k <> {} )
;
suppose
F . k <> {}
;
ex y being Element of ExtREAL st S3[k,y]then consider p being
object such that A41:
p in F . k
by XBOOLE_0:def 1;
A42:
max (
(- (f . p)),
0) is
Element of
ExtREAL
by XXREAL_0:def 1;
for
x being
object st
x in F . k holds
max (
(- (f . p)),
0)
= max (
(- (f . x)),
0)
proof
let x be
object ;
( x in F . k implies max ((- (f . p)),0) = max ((- (f . x)),0) )
assume
x in F . k
;
max ((- (f . p)),0) = max ((- (f . x)),0)
then
(
f . x = a . k &
f . p = a . k )
by A9, A38, A41, A4, MESFUNC3:def 1;
hence
max (
(- (f . p)),
0)
= max (
(- (f . x)),
0)
;
verum
end; hence
ex
y being
Element of
ExtREAL st
S3[
k,
y]
by A42;
verum end; end;
end;
consider a2 being FinSequence of ExtREAL such that
A43:
dom a2 = Seg (len a)
and
A44:
for k being Nat st k in Seg (len a) holds
S3[k,a2 . k]
from FINSEQ_1:sch 5(A37);
A45:
dom a2 = dom a
by A43, FINSEQ_1:def 3;
A46:
for k being Nat st k in dom F holds
for x being object st x in F . k holds
(max- f) . x = a2 . k
proof
let k be
Nat;
( k in dom F implies for x being object st x in F . k holds
(max- f) . x = a2 . k )
assume A47:
k in dom F
;
for x being object st x in F . k holds
(max- f) . x = a2 . k
let x be
object ;
( x in F . k implies (max- f) . x = a2 . k )
assume A48:
x in F . k
;
(max- f) . x = a2 . k
F . k in rng F
by A47, FUNCT_1:3;
then
x in union (rng F)
by A48, TARSKI:def 4;
then
x in dom f
by A4, MESFUNC3:def 1;
then A49:
x in dom (max- f)
by MESFUNC2:def 3;
a2 . k = max (
(- (f . x)),
0)
by A48, A47, A9, A45, A43, A44;
hence
(max- f) . x = a2 . k
by A49, MESFUNC2:def 3;
verum
end;
A50:
F,a2 are_Re-presentation_of max- f
by A10, A9, A45, A46, MESFUNC3:def 1;
defpred S4[ Nat, ExtReal] means $2 = (a2 . $1) * ((M * F) . $1);
A51:
for k being Nat st k in Seg (len F) holds
ex y being Element of ExtREAL st S4[k,y]
;
consider x2 being FinSequence of ExtREAL such that
A52:
( dom x2 = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S4[k,x2 . k] ) )
from FINSEQ_1:sch 5(A51);
A53:
dom x2 = dom F
by A52, FINSEQ_1:def 3;
A54:
dom F = Seg (len F)
by FINSEQ_1:def 3;
now for q being object st q in rng x2 holds
q in REAL let q be
object ;
( q in rng x2 implies b1 in REAL )assume
q in rng x2
;
b1 in REAL then consider p being
Element of
NAT such that A55:
(
p in dom x2 &
q = x2 . p )
by PARTFUN1:3;
reconsider p =
p as
Nat ;
A56:
q = (a2 . p) * ((M * F) . p)
by A55, A52;
per cases
( a2 . p is Real or F . p = {} )
by A1, A50, A55, A53, Th4, Th12;
suppose A57:
a2 . p is
Real
;
b1 in REAL
F . p c= union (rng F)
by A55, A53, FUNCT_1:3, ZFMISC_1:74;
then
F . p c= E
by A2, A4, MESFUNC3:def 1;
then
(
0 <= M . (F . p) &
M . (F . p) <= M . E )
by SUPINF_2:51, MEASURE1:31;
then
(
0 <= (M * F) . p &
(M * F) . p <= M . E )
by A55, A53, FUNCT_1:13;
then
(M * F) . p in REAL
by A3, XXREAL_0:14;
hence
q in REAL
by A56, A57, XREAL_0:def 1;
verum end; end; end;
then
rng x2 c= REAL
;
then reconsider rx2 = x2 as FinSequence of REAL by FINSEQ_1:def 4;
A58:
Sum rx2 = Sum x2
by MESFUNC3:2;
integral' (M,(max- f)) = Sum x2
proof
per cases
( dom (max- f) = {} or dom (max- f) <> {} )
;
suppose A61:
dom (max- f) <> {}
;
integral' (M,(max- f)) = Sum x2then
integral (
M,
(max- f))
= Sum x2
by A7, A52, A54, A8, A10, A9, A45, A46, MESFUNC3:def 1, MESFUNC4:3;
hence
integral' (
M,
(max- f))
= Sum x2
by A61, MESFUNC5:def 14;
verum end; end;
end;
then A62:
Integral (M,(max- f)) = Sum rx2
by A7, A8, A58, MESFUNC5:89;
A63:
( len rx1 = len F & len rx2 = len F )
by A26, A52, FINSEQ_1:def 3;
Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))
by A1, A2, MESFUNC2:34, MESFUN11:54;
then
Integral (M,f) = (Sum rx1) - (Sum rx2)
by A36, A62, Lm1;
then A64:
Integral (M,f) = Sum (rx1 - rx2)
by A63, INTEGRA5:2;
len (rx1 - rx2) = len rx1
by A63, INTEGRA5:2;
then A65:
dom (rx1 - rx2) = dom x
by A5, A27, FINSEQ_3:29;
for k being object st k in dom x holds
x . k = (rx1 - rx2) . k
proof
let k be
object ;
( k in dom x implies x . k = (rx1 - rx2) . k )
assume A66:
k in dom x
;
x . k = (rx1 - rx2) . k
then reconsider k1 =
k as
Nat ;
A67:
x . k = (a . k1) * ((M * F) . k1)
by A6, A66;
A68:
(rx1 - rx2) . k = (rx1 . k1) - (rx2 . k1)
by A65, A66, VALUED_1:13;
A69:
(
rx1 . k1 = (a1 . k1) * ((M * F) . k1) &
rx2 . k1 = (a2 . k1) * ((M * F) . k1) )
by A5, A26, A28, A52, A66;
per cases
( F . k1 = {} or F . k1 <> {} )
;
suppose A70:
F . k1 <> {}
;
x . k = (rx1 - rx2) . kthen consider p being
object such that A71:
p in F . k1
by XBOOLE_0:def 1;
F . k1 in rng F
by A5, A66, FUNCT_1:3;
then
p in union (rng F)
by A71, TARSKI:def 4;
then A72:
p in dom f
by A4, MESFUNC3:def 1;
then A73:
(
(max- f) . p = 0 implies
(max+ f) . p = f . p )
by MESFUNC2:22;
reconsider p =
p as
Element of
X by A71;
a . k1 is
Real
by A1, A4, A5, A66, A70, Th12;
then reconsider r =
f . p as
Real by A4, A5, A66, A71, MESFUNC3:def 1;
A74:
(
a1 . k1 = (max+ f) . p &
a2 . k1 = (max- f) . p )
by A5, A66, A71, A20, A46;
A75:
(
(max- f) . p = - (f . p) implies
(max+ f) . p = 0 )
by MESFUNC2:21;
per cases
( (max+ f) . p = f . p or (max- f) . p = 0 or (max+ f) . p = 0 or (max- f) . p = - (f . p) )
by MESFUNC2:18;
suppose A76:
(
(max+ f) . p = f . p or
(max- f) . p = 0 )
;
x . k = (rx1 - rx2) . kthen
(max- f) . p = 0
by MESFUNC2:19;
then
rx2 . k1 = 0
by A69, A74;
hence
x . k = (rx1 - rx2) . k
by A4, A5, A67, A68, A69, A74, A76, A66, A71, A73, MESFUNC3:def 1;
verum end; suppose A77:
(
(max+ f) . p = 0 or
(max- f) . p = - (f . p) )
;
x . k = (rx1 - rx2) . kthen
rx1 . k1 = 0
by A69, A74, A75;
then A78:
(rx1 - rx2) . k = - (rx2 . k1)
by A68;
a2 . k1 = - (f . p)
by A74, A72, A77, MESFUNC2:20;
then
rx2 . k1 = - ((f . p) * ((M * F) . k1))
by A69, XXREAL_3:92;
hence
x . k = (rx1 - rx2) . k
by A4, A5, A78, A67, A66, A71, MESFUNC3:def 1;
verum end; end; end; end;
end;
hence
Integral (M,f) = Sum x
by A64, A65, FUNCT_1:2, MESFUNC3:2; verum