let f be PartFunc of REAL,REAL; for a, c being Real st ].a,c.] c= dom f & f is_left_improper_integrable_on a,c & left_improper_integral (f,a,c) = ext_left_integral (f,a,c) holds
for b being Real st a < b & b <= c holds
( f is_left_improper_integrable_on a,b & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) )
let a, c be Real; ( ].a,c.] c= dom f & f is_left_improper_integrable_on a,c & left_improper_integral (f,a,c) = ext_left_integral (f,a,c) implies for b being Real st a < b & b <= c holds
( f is_left_improper_integrable_on a,b & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) ) )
assume that
A1:
].a,c.] c= dom f
and
A2:
f is_left_improper_integrable_on a,c
and
A3:
left_improper_integral (f,a,c) = ext_left_integral (f,a,c)
; for b being Real st a < b & b <= c holds
( f is_left_improper_integrable_on a,b & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) )
let b be Real; ( a < b & b <= c implies ( f is_left_improper_integrable_on a,b & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) ) )
assume A4:
( a < b & b <= c )
; ( f is_left_improper_integrable_on a,b & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) )
A5:
for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )
by A1, A2, A4, Lm7;
consider I being PartFunc of REAL,REAL such that
A6:
dom I = ].a,c.]
and
A7:
for x being Real st x in dom I holds
I . x = integral (f,x,c)
and
A8:
( I is_right_convergent_in a or I is_right_divergent_to+infty_in a or I is_right_divergent_to-infty_in a )
by A2;
reconsider AB = ].a,b.] as non empty Subset of REAL by A4, 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
A11:
for x being Element of AB holds Intf . x = H1(x)
from FUNCT_2:sch 4();
A12:
dom Intf = AB
by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
A13:
for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b)
proof
let x be
Real;
( x in dom Intf implies Intf . x = integral (f,x,b) )
assume
x in dom Intf
;
Intf . x = integral (f,x,b)
then
Intf . x = In (
(integral (f,x,b)),
REAL)
by A11, A12;
hence
Intf . x = integral (
f,
x,
b)
;
verum
end;
A14:
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 A15:
a < r
;
ex g being Real st
( g < r & a < g & g in dom Intf )
set R =
min (
b,
r);
consider g being
Real such that A16:
(
g < min (
b,
r) &
a < g &
g in dom I )
by A8, A9, A10, A15, A4, XXREAL_0:21, LIMFUNC2:10;
(
min (
b,
r)
<= b &
min (
b,
r)
<= r )
by XXREAL_0:17;
then A17:
(
g < b &
g < r )
by A16, XXREAL_0:2;
then
g in ].a,b.]
by A16, XXREAL_1:2;
hence
ex
g being
Real st
(
g < r &
a < g &
g in dom Intf )
by A12, A17, A16;
verum
end;
consider g being Real such that
A18:
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 I holds
|.((I . r1) - g).| < g1 ) )
by A8, A9, A10, LIMFUNC2:10;
set G = g - (integral (f,b,c));
A19:
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) - (g - (integral (f,b,c)))).| < 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) - (g - (integral (f,b,c)))).| < 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) - (g - (integral (f,b,c)))).| < g1 ) )
then consider r being
Real such that A20:
a < r
and A21:
for
r1 being
Real st
r1 < r &
a < r1 &
r1 in dom I holds
|.((I . r1) - g).| < g1
by A18;
set R =
min (
b,
r);
for
r1 being
Real st
r1 < min (
b,
r) &
a < r1 &
r1 in dom Intf holds
|.((Intf . r1) - (g - (integral (f,b,c)))).| < g1
proof
let r1 be
Real;
( r1 < min (b,r) & a < r1 & r1 in dom Intf implies |.((Intf . r1) - (g - (integral (f,b,c)))).| < g1 )
assume that A22:
r1 < min (
b,
r)
and A23:
a < r1
and A24:
r1 in dom Intf
;
|.((Intf . r1) - (g - (integral (f,b,c)))).| < g1
(
min (
b,
r)
<= r &
min (
b,
r)
<= b )
by XXREAL_0:17;
then A25:
(
r1 < r &
r1 < b )
by A22, XXREAL_0:2;
A26:
dom Intf c= dom I
by A4, A6, A12, XXREAL_1:42;
then A27:
|.((I . r1) - g).| < g1
by A25, A23, A21, A24;
A28:
r1 <= c
by A6, A24, A26, XXREAL_1:2;
then A29:
(
f is_integrable_on ['r1,c'] &
f | ['r1,c'] is
bounded )
by A2, A23;
A30:
[.r1,c.] = ['r1,c']
by A28, INTEGRA5:def 3;
then
['r1,c'] c= ].a,c.]
by A23, XXREAL_1:39;
then A31:
['r1,c'] c= dom f
by A1;
A32:
b in ['r1,c']
by A25, A4, A30, XXREAL_1:1;
(I . r1) - g =
(integral (f,r1,c)) - g
by A7, A24, A26
.=
((integral (f,r1,b)) + (integral (f,b,c))) - g
by A28, A29, A31, A32, INTEGRA6:17
.=
(integral (f,r1,b)) - (g - (integral (f,b,c)))
;
hence
|.((Intf . r1) - (g - (integral (f,b,c)))).| < g1
by A24, A27, A13;
verum
end;
hence
ex
r being
Real st
(
a < r & ( for
r1 being
Real st
r1 < r &
a < r1 &
r1 in dom Intf holds
|.((Intf . r1) - (g - (integral (f,b,c)))).| < g1 ) )
by A20, A4, XXREAL_0:21;
verum
end;
hence A33:
f is_left_improper_integrable_on a,b
by A12, A13, A14, A1, A2, A4, Lm7, LIMFUNC2:10; left_improper_integral (f,a,b) = ext_left_integral (f,a,b)
f is_left_ext_Riemann_integrable_on a,b
by A5, A12, A13, A14, A19, LIMFUNC2:10, INTEGR10:def 2;
hence
left_improper_integral (f,a,b) = ext_left_integral (f,a,b)
by A33, Th34; verum