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

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 )

ex r being Real st

( a < r & r < b & (r - a) * M < g1 )

proof end;

definition

let f be PartFunc of REAL,REAL;

let a, b be Real;

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

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

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;

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

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

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

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 ;

ex b_{1} 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 & b_{1} = lim_left (Intf,b) )

for b_{1}, b_{2} 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 & b_{1} = 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 & b_{2} = lim_left (Intf,b) ) holds

b_{1} = b_{2}

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

ex b

( 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 & b

proof end;

uniqueness for b

( 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 & b

( 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 & b

b

proof 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 b_{4} being Real holds

( b_{4} = 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 & b_{4} = lim_left (Intf,b) ) );

for f being PartFunc of REAL,REAL

for a, b being Real st f is_right_ext_Riemann_integrable_on a,b holds

for b

( b

( 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 & 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 ;

ex b_{1} 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 & b_{1} = lim_right (Intf,a) )

for b_{1}, b_{2} 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 & b_{1} = 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 & b_{2} = lim_right (Intf,a) ) holds

b_{1} = b_{2}

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

ex b

( 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 & b

proof end;

uniqueness for b

( 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 & b

( 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 & b

b

proof 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 b_{4} being Real holds

( b_{4} = 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 & b_{4} = lim_right (Intf,a) ) );

for f being PartFunc of REAL,REAL

for a, b being Real st f is_left_ext_Riemann_integrable_on a,b holds

for b

( b

( 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 & b

definition

let f be PartFunc of REAL,REAL;

let a be Real;

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

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

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;

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

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

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

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 ;

ex b_{1} 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 & b_{1} = lim_in+infty Intf )

for b_{1}, b_{2} 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 & b_{1} = 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 & b_{2} = lim_in+infty Intf ) holds

b_{1} = b_{2}

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

ex b

( 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 & b

proof end;

uniqueness for b

( 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 & b

( 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 & b

b

proof 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 b_{3} being Real holds

( b_{3} = 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 & b_{3} = lim_in+infty Intf ) );

for f being PartFunc of REAL,REAL

for a being Real st f is_+infty_ext_Riemann_integrable_on a holds

for b

( b

( 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 & b

definition

let f be PartFunc of REAL,REAL;

let b be Real;

assume A1: f is_-infty_ext_Riemann_integrable_on b ;

ex b_{1} 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 & b_{1} = lim_in-infty Intf )

for b_{1}, b_{2} 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 & b_{1} = 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 & b_{2} = lim_in-infty Intf ) holds

b_{1} = b_{2}

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

ex b

( 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 & b

proof end;

uniqueness for b

( 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 & b

( 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 & b

b

proof 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 b_{3} being Real holds

( b_{3} = 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 & b_{3} = lim_in-infty Intf ) );

for f being PartFunc of REAL,REAL

for b being Real st f is_-infty_ext_Riemann_integrable_on b holds

for b

( b

( 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 & b

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

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;

(infty_ext_right_integral (f,0)) + (infty_ext_left_integral (f,0)) is Real ;

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

(infty_ext_right_integral (f,0)) + (infty_ext_left_integral (f,0)) is Real ;

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

for f being PartFunc of REAL,REAL holds infty_ext_integral f = (infty_ext_right_integral (f,0)) + (infty_ext_left_integral (f,0));

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

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

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

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

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

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

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

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

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)

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)

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;

ex b_{1} being Function of REAL,REAL st

for t being Real holds b_{1} . t = exp_R . (- (s * t))

for b_{1}, b_{2} being Function of REAL,REAL st ( for t being Real holds b_{1} . t = exp_R . (- (s * t)) ) & ( for t being Real holds b_{2} . t = exp_R . (- (s * t)) ) holds

b_{1} = b_{2}

end;
func exp*- s -> Function of REAL,REAL means :: INTEGR10:def 11

for t being Real holds it . t = exp_R . (- (s * t));

existence for t being Real holds it . t = exp_R . (- (s * t));

ex b

for t being Real holds b

proof end;

uniqueness for b

b

proof end;

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

for s being Real

for b_{2} being Function of REAL,REAL holds

( b_{2} = exp*- s iff for t being Real holds b_{2} . t = exp_R . (- (s * t)) );

for s being Real

for b

( b

definition

let f be PartFunc of REAL,REAL;

ex b_{1} being PartFunc of REAL,REAL st

( dom b_{1} = right_open_halfline 0 & ( for s being Real st s in dom b_{1} holds

b_{1} . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) )

for b_{1}, b_{2} being PartFunc of REAL,REAL st dom b_{1} = right_open_halfline 0 & ( for s being Real st s in dom b_{1} holds

b_{1} . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) & dom b_{2} = right_open_halfline 0 & ( for s being Real st s in dom b_{2} holds

b_{2} . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) holds

b_{1} = b_{2}

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

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for f, b_{2} being PartFunc of REAL,REAL holds

( b_{2} = One-sided_Laplace_transform f iff ( dom b_{2} = right_open_halfline 0 & ( for s being Real st s in dom b_{2} holds

b_{2} . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ) );

for f, b

( b

b

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

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

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;