let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,COMPLEX
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f )
let f be Function of A,COMPLEX ; :: thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f )
let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f )
let S be middle_volume_Sequence of f,T; :: thesis: ( f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 implies ( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f ) )
assume that
A1: ( f is bounded & f is integrable ) and
A2: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f )
set seq = middle_sum f,S;
set xs = integral f;
A1R: ( Re f is bounded & Re f is integrable ) by A1, Def13, BND01;
A1I: ( Im f is bounded & Im f is integrable ) by A1, Def13, BND01;
reconsider xseq = middle_sum f,S as Function of NAT ,COMPLEX ;
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi )
proof
reconsider pjinf = Re f as Function of A,REAL ;
defpred S1[ Element of NAT , set ] means $2 = Re (S . $1);
A4: for x being Element of NAT ex y being Element of REAL * st S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of REAL * st S1[x,y]
Re (S . x) is Element of REAL * by FINSEQ_1:def 11;
hence ex y being Element of REAL * st S1[x,y] ; :: thesis: verum
end;
consider F being Function of NAT ,(REAL * ) such that
A5: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch 10(A4);
 A6: for x being Element of NAT holds dom (Re (S . x)) = Seg (len (S . x))
proof
let x be Element of NAT ; :: thesis: dom (Re (S . x)) = Seg (len (S . x))
thus dom (Re (S . x)) = dom (S . x) by COMSEQ_3:def 3
.= Seg (len (S . x)) by FINSEQ_1:def 3 ; :: thesis: verum
end;
for k being Element of NAT holds F . k is middle_volume of pjinf,T . k
proof
let k be Element of NAT ; :: thesis: F . k is middle_volume of pjinf,T . k
set Tk = T . k;
reconsider Fk = F . k as FinSequence of REAL by FINSEQ_1:def 11;
A7: F . k = Re (S . k) by A5;
then A8: dom Fk = Seg (len (S . k)) by A6
.= Seg (len (T . k)) by Def5 ;
then A9: dom Fk = dom (T . k) by FINSEQ_1:def 3;
A10: now
let j be Nat; :: thesis: ( j in dom (T . k) implies ex v being Element of REAL st
( v in rng (pjinf | (divset (T . k),j)) & Fk . j = v * (vol (divset (T . k),j)) ) )
assume A11: j in dom (T . k) ; :: thesis: ex v being Element of REAL st
( v in rng (pjinf | (divset (T . k),j)) & Fk . j = v * (vol (divset (T . k),j)) )
then consider r being Element of COMPLEX such that
A12: r in rng (f | (divset (T . k),j)) and
A13: (S . k) . j = r * (vol (divset (T . k),j)) by Def5;
reconsider v = Re r as Element of REAL ;
take v = v; :: thesis: ( v in rng (pjinf | (divset (T . k),j)) & Fk . j = v * (vol (divset (T . k),j)) )
consider t being set such that
A14: t in dom (f | (divset (T . k),j)) and
A15: r = (f | (divset (T . k),j)) . t by A12, FUNCT_1:def 5;
t in (dom f) /\ (divset (T . k),j) by A14, RELAT_1:90;
then t in dom f by XBOOLE_0:def 4;
then A16: t in dom (Re f) by COMSEQ_3:def 3;
A17: dom (f | (divset (T . k),j)) = (dom f) /\ (divset (T . k),j) by RELAT_1:90
.= (dom pjinf) /\ (divset (T . k),j) by COMSEQ_3:def 3
.= dom (pjinf | (divset (T . k),j)) by RELAT_1:90 ;
Re r = Re (f . t) by A14, A15, FUNCT_1:70
.= (Re f) . t by A16, COMSEQ_3:def 3
.= (pjinf | (divset (T . k),j)) . t by A14, A17, FUNCT_1:70 ;
hence v in rng (pjinf | (divset (T . k),j)) by A14, A17, FUNCT_1:12; :: thesis: Fk . j = v * (vol (divset (T . k),j))
thus Fk . j = Re ((S . k) . j) by A7, A9, A11, COMSEQ_3:def 3
.= v * (vol (divset (T . k),j)) by A13, LM001 ; :: thesis: verum
end;
len Fk = len (T . k) by A8, FINSEQ_1:def 3;
hence F . k is middle_volume of pjinf,T . k by A10, INTEGR15:def 1; :: thesis: verum
end;
then reconsider pjis = F as middle_volume_Sequence of pjinf,T by INTEGR15:def 3;
reconsider rseqi = middle_sum pjinf,pjis as Real_Sequence ;
A20: for k being Element of NAT holds rseqi . k = Re (xseq . k)
proof
let k be Element of NAT ; :: thesis: rseqi . k = Re (xseq . k)
A21: Re (S . k) is middle_volume of Re f,T . k by LMDef5;
thus rseqi . k = middle_sum pjinf,(pjis . k) by INTEGR15:def 4
.= Re (middle_sum f,(S . k)) by A5, A21, LMDefR0
.= Re (xseq . k) by Def8 ; :: thesis: verum
end;
take rseqi ; :: thesis: for k being Element of NAT holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi )
lim (middle_sum pjinf,pjis) = integral pjinf by A2, A1R, INTEGR15:9;
hence for k being Element of NAT holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi ) by A2, A1R, A20, COMPLEX1:28, INTEGR15:9; :: thesis: verum
end;
then consider rseqi being Real_Sequence such that
A31: for k being Element of NAT holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi ) ;
ex iseqi being Real_Sequence st
for k being Element of NAT holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi )
proof
reconsider pjinf = Im f as Function of A,REAL ;
defpred S1[ Element of NAT , set ] means $2 = Im (S . $1);
B4: for x being Element of NAT ex y being Element of REAL * st S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of REAL * st S1[x,y]
Im (S . x) is Element of REAL * by FINSEQ_1:def 11;
hence ex y being Element of REAL * st S1[x,y] ; :: thesis: verum
end;
consider F being Function of NAT ,(REAL * ) such that
B5: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch 10(B4);
 B6: for x being Element of NAT holds dom (Im (S . x)) = Seg (len (S . x))
