INTEGR10: Extended {R}iemann Integral of Functions of Real Variable and One-sided {L}aplace Transform

:: 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-2021 Association of Mizar Users

theorem Th1: :: INTEGR10:1

for a, b, g1, M being Real st a < b & 0 < g1 & 0 < M holds
ex r being Real st
( a < r & r < b & (b - r) * M < g1 )

proof end;

theorem Th2: :: INTEGR10:2

for a, b, g1, M being Real st a < b & 0 < g1 & 0 < M holds
ex r being Real st
( a < r & r < b & (r - a) * M < g1 )

proof end;

theorem :: INTEGR10:3

for a, b being Real holds (exp_R . b) - (exp_R . a) = integral (exp_R,a,b)

proof end;

definition

let f be PartFunc of REAL,REAL;
let a, b be Real;

pred f is_right_ext_Riemann_integrable_on a,b means :: 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 defines is_right_ext_Riemann_integrable_on INTEGR10:def 1 :

definition

let f be PartFunc of REAL,REAL;
let a, b be Real;

pred f is_left_ext_Riemann_integrable_on a,b means :: 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 defines is_left_ext_Riemann_integrable_on INTEGR10:def 2 :

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) );

proof end;

proof end;

end;

:: deftheorem Def3 defines ext_right_integral INTEGR10:def 3 :

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) );

proof end;

proof end;

end;

:: deftheorem Def4 defines ext_left_integral INTEGR10:def 4 :

definition

let f be PartFunc of REAL,REAL;
let a be Real;

pred f is_+infty_ext_Riemann_integrable_on a means :: 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 defines is_+infty_ext_Riemann_integrable_on INTEGR10:def 5 :

definition

let f be PartFunc of REAL,REAL;
let b be Real;

pred f is_-infty_ext_Riemann_integrable_on b means :: 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 defines is_-infty_ext_Riemann_integrable_on INTEGR10:def 6 :

definition

let f be PartFunc of REAL,REAL;
let a be Real;
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 );

proof end;

proof end;

end;

:: deftheorem Def7 defines infty_ext_right_integral INTEGR10:def 7 :

definition

let f be PartFunc of REAL,REAL;
let b be Real;
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 );

proof end;

proof end;

end;

:: deftheorem Def8 defines infty_ext_left_integral INTEGR10:def 8 :

definition

let f be PartFunc of REAL,REAL;

attr f 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 :

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));

end;

:: deftheorem defines infty_ext_integral INTEGR10:def 10 :

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)) )

proof end;

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)) )

proof end;

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)) )

proof end;

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)) )

proof end;

theorem Th8: :: INTEGR10:8

for f, g being PartFunc of REAL,REAL
for a being Real 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)) )

proof end;

theorem Th9: :: INTEGR10:9

for f being PartFunc of REAL,REAL
for a being Real 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)) )

proof end;

theorem :: INTEGR10:10

for f, g being PartFunc of REAL,REAL
for b being Real 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)) )

proof end;

theorem :: INTEGR10:11

for f being PartFunc of REAL,REAL
for b being Real 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)) )

proof end;

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)

proof end;

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)

proof end;

definition

let s be Real;

func exp*- s -> Function of REAL,REAL means :: INTEGR10:def 11
for t being Real holds it . t = exp_R . (- (s * t));

proof end;

proof end;

end;

:: deftheorem defines exp*- INTEGR10:def 11 :

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) ) );

proof end;

proof end;

end;

:: deftheorem Def12 defines One-sided_Laplace_transform INTEGR10:def 12 :

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) )

proof end;

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) )

proof end;