:: 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
::
:: Copyright (c) 2008-2019 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 () - () = 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 :
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;
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 :
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) )
proof end;
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
proof end;
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) )
proof end;
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
proof end;
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;
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 :
for f being PartFunc of REAL,REAL
for a being Real 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;
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 :
for f being PartFunc of REAL,REAL
for b being Real 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;
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 )
proof end;
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
proof end;
end;

:: deftheorem Def7 defines infty_ext_right_integral INTEGR10:def 7 :
for f being PartFunc of REAL,REAL
for a being Real 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;
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 )
proof end;
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
proof end;
end;

:: deftheorem Def8 defines infty_ext_left_integral INTEGR10:def 8 :
for f being PartFunc of REAL,REAL
for b being Real 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;
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
() + ();
coherence
() + () is Real
;
end;

:: deftheorem defines infty_ext_integral INTEGR10:def 10 :
for f being PartFunc of REAL,REAL holds infty_ext_integral f = () + ();

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) = () + () )
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 * () )
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) = () + () )
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 * () )
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));
existence
ex b1 being Function of REAL,REAL st
for t being Real holds b1 . t = exp_R . (- (s * t))
proof end;
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
proof end;
end;

:: deftheorem defines exp*- INTEGR10:def 11 :
for s being Real
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 (#) ()),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 (#) ()),0) ) )
proof end;
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 (#) ()),0) ) & dom b2 = right_open_halfline 0 & ( for s being Real st s in dom b2 holds
b2 . s = infty_ext_right_integral ((f (#) ()),0) ) holds
b1 = b2
proof end;
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 (#) ()),0) ) ) );

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 (#) () is_+infty_ext_Riemann_integrable_on 0 ) & ( for s being Real st s in right_open_halfline 0 holds
g (#) () is_+infty_ext_Riemann_integrable_on 0 ) holds
( ( for s being Real st s in right_open_halfline 0 holds
(f + g) (#) () is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (f + 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 (#) () is_+infty_ext_Riemann_integrable_on 0 ) holds
( ( for s being Real st s in right_open_halfline 0 holds
(a (#) f) (#) () is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (a (#) f) = a (#) )
proof end;