proof
let x be Element of NAT ; :: thesis: dom (Im (S . x)) = Seg (len (S . x))
dom (Im (S . x)) = dom (S . x) by COMSEQ_3:def 4
.= Seg (len (S . x)) by FINSEQ_1:def 3 ;
hence dom (Im (S . x)) = Seg (len (S . x)) ; :: thesis: verum
end;
for k being Element of NAT holds F . k is middle_volume of pjinf,T . k
proof
let k be Element of NAT ; :: thesis: F . k is middle_volume of pjinf,T . k
reconsider Tk = T . k as FinSequence ;
reconsider Fk = F . k as FinSequence of REAL by FINSEQ_1:def 11;
B7: F . k = Im (S . k) by B5;
then B8: dom Fk = Seg (len (S . k)) by B6
.= Seg (len Tk) by Def5 ;
then B9: dom Fk = dom Tk by FINSEQ_1:def 3;
B10: now
let j be Nat; :: thesis: ( j in dom Tk implies ex v being Element of REAL st
( v in rng (pjinf | (divset (T . k),j)) & Fk . j = v * (vol (divset (T . k),j)) ) )
assume B11: j in dom Tk ; :: thesis: ex v being Element of REAL st
( v in rng (pjinf | (divset (T . k),j)) & Fk . j = v * (vol (divset (T . k),j)) )
then consider r being Element of COMPLEX such that
B12: r in rng (f | (divset (T . k),j)) and
B13: (S . k) . j = r * (vol (divset (T . k),j)) by Def5;
reconsider v = Im r as Element of REAL ;
take v = v; :: thesis: ( v in rng (pjinf | (divset (T . k),j)) & Fk . j = v * (vol (divset (T . k),j)) )
consider t being set such that
B14: t in dom (f | (divset (T . k),j)) and
B15: r = (f | (divset (T . k),j)) . t by B12, FUNCT_1:def 5;
t in (dom f) /\ (divset (T . k),j) by B14, RELAT_1:90;
then t in dom f by XBOOLE_0:def 4;
then B16: t in dom (Im f) by COMSEQ_3:def 4;
B17: dom (f | (divset (T . k),j)) = (dom f) /\ (divset (T . k),j) by RELAT_1:90
.= (dom pjinf) /\ (divset (T . k),j) by COMSEQ_3:def 4
.= dom (pjinf | (divset (T . k),j)) by RELAT_1:90 ;
Im r = Im (f . t) by B14, B15, FUNCT_1:70
.= (Im f) . t by B16, COMSEQ_3:def 4
.= (pjinf | (divset (T . k),j)) . t by B14, B17, FUNCT_1:70 ;
hence v in rng (pjinf | (divset (T . k),j)) by B14, B17, FUNCT_1:12; :: thesis: Fk . j = v * (vol (divset (T . k),j))
thus Fk . j = Im ((S . k) . j) by B7, B9, B11, COMSEQ_3:def 4
.= v * (vol (divset (T . k),j)) by B13, LM001 ; :: thesis: verum
end;
len Fk = len Tk by B8, FINSEQ_1:def 3;
hence F . k is middle_volume of pjinf,T . k by B10, INTEGR15:def 1; :: thesis: verum
end;
then reconsider pjis = F as middle_volume_Sequence of pjinf,T by INTEGR15:def 3;
reconsider iseqi = middle_sum pjinf,pjis as Real_Sequence ;
B20: for k being Element of NAT holds iseqi . k = Im (xseq . k)
proof
let k be Element of NAT ; :: thesis: iseqi . k = Im (xseq . k)
B21: Im (S . k) is middle_volume of Im f,T . k by LMDef5;
thus iseqi . k = middle_sum pjinf,(pjis . k) by INTEGR15:def 4
.= Im (middle_sum f,(S . k)) by B5, B21, LMDefI0
.= Im (xseq . k) by Def8 ; :: thesis: verum
end;
take iseqi ; :: thesis: for k being Element of NAT holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi )
lim (middle_sum pjinf,pjis) = integral pjinf by A2, A1I, INTEGR15:9;
hence for k being Element of NAT holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi ) by A2, A1I, B20, COMPLEX1:28, INTEGR15:9; :: thesis: verum
end;
then consider iseqi being Real_Sequence such that
B31: for k being Element of NAT holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi ) ;
thus middle_sum f,S is convergent by A31, B31, COMSEQ_3:38; :: thesis: lim (middle_sum f,S) = integral f
thus lim (middle_sum f,S) = (lim rseqi) + ((lim iseqi) * <i> ) by A31, B31, COMSEQ_3:39
.= integral f by COMPLEX1:29, A31, B31 ; :: thesis: verum