let f be PartFunc of REAL,REAL; :: thesis: for b being Real st left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b & abs f is_-infty_ext_Riemann_integrable_on b holds
max+ f is_-infty_ext_Riemann_integrable_on b
let b be Real; :: thesis: ( left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b & abs f is_-infty_ext_Riemann_integrable_on b implies max+ f is_-infty_ext_Riemann_integrable_on b )
assume that
A1: left_closed_halfline b c= dom f and
A2: f is_-infty_ext_Riemann_integrable_on b and
A3: abs f is_-infty_ext_Riemann_integrable_on b ; :: thesis: max+ f is_-infty_ext_Riemann_integrable_on b
A4: b in REAL by XREAL_0:def 1;
A5: left_closed_halfline b = ].-infty,b.] by LIMFUNC1:def 1;
set G = infty_ext_left_integral (f,b);
set AG = infty_ext_left_integral ((abs f),b);
consider I being PartFunc of REAL,REAL such that
A6: dom I = left_closed_halfline b and
A7: for x being Real st x in dom I holds
I . x = integral (f,x,b) and
A8: I is convergent_in-infty and
A9: infty_ext_left_integral (f,b) = lim_in-infty I by A2, INTEGR10:def 8;
consider AI being PartFunc of REAL,REAL such that
A10: dom AI = left_closed_halfline b and
A11: for x being Real st x in dom AI holds
AI . x = integral ((abs f),x,b) and
A12: AI is convergent_in-infty and
A13: infty_ext_left_integral ((abs f),b) = lim_in-infty AI by A3, INTEGR10:def 8;
A14: for d being Real st d <= b holds
( max+ f is_integrable_on ['d,b'] & (max+ f) | ['d,b'] is bounded )
proof
let d be Real; :: thesis: ( d <= b implies ( max+ f is_integrable_on ['d,b'] & (max+ f) | ['d,b'] is bounded ) )
assume A15: d <= b ; :: thesis: ( max+ f is_integrable_on ['d,b'] & (max+ f) | ['d,b'] is bounded )
then A16: ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A2, INTEGR10:def 6;
A17: (f || ['d,b']) | ['d,b'] is bounded by A15, A2, INTEGR10:def 6;
A18: d in REAL by XREAL_0:def 1;
['d,b'] = [.d,b.] by A15, INTEGRA5:def 3;
then ['d,b'] c= ].-infty,b.] by A18, XXREAL_0:12, XXREAL_1:39;
then A19: ['d,b'] c= dom f by A1, A5;
then A20: dom (f || ['d,b']) = ['d,b'] by RELAT_1:62;
A21: max+ (f || ['d,b']) = max+ (f | ['d,b']) by A19, Th59
.= (max+ f) || ['d,b'] by MESFUNC6:66 ;
A22: f || ['d,b'] is Function of ['d,b'],REAL by A20, FUNCT_2:67;
f || ['d,b'] is integrable by A15, A2, INTEGR10:def 6, INTEGRA5:def 1;
hence max+ f is_integrable_on ['d,b'] by A21, A17, A22, INTEGRA4:20, INTEGRA5:def 1; :: thesis: (max+ f) | ['d,b'] is bounded
f | ['d,b'] is bounded_above by A16, SEQ_2:def 8;
then ( (max+ f) | ['d,b'] is bounded_above & (max+ f) | ['d,b'] is bounded_below ) by INTEGRA4:14, INTEGRA4:15;
hence (max+ f) | ['d,b'] is bounded by SEQ_2:def 8; :: thesis: verum
end;
ex Intf being PartFunc of REAL,REAL st
( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral ((max+ f),x,b) ) & Intf is convergent_in-infty )
proof
reconsider A = ].-infty,b.] as non empty Subset of REAL by A4, XXREAL_0:12, XXREAL_1:32;
deffunc H1( Element of A) -> Element of REAL = In ((integral ((max+ f),$1,b)),REAL);
consider Intf being Function of A,REAL such that
A23: for x being Element of A holds Intf . x = H1(x) from FUNCT_2:sch 4();
 A24: dom Intf = A by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
take Intf ; :: thesis: ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral ((max+ f),x,b) ) & Intf is convergent_in-infty )
A25: for x being Real st x in dom Intf holds
Intf . x = integral ((max+ f),x,b)
proof
let x be Real; :: thesis: ( x in dom Intf implies Intf . x = integral ((max+ f),x,b) )
assume x in dom Intf ; :: thesis: Intf . x = integral ((max+ f),x,b)
then x is Element of A by FUNCT_2:def 1;
then Intf . x = In ((integral ((max+ f),x,b)),REAL) by A23;
hence Intf . x = integral ((max+ f),x,b) ; :: thesis: verum
end;
A26: for r being Real ex g being Real st
( g < r & g in dom Intf ) by A5, A6, A8, A24, LIMFUNC1:45;
for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r1 < r & r1 in dom Intf holds
|.((Intf . r1) - (((infty_ext_left_integral (f,b)) + (infty_ext_left_integral ((abs f),b))) / 2)).| < g1
proof
let g1 be Real; :: thesis: ( 0 < g1 implies ex r being Real st
for r1 being Real st r1 < r & r1 in dom Intf holds
|.((Intf . r1) - (((infty_ext_left_integral (f,b)) + (infty_ext_left_integral ((abs f),b))) / 2)).| < g1 )
assume A27: 0 < g1 ; :: thesis: ex r being Real st
for r1 being Real st r1 < r & r1 in dom Intf holds
|.((Intf . r1) - (((infty_ext_left_integral (f,b)) + (infty_ext_left_integral ((abs f),b))) / 2)).| < g1
then consider R1 being Real such that
A28: for r1 being Real st r1 < R1 & r1 in dom I holds
|.((I . r1) - (infty_ext_left_integral (f,b))).| < g1 by A8, A9, LIMFUNC1:78;
consider R2 being Real such that
A29: for r1 being Real st r1 < R2 & r1 in dom AI holds
|.((AI . r1) - (infty_ext_left_integral ((abs f),b))).| < g1 by A12, A13, A27, LIMFUNC1:78;
set RR1 = min (b,R1);
set RR2 = min (b,R2);
take R = min ((min (b,R1)),(min (b,R2))); :: thesis: for r1 being Real st r1 < R & r1 in dom Intf holds
|.((Intf . r1) - (((infty_ext_left_integral (f,b)) + (infty_ext_left_integral ((abs f),b))) / 2)).| < g1
hereby :: thesis: verum
let r1 be Real; :: thesis: ( r1 < R & r1 in dom Intf implies |.((Intf . r1) - (((infty_ext_left_integral (f,b)) + (infty_ext_left_integral ((abs f),b))) / 2)).| < g1 )
assume A30: ( r1 < R & r1 in dom Intf ) ; :: thesis: |.((Intf . r1) - (((infty_ext_left_integral (f,b)) + (infty_ext_left_integral ((abs f),b))) / 2)).| < g1
A31: r1 in REAL by XREAL_0:def 1;
( b >= min (b,R1) & R1 >= min (b,R1) & R2 >= min (b,R2) & min (b,R1) >= R & min (b,R2) >= R ) by XXREAL_0:17;
then ( b >= R & R1 >= R & R2 >= R ) by XXREAL_0:2;
then A32: ( b > r1 & R1 > r1 & R2 > r1 ) by A30, XXREAL_0:2;
[.r1,b.] c= ].-infty,b.] by A31, XXREAL_0:12, XXREAL_1:39;
then A33: [.r1,b.] c= dom f by A1, A5;
( f is_integrable_on ['r1,b'] & f | ['r1,b'] is bounded ) by A32, A2, INTEGR10:def 6;
then 2 * (integral ((max+ f),r1,b)) = (integral (f,r1,b)) + (integral ((abs f),r1,b)) by A32, A33, Th62;
then 2 * (Intf . r1) = (integral (f,r1,b)) + (integral ((abs f),r1,b)) by A25, A30;
then 2 * (Intf . r1) = (I . r1) + (integral ((abs f),r1,b)) by A5, A30, A24, A6, A7;
then 2 * (Intf . r1) = (I . r1) + (AI . r1) by A5, A30, A24, A10, A11;
then (Intf . r1) - (((infty_ext_left_integral (f,b)) + (infty_ext_left_integral ((abs f),b))) / 2) = (((I . r1) - (infty_ext_left_integral (f,b))) + ((AI . r1) - (infty_ext_left_integral ((abs f),b)))) / 2 ;
then A34: |.((Intf . r1) - (((infty_ext_left_integral (f,b)) + (infty_ext_left_integral ((abs f),b))) / 2)).| = |.(((I . r1) - (infty_ext_left_integral (f,b))) + ((AI . r1) - (infty_ext_left_integral ((abs f),b)))).| / |.2.| by COMPLEX1:67
.= |.(((I . r1) - (infty_ext_left_integral (f,b))) + ((AI . r1) - (infty_ext_left_integral ((abs f),b)))).| / 2 by ABSVALUE:def 1 ;
A35: |.(((I . r1) - (infty_ext_left_integral (f,b))) + ((AI . r1) - (infty_ext_left_integral ((abs f),b)))).| <= |.((I . r1) - (infty_ext_left_integral (f,b))).| + |.((AI . r1) - (infty_ext_left_integral ((abs f),b))).| by COMPLEX1:56;
( |.((I . r1) - (infty_ext_left_integral (f,b))).| < g1 & |.((AI . r1) - (infty_ext_left_integral ((abs f),b))).| < g1 ) by A5, A6, A10, A24, A28, A29, A32, A30;
then |.((I . r1) - (infty_ext_left_integral (f,b))).| + |.((AI . r1) - (infty_ext_left_integral ((abs f),b))).| < g1 + g1 by XREAL_1:8;
then |.(((I . r1) - (infty_ext_left_integral (f,b))) + ((AI . r1) - (infty_ext_left_integral ((abs f),b)))).| < 2 * g1 by A35, XXREAL_0:2;
then |.((Intf . r1) - (((infty_ext_left_integral (f,b)) + (infty_ext_left_integral ((abs f),b))) / 2)).| < (2 * g1) / 2 by A34, XREAL_1:74;
hence |.((Intf . r1) - (((infty_ext_left_integral (f,b)) + (infty_ext_left_integral ((abs f),b))) / 2)).| < g1 ; :: thesis: verum
end;
end;
hence ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral ((max+ f),x,b) ) & Intf is convergent_in-infty ) by A5, A25, A26, LIMFUNC1:45, FUNCT_2:def 1; :: thesis: verum
end;
hence max+ f is_-infty_ext_Riemann_integrable_on b by A14, INTEGR10:def 6; :: thesis: verum