let n be Element of NAT ; for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n) st f is bounded holds
( f is integrable iff ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
let A be non empty closed_interval Subset of REAL; for f being Function of A,(REAL n) st f is bounded holds
( f is integrable iff ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
let f be Function of A,(REAL n); ( f is bounded implies ( f is integrable iff ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) )
assume A1:
f is bounded
; ( f is integrable iff ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
hereby ( ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable )
reconsider I =
integral f as
Element of
REAL n ;
assume A2:
f is
integrable
;
ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )take I =
I;
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )thus
for
T being
DivSequence of
A for
S being
middle_volume_Sequence of
f,
T st
delta T is
convergent &
lim (delta T) = 0 holds
(
middle_sum (
f,
S) is
convergent &
lim (middle_sum (f,S)) = I )
by A1, A2, Th11;
verum
end;
now ( ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable )assume
ex
I being
Element of
REAL n st
for
T being
DivSequence of
A for
S being
middle_volume_Sequence of
f,
T st
delta T is
convergent &
lim (delta T) = 0 holds
(
middle_sum (
f,
S) is
convergent &
lim (middle_sum (f,S)) = I )
;
f is integrable then consider I being
Element of
REAL n such that A3:
for
T being
DivSequence of
A for
S being
middle_volume_Sequence of
f,
T st
delta T is
convergent &
lim (delta T) = 0 holds
(
middle_sum (
f,
S) is
convergent &
lim (middle_sum (f,S)) = I )
;
now for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is integrable let i be
Element of
NAT ;
( i in Seg n implies (proj (i,n)) * f is integrable )reconsider Ii =
I . i as
Element of
REAL by XREAL_0:def 1;
assume A4:
i in Seg n
;
(proj (i,n)) * f is integrable A5:
now for T being DivSequence of A
for Si being middle_volume_Sequence of (proj (i,n)) * f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii )set x =
I;
let T be
DivSequence of
A;
for Si being middle_volume_Sequence of (proj (i,n)) * f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii )let Si be
middle_volume_Sequence of
(proj (i,n)) * f,
T;
( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii ) )defpred S1[
Element of
NAT ,
set ]
means ex
H,
z being
FinSequence st
(
H = T . $1 &
z = $2 &
len z = len H & ( for
j being
Element of
NAT st
j in dom H holds
ex
rji being
Element of
REAL n ex
tji being
Element of
REAL st
(
tji in dom (f | (divset ((T . $1),j))) &
(Si . $1) . j = (vol (divset ((T . $1),j))) * ((((proj (i,n)) * f) | (divset ((T . $1),j))) . tji) &
rji = (f | (divset ((T . $1),j))) . tji &
z . j = (vol (divset ((T . $1),j))) * rji ) ) );
reconsider xs =
I as
Element of
REAL n ;
A6:
for
k being
Element of
NAT ex
y being
Element of
(REAL n) * st
S1[
k,
y]
proof
let k be
Element of
NAT ;
ex y being Element of (REAL n) * st S1[k,y]
reconsider Tk =
T . k as
FinSequence ;
defpred S2[
Nat,
set ]
means ex
j being
Element of
NAT st
( $1
= j & ex
rji being
Element of
REAL n ex
tji being
Element of
REAL st
(
tji in dom (f | (divset ((T . k),j))) &
(Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) &
rji = (f | (divset ((T . k),j))) . tji & $2
= (vol (divset ((T . k),j))) * rji ) );
A7:
for
j being
Nat st
j in Seg (len Tk) holds
ex
x being
Element of
REAL n st
S2[
j,
x]
proof
dom (proj (i,n)) = REAL n
by FUNCT_2:def 1;
then A8:
rng f c= dom (proj (i,n))
;
let j0 be
Nat;
( j0 in Seg (len Tk) implies ex x being Element of REAL n st S2[j0,x] )
assume A9:
j0 in Seg (len Tk)
;
ex x being Element of REAL n st S2[j0,x]
then reconsider j =
j0 as
Element of
NAT ;
j in dom Tk
by A9, FINSEQ_1:def 3;
then consider r being
Element of
REAL such that A10:
r in rng (((proj (i,n)) * f) | (divset ((T . k),j)))
and A11:
(Si . k) . j = r * (vol (divset ((T . k),j)))
by Def1;
consider tji being
object such that A12:
tji in dom (((proj (i,n)) * f) | (divset ((T . k),j)))
and A13:
r = (((proj (i,n)) * f) | (divset ((T . k),j))) . tji
by A10, FUNCT_1:def 3;
tji in (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j))
by A12, RELAT_1:61;
then reconsider tji =
tji as
Element of
REAL ;
A14:
dom (f | (divset ((T . k),j))) =
(dom f) /\ (divset ((T . k),j))
by RELAT_1:61
.=
(dom ((proj (i,n)) * f)) /\ (divset ((T . k),j))
by A8, RELAT_1:27
.=
dom (((proj (i,n)) * f) | (divset ((T . k),j)))
by RELAT_1:61
;
then
(f | (divset ((T . k),j))) . tji in rng (f | (divset ((T . k),j)))
by A12, FUNCT_1:3;
then reconsider rji =
(f | (divset ((T . k),j))) . tji as
Element of
REAL n ;
reconsider x =
(vol (divset ((T . k),j))) * rji as
Element of
REAL n ;
take
x
;
S2[j0,x]
thus
S2[
j0,
x]
by A11, A12, A13, A14;
verum
end;
consider p being
FinSequence of
REAL n such that A15:
(
dom p = Seg (len Tk) & ( for
j being
Nat st
j in Seg (len Tk) holds
S2[
j,
p . j] ) )
from FINSEQ_1:sch 5(A7);
reconsider x =
p as
Element of
(REAL n) * by FINSEQ_1:def 11;
take
x
;
S1[k,x]
A16:
now for jj0 being Element of NAT st jj0 in dom Tk holds
ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * ((((proj (i,n)) * f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji )let jj0 be
Element of
NAT ;
( jj0 in dom Tk implies ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * ((((proj (i,n)) * f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) )reconsider j0 =
jj0 as
Nat ;
A17:
dom Tk = Seg (len Tk)
by FINSEQ_1:def 3;
assume
jj0 in dom Tk
;
ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * ((((proj (i,n)) * f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji )then
S2[
j0,
p . j0]
by A15, A17;
hence
ex
rji being
Element of
REAL n ex
tji being
Element of
REAL st
(
tji in dom (f | (divset ((T . k),jj0))) &
(Si . k) . jj0 = (vol (divset ((T . k),jj0))) * ((((proj (i,n)) * f) | (divset ((T . k),jj0))) . tji) &
rji = (f | (divset ((T . k),jj0))) . tji &
p . jj0 = (vol (divset ((T . k),jj0))) * rji )
;
verum end;
len p = len Tk
by A15, FINSEQ_1:def 3;
hence
S1[
k,
x]
by A16;
verum
end; consider S being
sequence of
((REAL n) *) such that A18:
for
x being
Element of
NAT holds
S1[
x,
S . x]
from FUNCT_2:sch 3(A6);
for
k being
Element of
NAT holds
S . k is
middle_volume of
f,
T . k
proof
let k be
Element of
NAT ;
S . k is middle_volume of f,T . k
consider H,
z being
FinSequence such that A19:
(
H = T . k &
z = S . k &
len H = len z )
and A20:
for
j being
Element of
NAT st
j in dom H holds
ex
rji being
Element of
REAL n ex
tji being
Element of
REAL st
(
tji in dom (f | (divset ((T . k),j))) &
(Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) &
rji = (f | (divset ((T . k),j))) . tji &
z . j = (vol (divset ((T . k),j))) * rji )
by A18;
A21:
now for x being Nat st x in dom H holds
ex rji being Element of REAL n st
( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji )let x be
Nat;
( x in dom H implies ex rji being Element of REAL n st
( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji ) )assume A22:
x in dom H
;
ex rji being Element of REAL n st
( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji )then reconsider j =
x as
Element of
NAT ;
consider rji being
Element of
REAL n,
tji being
Element of
REAL such that A23:
tji in dom (f | (divset ((T . k),j)))
and
(Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji)
and A24:
rji = (f | (divset ((T . k),j))) . tji
and A25:
z . j = (vol (divset ((T . k),j))) * rji
by A20, A22;
take rji =
rji;
( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji )thus
rji in rng (f | (divset ((T . k),x)))
by A23, A24, FUNCT_1:3;
z . x = (vol (divset ((T . k),x))) * rjithus
z . x = (vol (divset ((T . k),x))) * rji
by A25;
verum end;
thus
S . k is
middle_volume of
f,
T . k
by A19, A21, Def5;
verum
end; then reconsider S =
S as
middle_volume_Sequence of
f,
T by Def7;
set seq =
middle_sum (
f,
S);
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) ;
assume
(
delta T is
convergent &
lim (delta T) = 0 )
;
( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii )then
(
middle_sum (
f,
S) is
convergent &
lim (middle_sum (f,S)) = I )
by A3;
then consider rseqi being
Real_Sequence such that A26:
for
k being
Nat holds
(
rseqi . k = (xseq . k) . i &
rseqi is
convergent &
xs . i = lim rseqi )
by A4, REAL_NS1:11;
for
k being
Element of
NAT holds
rseqi . k = (middle_sum (((proj (i,n)) * f),Si)) . k
proof
let k be
Element of
NAT ;
rseqi . k = (middle_sum (((proj (i,n)) * f),Si)) . k
consider H,
z being
FinSequence such that A27:
H = T . k
and A28:
z = S . k
and A29:
len H = len z
and A30:
for
j being
Element of
NAT st
j in dom H holds
ex
rji being
Element of
REAL n ex
tji being
Element of
REAL st
(
tji in dom (f | (divset ((T . k),j))) &
(Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) &
rji = (f | (divset ((T . k),j))) . tji &
z . j = (vol (divset ((T . k),j))) * rji )
by A18;
dom (proj (i,n)) = REAL n
by FUNCT_2:def 1;
then
rng (S . k) c= dom (proj (i,n))
;
then A31:
dom ((proj (i,n)) * (S . k)) =
dom (S . k)
by RELAT_1:27
.=
Seg (len H)
by A28, A29, FINSEQ_1:def 3
.=
Seg (len (Si . k))
by A27, Def1
.=
dom (Si . k)
by FINSEQ_1:def 3
;
A32:
for
j being
Nat st
j in dom ((proj (i,n)) * (S . k)) holds
((proj (i,n)) * (S . k)) . j = (Si . k) . j
proof
let j0 be
Nat;
( j0 in dom ((proj (i,n)) * (S . k)) implies ((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0 )
reconsider j =
j0 as
Element of
NAT by ORDINAL1:def 12;
dom (proj (i,n)) = REAL n
by FUNCT_2:def 1;
then A33:
rng f c= dom (proj (i,n))
;
assume A34:
j0 in dom ((proj (i,n)) * (S . k))
;
((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0
then
j0 in Seg (len (Si . k))
by A31, FINSEQ_1:def 3;
then
j0 in Seg (len H)
by A27, Def1;
then
j in dom H
by FINSEQ_1:def 3;
then consider rji being
Element of
REAL n,
tji being
Element of
REAL such that A35:
tji in dom (f | (divset ((T . k),j)))
and A36:
(Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji)
and A37:
rji = (f | (divset ((T . k),j))) . tji
and A38:
z . j = (vol (divset ((T . k),j))) * rji
by A30;
A39:
dom (f | (divset ((T . k),j))) =
(dom f) /\ (divset ((T . k),j))
by RELAT_1:61
.=
(dom ((proj (i,n)) * f)) /\ (divset ((T . k),j))
by A33, RELAT_1:27
.=
dom (((proj (i,n)) * f) | (divset ((T . k),j)))
by RELAT_1:61
;
then
tji in (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j))
by A35, RELAT_1:61;
then A40:
tji in dom ((proj (i,n)) * f)
by XBOOLE_0:def 4;
A41:
(((proj (i,n)) * f) | (divset ((T . k),j))) . tji =
((proj (i,n)) * f) . tji
by A35, A39, FUNCT_1:47
.=
(proj (i,n)) . (f . tji)
by A40, FUNCT_1:12
.=
(proj (i,n)) . rji
by A35, A37, FUNCT_1:47
;
((proj (i,n)) * (S . k)) . j =
(proj (i,n)) . ((S . k) . j)
by A34, FUNCT_1:12
.=
((vol (divset ((T . k),j))) * rji) . i
by A28, A38, PDIFF_1:def 1
.=
(vol (divset ((T . k),j))) * (rji . i)
by RVSUM_1:44
.=
(Si . k) . j
by A36, A41, PDIFF_1:def 1
;
hence
((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0
;
verum
end;
consider Fi being
FinSequence of
REAL such that A42:
Fi = (proj (i,n)) * (S . k)
and A43:
(middle_sum (f,(S . k))) . i = Sum Fi
by A4, Def6;
thus rseqi . k =
(xseq . k) . i
by A26
.=
Sum Fi
by A43, Def8
.=
middle_sum (
((proj (i,n)) * f),
(Si . k))
by A31, A32, A42, FINSEQ_1:13
.=
(middle_sum (((proj (i,n)) * f),Si)) . k
by Def4
;
verum
end; hence
(
middle_sum (
((proj (i,n)) * f),
Si) is
convergent &
lim (middle_sum (((proj (i,n)) * f),Si)) = Ii )
by A26, FUNCT_2:63;
verum end;
(proj (i,n)) * f is
bounded
by A1, A4;
hence
(proj (i,n)) * f is
integrable
by A5, Th10;
verum end; hence
f is
integrable
;
verum end;
hence
( ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable )
; verum