let n be Element of NAT ; for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
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 A be non empty closed_interval Subset of REAL; for f being Function of A,(REAL n)
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,(REAL n); 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;
REAL n = the carrier of (REAL-NS n)
by REAL_NS1:def 4;
then reconsider xseq = middle_sum (f,S) as sequence of (REAL n) ;
A3:
for i being Nat st i in Seg n holds
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi )
proof
let i be
Nat;
( i in Seg n implies ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi ) )
reconsider pjinf =
(proj (i,n)) * f as
Function of
A,
REAL ;
defpred S1[
Element of
NAT ,
set ]
means $2
= (proj (i,n)) * (S . $1);
A4:
for
x being
Element of
NAT ex
y being
Element of
REAL * st
S1[
x,
y]
consider F being
sequence of
(REAL *) such that A5:
for
x being
Element of
NAT holds
S1[
x,
F . x]
from FUNCT_2:sch 3(A4);
A6:
for
x being
Element of
NAT holds
(
(proj (i,n)) * (S . x) is
FinSequence of
REAL &
dom ((proj (i,n)) * (S . x)) = Seg (len (S . x)) &
rng ((proj (i,n)) * (S . x)) c= REAL )
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 ;
A7:
F . k = (proj (i,n)) * (S . k)
by A5;
then A8:
dom Fk =
Seg (len (S . k))
by A6
.=
Seg (len Tk)
by Def5
;
then A9:
dom Fk = dom Tk
by FINSEQ_1:def 3;
A10:
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))) ) )
dom (proj (i,n)) = REAL n
by FUNCT_2:def 1;
then A11:
rng f c= dom (proj (i,n))
;
assume A12:
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
REAL n such that A13:
r in rng (f | (divset ((T . k),j)))
and A14:
(S . k) . j = (vol (divset ((T . k),j))) * r
by Def5;
reconsider v =
(proj (i,n)) . 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 ((proj (i,n)) * f)
by A11, RELAT_1:27;
A18:
dom (f | (divset ((T . k),j))) =
(dom f) /\ (divset ((T . k),j))
by RELAT_1:61
.=
(dom pjinf) /\ (divset ((T . k),j))
by A11, RELAT_1:27
.=
dom (pjinf | (divset ((T . k),j)))
by RELAT_1:61
;
(proj (i,n)) . r =
(proj (i,n)) . (f . t)
by A15, A16, FUNCT_1:47
.=
((proj (i,n)) * f) . t
by A17, FUNCT_1:12
.=
(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 =
(proj (i,n)) . ((S . k) . j)
by A7, A9, A12, FUNCT_1:12
.=
((vol (divset ((T . k),j))) * r) . i
by A14, PDIFF_1:def 1
.=
(vol (divset ((T . k),j))) * (r . i)
by RVSUM_1:44
.=
v * (vol (divset ((T . k),j)))
by PDIFF_1:def 1
;
verum end;
len Fk = len Tk
by A8, FINSEQ_1:def 3;
hence
F . k is
middle_volume of
pjinf,
T . k
by A10, Def1;
verum
end;
then reconsider pjis =
F as
middle_volume_Sequence of
pjinf,
T by Def3;
reconsider rseqi =
middle_sum (
pjinf,
pjis) as
Real_Sequence ;
assume A19:
i in Seg n
;
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi )
A20:
for
k being
Nat holds
rseqi . k = (xseq . k) . i
take
rseqi
;
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi )
A22:
(
(proj (i,n)) * f is
bounded &
pjinf is
integrable )
by A1, A19;
then
lim (middle_sum (pjinf,pjis)) = integral pjinf
by A2, Th9;
hence
for
k being
Nat holds
(
rseqi . k = (xseq . k) . i &
rseqi is
convergent &
(integral f) . i = lim rseqi )
by A2, A19, A22, A20, Def14, Th9;
verum
end;
reconsider x = integral f as Point of (REAL-NS n) by REAL_NS1:def 4;
integral f = x
;
hence
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
by A3, REAL_NS1:11; verum