let A be non empty closed_interval Subset of REAL; for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )
let f be Function of A,REAL; for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )
let D be Division of A; for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )
let e be Real; ( f | A is bounded_below & 0 < e implies ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) )
assume that
A1:
f | A is bounded_below
and
A2:
0 < e
; ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )
defpred S1[ Nat, Real] means ex r being Element of REAL st
( r in rng (f | (divset (D,$1))) & $2 = r * (vol (divset (D,$1))) & (lower_volume (f,D)) . $1 <= $2 & $2 < ((lower_volume (f,D)) . $1) + e );
A3:
for k being Nat st k in Seg (len D) holds
ex x being Element of REAL st S1[k,x]
proof
let k be
Nat;
( k in Seg (len D) implies ex x being Element of REAL st S1[k,x] )
assume
k in Seg (len D)
;
ex x being Element of REAL st S1[k,x]
then A4:
k in dom D
by FINSEQ_1:def 3;
dom f = A
by FUNCT_2:def 1;
then
dom (f | (divset (D,k))) = divset (
D,
k)
by A4, INTEGRA1:8, RELAT_1:62;
then A5:
not
rng (f | (divset (D,k))) is
empty
by RELAT_1:42;
rng f is
bounded_below
by A1, INTEGRA1:11;
then A6:
rng (f | (divset (D,k))) is
bounded_below
by RELAT_1:70, XXREAL_2:44;
per cases
( vol (divset (D,k)) = 0 or vol (divset (D,k)) <> 0 )
;
suppose A7:
vol (divset (D,k)) = 0
;
ex x being Element of REAL st S1[k,x]consider r being
object such that A8:
r in rng (f | (divset (D,k)))
by A5;
reconsider r =
r as
Element of
REAL by A8;
reconsider x =
r * (vol (divset (D,k))) as
Element of
REAL by XREAL_0:def 1;
A9:
(lower_volume (f,D)) . k =
(lower_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k)))
by A4, INTEGRA1:def 7
.=
0
by A7
;
then
x < ((lower_volume (f,D)) . k) + e
by A2, A7;
hence
ex
x being
Element of
REAL st
S1[
k,
x]
by A7, A8, A9;
verum end; suppose A10:
vol (divset (D,k)) <> 0
;
ex x being Element of REAL st S1[k,x]set l =
lower_bound (rng (f | (divset (D,k))));
set e1 =
e / (vol (divset (D,k)));
A11:
0 < vol (divset (D,k))
by A10, INTEGRA1:9;
then
0 < e / (vol (divset (D,k)))
by A2, XREAL_1:139;
then consider r being
Real such that A12:
r in rng (f | (divset (D,k)))
and A13:
r < (lower_bound (rng (f | (divset (D,k))))) + (e / (vol (divset (D,k))))
by A6, A5, SEQ_4:def 2;
A14:
(lower_volume (f,D)) . k = (lower_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k)))
by A4, INTEGRA1:def 7;
reconsider x =
r * (vol (divset (D,k))) as
Element of
REAL by XREAL_0:def 1;
x < ((lower_bound (rng (f | (divset (D,k))))) + (e / (vol (divset (D,k))))) * (vol (divset (D,k)))
by A11, A13, XREAL_1:68;
then
x < ((lower_volume (f,D)) . k) + ((e / (vol (divset (D,k)))) * (vol (divset (D,k))))
by A14;
then A15:
x < ((lower_volume (f,D)) . k) + e
by A10, XCMPLX_1:87;
lower_bound (rng (f | (divset (D,k)))) <= r
by A6, A12, SEQ_4:def 2;
then
(lower_volume (f,D)) . k <= x
by A11, A14, XREAL_1:64;
hence
ex
x being
Element of
REAL st
S1[
k,
x]
by A12, A15;
verum end; end;
end;
consider p being FinSequence of REAL such that
A16:
( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds
S1[k,p . k] ) )
from FINSEQ_1:sch 5(A3);
A17:
now for i being Nat st i in dom D holds
ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) )let i be
Nat;
( i in dom D implies ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) )assume
i in dom D
;
ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) )then
i in Seg (len D)
by FINSEQ_1:def 3;
then consider r being
Element of
REAL such that A18:
(
r in rng (f | (divset (D,i))) &
p . i = r * (vol (divset (D,i))) )
and
(lower_volume (f,D)) . i <= p . i
and
p . i < ((lower_volume (f,D)) . i) + e
by A16;
take r =
r;
( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) )thus
(
r in rng (f | (divset (D,i))) &
p . i = r * (vol (divset (D,i))) )
by A18;
verum end;
len p = len D
by A16, FINSEQ_1:def 3;
then reconsider p = p as middle_volume of f,D by A17, Def1;
now for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e )let i be
Nat;
( i in dom D implies ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) )assume
i in dom D
;
( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e )then
i in Seg (len D)
by FINSEQ_1:def 3;
then
ex
r being
Element of
REAL st
(
r in rng (f | (divset (D,i))) &
p . i = r * (vol (divset (D,i))) &
(lower_volume (f,D)) . i <= p . i &
p . i < ((lower_volume (f,D)) . i) + e )
by A16;
hence
(
(lower_volume (f,D)) . i <= p . i &
p . i < ((lower_volume (f,D)) . i) + e )
;
verum end;
hence
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )
; verum