let A be non empty closed_interval Subset of REAL; for f being Function of A,REAL st f is bounded holds
( f is integrable iff ex I being Real 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; ( f is bounded implies ( f is integrable iff ex I being Real 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 Real 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 Real 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 A2:
f is
integrable
;
ex I being Real 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
Real ;
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, Th9;
verum
end;
A3:
f | A is bounded
by A1;
now ( ex I being Real 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 )given I being
Real such that A4:
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 A5:
for
T being
DivSequence of
A st
delta T is
convergent &
lim (delta T) = 0 holds
lim (upper_sum (f,T)) = I
proof
let T be
DivSequence of
A;
( delta T is convergent & lim (delta T) = 0 implies lim (upper_sum (f,T)) = I )
set S = the
middle_volume_Sequence of
f,
T;
A6:
now for i being Nat holds 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . ilet i be
Nat;
0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . iA7:
i in NAT
by ORDINAL1:def 12;
(middle_sum (f, the middle_volume_Sequence of f,T)) . i <= (upper_sum (f,T)) . i
by A3, Th6, A7;
then
((middle_sum (f, the middle_volume_Sequence of f,T)) . i) - ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) <= ((upper_sum (f,T)) . i) - ((middle_sum (f, the middle_volume_Sequence of f,T)) . i)
by XREAL_1:9;
hence
0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i
by VALUED_1:15, A7;
verum end;
assume A8:
(
delta T is
convergent &
lim (delta T) = 0 )
;
lim (upper_sum (f,T)) = I
then A9:
upper_sum (
f,
T) is
convergent
by A3, INTEGRA4:9;
A10:
now for e1 being Real st 0 < e1 holds
(lim (upper_sum (f,T))) - I <= e1let e1 be
Real;
( 0 < e1 implies (lim (upper_sum (f,T))) - I <= e1 )reconsider e =
e1 as
Element of
REAL by XREAL_0:def 1;
assume
0 < e1
;
(lim (upper_sum (f,T))) - I <= e1then consider S being
middle_volume_Sequence of
f,
T such that A11:
for
i being
Element of
NAT holds
((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i
by A3, Th8;
A12:
now for i being Nat holds ((upper_sum (f,T)) - (middle_sum (f,S))) . i <= elet i be
Nat;
((upper_sum (f,T)) - (middle_sum (f,S))) . i <= eA13:
i in NAT
by ORDINAL1:def 12;
((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i
by A11, A13;
then
(((upper_sum (f,T)) . i) - e) + e <= ((middle_sum (f,S)) . i) + e
by XREAL_1:6;
then
((upper_sum (f,T)) . i) - ((middle_sum (f,S)) . i) <= (((middle_sum (f,S)) . i) + e) - ((middle_sum (f,S)) . i)
by XREAL_1:9;
hence
((upper_sum (f,T)) - (middle_sum (f,S))) . i <= e
by VALUED_1:15, A13;
verum end; A14:
middle_sum (
f,
S) is
convergent
by A4, A8;
then A15:
(upper_sum (f,T)) - (middle_sum (f,S)) is
convergent
by A9;
lim ((upper_sum (f,T)) - (middle_sum (f,S))) =
(lim (upper_sum (f,T))) - (lim (middle_sum (f,S)))
by A9, A14, SEQ_2:12
.=
(lim (upper_sum (f,T))) - I
by A4, A8
;
hence
(lim (upper_sum (f,T))) - I <= e1
by A12, A15, PREPOWER:2;
verum end;
A16:
middle_sum (
f, the
middle_volume_Sequence of
f,
T) is
convergent
by A4, A8;
then A17:
(upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T)) is
convergent
by A9;
lim ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) =
(lim (upper_sum (f,T))) - (lim (middle_sum (f, the middle_volume_Sequence of f,T)))
by A9, A16, SEQ_2:12
.=
(lim (upper_sum (f,T))) - I
by A4, A8
;
then
0 <= (lim (upper_sum (f,T))) - I
by A6, A17, SEQ_2:17;
then
(lim (upper_sum (f,T))) - I = 0
by A10, XREAL_1:5;
hence
lim (upper_sum (f,T)) = I
;
verum
end; A18:
for
T being
DivSequence of
A st
delta T is
convergent &
lim (delta T) = 0 holds
I = lim (lower_sum (f,T))
proof
let T be
DivSequence of
A;
( delta T is convergent & lim (delta T) = 0 implies I = lim (lower_sum (f,T)) )
set S = the
middle_volume_Sequence of
f,
T;
A19:
now for i being Nat holds 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . ilet i be
Nat;
0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . iA20:
i in NAT
by ORDINAL1:def 12;
(lower_sum (f,T)) . i <= (middle_sum (f, the middle_volume_Sequence of f,T)) . i
by A3, Th5, A20;
then
((lower_sum (f,T)) . i) - ((lower_sum (f,T)) . i) <= ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) - ((lower_sum (f,T)) . i)
by XREAL_1:9;
hence
0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i
by VALUED_1:15, A20;
verum end;
assume A21:
(
delta T is
convergent &
lim (delta T) = 0 )
;
I = lim (lower_sum (f,T))
then A22:
lower_sum (
f,
T) is
convergent
by A3, INTEGRA4:8;
A23:
now for e1 being Real st 0 < e1 holds
I - (lim (lower_sum (f,T))) <= e1let e1 be
Real;
( 0 < e1 implies I - (lim (lower_sum (f,T))) <= e1 )reconsider e =
e1 as
Element of
REAL by XREAL_0:def 1;
assume
0 < e1
;
I - (lim (lower_sum (f,T))) <= e1then consider S being
middle_volume_Sequence of
f,
T such that A24:
for
i being
Element of
NAT holds
(middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e
by A3, Th7;
A25:
now for i being Nat holds ((middle_sum (f,S)) - (lower_sum (f,T))) . i <= elet i be
Nat;
((middle_sum (f,S)) - (lower_sum (f,T))) . i <= eA26:
i in NAT
by ORDINAL1:def 12;
(middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e
by A24, A26;
then
((middle_sum (f,S)) . i) - ((lower_sum (f,T)) . i) <= (((lower_sum (f,T)) . i) + e) - ((lower_sum (f,T)) . i)
by XREAL_1:9;
hence
((middle_sum (f,S)) - (lower_sum (f,T))) . i <= e
by VALUED_1:15, A26;
verum end; A27:
middle_sum (
f,
S) is
convergent
by A4, A21;
then A28:
(middle_sum (f,S)) - (lower_sum (f,T)) is
convergent
by A22;
lim ((middle_sum (f,S)) - (lower_sum (f,T))) =
(lim (middle_sum (f,S))) - (lim (lower_sum (f,T)))
by A22, A27, SEQ_2:12
.=
I - (lim (lower_sum (f,T)))
by A4, A21
;
hence
I - (lim (lower_sum (f,T))) <= e1
by A25, A28, PREPOWER:2;
verum end;
A29:
middle_sum (
f, the
middle_volume_Sequence of
f,
T) is
convergent
by A4, A21;
then A30:
(middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T)) is
convergent
by A22;
lim ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) =
(lim (middle_sum (f, the middle_volume_Sequence of f,T))) - (lim (lower_sum (f,T)))
by A22, A29, SEQ_2:12
.=
I - (lim (lower_sum (f,T)))
by A4, A21
;
then
0 <= I - (lim (lower_sum (f,T)))
by A19, A30, SEQ_2:17;
then
I - (lim (lower_sum (f,T))) = 0
by A23, XREAL_1:5;
hence
I = lim (lower_sum (f,T))
;
verum
end; hence
f is
integrable
by A3, INTEGRA4:12;
verum end;
hence
( ex I being Real 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