:: Extended {R}iemann Integral of Functions of Real Variable and One-sided {L}aplace Transform :: by Masahiko Yamazaki , Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura :: :: Received July 22, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin theorem Th1: :: INTEGR10:1 for a, b, g1, M being real number st a < b & 0 < g1 & 0 < M holds ex r being Element of REAL st ( a < r & r < b & (b - r) * M < g1 ) proofend; theorem Th2: :: INTEGR10:2 for a, b, g1, M being real number st a < b & 0 < g1 & 0 < M holds ex r being Element of REAL st ( a < r & r < b & (r - a) * M < g1 ) proofend; theorem :: INTEGR10:3 for b, a being Element of REAL holds (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) proofend; begin definition let f be PartFunc of REAL,REAL; let a, b be Real; predf is_right_ext_Riemann_integrable_on a,b means :Def1: :: INTEGR10:def 1 ( ( for d being Real st a <= d & d < b holds ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b ) ); end; :: deftheorem Def1 defines is_right_ext_Riemann_integrable_on INTEGR10:def_1_:_ for f being PartFunc of REAL,REAL for a, b being Real holds ( f is_right_ext_Riemann_integrable_on a,b iff ( ( for d being Real st a <= d & d < b holds ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b ) ) ); definition let f be PartFunc of REAL,REAL; let a, b be Real; predf is_left_ext_Riemann_integrable_on a,b means :Def2: :: INTEGR10:def 2 ( ( for d being Real st a < d & d <= b holds ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a ) ); end; :: deftheorem Def2 defines is_left_ext_Riemann_integrable_on INTEGR10:def_2_:_ for f being PartFunc of REAL,REAL for a, b being Real holds ( f is_left_ext_Riemann_integrable_on a,b iff ( ( for d being Real st a < d & d <= b holds ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a ) ) ); definition let f be PartFunc of REAL,REAL; let a, b be Real; assume A1: f is_right_ext_Riemann_integrable_on a,b ; func ext_right_integral (f,a,b) -> Real means :Def3: :: INTEGR10:def 3 ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & it = lim_left (Intf,b) ); existence ex b1 being Real ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & b1 = lim_left (Intf,b) ) proofend; uniqueness for b1, b2 being Real st ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & b1 = lim_left (Intf,b) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & b2 = lim_left (Intf,b) ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines ext_right_integral INTEGR10:def_3_:_ for f being PartFunc of REAL,REAL for a, b being Real st f is_right_ext_Riemann_integrable_on a,b holds for b4 being Real holds ( b4 = ext_right_integral (f,a,b) iff ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & b4 = lim_left (Intf,b) ) ); definition let f be PartFunc of REAL,REAL; let a, b be Real; assume A1: f is_left_ext_Riemann_integrable_on a,b ; func ext_left_integral (f,a,b) -> Real means :Def4: :: INTEGR10:def 4 ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & it = lim_right (Intf,a) ); existence ex b1 being Real ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & b1 = lim_right (Intf,a) ) proofend; uniqueness for b1, b2 being Real st ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & b1 = lim_right (Intf,a) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & b2 = lim_right (Intf,a) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines ext_left_integral INTEGR10:def_4_:_ for f being PartFunc of REAL,REAL for a, b being Real st f is_left_ext_Riemann_integrable_on a,b holds for b4 being Real holds ( b4 = ext_left_integral (f,a,b) iff ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & b4 = lim_right (Intf,a) ) ); definition let f be PartFunc of REAL,REAL; let a be real number ; predf is_+infty_ext_Riemann_integrable_on a means :Def5: :: INTEGR10:def 5 ( ( for b being Real st a <= b holds ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty ) ); end; :: deftheorem Def5 defines is_+infty_ext_Riemann_integrable_on INTEGR10:def_5_:_ for f being PartFunc of REAL,REAL for a being real number holds ( f is_+infty_ext_Riemann_integrable_on a iff ( ( for b being Real st a <= b holds ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty ) ) ); definition let f be PartFunc of REAL,REAL; let b be real number ; predf is_-infty_ext_Riemann_integrable_on b means :Def6: :: INTEGR10:def 6 ( ( for a being Real st a <= b holds ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ) & 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 (f,x,b) ) & Intf is convergent_in-infty ) ); end; :: deftheorem Def6 defines is_-infty_ext_Riemann_integrable_on INTEGR10:def_6_:_ for f being PartFunc of REAL,REAL for b being real number holds ( f is_-infty_ext_Riemann_integrable_on b iff ( ( for a being Real st a <= b holds ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ) & 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 (f,x,b) ) & Intf is convergent_in-infty ) ) ); definition let f be PartFunc of REAL,REAL; let a be real number ; assume A1: f is_+infty_ext_Riemann_integrable_on a ; func infty_ext_right_integral (f,a) -> Real means :Def7: :: INTEGR10:def 7 ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & it = lim_in+infty Intf ); existence ex b1 being Real ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & b1 = lim_in+infty Intf ) proofend; uniqueness for b1, b2 being Real st ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & b1 = lim_in+infty Intf ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & b2 = lim_in+infty Intf ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines infty_ext_right_integral INTEGR10:def_7_:_ for f being PartFunc of REAL,REAL for a being real number st f is_+infty_ext_Riemann_integrable_on a holds for b3 being Real holds ( b3 = infty_ext_right_integral (f,a) iff ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & b3 = lim_in+infty Intf ) ); definition let f be PartFunc of REAL,REAL; let b be real number ; assume A1: f is_-infty_ext_Riemann_integrable_on b ; func infty_ext_left_integral (f,b) -> Real means :Def8: :: INTEGR10:def 8 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 (f,x,b) ) & Intf is convergent_in-infty & it = lim_in-infty Intf ); existence ex b1 being Real 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 (f,x,b) ) & Intf is convergent_in-infty & b1 = lim_in-infty Intf ) proofend; uniqueness for b1, b2 being Real st 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 (f,x,b) ) & Intf is convergent_in-infty & b1 = lim_in-infty Intf ) & 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 (f,x,b) ) & Intf is convergent_in-infty & b2 = lim_in-infty Intf ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines infty_ext_left_integral INTEGR10:def_8_:_ for f being PartFunc of REAL,REAL for b being real number st f is_-infty_ext_Riemann_integrable_on b holds for b3 being Real holds ( b3 = infty_ext_left_integral (f,b) iff 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 (f,x,b) ) & Intf is convergent_in-infty & b3 = lim_in-infty Intf ) ); definition let f be PartFunc of REAL,REAL; attrf is infty_ext_Riemann_integrable means :: INTEGR10:def 9 ( f is_+infty_ext_Riemann_integrable_on 0 & f is_-infty_ext_Riemann_integrable_on 0 ); end; :: deftheorem defines infty_ext_Riemann_integrable INTEGR10:def_9_:_ for f being PartFunc of REAL,REAL holds ( f is infty_ext_Riemann_integrable iff ( f is_+infty_ext_Riemann_integrable_on 0 & f is_-infty_ext_Riemann_integrable_on 0 ) ); definition let f be PartFunc of REAL,REAL; func infty_ext_integral f -> Real equals :: INTEGR10:def 10 (infty_ext_right_integral (f,0)) + (infty_ext_left_integral (f,0)); coherence (infty_ext_right_integral (f,0)) + (infty_ext_left_integral (f,0)) is Real ; end; :: deftheorem defines infty_ext_integral INTEGR10:def_10_:_ for f being PartFunc of REAL,REAL holds infty_ext_integral f = (infty_ext_right_integral (f,0)) + (infty_ext_left_integral (f,0)); begin theorem :: INTEGR10:4 for f, g being PartFunc of REAL,REAL for a, b being Real st a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_right_ext_Riemann_integrable_on a,b & g is_right_ext_Riemann_integrable_on a,b holds ( f + g is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) ) proofend; theorem :: INTEGR10:5 for f being PartFunc of REAL,REAL for a, b being Real st a < b & ['a,b'] c= dom f & f is_right_ext_Riemann_integrable_on a,b holds for r being Real holds ( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) ) proofend; theorem :: INTEGR10:6 for f, g being PartFunc of REAL,REAL for a, b being Real st a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_left_ext_Riemann_integrable_on a,b & g is_left_ext_Riemann_integrable_on a,b holds ( f + g is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) ) proofend; theorem :: INTEGR10:7 for f being PartFunc of REAL,REAL for a, b being Real st a < b & ['a,b'] c= dom f & f is_left_ext_Riemann_integrable_on a,b holds for r being Real holds ( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) ) proofend; theorem Th8: :: INTEGR10:8 for f, g being PartFunc of REAL,REAL for a being real number st right_closed_halfline a c= dom f & right_closed_halfline a c= dom g & f is_+infty_ext_Riemann_integrable_on a & g is_+infty_ext_Riemann_integrable_on a holds ( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) ) proofend; theorem Th9: :: INTEGR10:9 for f being PartFunc of REAL,REAL for a being real number st right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a holds for r being Real holds ( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) ) proofend; theorem :: INTEGR10:10 for f, g being PartFunc of REAL,REAL for b being real number st left_closed_halfline b c= dom f & left_closed_halfline b c= dom g & f is_-infty_ext_Riemann_integrable_on b & g is_-infty_ext_Riemann_integrable_on b holds ( f + g is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((f + g),b) = (infty_ext_left_integral (f,b)) + (infty_ext_left_integral (g,b)) ) proofend; theorem :: INTEGR10:11 for f being PartFunc of REAL,REAL for b being real number st left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b holds for r being Real holds ( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) ) proofend; theorem :: INTEGR10:12 for f being PartFunc of REAL,REAL for a, b being Real st a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds ext_right_integral (f,a,b) = integral (f,a,b) proofend; theorem :: INTEGR10:13 for f being PartFunc of REAL,REAL for a, b being Real st a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds ext_left_integral (f,a,b) = integral (f,a,b) proofend; begin definition let s be real number ; func exp*- s -> Function of REAL,REAL means :: INTEGR10:def 11 for t being Real holds it . t = exp_R . (- (s * t)); existence ex b1 being Function of REAL,REAL st for t being Real holds b1 . t = exp_R . (- (s * t)) proofend; uniqueness for b1, b2 being Function of REAL,REAL st ( for t being Real holds b1 . t = exp_R . (- (s * t)) ) & ( for t being Real holds b2 . t = exp_R . (- (s * t)) ) holds b1 = b2 proofend; end; :: deftheorem defines exp*- INTEGR10:def_11_:_ for s being real number for b2 being Function of REAL,REAL holds ( b2 = exp*- s iff for t being Real holds b2 . t = exp_R . (- (s * t)) ); definition let f be PartFunc of REAL,REAL; func One-sided_Laplace_transform f -> PartFunc of REAL,REAL means :Def12: :: INTEGR10:def 12 ( dom it = right_open_halfline 0 & ( for s being Real st s in dom it holds it . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ); existence ex b1 being PartFunc of REAL,REAL st ( dom b1 = right_open_halfline 0 & ( for s being Real st s in dom b1 holds b1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ) proofend; uniqueness for b1, b2 being PartFunc of REAL,REAL st dom b1 = right_open_halfline 0 & ( for s being Real st s in dom b1 holds b1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) & dom b2 = right_open_halfline 0 & ( for s being Real st s in dom b2 holds b2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) holds b1 = b2 proofend; end; :: deftheorem Def12 defines One-sided_Laplace_transform INTEGR10:def_12_:_ for f, b2 being PartFunc of REAL,REAL holds ( b2 = One-sided_Laplace_transform f iff ( dom b2 = right_open_halfline 0 & ( for s being Real st s in dom b2 holds b2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ) ); begin theorem :: INTEGR10:14 for f, g being PartFunc of REAL,REAL st dom f = right_closed_halfline 0 & dom g = right_closed_halfline 0 & ( for s being Real st s in right_open_halfline 0 holds f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & ( for s being Real st s in right_open_halfline 0 holds g (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) holds ( ( for s being Real st s in right_open_halfline 0 holds (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (f + g) = (One-sided_Laplace_transform f) + (One-sided_Laplace_transform g) ) proofend; theorem :: INTEGR10:15 for f being PartFunc of REAL,REAL for a being Real st dom f = right_closed_halfline 0 & ( for s being Real st s in right_open_halfline 0 holds f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) holds ( ( for s being Real st s in right_open_halfline 0 holds (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (a (#) f) = a (#) (One-sided_Laplace_transform f) ) proofend;