let f be PartFunc of REAL,REAL; for a, b being Real st a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds
( f is_left_ext_Riemann_integrable_on a,b & ext_left_integral (f,a,b) = integral (f,a,b) )
let a, b be Real; ( a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies ( f is_left_ext_Riemann_integrable_on a,b & ext_left_integral (f,a,b) = integral (f,a,b) ) )
assume that
A1:
a < b
and
A2:
['a,b'] c= dom f
and
A3:
f is_integrable_on ['a,b']
and
A4:
f | ['a,b'] is bounded
; ( f is_left_ext_Riemann_integrable_on a,b & ext_left_integral (f,a,b) = integral (f,a,b) )
reconsider AB = ].a,b.] as non empty Subset of REAL by A1, XXREAL_1:2;
deffunc H1( Element of AB) -> Element of REAL = In ((integral (f,$1,b)),REAL);
consider Intf being Function of AB,REAL such that
A5:
for x being Element of AB holds Intf . x = H1(x)
from FUNCT_2:sch 4();
A6:
dom Intf = AB
by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
consider M0 being Real such that
A7:
for x being object st x in ['a,b'] /\ (dom f) holds
|.(f . x).| <= M0
by A4, RFUNCT_1:73;
reconsider M = M0 + 1 as Real ;
A8:
for x being Real st x in ['a,b'] holds
|.(f . x).| < M
a in { r where r is Real : ( a <= r & r <= b ) }
by A1;
then
a in [.a,b.]
by RCOMP_1:def 1;
then
a in ['a,b']
by A1, INTEGRA5:def 3;
then
|.(f . a).| < M
by A8;
then A10:
0 < M
by COMPLEX1:46;
A11:
for g1 being Real st 0 < g1 holds
ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1 ) )
proof
let g1 be
Real;
( 0 < g1 implies ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1 ) ) )
assume
0 < g1
;
ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1 ) )
then consider r being
Real such that A12:
a < r
and A13:
r < b
and A14:
(r - a) * M < g1
by A1, A10, INTEGR10:2;
take
r
;
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1 ) )
thus
a < r
by A12;
for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1
now for r1 being Real st a < r1 & r1 < r & r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1let r1 be
Real;
( a < r1 & r1 < r & r1 in dom Intf implies |.((Intf . r1) - (integral (f,a,b))).| < g1 )assume that A15:
a < r1
and A16:
r1 < r
and
r1 in dom Intf
;
|.((Intf . r1) - (integral (f,a,b))).| < g1
r1 < b
by A16, A13, XXREAL_0:2;
then reconsider rr =
r1 as
Element of
AB by A15, XXREAL_1:2;
A17:
Intf . r1 = H1(
rr)
by A5;
r1 - a < r - a
by A16, XREAL_1:14;
then A18:
M * (r1 - a) < M * (r - a)
by A10, XREAL_1:68;
A19:
['a,b'] = [.a,b.]
by A1, INTEGRA5:def 3;
A20:
r1 <= b
by A13, A16, XXREAL_0:2;
then A21:
r1 in ['a,b']
by A15, A19, XXREAL_1:1;
[.a,r1.] = ['a,r1']
by A15, INTEGRA5:def 3;
then
['a,r1'] c= ['a,b']
by A19, A20, XXREAL_1:34;
then A22:
for
x being
Real st
x in ['a,r1'] holds
|.(f . x).| <= M
by A8;
a in ['a,b']
by A1, A19, XXREAL_1:1;
then
|.(integral (f,a,r1)).| <= M * (r1 - a)
by A1, A2, A3, A4, A15, A21, A22, INTEGRA6:23;
then A23:
|.(integral (f,a,r1)).| < M * (r - a)
by A18, XXREAL_0:2;
|.((Intf . r1) - (integral (f,a,b))).| =
|.((integral (f,a,b)) - (Intf . r1)).|
by COMPLEX1:60
.=
|.(((integral (f,a,r1)) + (integral (f,r1,b))) - (integral (f,r1,b))).|
by A1, A2, A3, A4, A17, A21, INTEGRA6:17
.=
|.(integral (f,a,r1)).|
;
hence
|.((Intf . r1) - (integral (f,a,b))).| < g1
by A14, A23, XXREAL_0:2;
verum end;
hence
for
r1 being
Real st
r1 < r &
a < r1 &
r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1
;
verum
end;
A24:
for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b)
A26:
for r being Real st a < r holds
ex g being Real st
( g < r & a < g & g in dom Intf )
proof
let r be
Real;
( a < r implies ex g being Real st
( g < r & a < g & g in dom Intf ) )
assume A27:
a < r
;
ex g being Real st
( g < r & a < g & g in dom Intf )
end;
then A33:
Intf is_right_convergent_in a
by A11, LIMFUNC2:10;
then A34:
integral (f,a,b) = lim_right (Intf,a)
by A11, LIMFUNC2:42;
for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )
by A2, A3, A4, INTEGRA6:18;
hence
f is_left_ext_Riemann_integrable_on a,b
by A6, A24, A26, A11, LIMFUNC2:10, INTEGR10:def 2; ext_left_integral (f,a,b) = integral (f,a,b)
hence
ext_left_integral (f,a,b) = integral (f,a,b)
by A6, A24, A33, A34, INTEGR10:def 4; verum