let f, Intf be PartFunc of REAL,REAL; :: thesis: for b being Real st f is_-infty_improper_integrable_on b & dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty holds
improper_integral_-infty (f,b) = lim_in-infty Intf
let b be Real; :: thesis: ( f is_-infty_improper_integrable_on b & dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty implies improper_integral_-infty (f,b) = lim_in-infty Intf )
assume that
A1: f is_-infty_improper_integrable_on b and
A2: dom Intf = left_closed_halfline b and
A3: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A4: Intf is convergent_in-infty ; :: thesis: improper_integral_-infty (f,b) = lim_in-infty Intf
A5: f is_-infty_ext_Riemann_integrable_on b by A1, A2, A3, A4, INTEGR10:def 6;
then A6: improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) by A1, Th22;
consider I being PartFunc of REAL,REAL such that
A7: dom I = left_closed_halfline b and
A8: for x being Real st x in dom I holds
I . x = integral (f,x,b) and
I is convergent_in-infty and
A9: infty_ext_left_integral (f,b) = lim_in-infty I by A5, INTEGR10:def 8;
now :: thesis: for x being Element of REAL st x in dom Intf holds
Intf . x = I . x
let x be Element of REAL ; :: thesis: ( x in dom Intf implies Intf . x = I . x )
assume A10: x in dom Intf ; :: thesis: Intf . x = I . x
then Intf . x = integral (f,x,b) by A3;
hence Intf . x = I . x by A2, A7, A8, A10; :: thesis: verum
end;
hence improper_integral_-infty (f,b) = lim_in-infty Intf by A6, A9, A2, A7, PARTFUN1:5; :: thesis: verum