let f be PartFunc of REAL,REAL; :: thesis: ( dom f = REAL & f is_improper_integrable_on_REAL & abs f is infty_ext_Riemann_integrable implies ( f is_integrable_on L-Meas & improper_integral_on_REAL f = Integral (L-Meas,f) ) )
assume that
A1: dom f = REAL and
A2: f is_improper_integrable_on_REAL and
A3: abs f is infty_ext_Riemann_integrable ; :: thesis: ( f is_integrable_on L-Meas & improper_integral_on_REAL f = Integral (L-Meas,f) )
A4: ( abs f is_+infty_ext_Riemann_integrable_on 0 & abs f is_-infty_ext_Riemann_integrable_on 0 ) by A3, INTEGR10:def 9;
A5: ( f is_-infty_improper_integrable_on 0 & f is_+infty_improper_integrable_on 0 & improper_integral_on_REAL f = (improper_integral_-infty (f,0)) + (improper_integral_+infty (f,0)) ) by A1, A2, INTEGR25:36;
( not ].-infty,0.] is empty & not [.0,+infty.[ is empty ) by XXREAL_1:31, XXREAL_1:32;
then reconsider L = left_closed_halfline 0, R = right_closed_halfline 0 as non empty Subset of REAL by LIMFUNC1:def 1, LIMFUNC1:def 2;
A6: ( L = ].-infty,0.] & R = [.0,+infty.[ ) by LIMFUNC1:def 1, LIMFUNC1:def 2;
then L \/ R = REAL by XXREAL_1:224, XXREAL_1:415;
then A7: f | (L \/ R) = f ;
( f | L is_integrable_on L-Meas & f | R is_integrable_on L-Meas ) by A1, A4, A5, Th83, Th84;
hence A8: f is_integrable_on L-Meas by A7, A1, Th53; :: thesis: improper_integral_on_REAL f = Integral (L-Meas,f)
A9: ( improper_integral_-infty (f,0) = Integral (L-Meas,(f | L)) & improper_integral_+infty (f,0) = Integral (L-Meas,(f | R)) ) by A4, A5, A1, Th83, Th84;
REAL = ].-infty,+infty.[ by XXREAL_1:224;
then reconsider E = REAL as Element of L-Field by MEASUR10:5, MEASUR12:75;
reconsider A1 = L as Element of L-Field by A6, MEASUR10:5, MEASUR12:75;
reconsider B1 = R as Element of L-Field by A6, MEASUR10:5, MEASUR12:75;
A10: f is A1 -measurable by A1, A2, Th38;
set C = {0};
A11: {0} = [.0,0.] by XXREAL_1:17;
then reconsider C = {0} as Element of L-Field by MEASUR10:5, MEASUR12:75;
A12: L-Meas . C = 0 - 0 by A11, MESFUN14:5
.= 0 ;
A13: dom (f | L) = L by A1, RELAT_1:62;
then A1 = (dom f) /\ A1 by RELAT_1:61;
then A14: Integral (L-Meas,(f | L)) = Integral (L-Meas,((f | L) | (L \ C))) by A12, A13, A10, MESFUNC6:76, MESFUNC6:89
.= Integral (L-Meas,(f | (L \ C))) by XBOOLE_1:36, RELAT_1:74 ;
A15: A1 \ C = ].-infty,0.[ by A6, XXREAL_1:137;
then (A1 \ C) \/ B1 = ].-infty,+infty.[ by A6, XXREAL_1:173;
then f = f | ((A1 \ C) \/ B1) by XXREAL_1:224;
then Integral (L-Meas,f) = (Integral (L-Meas,(f | L))) + (Integral (L-Meas,(f | R))) by A14, A15, A8, A6, XXREAL_1:94, MESFUNC6:92;
hence improper_integral_on_REAL f = Integral (L-Meas,f) by A9, A1, A2, INTEGR25:36; :: thesis: verum