let f be PartFunc of REAL,REAL; :: thesis: for a being Real
for A being non empty Subset of REAL st dom f = REAL & f is_improper_integrable_on_REAL & f is nonpositive holds
( improper_integral_on_REAL f = Integral (L-Meas,f) & ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = -infty ) )
let a be Real; :: thesis: for A being non empty Subset of REAL st dom f = REAL & f is_improper_integrable_on_REAL & f is nonpositive holds
( improper_integral_on_REAL f = Integral (L-Meas,f) & ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = -infty ) )
let A be non empty Subset of REAL; :: thesis: ( dom f = REAL & f is_improper_integrable_on_REAL & f is nonpositive implies ( improper_integral_on_REAL f = Integral (L-Meas,f) & ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = -infty ) ) )
assume that
A1: dom f = REAL and
A2: f is_improper_integrable_on_REAL and
A3: f is nonpositive ; :: thesis: ( improper_integral_on_REAL f = Integral (L-Meas,f) & ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = -infty ) )
A4: - f is_improper_integrable_on_REAL by A1, A2, INTEGR25:50;
A5: improper_integral_on_REAL (- f) = - (improper_integral_on_REAL f) by A1, A2, INTEGR25:50;
for x being object st x in dom (- f) holds
0 <= (- f) . x

proof

let x be object ; :: thesis: ( x in dom (- f) implies 0 <= (- f) . x )
assume x in dom (- f) ; :: thesis: 0 <= (- f) . x
then A6: f . x <= 0 by A3, MESFUNC6:53;
(- f) . x = - (f . x) by VALUED_1:8;
hence 0 <= (- f) . x by A6; :: thesis: verum

end;

then A7: - f is nonnegative by MESFUNC6:52;
REAL = ].-infty,+infty.[ by XXREAL_1:224;
then reconsider E = REAL as Element of L-Field by MEASUR10:5, MEASUR12:75;
A8: f is E -measurable by A1, A2, Th38;
A9: dom (- f) = dom f by VALUED_1:8;
then - (improper_integral_on_REAL f) = Integral (L-Meas,(- f)) by A1, A4, A5, A7, Th54;
then - (improper_integral_on_REAL f) = - (Integral (L-Meas,f)) by A1, A8, Th39;
hence improper_integral_on_REAL f = Integral (L-Meas,f) by XXREAL_3:10; :: thesis: ( ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = -infty ) )
A10: ( right_closed_halfline 0 c= dom f & left_closed_halfline 0 c= dom f ) by A1;

hereby :: thesis: ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = -infty )

assume f is infty_ext_Riemann_integrable ; :: thesis: f is_integrable_on L-Meas
then ( f is_+infty_ext_Riemann_integrable_on 0 & f is_-infty_ext_Riemann_integrable_on 0 ) by INTEGR10:def 9;
then ( (- 1) (#) f is_+infty_ext_Riemann_integrable_on 0 & (- 1) (#) f is_-infty_ext_Riemann_integrable_on 0 ) by A10, INTEGR10:9, INTEGR10:11;
then ( - f is_+infty_ext_Riemann_integrable_on 0 & - f is_-infty_ext_Riemann_integrable_on 0 ) by VALUED_1:def 6;
then - f is infty_ext_Riemann_integrable by INTEGR10:def 9;
then - f is_integrable_on L-Meas by A1, A4, A7, A9, Th54;
then (- 1) (#) (- f) is_integrable_on L-Meas by MESFUNC6:102;
hence f is_integrable_on L-Meas ; :: thesis: verum

end;

hereby :: thesis: verum

assume A11: not f is infty_ext_Riemann_integrable ; :: thesis: Integral (L-Meas,f) = -infty
A12: ( f is_-infty_improper_integrable_on 0 & f is_+infty_improper_integrable_on 0 ) by A1, A2, INTEGR25:36;
not ].-infty,0.] is empty by XXREAL_1:32;
then reconsider A1 = left_closed_halfline 0 as non empty Subset of REAL by LIMFUNC1:def 1;
not [.0,+infty.[ is empty by XXREAL_1:31;
then reconsider B1 = right_closed_halfline 0 as non empty Subset of REAL by LIMFUNC1:def 2;
A1 = ].-infty,0.] by LIMFUNC1:def 1;
then reconsider A1 = A1 as Element of L-Field by MEASUR10:5, MEASUR12:75;
B1 = [.0,+infty.[ by LIMFUNC1:def 2;
then reconsider B1 = B1 as Element of L-Field by MEASUR10:5, MEASUR12:75;

per cases ( not f is_+infty_ext_Riemann_integrable_on 0 or not f is_-infty_ext_Riemann_integrable_on 0 ) by A11, INTEGR10:def 9;

suppose not f is_+infty_ext_Riemann_integrable_on 0 ; :: thesis: Integral (L-Meas,f) = -infty

then A13: Integral (L-Meas,(f | B1)) = -infty by A12, A3, A1, Th50;
Integral (L-Meas,(f | B1)) >= Integral (L-Meas,(f | E)) by A1, A3, A2, Th38, Th40;
hence Integral (L-Meas,f) = -infty by A13, XXREAL_0:6; :: thesis: verum

end;

suppose not f is_-infty_ext_Riemann_integrable_on 0 ; :: thesis: Integral (L-Meas,f) = -infty

then A14: Integral (L-Meas,(f | A1)) = -infty by A12, A3, A1, Th48;
Integral (L-Meas,(f | A1)) >= Integral (L-Meas,(f | E)) by A1, A3, A2, Th38, Th40;
hence Integral (L-Meas,f) = -infty by A14, XXREAL_0:6; :: thesis: verum

end;

end;

end;