let f be PartFunc of REAL,REAL; :: thesis:
let a be Real; :: thesis:
let A be non empty Subset of REAL; :: thesis:
assume that
A1: right_closed_halfline a c= dom f and
A2: A = right_closed_halfline a and
A3: f is_+infty_improper_integrable_on a and
A4: f is nonnegative and
A5: not f is_+infty_ext_Riemann_integrable_on a ; :: thesis:
A6: for b being Real st a <= b holds
( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A3, INTEGR25:def 2;
A7: A = [.a,+infty.[ by A2, LIMFUNC1:def 2;
then reconsider A1 = A as Element of L-Field by MEASUR10:5, MEASUR12:75;
A8: R_EAL f is A1 -measurable by A1, A2, A7, A3, Th36, MESFUNC6:def 1;
A9: A1 = dom (f | A1) by A1, A2, RELAT_1:62;
then A1 = (dom f) /\ A1 by RELAT_1:61;
then A1 = (dom (R_EAL f)) /\ A1 by MESFUNC5:def 7;
then (R_EAL f) | A1 is A1 -measurable by A8, MESFUNC5:42;
then A10: R_EAL (f | A1) is A1 -measurable by Th16;
f | A1 is nonnegative by A4, MESFUNC6:55;
then A11: R_EAL (f | A1) is nonnegative by MESFUNC5:def 7;
A1 = dom (R_EAL (f | A1)) by A9, MESFUNC5:def 7;
then A12: integral+ (L-Meas,(max- (R_EAL (f | A1)))) < +infty by A10, A11, MESFUN11:53;
A13: A1 = dom (R_EAL (f | A1)) by A9, MESFUNC5:def 7;
consider E being SetSequence of L-Field such that
A14: ( ( for n being Nat holds E . n = [.a,(a + n).] ) & E is non-descending & E is convergent & Union E = [.a,+infty.[ ) by Th25;
A15: lim E = Union E by A14, SETLIM_1:80;
then A1 \ (lim E) = {} by A14, A7, XBOOLE_1:37;
then L-Meas . (A1 \ (lim E)) = 0 by VALUED_0:def 19;
then consider I being ExtREAL_sequence such that
A16: for n being Nat holds I . n = Integral (L-Meas,((R_EAL (f | A)) | ((Partial_Union E) . n))) and
I is convergent and
A17: Integral (L-Meas,(R_EAL (f | A))) = lim I by A10, A13, A12, A14, A7, A15, Th19;
consider Intf being PartFunc of REAL,REAL such that
A18: dom Intf = right_closed_halfline a and
A19: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
A20: ( Intf is convergent_in+infty or Intf is divergent_in+infty_to+infty or Intf is divergent_in+infty_to-infty ) by A3, INTEGR25:def 2;
A21: for x being Real st x in dom Intf holds
Intf . x >= 0

proof

let x be Real; :: thesis:
assume A22: x in dom Intf ; :: thesis:
then A23: ( a <= x & x < +infty ) by A18, A2, A7, XXREAL_1:3;
then reconsider AX = [.a,x.] as non empty closed_interval Subset of REAL by XXREAL_1:30, MEASURE5:def 3;
AX c= [.a,+infty.[ by A23, XXREAL_1:43;
then AX c= dom f by A1, A2, A7;
then dom (f | AX) = AX by RELAT_1:62;
then reconsider f1 = f | AX as Function of AX,REAL by FUNCT_2:def 1, RELSET_1:5;
A24: AX = ['a,x'] by A23, INTEGRA5:def 3;
then A25: f1 | AX is bounded by A23, A3, INTEGR25:def 2;
for r being Real st r in AX holds
f1 . r >= 0

proof

let r be Real; :: thesis:
assume A26: r in AX ; :: thesis:
f . r >= 0 by A4, MESFUNC6:51;
hence f1 . r >= 0 by A26, FUNCT_1:49; :: thesis:

end;

then integral f1 >= 0 by A25, INTEGRA2:32;
then integral (f,AX) >= 0 by INTEGRA5:def 2;
then integral (f,a,x) >= 0 by A23, A24, INTEGRA5:def 4;
hence Intf . x >= 0 by A19, A22; :: thesis:

end;

A27: now :: thesis:

assume A28: Intf is divergent_in+infty_to-infty ; :: thesis:
then consider r being Real such that
A29: for r1 being Real st r < r1 & r1 in dom Intf holds
Intf . r1 < 0 by LIMFUNC1:47;
consider r1 being Real such that
A30: ( r < r1 & r1 in dom Intf ) by A28, LIMFUNC1:47;
Intf . r1 < 0 by A29, A30;
hence contradiction by A21, A30; :: thesis:

end;

then A31: improper_integral_+infty (f,a) = +infty by A3, A18, A19, A20, A5, A6, INTEGR10:def 5, INTEGR25:def 4;
for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= I . m

proof

let g be Real; :: thesis:
assume 0 < g ; :: thesis:
consider r being Real such that
A32: for r1 being Real st r < r1 & r1 in dom Intf holds
g < Intf . r1 by A27, A18, A19, A20, A5, A6, INTEGR10:def 5, LIMFUNC1:46;
consider r1 being Real such that
A33: ( r < r1 & r1 in dom Intf ) by A27, A18, A19, A20, A5, A6, INTEGR10:def 5, LIMFUNC1:46;
g < Intf . r1 by A32, A33;
then A34: g < integral (f,a,r1) by A33, A19;
consider n being Nat such that
A35: r1 - a < n by SEQ_4:3;
A36: r1 < a + n by A35, XREAL_1:19;
take n ; :: thesis:
thus for m being Nat st n <= m holds
g <= I . m :: thesis:

proof

let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then a + n <= a + m by XREAL_1:6;
then A37: r1 < a + m by A36, XXREAL_0:2;
A38: a + m < +infty by XREAL_0:def 1, XXREAL_0:9;
A39: a <= a + m by XREAL_1:31;
then A40: ( f is_integrable_on ['a,(a + m)'] & f | ['a,(a + m)'] is bounded ) by A3, INTEGR25:def 2;
A41: ['a,(a + m)'] = [.a,(a + m).] by XREAL_1:31, INTEGRA5:def 3;
then ['a,(a + m)'] c= [.a,+infty.[ by A38, XXREAL_1:43;
then A42: ['a,(a + m)'] c= dom f by A1, A7, A2;
A43: ( a <= r1 & r1 < +infty ) by A33, A18, A2, A7, XXREAL_1:3;
then r1 in ['a,(a + m)'] by A37, A41, XXREAL_1:1;
then A44: integral (f,a,(a + m)) = (integral (f,a,r1)) + (integral (f,r1,(a + m))) by A39, A40, A42, INTEGRA6:17;
[.r1,(a + m).] c= [.a,+infty.[ by A43, A38, XXREAL_1:43;
then A45: [.r1,(a + m).] c= dom f by A1, A7, A2;
f | [.r1,(a + m).] is bounded by A40, A41, A43, XXREAL_1:34, RFUNCT_1:74;
then integral (f,r1,(a + m)) >= 0 by A4, A37, A45, Th12, MESFUNC6:55;
then A46: integral (f,a,r1) <= integral (f,a,(a + m)) by A44, XREAL_1:31;
A47: E . m = [.a,(a + m).] by A14;
(R_EAL (f | A)) | (E . m) = (f | A) | (E . m) by MESFUNC5:def 7;
then A48: (R_EAL (f | A)) | (E . m) = f | (E . m) by A47, A38, A7, XXREAL_1:43, RELAT_1:74;
A49: f || ['a,(a + m)'] is bounded by A39, A3, INTEGR25:def 2;
I . m = Integral (L-Meas,((R_EAL (f | A)) | ((Partial_Union E) . m))) by A16
.= Integral (L-Meas,((R_EAL (f | A)) | (E . m))) by A14, PROB_4:15
.= Integral (L-Meas,(R_EAL (f | (E . m)))) by A48, MESFUNC5:def 7
.= Integral (L-Meas,(f | (E . m))) by MESFUNC6:def 3
.= Integral (L-Meas,(f | [.a,(a + m).])) by A14
.= integral (f,a,(a + m)) by A49, A39, A41, A42, A3, INTEGR25:def 2, MESFUN14:50 ;
hence g <= I . m by A46, A34, XXREAL_0:2; :: thesis:

end;

then I is convergent_to_+infty by MESFUNC5:def 9;
then A50: Integral (L-Meas,(R_EAL (f | A))) = +infty by A17, MESFUNC5:def 12;
hence improper_integral_+infty (f,a) = Integral (L-Meas,(f | A)) by A31, MESFUNC6:def 3; :: thesis:
thus Integral (L-Meas,(f | A)) = +infty by A50, MESFUNC6:def 3; :: thesis: