let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for F being Functional_Sequence of X,ExtREAL
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 & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
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 F being Functional_Sequence of X,ExtREAL
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 & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
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 F being Functional_Sequence of X,ExtREAL
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 & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
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 Functional_Sequence of X,ExtREAL; 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 & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
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 & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
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 & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) implies 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
and
A4:
for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) )
and
A5:
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;
set G = - F;
A6:
E c= dom (- f)
by A1, MESFUNC1:def 7;
then A7:
- F is additive
by Th47;
A8:
for n being Nat holds
( (- F) . n is_simple_func_in S & (- F) . n is nonnegative & E c= dom ((- F) . n) )
A9:
for x being Element of X st x in E holds
( (- F) # x is summable & (- f) . x = Sum ((- F) # x) )
consider J being ExtREAL_sequence such that
A12:
( ( for n being Nat holds J . n = Integral (M,(((- F) . n) | E)) ) & J is summable & Integral (M,((- f) | E)) = Sum J )
by A2, A1, A3, A6, A7, A8, A9, MESFUNC9:47, MEASUR11:63;
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 )
thus
I is summable
by A12, Th45; Integral (M,(f | E)) = Sum I
A16:
Integral (M,((- f) | E)) = - (Integral (M,(f | E)))
by A1, A3, Th55;
Partial_Sums J is convergent
by A12, MESFUNC9:def 2;
then lim (- (Partial_Sums J)) =
- (lim (Partial_Sums J))
by DBLSEQ_3:17
.=
- (Integral (M,((- f) | E)))
by A12, MESFUNC9:def 3
;
then
lim (Partial_Sums I) = - (Integral (M,((- f) | E)))
by Th44;
hence
Integral (M,(f | E)) = Sum I
by A16, MESFUNC9:def 3; verum