let A be non empty closed_interval Subset of REAL; 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; 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; 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; ( 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 )
; ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
set seq = middle_sum (f,S);
set xs = integral f;
A3:
( Re f is bounded & Re f is integrable )
by A1, Th13;
A4:
( Im f is bounded & Im f is integrable )
by A1, Th13;
reconsider xseq = middle_sum (f,S) as sequence of COMPLEX ;
ex rseqi being Real_Sequence st
for k being 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);
A5:
for
x being
Element of
NAT ex
y being
Element of
REAL * st
S1[
x,
y]
consider F being
sequence of
(REAL *) such that A6:
for
x being
Element of
NAT holds
S1[
x,
F . x]
from FUNCT_2:sch 3(A5);
A7:
for
x being
Element of
NAT holds
dom (Re (S . x)) = Seg (len (S . x))
for
k being
Element of
NAT holds
F . k is
middle_volume of
pjinf,
T . k
proof
let k be
Element of
NAT ;
F . k is middle_volume of pjinf,T . k
set Tk =
T . k;
reconsider Fk =
F . k as
FinSequence of
REAL ;
A8:
F . k = Re (S . k)
by A6;
then A9:
dom Fk =
Seg (len (S . k))
by A7
.=
Seg (len (T . k))
by Def1
;
then A10:
dom Fk = dom (T . k)
by FINSEQ_1:def 3;
A11:
now for j being Nat st j in dom (T . k) holds
ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )let j be
Nat;
( 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 A12:
j in dom (T . k)
;
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 A13:
r in rng (f | (divset ((T . k),j)))
and A14:
(S . k) . j = r * (vol (divset ((T . k),j)))
by Def1;
reconsider v =
Re r as
Element of
REAL ;
take v =
v;
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )consider t being
object such that A15:
t in dom (f | (divset ((T . k),j)))
and A16:
r = (f | (divset ((T . k),j))) . t
by A13, FUNCT_1:def 3;
t in (dom f) /\ (divset ((T . k),j))
by A15, RELAT_1:61;
then
t in dom f
by XBOOLE_0:def 4;
then A17:
t in dom (Re f)
by COMSEQ_3:def 3;
A18:
dom (f | (divset ((T . k),j))) =
(dom f) /\ (divset ((T . k),j))
by RELAT_1:61
.=
(dom pjinf) /\ (divset ((T . k),j))
by COMSEQ_3:def 3
.=
dom (pjinf | (divset ((T . k),j)))
by RELAT_1:61
;
Re r =
Re (f . t)
by A15, A16, FUNCT_1:47
.=
(Re f) . t
by A17, COMSEQ_3:def 3
.=
(pjinf | (divset ((T . k),j))) . t
by A15, A18, FUNCT_1:47
;
hence
v in rng (pjinf | (divset ((T . k),j)))
by A15, A18, FUNCT_1:3;
Fk . j = v * (vol (divset ((T . k),j)))thus Fk . j =
Re ((S . k) . j)
by A8, A10, A12, COMSEQ_3:def 3
.=
v * (vol (divset ((T . k),j)))
by A14, Th1
;
verum end;
len Fk = len (T . k)
by A9, FINSEQ_1:def 3;
hence
F . k is
middle_volume of
pjinf,
T . k
by A11, INTEGR15:def 1;
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 ;
A19:
for
k being
Nat holds
rseqi . k = Re (xseq . k)
take
rseqi
;
for k being Nat holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi )
lim (middle_sum (pjinf,pjis)) = integral pjinf
by A2, A3, INTEGR15:9;
hence
for
k being
Nat holds
(
rseqi . k = Re (xseq . k) &
rseqi is
convergent &
Re (integral f) = lim rseqi )
by A2, A3, A19, COMPLEX1:12, INTEGR15:9;
verum
end;
then consider rseqi being Real_Sequence such that
A21:
for k being Nat holds
( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi )
;
ex iseqi being Real_Sequence st
for k being 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);
A22:
for
x being
Element of
NAT ex
y being
Element of
REAL * st
S1[
x,
y]
consider F being
sequence of
(REAL *) such that A23:
for
x being
Element of
NAT holds
S1[
x,
F . x]
from FUNCT_2:sch 3(A22);
A24:
for
x being
Element of
NAT holds
dom (Im (S . x)) = Seg (len (S . x))
for
k being
Element of
NAT holds
F . k is
middle_volume of
pjinf,
T . k
proof
let k be
Element of
NAT ;
F . k is middle_volume of pjinf,T . k
reconsider Tk =
T . k as
FinSequence ;
reconsider Fk =
F . k as
FinSequence of
REAL ;
A25:
F . k = Im (S . k)
by A23;
then A26:
dom Fk =
Seg (len (S . k))
by A24
.=
Seg (len Tk)
by Def1
;
then A27:
dom Fk = dom Tk
by FINSEQ_1:def 3;
A28:
now for j being Nat st j in dom Tk holds
ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )let j be
Nat;
( 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 A29:
j in dom Tk
;
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 A30:
r in rng (f | (divset ((T . k),j)))
and A31:
(S . k) . j = r * (vol (divset ((T . k),j)))
by Def1;
reconsider v =
Im r as
Element of
REAL ;
take v =
v;
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )consider t being
object such that A32:
t in dom (f | (divset ((T . k),j)))
and A33:
r = (f | (divset ((T . k),j))) . t
by A30, FUNCT_1:def 3;
t in (dom f) /\ (divset ((T . k),j))
by A32, RELAT_1:61;
then
t in dom f
by XBOOLE_0:def 4;
then A34:
t in dom (Im f)
by COMSEQ_3:def 4;
A35:
dom (f | (divset ((T . k),j))) =
(dom f) /\ (divset ((T . k),j))
by RELAT_1:61
.=
(dom pjinf) /\ (divset ((T . k),j))
by COMSEQ_3:def 4
.=
dom (pjinf | (divset ((T . k),j)))
by RELAT_1:61
;
Im r =
Im (f . t)
by A32, A33, FUNCT_1:47
.=
(Im f) . t
by A34, COMSEQ_3:def 4
.=
(pjinf | (divset ((T . k),j))) . t
by A32, A35, FUNCT_1:47
;
hence
v in rng (pjinf | (divset ((T . k),j)))
by A32, A35, FUNCT_1:3;
Fk . j = v * (vol (divset ((T . k),j)))thus Fk . j =
Im ((S . k) . j)
by A25, A27, A29, COMSEQ_3:def 4
.=
v * (vol (divset ((T . k),j)))
by A31, Th1
;
verum end;
len Fk = len Tk
by A26, FINSEQ_1:def 3;
hence
F . k is
middle_volume of
pjinf,
T . k
by A28, INTEGR15:def 1;
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 ;
A36:
for
k being
Nat holds
iseqi . k = Im (xseq . k)
take
iseqi
;
for k being Nat holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi )
lim (middle_sum (pjinf,pjis)) = integral pjinf
by A2, A4, INTEGR15:9;
hence
for
k being
Nat holds
(
iseqi . k = Im (xseq . k) &
iseqi is
convergent &
Im (integral f) = lim iseqi )
by A2, A4, A36, COMPLEX1:12, INTEGR15:9;
verum
end;
then consider iseqi being Real_Sequence such that
A38:
for k being Nat holds
( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi )
;
thus
middle_sum (f,S) is convergent
by A21, A38, COMSEQ_3:38; lim (middle_sum (f,S)) = integral f
thus lim (middle_sum (f,S)) =
(lim rseqi) + ((lim iseqi) * <i>)
by A21, A38, COMSEQ_3:39
.=
integral f
by A21, A38, COMPLEX1:13
; verum