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
ext_right_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 ext_right_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
; ext_right_integral (f,a,b) = integral (f,a,b)
reconsider AB = [.a,b.[ as non empty Subset of REAL by A1, XXREAL_1:3;
deffunc H1( Element of AB) -> Element of REAL = In ((integral (f,a,$1)),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
( r < b & ( for r1 being Real st r < r1 & r1 < b & 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
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1 ) ) )
assume
0 < g1
;
ex r being Real st
( r < b & ( for r1 being Real st r < r1 & r1 < b & 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:
(b - r) * M < g1
by A1, A10, Th1;
reconsider r =
r as
Real ;
take
r
;
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1 ) )
thus
r < b
by A13;
for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1
now for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
|.((Intf . r1) - (integral (f,a,b))).| < g1let r1 be
Real;
( r < r1 & r1 < b & r1 in dom Intf implies |.((Intf . r1) - (integral (f,a,b))).| < g1 )assume that A15:
r < r1
and A16:
r1 < b
and
r1 in dom Intf
;
|.((Intf . r1) - (integral (f,a,b))).| < g1A17:
a <= r1
by A12, A15, XXREAL_0:2;
then reconsider rr =
r1 as
Element of
AB by A16, XXREAL_1:3;
A18:
Intf . r1 = H1(
rr)
by A5;
r1 in [.a,b.]
by A16, XXREAL_1:1, A17;
then A19:
r1 in ['a,b']
by A1, INTEGRA5:def 3;
b - r1 < b - r
by A15, XREAL_1:15;
then A20:
M * (b - r1) < M * (b - r)
by A10, XREAL_1:68;
A21:
['a,b'] = [.a,b.]
by A1, INTEGRA5:def 3;
[.r1,b.] = ['r1,b']
by A16, INTEGRA5:def 3;
then
['r1,b'] c= ['a,b']
by A21, A17, XXREAL_1:34;
then A22:
for
x being
Real st
x in ['r1,b'] holds
|.(f . x).| <= M
by A8;
b in ['a,b']
by A1, A21, XXREAL_1:1;
then
|.(integral (f,r1,b)).| <= M * (b - r1)
by A1, A2, A3, A4, A16, A19, A22, INTEGRA6:23;
then A23:
|.(integral (f,r1,b)).| < M * (b - r)
by A20, 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,a,r1))).|
by A1, A2, A3, A4, A18, A19, INTEGRA6:17
.=
|.(integral (f,r1,b)).|
;
hence
|.((Intf . r1) - (integral (f,a,b))).| < g1
by A14, A23, XXREAL_0:2;
verum end;
hence
for
r1 being
Real st
r < r1 &
r1 < b &
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,a,x)
for r being Real st r < b holds
ex g being Real st
( r < g & g < b & g in dom Intf )
proof
let r be
Real;
( r < b implies ex g being Real st
( r < g & g < b & g in dom Intf ) )
assume A26:
r < b
;
ex g being Real st
( r < g & g < b & g in dom Intf )
end;
then A32:
Intf is_left_convergent_in b
by A11, LIMFUNC2:7;
then A33:
integral (f,a,b) = lim_left (Intf,b)
by A11, LIMFUNC2:41;
for d being Real st a <= d & d < b holds
( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded )
by A2, A3, A4, INTEGRA6:18;
then
f is_right_ext_Riemann_integrable_on a,b
by A6, A24, A32;
hence
ext_right_integral (f,a,b) = integral (f,a,b)
by A6, A24, A32, A33, Def3; verum