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