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 st E c= dom f & f is nonpositive & f is E -measurable holds
ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )
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 st E c= dom f & f is nonpositive & f is E -measurable holds
ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )
let M be sigma_Measure of S; for E being Element of S
for f being PartFunc of X,ExtREAL st E c= dom f & f is nonpositive & f is E -measurable holds
ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )
let E be Element of S; for f being PartFunc of X,ExtREAL st E c= dom f & f is nonpositive & f is E -measurable holds
ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )
let f be PartFunc of X,ExtREAL; ( E c= dom f & f is nonpositive & f is E -measurable implies ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) ) )
assume that
A1:
E c= dom f
and
A2:
f is nonpositive
and
A3:
f is E -measurable
; ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )
set g = - f;
A4:
E c= dom (- f)
by A1, MESFUNC1:def 7;
then consider G being Functional_Sequence of X,ExtREAL such that
A5:
( G is additive & ( for n being Nat holds
( G . n is_simple_func_in S & G . n is nonnegative & G . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( G # x is summable & (- f) . x = Sum (G # x) ) ) & ex J being ExtREAL_sequence st
( ( for n being Nat holds J . n = Integral (M,((G . n) | E)) ) & J is summable & Integral (M,((- f) | E)) = Sum J ) )
by A1, A2, A3, MESFUNC9:48, MEASUR11:63;
take F = - G; ( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )
thus
F is additive
by A5, Th41; ( ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )
thus
for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable )
( ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )
thus
for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) )
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
thus
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
verumproof
consider J being
ExtREAL_sequence such that A9:
( ( for
n being
Nat holds
J . n = Integral (
M,
((G . n) | E)) ) &
J is
summable &
Integral (
M,
((- f) | E))
= Sum J )
by A5;
take I =
- J;
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
thus
for
n being
Nat holds
I . n = Integral (
M,
((F . n) | E))
( I is summable & Integral (M,(f | E)) = Sum I )proof
let n be
Nat;
I . n = Integral (M,((F . n) | E))
dom I = NAT
by FUNCT_2:def 1;
then A10:
n in dom I
by ORDINAL1:def 12;
A11:
J . n = Integral (
M,
((G . n) | E))
by A9;
F . n = - (G . n)
by Th37;
then A12:
(F . n) | E = - ((G . n) | E)
by Th3;
A13:
G . n is_simple_func_in S
by A5;
then consider GG being
Finite_Sep_Sequence of
S such that A14:
(
dom (G . n) = union (rng GG) & ( for
k being
Nat for
x,
y being
Element of
X st
k in dom GG &
x in GG . k &
y in GG . k holds
(G . n) . x = (G . n) . y ) )
by MESFUNC2:def 4;
reconsider V =
union (rng GG) as
Element of
S by MESFUNC2:31;
reconsider VE =
V /\ E as
Element of
S ;
A15:
VE = dom ((G . n) | E)
by A14, RELAT_1:61;
(G . n) | E is
VE -measurable
by A13, MESFUNC2:34, MESFUNC5:34;
then
Integral (
M,
((F . n) | E))
= - (Integral (M,((G . n) | E)))
by A12, A15, Th52;
hence
I . n = Integral (
M,
((F . n) | E))
by A10, A11, MESFUNC1:def 7;
verum
end;
thus
I is
summable
by A9, Th45;
Integral (M,(f | E)) = Sum I
A16:
Partial_Sums J is
convergent
by A9, MESFUNC9:def 2;
A17:
Sum I =
lim (Partial_Sums I)
by MESFUNC9:def 3
.=
lim (- (Partial_Sums J))
by Th44
.=
- (lim (Partial_Sums J))
by A16, DBLSEQ_3:17
.=
- (Integral (M,((- f) | E)))
by A9, MESFUNC9:def 3
;
A18:
dom (f | E) = E
by A1, RELAT_1:62;
A19:
E = (dom f) /\ E
by A1, XBOOLE_1:28;
(- f) | E = - (f | E)
by Th3;
then
Integral (
M,
((- f) | E))
= - (Integral (M,(f | E)))
by A3, A18, A19, Th52, MESFUNC5:42;
hence
Integral (
M,
(f | E))
= Sum I
by A17;
verum
end;