begin
theorem Th1:
theorem Th2:
theorem
begin
:: 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 ) ) );
:: 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:
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) )
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
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:
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) )
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
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) ) );
:: 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 ) ) );
:: 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:
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 )
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
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:
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 )
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
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 ) );
:: 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 ) );
:: 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
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)) )
theorem
theorem
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)) )
theorem
theorem Th8:
theorem Th9:
theorem
theorem
theorem
theorem
begin
:: 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)) );
:: 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
theorem