let X be non empty set ; :: thesis: 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 st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for F being Functional_Sequence of X,ExtREAL
for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )
let M be sigma_Measure of S; :: thesis: for F being Functional_Sequence of X,ExtREAL
for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )
let F be Functional_Sequence of X,ExtREAL; :: thesis: for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )
let E be Element of S; :: thesis: ( E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds
F # x is convergent ) implies ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I ) )
assume that
A1: E = dom (F . 0) and
A2: F . 0 is nonpositive and
A3: F is with_the_same_dom and
A4: for n being Nat holds F . n is E -measurable and
A5: for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(F . n) . x >= (F . m) . x and
A6: for x being Element of X st x in E holds
F # x is convergent ; :: thesis: ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )
set G = - F;
A7: (- F) . 0 = - (F . 0) by Th37;
then A8: E = dom ((- F) . 0) by A1, MESFUNC1:def 7;
A11: for n being Nat holds (- F) . n is E -measurable
proof
let n be Nat; :: thesis: (- F) . n is E -measurable
E = dom (F . n) by A1, A3, MESFUNC8:def 2;
then - (F . n) is E -measurable by A4, MEASUR11:63;
hence (- F) . n is E -measurable by Th37; :: thesis: verum
end;
A13: for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
((- F) . n) . x <= ((- F) . m) . x
proof
let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X st x in E holds
((- F) . n) . x <= ((- F) . m) . x )
assume A14: n <= m ; :: thesis: for x being Element of X st x in E holds
((- F) . n) . x <= ((- F) . m) . x
let x be Element of X; :: thesis: ( x in E implies ((- F) . n) . x <= ((- F) . m) . x )
assume A15: x in E ; :: thesis: ((- F) . n) . x <= ((- F) . m) . x
then A17: ( x in dom ((- F) . n) & x in dom ((- F) . m) ) by A8, A3, Th40, MESFUNC8:def 2;
( (- F) . n = - (F . n) & (- F) . m = - (F . m) ) by Th37;
then ( ((- F) . n) . x = - ((F . n) . x) & ((- F) . m) . x = - ((F . m) . x) ) by A17, MESFUNC1:def 7;
hence ((- F) . n) . x <= ((- F) . m) . x by A15, A5, A14, XXREAL_3:38; :: thesis: verum
end;
A18: for x being Element of X st x in E holds
(- F) # x is convergent
proof
let x be Element of X; :: thesis: ( x in E implies (- F) # x is convergent )
assume x in E ; :: thesis: (- F) # x is convergent
then F # x is convergent by A6;
then - (F # x) is convergent by DBLSEQ_3:17;
hence (- F) # x is convergent by Th38; :: thesis: verum
end;
consider J being ExtREAL_sequence such that
A19: ( ( for n being Nat holds J . n = Integral (M,((- F) . n)) ) & J is convergent & Integral (M,(lim (- F))) = lim J ) by A8, A2, A7, A3, Th40, A11, A13, A18, MESFUNC9:52;
set I = - J;
take - J ; :: thesis: ( ( for n being Nat holds (- J) . n = Integral (M,(F . n)) ) & - J is convergent & Integral (M,(lim F)) = lim (- J) )
thus for n being Nat holds (- J) . n = Integral (M,(F . n)) :: thesis: ( - J is convergent & Integral (M,(lim F)) = lim (- J) )
proof
let n be Nat; :: thesis: (- J) . n = Integral (M,(F . n))
n in NAT by ORDINAL1:def 12;
then A20: n in dom (- J) by FUNCT_2:def 1;
A21: dom (F . n) = E by A1, A3, MESFUNC8:def 2;
(- F) . n = - (F . n) by Th37;
then Integral (M,((- F) . n)) = - (Integral (M,(F . n))) by A21, A4, Th52;
then J . n = - (Integral (M,(F . n))) by A19;
then (- J) . n = - (- (Integral (M,(F . n)))) by A20, MESFUNC1:def 7;
hence (- J) . n = Integral (M,(F . n)) ; :: thesis: verum
end;
thus - J is convergent by A19, DBLSEQ_3:17; :: thesis: Integral (M,(lim F)) = lim (- J)
A23: lim (- J) = - (Integral (M,(lim (- F)))) by A19, DBLSEQ_3:17;
A24: E = dom (lim F) by A1, MESFUNC8:def 9;
then A25: dom (- (lim F)) = E by MESFUNC1:def 7;
then A26: dom (lim (- F)) = dom (- (lim F)) by A8, MESFUNC8:def 9;
for x being Element of X st x in dom (lim (- F)) holds
(lim (- F)) . x = (- (lim F)) . x
proof
let x be Element of X; :: thesis: ( x in dom (lim (- F)) implies (lim (- F)) . x = (- (lim F)) . x )
assume A27: x in dom (lim (- F)) ; :: thesis: (lim (- F)) . x = (- (lim F)) . x
then A30: (lim (- F)) . x = lim ((- F) # x) by MESFUNC8:def 9;
A28: F # x is convergent by A27, A26, A25, A6;
(- F) # x = - (F # x) by Th38;
then A29: lim ((- F) # x) = - (lim (F # x)) by A28, DBLSEQ_3:17;
lim (F # x) = (lim F) . x by A27, A26, A25, A24, MESFUNC8:def 9;
hence (lim (- F)) . x = (- (lim F)) . x by A29, A30, A27, A26, MESFUNC1:def 7; :: thesis: verum
end;
then lim (- F) = - (lim F) by A26, PARTFUN1:5;
then Integral (M,(lim (- F))) = - (Integral (M,(lim F))) by A1, A3, A4, A6, A24, Th52, MESFUNC8:25;
hence Integral (M,(lim F)) = lim (- J) by A23; :: thesis: verum