let n be Element of NAT ; :: thesis: for A being 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 closed-interval Subset of REAL ; :: thesis: 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); :: thesis: ( 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 AS:
f is bounded
; :: thesis: ( 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 :: thesis: ( 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 AS1:
f is
integrable
;
:: thesis: 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 )reconsider I =
integral f as
Element of
REAL n ;
take I =
I;
:: thesis: 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 PX04n, AS, AS1;
:: thesis: verum
end;
now 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 )
;
:: thesis: f is integrable then consider I being
Element of
REAL n such that P1:
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 let i be
Element of
NAT ;
:: thesis: ( i in Seg n implies (proj i,n) * f is integrable )assume AS1:
i in Seg n
;
:: thesis: (proj i,n) * f is integrable then P2:
(proj i,n) * f is
bounded
by AS, Defboundn;
reconsider Ii =
I . i as
Element of
REAL ;
now let T be
DivSequence of
A;
:: thesis: 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;
:: thesis: ( 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 ) )assume AS2:
(
delta T is
convergent &
lim (delta T) = 0 )
;
:: thesis: ( 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 ) ) );
A1:
for
k being
Element of
NAT ex
y being
Element of
(REAL n) * st
S1[
k,
y]
proof
let k be
Element of
NAT ;
:: thesis: ex y being Element of (REAL n) * st S1[k,y]
reconsider Tk =
T . k as
FinSequence by INTEGRA1:def 3;
reconsider Sik =
Si . k as
FinSequence of
REAL ;
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 ) );
PN:
for
j being
Nat st
j in Seg (len Tk) holds
ex
x being
Element of
REAL n st
S2[
j,
x]
proof
let j0 be
Nat;
:: thesis: ( j0 in Seg (len Tk) implies ex x being Element of REAL n st S2[j0,x] )
assume GGG:
j0 in Seg (len Tk)
;
:: thesis: ex x being Element of REAL n st S2[j0,x]
then reconsider j =
j0 as
Element of
NAT ;
j in dom Tk
by FINSEQ_1:def 3, GGG;
then consider r being
Element of
REAL such that PN1:
(
r in rng (((proj i,n) * f) | (divset (T . k),j)) &
(Si . k) . j = r * (vol (divset (T . k),j)) )
by defx0;
consider tji being
set such that PN2:
(
tji in dom (((proj i,n) * f) | (divset (T . k),j)) &
r = (((proj i,n) * f) | (divset (T . k),j)) . tji )
by PN1, FUNCT_1:def 5;
dom (proj i,n) = REAL n
by FUNCT_2:def 1;
then K1:
rng f c= dom (proj i,n)
;
K2:
dom (f | (divset (T . k),j)) =
(dom f) /\ (divset (T . k),j)
by RELAT_1:90
.=
(dom ((proj i,n) * f)) /\ (divset (T . k),j)
by K1, RELAT_1:46
.=
dom (((proj i,n) * f) | (divset (T . k),j))
by RELAT_1:90
;
tji in (dom ((proj i,n) * f)) /\ (divset (T . k),j)
by RELAT_1:90, PN2;
then reconsider tji =
tji as
Element of
REAL ;
(f | (divset (T . k),j)) . tji in rng (f | (divset (T . k),j))
by K2, PN2, FUNCT_1:12;
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
;
:: thesis: S2[j0,x]
thus
S2[
j0,
x]
by PN1, PN2, K2;
:: thesis: verum
end;
consider p being
FinSequence of
REAL n such that PN1:
(
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(PN);
reconsider x =
p as
Element of
(REAL n) * by FINSEQ_1:def 11;
take
x
;
:: thesis: S1[k,x]
AAA:
len p = len Tk
by PN1, FINSEQ_1:def 3;
now let jj0 be
Element of
NAT ;
:: thesis: ( 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 ) )assume AS0:
jj0 in dom Tk
;
:: thesis: 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 ;
dom Tk = Seg (len Tk)
by FINSEQ_1:def 3;
then
S2[
j0,
p . j0]
by PN1, AS0;
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 )
;
:: thesis: verum end;
hence
S1[
k,
x]
by AAA;
:: thesis: verum
end; consider S being
Function of
NAT ,
((REAL n) * ) such that A2:
for
x being
Element of
NAT holds
S1[
x,
S . x]
from FUNCT_2:sch 10(A1);
for
k being
Element of
NAT holds
S . k is
middle_volume of
f,
T . k
proof
let k be
Element of
NAT ;
:: thesis: S . k is middle_volume of f,T . k
consider H,
z being
FinSequence such that P1:
(
H = T . k &
z = S . k &
len H = len z & ( 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 A2;
E1:
S . k is
FinSequence of
REAL n
by FINSEQ_1:def 11;
now let x be
Nat;
:: thesis: ( 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 AA:
x in dom H
;
:: thesis: 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 AB:
(
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 AA, P1;
take rji =
rji;
:: thesis: ( 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 AB, FUNCT_1:12;
:: thesis: z . x = (vol (divset (T . k),x)) * rjithus
z . x = (vol (divset (T . k),x)) * rji
by AB;
:: thesis: verum end;
hence
S . k is
middle_volume of
f,
T . k
by E1, defxn0, P1;
:: thesis: verum
end; then reconsider S =
S as
middle_volume_Sequence of
f,
T by defxn2;
set x =
I;
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
Function of
NAT ,
(REAL n) ;
reconsider xs =
I as
Element of
REAL n ;
(
middle_sum f,
S is
convergent &
lim (middle_sum f,S) = I )
by AS2, P1;
then consider rseqi being
Real_Sequence such that R1:
for
k being
Element of
NAT holds
(
rseqi . k = (xseq . k) . i &
rseqi is
convergent &
xs . i = lim rseqi )
by REAL_NS1:11, AS1;
for
k being
Element of
NAT holds
rseqi . k = (middle_sum ((proj i,n) * f),Si) . k
proof
let k be
Element of
NAT ;
:: thesis: rseqi . k = (middle_sum ((proj i,n) * f),Si) . k
consider H,
z being
FinSequence such that PP1:
(
H = T . k &
z = S . k &
len H = len z & ( 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 A2;
dom (proj i,n) = REAL n
by FUNCT_2:def 1;
then
rng (S . k) c= dom (proj i,n)
;
then E1:
dom ((proj i,n) * (S . k)) =
dom (S . k)
by RELAT_1:46
.=
Seg (len H)
by PP1, FINSEQ_1:def 3
.=
Seg (len (Si . k))
by defx0, PP1
.=
dom (Si . k)
by FINSEQ_1:def 3
;
E2:
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;
:: thesis: ( j0 in dom ((proj i,n) * (S . k)) implies ((proj i,n) * (S . k)) . j0 = (Si . k) . j0 )
assume ASX:
j0 in dom ((proj i,n) * (S . k))
;
:: thesis: ((proj i,n) * (S . k)) . j0 = (Si . k) . j0
reconsider j =
j0 as
Element of
NAT by ORDINAL1:def 13;
j0 in Seg (len (Si . k))
by ASX, E1, FINSEQ_1:def 3;
then
j0 in Seg (len H)
by defx0, PP1;
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 U1:
(
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 PP1;
dom (proj i,n) = REAL n
by FUNCT_2:def 1;
then K1:
rng f c= dom (proj i,n)
;
K2:
dom (f | (divset (T . k),j)) =
(dom f) /\ (divset (T . k),j)
by RELAT_1:90
.=
(dom ((proj i,n) * f)) /\ (divset (T . k),j)
by K1, RELAT_1:46
.=
dom (((proj i,n) * f) | (divset (T . k),j))
by RELAT_1:90
;
then
tji in (dom ((proj i,n) * f)) /\ (divset (T . k),j)
by U1, RELAT_1:90;
then K3:
tji in dom ((proj i,n) * f)
by XBOOLE_0:def 4;
V1:
(((proj i,n) * f) | (divset (T . k),j)) . tji =
((proj i,n) * f) . tji
by U1, K2, FUNCT_1:70
.=
(proj i,n) . (f . tji)
by FUNCT_1:22, K3
.=
(proj i,n) . rji
by U1, FUNCT_1:70
;
((proj i,n) * (S . k)) . j =
(proj i,n) . ((S . k) . j)
by FUNCT_1:22, ASX
.=
((vol (divset (T . k),j)) * rji) . i
by U1, PP1, PDIFF_1:def 1
.=
(vol (divset (T . k),j)) * (rji . i)
by RVSUM_1:66
.=
(Si . k) . j
by U1, V1, PDIFF_1:def 1
;
hence
((proj i,n) * (S . k)) . j0 = (Si . k) . j0
;
:: thesis: verum
end;
consider Fi being
FinSequence of
REAL such that P14:
(
Fi = (proj i,n) * (S . k) &
(middle_sum f,(S . k)) . i = Sum Fi )
by defxn1, AS1;
thus rseqi . k =
(xseq . k) . i
by R1
.=
Sum Fi
by defxn3, P14
.=
middle_sum ((proj i,n) * f),
(Si . k)
by E2, FINSEQ_1:17, E1, P14
.=
(middle_sum ((proj i,n) * f),Si) . k
by defx3
;
:: thesis: verum
end; hence
(
middle_sum ((proj i,n) * f),
Si is
convergent &
lim (middle_sum ((proj i,n) * f),Si) = Ii )
by R1, FUNCT_2:113;
:: thesis: verum end; hence
(proj i,n) * f is
integrable
by P2, PX05;
:: thesis: verum end; hence
f is
integrable
by Intablen;
:: thesis: 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 )
; :: thesis: verum