let A be non empty closed_interval Subset of REAL; for Y being RealBanachSpace
for h being Function of A, the carrier of Y
for f being Function of A,REAL st h is bounded & h is integrable & f = ||.h.|| & f is integrable holds
||.(integral h).|| <= integral f
let Y be RealBanachSpace; for h being Function of A, the carrier of Y
for f being Function of A,REAL st h is bounded & h is integrable & f = ||.h.|| & f is integrable holds
||.(integral h).|| <= integral f
let h be Function of A, the carrier of Y; for f being Function of A,REAL st h is bounded & h is integrable & f = ||.h.|| & f is integrable holds
||.(integral h).|| <= integral f
let f be Function of A,REAL; ( h is bounded & h is integrable & f = ||.h.|| & f is integrable implies ||.(integral h).|| <= integral f )
assume A1:
( h is bounded & h is integrable & f = ||.h.|| & f is integrable )
; ||.(integral h).|| <= integral f
then A2:
f is bounded
by Th1914;
consider T being DivSequence of A such that
A3:
( delta T is convergent & lim (delta T) = 0 )
by INTEGRA4:11;
set S = the middle_volume_Sequence of h,T;
A4:
dom f = dom h
by A1, NORMSP_0:def 3;
defpred S1[ Element of NAT , set ] means ex p being FinSequence of REAL st
( p = $2 & len p = len (T . $1) & ( for i being Nat st i in dom (T . $1) holds
( p . i in dom (h | (divset ((T . $1),i))) & ex z being Point of Y st
( z = (h | (divset ((T . $1),i))) . (p . i) & ( the middle_volume_Sequence of h,T . $1) . i = (vol (divset ((T . $1),i))) * z ) ) ) );
A5:
for k being Element of NAT ex p being Element of REAL * st S1[k,p]
proof
let k be
Element of
NAT ;
ex p being Element of REAL * st S1[k,p]
defpred S2[
Nat,
set ]
means ( $2
in dom (h | (divset ((T . k),$1))) & ex
c being
Point of
Y st
(
c = (h | (divset ((T . k),$1))) . $2 &
( the middle_volume_Sequence of h,T . k) . $1
= (vol (divset ((T . k),$1))) * c ) );
A6:
Seg (len (T . k)) = dom (T . k)
by FINSEQ_1:def 3;
A7:
for
i being
Nat st
i in Seg (len (T . k)) holds
ex
x being
Element of
REAL st
S2[
i,
x]
proof
let i be
Nat;
( i in Seg (len (T . k)) implies ex x being Element of REAL st S2[i,x] )
assume
i in Seg (len (T . k))
;
ex x being Element of REAL st S2[i,x]
then
i in dom (T . k)
by FINSEQ_1:def 3;
then consider c being
Point of
Y such that A8:
(
c in rng (h | (divset ((T . k),i))) &
( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * c )
by INTEGR18:def 1;
consider x being
object such that A9:
(
x in dom (h | (divset ((T . k),i))) &
c = (h | (divset ((T . k),i))) . x )
by A8, FUNCT_1:def 3;
(
x in dom h &
x in divset (
(T . k),
i) )
by A9, RELAT_1:57;
then reconsider x =
x as
Element of
REAL ;
take
x
;
S2[i,x]
thus
S2[
i,
x]
by A8, A9;
verum
end;
consider p being
FinSequence of
REAL such that A10:
(
dom p = Seg (len (T . k)) & ( for
i being
Nat st
i in Seg (len (T . k)) holds
S2[
i,
p . i] ) )
from FINSEQ_1:sch 5(A7);
take
p
;
( p is Element of REAL * & S1[k,p] )
len p = len (T . k)
by A10, FINSEQ_1:def 3;
hence
(
p is
Element of
REAL * &
S1[
k,
p] )
by A10, A6, FINSEQ_1:def 11;
verum
end;
consider F being sequence of (REAL *) such that
A11:
for x being Element of NAT holds S1[x,F . x]
from FUNCT_2:sch 3(A5);
defpred S2[ Element of NAT , set ] means ex q being middle_volume of f,T . $1 st
( q = $2 & ( for i being Nat st i in dom (T . $1) holds
ex z being Element of REAL st
( (F . $1) . i in dom (f | (divset ((T . $1),i))) & z = (f | (divset ((T . $1),i))) . ((F . $1) . i) & q . i = (vol (divset ((T . $1),i))) * z ) ) );
A12:
for k being Element of NAT ex y being Element of REAL * st S2[k,y]
proof
let k be
Element of
NAT ;
ex y being Element of REAL * st S2[k,y]
defpred S3[
Nat,
set ]
means ex
c being
Element of
REAL st
(
(F . k) . $1
in dom (f | (divset ((T . k),$1))) &
c = (f | (divset ((T . k),$1))) . ((F . k) . $1) & $2
= (vol (divset ((T . k),$1))) * c );
A13:
Seg (len (T . k)) = dom (T . k)
by FINSEQ_1:def 3;
A14:
for
i being
Nat st
i in Seg (len (T . k)) holds
ex
x being
Element of
REAL st
S3[
i,
x]
proof
let i be
Nat;
( i in Seg (len (T . k)) implies ex x being Element of REAL st S3[i,x] )
assume
i in Seg (len (T . k))
;
ex x being Element of REAL st S3[i,x]
then A15:
i in dom (T . k)
by FINSEQ_1:def 3;
consider p being
FinSequence of
REAL such that A16:
(
p = F . k &
len p = len (T . k) & ( for
i being
Nat st
i in dom (T . k) holds
(
p . i in dom (h | (divset ((T . k),i))) & ex
z being
Point of
Y st
(
z = (h | (divset ((T . k),i))) . (p . i) &
( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) ) ) )
by A11;
p . i in dom (h | (divset ((T . k),i)))
by A15, A16;
then A171:
(
p . i in dom h &
p . i in divset (
(T . k),
i) )
by RELAT_1:57;
(
(vol (divset ((T . k),i))) * ((f | (divset ((T . k),i))) . (p . i)) in REAL &
(f | (divset ((T . k),i))) . (p . i) in REAL )
by XREAL_0:def 1;
hence
ex
x being
Element of
REAL st
S3[
i,
x]
by A16, A171, A4, RELAT_1:57;
verum
end;
consider q being
FinSequence of
REAL such that A18:
(
dom q = Seg (len (T . k)) & ( for
i being
Nat st
i in Seg (len (T . k)) holds
S3[
i,
q . i] ) )
from FINSEQ_1:sch 5(A14);
A19:
len q = len (T . k)
by A18, FINSEQ_1:def 3;
then reconsider q =
q as
middle_volume of
f,
T . k by A19, INTEGR15:def 1;
q is
Element of
REAL *
by FINSEQ_1:def 11;
hence
ex
y being
Element of
REAL * st
S2[
k,
y]
by A13, A18;
verum
end;
consider Sf being sequence of (REAL *) such that
A21:
for x being Element of NAT holds S2[x,Sf . x]
from FUNCT_2:sch 3(A12);
then reconsider Sf = Sf as middle_volume_Sequence of f,T by INTEGR15:def 3;
A22:
( middle_sum (f,Sf) is convergent & lim (middle_sum (f,Sf)) = integral f )
by A1, A2, A3, INTEGR15:9;
A23:
( middle_sum (h, the middle_volume_Sequence of h,T) is convergent & lim (middle_sum (h, the middle_volume_Sequence of h,T)) = integral h )
by A1, A3, INTEGR18:def 6;
A24:
for k being Element of NAT holds ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k
proof
let k be
Element of
NAT ;
||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k
A25:
(middle_sum (f,Sf)) . k = middle_sum (
f,
(Sf . k))
by INTEGR15:def 4;
A28:
ex
p being
FinSequence of
REAL st
(
p = F . k &
len p = len (T . k) & ( for
i being
Nat st
i in dom (T . k) holds
(
p . i in dom (h | (divset ((T . k),i))) & ex
z being
Point of
Y st
(
z = (h | (divset ((T . k),i))) . (p . i) &
( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) ) ) )
by A11;
A29:
ex
q being
middle_volume of
f,
T . k st
(
q = Sf . k & ( for
i being
Nat st
i in dom (T . k) holds
ex
z being
Element of
REAL st
(
(F . k) . i in dom (f | (divset ((T . k),i))) &
z = (f | (divset ((T . k),i))) . ((F . k) . i) &
q . i = (vol (divset ((T . k),i))) * z ) ) )
by A21;
A30:
len (Sf . k) = len (T . k)
by INTEGR15:def 1;
A31:
len ( the middle_volume_Sequence of h,T . k) = len (T . k)
by INTEGR18:def 1;
now for i being Nat st i in dom ( the middle_volume_Sequence of h,T . k) holds
||.(( the middle_volume_Sequence of h,T . k) /. i).|| <= (Sf . k) . ilet i be
Nat;
( i in dom ( the middle_volume_Sequence of h,T . k) implies ||.(( the middle_volume_Sequence of h,T . k) /. i).|| <= (Sf . k) . i )assume A32:
i in dom ( the middle_volume_Sequence of h,T . k)
;
||.(( the middle_volume_Sequence of h,T . k) /. i).|| <= (Sf . k) . ithen
i in Seg (len (T . k))
by A31, FINSEQ_1:def 3;
then A34:
i in dom (T . k)
by FINSEQ_1:def 3;
then A36:
(F . k) . i in dom (h | (divset ((T . k),i)))
by A28;
consider z being
Point of
Y such that A37:
(
z = (h | (divset ((T . k),i))) . ((F . k) . i) &
( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z )
by A28, A34;
A38:
ex
w being
Element of
REAL st
(
(F . k) . i in dom (f | (divset ((T . k),i))) &
w = (f | (divset ((T . k),i))) . ((F . k) . i) &
(Sf . k) . i = (vol (divset ((T . k),i))) * w )
by A29, A34;
( the middle_volume_Sequence of h,T . k) . i = ( the middle_volume_Sequence of h,T . k) /. i
by A32, PARTFUN1:def 6;
then A41:
||.(( the middle_volume_Sequence of h,T . k) /. i).|| =
|.(vol (divset ((T . k),i))).| * ||.z.||
by A37, NORMSP_1:def 1
.=
(vol (divset ((T . k),i))) * ||.z.||
by INTEGRA1:9, ABSVALUE:def 1
;
A42:
(
dom (h | (divset ((T . k),i))) c= dom h &
dom (f | (divset ((T . k),i))) c= dom f )
by RELAT_1:60;
A43:
(h | (divset ((T . k),i))) . ((F . k) . i) = h . ((F . k) . i)
by A36, FUNCT_1:47;
(f | (divset ((T . k),i))) . ((F . k) . i) =
f . ((F . k) . i)
by A38, FUNCT_1:47
.=
||.(h /. ((F . k) . i)).||
by A42, A1, A38, NORMSP_0:def 2
;
hence
||.(( the middle_volume_Sequence of h,T . k) /. i).|| <= (Sf . k) . i
by A41, A43, A38, A37, A42, A36, PARTFUN1:def 6;
verum end;
then
||.(middle_sum (h,( the middle_volume_Sequence of h,T . k))).|| <= Sum (Sf . k)
by A30, A31, INTEGR20:10;
hence
||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k
by A25, INTEGR18:def 4;
verum
end;
A45:
now for i being Nat holds ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i <= (middle_sum (f,Sf)) . ilet i be
Nat;
||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i <= (middle_sum (f,Sf)) . iXX:
i in NAT
by ORDINAL1:def 12;
||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i = ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . i).||
by NORMSP_0:def 4;
hence
||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i <= (middle_sum (f,Sf)) . i
by A24, XX;
verum end;
||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| is convergent
by A1, A3, NORMSP_1:23;
then
lim ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| <= lim (middle_sum (f,Sf))
by A45, A22, SEQ_2:18;
hence
||.(integral h).|| <= integral f
by A22, A23, LOPBAN_1:41; verum