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 being Element of S
for E being SetSequence of S st f is A -measurable & A = dom f & E is disjoint_valued & A = Union E & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S
for E being SetSequence of S st f is A -measurable & A = dom f & E is disjoint_valued & A = Union E & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for A being Element of S
for E being SetSequence of S st f is A -measurable & A = dom f & E is disjoint_valued & A = Union E & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I )
let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S
for E being SetSequence of S st f is A -measurable & A = dom f & E is disjoint_valued & A = Union E & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I )
let A be Element of S; :: thesis: for E being SetSequence of S st f is A -measurable & A = dom f & E is disjoint_valued & A = Union E & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I )
let E be SetSequence of S; :: thesis: ( f is A -measurable & A = dom f & E is disjoint_valued & A = Union E & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) implies ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I ) )
assume that
A1: f is A -measurable and
A2: A = dom f and
A3: E is disjoint_valued and
A4: A = Union E and
A5: ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) ; :: thesis: ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I )
A6: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;
A7: ( max+ f is A -measurable & max- f is A -measurable ) by A1, A2, MESFUNC2:25, MESFUNC2:26;
A8: ( A = dom (max+ f) & A = dom (max- f) ) by A2, MESFUNC2:def 2, MESFUNC2:def 3;
consider I1 being nonnegative ExtREAL_sequence such that
A9: for n being Nat holds I1 . n = Integral (M,((max+ f) | (E . n))) and
A10: ( I1 is summable & Integral (M,(max+ f)) = Sum I1 ) by A7, A8, A3, A4, Lm1, MESFUN11:5;
consider I2 being nonnegative ExtREAL_sequence such that
A11: for n being Nat holds I2 . n = Integral (M,((max- f) | (E . n))) and
A12: ( I2 is summable & Integral (M,(max- f)) = Sum I2 ) by A7, A8, A3, A4, Lm1, MESFUN11:5;
A13: for n being Nat holds
( E . n is Element of S & E . n c= dom f )
proof
let n be Nat; :: thesis: ( E . n is Element of S & E . n c= dom f )
dom E = NAT by FUNCT_2:def 1;
then A14: E . n in rng E by FUNCT_1:3, ORDINAL1:def 12;
hence E . n is Element of S ; :: thesis: E . n c= dom f
E . n c= union (rng E) by A14, ZFMISC_1:74;
hence E . n c= dom f by A2, A4, CARD_3:def 4; :: thesis: verum
end;
A15: for n being Nat holds I1 . n = integral+ (M,((max+ f) | (E . n)))
proof
let n be Nat; :: thesis: I1 . n = integral+ (M,((max+ f) | (E . n)))
reconsider En = E . n as Element of S by A13;
A16: max+ f is En -measurable by A7, A2, A13, MESFUNC1:30;
A17: dom ((max+ f) | (E . n)) = En by A2, A8, A13, RELAT_1:62;
then (dom (max+ f)) /\ En = En by RELAT_1:61;
then A18: (max+ f) | (E . n) is En -measurable by A16, MESFUNC5:42;
I1 . n = Integral (M,((max+ f) | (E . n))) by A9;
hence I1 . n = integral+ (M,((max+ f) | (E . n))) by A17, A18, A6, MESFUNC5:15, MESFUNC5:88; :: thesis: verum
end;
A19: for n being Nat holds I2 . n = integral+ (M,((max- f) | (E . n)))
proof
let n be Nat; :: thesis: I2 . n = integral+ (M,((max- f) | (E . n)))
reconsider En = E . n as Element of S by A13;
A20: max- f is En -measurable by A7, A2, A13, MESFUNC1:30;
A21: dom ((max- f) | (E . n)) = En by A2, A8, A13, RELAT_1:62;
then (dom (max- f)) /\ En = En by RELAT_1:61;
then A22: (max- f) | (E . n) is En -measurable by A20, MESFUNC5:42;
I2 . n = Integral (M,((max- f) | (E . n))) by A11;
hence I2 . n = integral+ (M,((max- f) | (E . n))) by A21, A22, A6, MESFUNC5:15, MESFUNC5:88; :: thesis: verum
end;
per cases ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) by A5;
suppose integral+ (M,(max+ f)) < +infty ; :: thesis: ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I )
then A23: Integral (M,(max+ f)) < +infty by A7, A8, MESFUNC5:88, MESFUN11:5;
then A24: lim (Partial_Sums I1) < +infty by A10, MESFUNC9:def 3;
for n being set st n in dom I1 holds
I1 . n < +infty
proof
let n be set ; :: thesis: ( n in dom I1 implies I1 . n < +infty )
assume A25: n in dom I1 ; :: thesis: I1 . n < +infty
then ( E . n is Element of S & E . n c= dom (max+ f) ) by A2, A8, A13;
then Integral (M,((max+ f) | (E . n))) <= Integral (M,((max+ f) | A)) by A8, A7, MESFUNC5:93, MESFUN11:5;
then Integral (M,((max+ f) | (E . n))) < +infty by A8, A23, XXREAL_0:2;
hence I1 . n < +infty by A9, A25; :: thesis: verum
end;
then reconsider I1 = I1 as without+infty ExtREAL_sequence by MESFUNC5:11;
take I = I1 - I2; :: thesis: ( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I )
thus for n being Nat holds I . n = Integral (M,(f | (E . n))) :: thesis: ( I is summable & Integral (M,f) = Sum I )
proof
let n be Nat; :: thesis: I . n = Integral (M,(f | (E . n)))
A26: n is Element of NAT by ORDINAL1:def 12;
Integral (M,(f | (E . n))) = (integral+ (M,(max+ (f | (E . n))))) - (integral+ (M,(max- (f | (E . n))))) by MESFUNC5:def 16
.= (integral+ (M,((max+ f) | (E . n)))) - (integral+ (M,(max- (f | (E . n))))) by MESFUNC5:28
.= (integral+ (M,((max+ f) | (E . n)))) - (integral+ (M,((max- f) | (E . n)))) by MESFUNC5:28
.= (I1 . n) - (integral+ (M,((max- f) | (E . n)))) by A15
.= (I1 . n) - (I2 . n) by A19 ;
hence I . n = Integral (M,(f | (E . n))) by A26, DBLSEQ_3:7; :: thesis: verum
end;
( Partial_Sums I1 is nonnegative & Partial_Sums I1 is non-decreasing ) by MESFUNC9:16;
then A27: ( Partial_Sums I1 is convergent_to_+infty or Partial_Sums I1 is convergent_to_finite_number ) by DBLSEQ_3:62;
then consider LI1 being Real such that
A28: lim (Partial_Sums I1) = LI1 and
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums I1) . m) - (lim (Partial_Sums I1))).| < p by A24, MESFUNC9:7;
A29: ( Partial_Sums I2 is nonnegative & Partial_Sums I2 is non-decreasing ) by MESFUNC9:16;
then A30: ( Partial_Sums I2 is convergent_to_+infty or Partial_Sums I2 is convergent_to_finite_number ) by DBLSEQ_3:62;
A31: Partial_Sums I = (Partial_Sums I1) - (Partial_Sums I2) by Th3;
Partial_Sums I is convergent by A30, A31, A24, A27, MESFUNC5:def 12, DBLSEQ_3:25;
hence I is summable by MESFUNC9:def 2; :: thesis: Integral (M,f) = Sum I
A32: Integral (M,f) = (integral+ (M,(max+ f))) - (integral+ (M,(max- f))) by MESFUNC5:def 16
.= (Integral (M,(max+ f))) - (integral+ (M,(max- f))) by A7, A8, MESFUNC5:88, MESFUN11:5
.= (Integral (M,(max+ f))) - (Integral (M,(max- f))) by A7, A8, MESFUNC5:88, MESFUN11:5
.= (lim (Partial_Sums I1)) - (Integral (M,(max- f))) by A10, MESFUNC9:def 3
.= (lim (Partial_Sums I1)) - (lim (Partial_Sums I2)) by A12, MESFUNC9:def 3 ;
thus Integral (M,f) = Sum I :: thesis: verum
proof
per cases ( Partial_Sums I2 is convergent_to_+infty or Partial_Sums I2 is convergent_to_finite_number ) by A29, DBLSEQ_3:62;
end;
end;
end;
suppose integral+ (M,(max- f)) < +infty ; :: thesis: ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I )
then A36: Integral (M,(max- f)) < +infty by A7, A8, MESFUNC5:88, MESFUN11:5;
then A37: lim (Partial_Sums I2) < +infty by A12, MESFUNC9:def 3;
for n being set st n in dom I2 holds
I2 . n < +infty
proof
let n be set ; :: thesis: ( n in dom I2 implies I2 . n < +infty )
assume A38: n in dom I2 ; :: thesis: I2 . n < +infty
then ( E . n is Element of S & E . n c= dom (max- f) ) by A2, A8, A13;
then Integral (M,((max- f) | (E . n))) <= Integral (M,((max- f) | A)) by A8, A7, MESFUNC5:93, MESFUN11:5;
then Integral (M,((max- f) | (E . n))) < +infty by A8, A36, XXREAL_0:2;
hence I2 . n < +infty by A11, A38; :: thesis: verum
end;
then reconsider I2 = I2 as without+infty ExtREAL_sequence by MESFUNC5:11;
take I = I1 - I2; :: thesis: ( ( for n being Nat holds I . n = Integral (M,(f | (E . n))) ) & I is summable & Integral (M,f) = Sum I )
thus for n being Nat holds I . n = Integral (M,(f | (E . n))) :: thesis: ( I is summable & Integral (M,f) = Sum I )
proof
let n be Nat; :: thesis: I . n = Integral (M,(f | (E . n)))
A39: n is Element of NAT by ORDINAL1:def 12;
Integral (M,(f | (E . n))) = (integral+ (M,(max+ (f | (E . n))))) - (integral+ (M,(max- (f | (E . n))))) by MESFUNC5:def 16
.= (integral+ (M,((max+ f) | (E . n)))) - (integral+ (M,(max- (f | (E . n))))) by MESFUNC5:28
.= (integral+ (M,((max+ f) | (E . n)))) - (integral+ (M,((max- f) | (E . n)))) by MESFUNC5:28
.= (I1 . n) - (integral+ (M,((max- f) | (E . n)))) by A15
.= (I1 . n) - (I2 . n) by A19 ;
hence I . n = Integral (M,(f | (E . n))) by A39, DBLSEQ_3:7; :: thesis: verum
end;
( Partial_Sums I2 is nonnegative & Partial_Sums I2 is non-decreasing ) by MESFUNC9:16;
then A40: ( Partial_Sums I2 is convergent_to_+infty or Partial_Sums I2 is convergent_to_finite_number ) by DBLSEQ_3:62;
then consider LI2 being Real such that
A41: lim (Partial_Sums I2) = LI2 and
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums I2) . m) - (lim (Partial_Sums I2))).| < p by A37, MESFUNC9:7;
A42: ( Partial_Sums I1 is nonnegative & Partial_Sums I1 is non-decreasing ) by MESFUNC9:16;
then A43: ( Partial_Sums I1 is convergent_to_+infty or Partial_Sums I1 is convergent_to_finite_number ) by DBLSEQ_3:62;
Partial_Sums I = (Partial_Sums I1) - (Partial_Sums I2) by Th3;
then Partial_Sums I is convergent by A43, A40, A37, MESFUNC5:def 12, DBLSEQ_3:25;
hence I is summable by MESFUNC9:def 2; :: thesis: Integral (M,f) = Sum I
A44: Integral (M,f) = (integral+ (M,(max+ f))) - (integral+ (M,(max- f))) by MESFUNC5:def 16
.= (Integral (M,(max+ f))) - (integral+ (M,(max- f))) by A7, A8, MESFUNC5:88, MESFUN11:5
.= (Integral (M,(max+ f))) - (Integral (M,(max- f))) by A7, A8, MESFUNC5:88, MESFUN11:5
.= (lim (Partial_Sums I1)) - (Integral (M,(max- f))) by A10, MESFUNC9:def 3
.= (lim (Partial_Sums I1)) - (lim (Partial_Sums I2)) by A12, MESFUNC9:def 3 ;
thus Integral (M,f) = Sum I :: thesis: verum
proof
per cases ( Partial_Sums I1 is convergent_to_+infty or Partial_Sums I1 is convergent_to_finite_number ) by A42, DBLSEQ_3:62;
end;
end;
end;
end;