begin
theorem Th1:
theorem Th2:
theorem
begin
:: deftheorem Def1 defines is_right_ext_Riemann_integrable_on INTEGR10:def 1 :
:: deftheorem Def2 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:
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 :
:: deftheorem Def6 defines is_-infty_ext_Riemann_integrable_on INTEGR10:def 6 :
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 :
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 :
:: deftheorem defines infty_ext_Riemann_integrable INTEGR10:def 9 :
:: deftheorem defines infty_ext_integral INTEGR10:def 10 :
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 :
:: deftheorem Def12 defines One-sided_Laplace_transform INTEGR10:def 12 :
begin
theorem
theorem