:: INTEGR10 semantic presentation
begin
theorem Th1: :: INTEGR10:1
for a, b, g1, M being real number st a < b & 0 < g1 & 0 < M holds
ex r being Element of REAL st
( a < r & r < b & (b - r) * M < g1 )
proof
let a, b, g1, M be real number ; ::_thesis: ( a < b & 0 < g1 & 0 < M implies ex r being Element of REAL st
( a < r & r < b & (b - r) * M < g1 ) )
assume that
A1: a < b and
A2: 0 < g1 and
A3: 0 < M ; ::_thesis: ex r being Element of REAL st
( a < r & r < b & (b - r) * M < g1 )
set r3 = max (a,(b - (g1 / M)));
b - (g1 / M) < b by A2, A3, XREAL_1:44, XREAL_1:139;
then max (a,(b - (g1 / M))) < b by A1, XXREAL_0:16;
then consider q being real number such that
A4: max (a,(b - (g1 / M))) < q and
A5: q < b by XREAL_1:5;
reconsider r = q as Real by XREAL_0:def_1;
take r ; ::_thesis: ( a < r & r < b & (b - r) * M < g1 )
b - (g1 / M) <= max (a,(b - (g1 / M))) by XXREAL_0:25;
then b - (g1 / M) < r by A4, XXREAL_0:2;
then (b - (g1 / M)) - (r - (g1 / M)) < r - (r - (g1 / M)) by XREAL_1:14;
then (b - r) * 1 < g1 / M ;
then ( a <= max (a,(b - (g1 / M))) & (b - r) * M < g1 / 1 ) by A3, XREAL_1:111, XXREAL_0:25;
hence ( a < r & r < b & (b - r) * M < g1 ) by A4, A5, XXREAL_0:2; ::_thesis: verum
end;
theorem Th2: :: INTEGR10:2
for a, b, g1, M being real number st a < b & 0 < g1 & 0 < M holds
ex r being Element of REAL st
( a < r & r < b & (r - a) * M < g1 )
proof
let a, b, g1, M be real number ; ::_thesis: ( a < b & 0 < g1 & 0 < M implies ex r being Element of REAL st
( a < r & r < b & (r - a) * M < g1 ) )
assume that
A1: a < b and
A2: ( 0 < g1 & 0 < M ) ; ::_thesis: ex r being Element of REAL st
( a < r & r < b & (r - a) * M < g1 )
- b < - a by A1, XREAL_1:24;
then consider r1 being Real such that
A3: ( - b < r1 & r1 < - a ) and
A4: ((- a) - r1) * M < g1 by A2, Th1;
reconsider r = - r1 as Real ;
take r ; ::_thesis: ( a < r & r < b & (r - a) * M < g1 )
( - (- b) > - r1 & - r1 > - (- a) ) by A3, XREAL_1:24;
hence ( a < r & r < b & (r - a) * M < g1 ) by A4; ::_thesis: verum
end;
theorem :: INTEGR10:3
for b, a being Element of REAL holds (exp_R . b) - (exp_R . a) = integral (exp_R,a,b)
proof
let b, a be Element of REAL ; ::_thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b)
A1: min (a,b) <= a by XXREAL_0:17;
A2: [.(min (a,b)),(max (a,b)).] c= REAL ;
( exp_R | REAL is continuous & a <= max (a,b) ) by XXREAL_0:25;
then A3: exp_R . (max (a,b)) = (integral (exp_R,(min (a,b)),(max (a,b)))) + (exp_R . (min (a,b))) by A1, A2, INTEGRA7:20, INTEGRA7:27, SIN_COS:47, XXREAL_0:2;
A4: ( min (a,b) = a implies (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) )
proof
assume A5: min (a,b) = a ; ::_thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b)
then max (a,b) = b by XXREAL_0:36;
hence (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) by A3, A5; ::_thesis: verum
end;
( min (a,b) = b implies (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) )
proof
assume A6: min (a,b) = b ; ::_thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b)
then A7: max (a,b) = a by XXREAL_0:36;
( b < a implies (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) )
proof
assume b < a ; ::_thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b)
then integral (exp_R,a,b) = - (integral (exp_R,['b,a'])) by INTEGRA5:def_4;
then exp_R . a = (- (integral (exp_R,a,b))) + (exp_R . b) by A1, A3, A6, A7, INTEGRA5:def_4;
hence (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) ; ::_thesis: verum
end;
hence (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) by A1, A4, A6, XXREAL_0:1; ::_thesis: verum
end;
hence (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) by A4, XXREAL_0:15; ::_thesis: verum
end;
begin
definition
let f be PartFunc of REAL,REAL;
let a, b be Real;
predf is_right_ext_Riemann_integrable_on a,b means :Def1: :: 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 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 ) ) );
definition
let f be PartFunc of REAL,REAL;
let a, b be Real;
predf is_left_ext_Riemann_integrable_on a,b means :Def2: :: 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 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: :: 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
consider Intf being PartFunc of REAL,REAL such that
A2: ( 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 ) by A1, Def1;
take lim_left (Intf,b) ; ::_thesis: 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 & lim_left (Intf,b) = lim_left (Intf,b) )
thus 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 & lim_left (Intf,b) = lim_left (Intf,b) ) by A2; ::_thesis: verum
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
let y1, y2 be Real; ::_thesis: ( 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 & y1 = 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 & y2 = lim_left (Intf,b) ) implies y1 = y2 )
assume ex Intf1 being PartFunc of REAL,REAL st
( dom Intf1 = [.a,b.[ & ( for x being Real st x in dom Intf1 holds
Intf1 . x = integral (f,a,x) ) & Intf1 is_left_convergent_in b & y1 = lim_left (Intf1,b) ) ; ::_thesis: ( for Intf being PartFunc of REAL,REAL holds
( not dom Intf = [.a,b.[ or ex x being Real st
( x in dom Intf & not Intf . x = integral (f,a,x) ) or not Intf is_left_convergent_in b or not y2 = lim_left (Intf,b) ) or y1 = y2 )
then consider Intf1 being PartFunc of REAL,REAL such that
A3: dom Intf1 = [.a,b.[ and
A4: for x being Real st x in dom Intf1 holds
Intf1 . x = integral (f,a,x) and
Intf1 is_left_convergent_in b and
A5: y1 = lim_left (Intf1,b) ;
assume ex Intf2 being PartFunc of REAL,REAL st
( dom Intf2 = [.a,b.[ & ( for x being Real st x in dom Intf2 holds
Intf2 . x = integral (f,a,x) ) & Intf2 is_left_convergent_in b & y2 = lim_left (Intf2,b) ) ; ::_thesis: y1 = y2
then consider Intf2 being PartFunc of REAL,REAL such that
A6: dom Intf2 = [.a,b.[ and
A7: for x being Real st x in dom Intf2 holds
Intf2 . x = integral (f,a,x) and
Intf2 is_left_convergent_in b and
A8: y2 = lim_left (Intf2,b) ;
now__::_thesis:_for_x_being_Real_st_x_in_dom_Intf1_holds_
Intf1_._x_=_Intf2_._x
let x be Real; ::_thesis: ( x in dom Intf1 implies Intf1 . x = Intf2 . x )
assume A9: x in dom Intf1 ; ::_thesis: Intf1 . x = Intf2 . x
hence Intf1 . x = integral (f,a,x) by A4
.= Intf2 . x by A3, A6, A7, A9 ;
::_thesis: verum
end;
hence y1 = y2 by A3, A5, A6, A8, PARTFUN1:5; ::_thesis: verum
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
consider Intf being PartFunc of REAL,REAL such that
A2: ( 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 ) by A1, Def2;
take lim_right (Intf,a) ; ::_thesis: 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 & lim_right (Intf,a) = lim_right (Intf,a) )
thus 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 & lim_right (Intf,a) = lim_right (Intf,a) ) by A2; ::_thesis: verum
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
let y1, y2 be Real; ::_thesis: ( 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 & y1 = 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 & y2 = lim_right (Intf,a) ) implies y1 = y2 )
assume ex Intf1 being PartFunc of REAL,REAL st
( dom Intf1 = ].a,b.] & ( for x being Real st x in dom Intf1 holds
Intf1 . x = integral (f,x,b) ) & Intf1 is_right_convergent_in a & y1 = lim_right (Intf1,a) ) ; ::_thesis: ( for Intf being PartFunc of REAL,REAL holds
( not dom Intf = ].a,b.] or ex x being Real st
( x in dom Intf & not Intf . x = integral (f,x,b) ) or not Intf is_right_convergent_in a or not y2 = lim_right (Intf,a) ) or y1 = y2 )
then consider Intf1 being PartFunc of REAL,REAL such that
A3: dom Intf1 = ].a,b.] and
A4: for x being Real st x in dom Intf1 holds
Intf1 . x = integral (f,x,b) and
Intf1 is_right_convergent_in a and
A5: y1 = lim_right (Intf1,a) ;
assume ex Intf2 being PartFunc of REAL,REAL st
( dom Intf2 = ].a,b.] & ( for x being Real st x in dom Intf2 holds
Intf2 . x = integral (f,x,b) ) & Intf2 is_right_convergent_in a & y2 = lim_right (Intf2,a) ) ; ::_thesis: y1 = y2
then consider Intf2 being PartFunc of REAL,REAL such that
A6: dom Intf2 = ].a,b.] and
A7: for x being Real st x in dom Intf2 holds
Intf2 . x = integral (f,x,b) and
Intf2 is_right_convergent_in a and
A8: y2 = lim_right (Intf2,a) ;
now__::_thesis:_for_x_being_Real_st_x_in_dom_Intf1_holds_
Intf1_._x_=_Intf2_._x
let x be Real; ::_thesis: ( x in dom Intf1 implies Intf1 . x = Intf2 . x )
assume A9: x in dom Intf1 ; ::_thesis: Intf1 . x = Intf2 . x
hence Intf1 . x = integral (f,x,b) by A4
.= Intf2 . x by A3, A6, A7, A9 ;
::_thesis: verum
end;
hence y1 = y2 by A3, A5, A6, A8, PARTFUN1:5; ::_thesis: verum
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 number ;
predf is_+infty_ext_Riemann_integrable_on a means :Def5: :: 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 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 ) ) );
definition
let f be PartFunc of REAL,REAL;
let b be real number ;
predf is_-infty_ext_Riemann_integrable_on b means :Def6: :: 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 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: :: 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
consider Intf being PartFunc of REAL,REAL such that
A2: ( 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 ) by A1, Def5;
take lim_in+infty Intf ; ::_thesis: 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 & lim_in+infty Intf = lim_in+infty Intf )
thus 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 & lim_in+infty Intf = lim_in+infty Intf ) by A2; ::_thesis: verum
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
let L1, L2 be Real; ::_thesis: ( 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 & L1 = 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 & L2 = lim_in+infty Intf ) implies L1 = L2 )
assume ex Intf1 being PartFunc of REAL,REAL st
( dom Intf1 = right_closed_halfline a & ( for x being Real st x in dom Intf1 holds
Intf1 . x = integral (f,a,x) ) & Intf1 is convergent_in+infty & L1 = lim_in+infty Intf1 ) ; ::_thesis: ( for Intf being PartFunc of REAL,REAL holds
( not dom Intf = right_closed_halfline a or ex x being Real st
( x in dom Intf & not Intf . x = integral (f,a,x) ) or not Intf is convergent_in+infty or not L2 = lim_in+infty Intf ) or L1 = L2 )
then consider Intf1 being PartFunc of REAL,REAL such that
A3: dom Intf1 = right_closed_halfline a and
A4: for x being Real st x in dom Intf1 holds
Intf1 . x = integral (f,a,x) and
Intf1 is convergent_in+infty and
A5: L1 = lim_in+infty Intf1 ;
assume ex Intf2 being PartFunc of REAL,REAL st
( dom Intf2 = right_closed_halfline a & ( for x being Real st x in dom Intf2 holds
Intf2 . x = integral (f,a,x) ) & Intf2 is convergent_in+infty & L2 = lim_in+infty Intf2 ) ; ::_thesis: L1 = L2
then consider Intf2 being PartFunc of REAL,REAL such that
A6: dom Intf2 = right_closed_halfline a and
A7: for x being Real st x in dom Intf2 holds
Intf2 . x = integral (f,a,x) and
Intf2 is convergent_in+infty and
A8: L2 = lim_in+infty Intf2 ;
now__::_thesis:_for_x_being_Real_st_x_in_dom_Intf1_holds_
Intf1_._x_=_Intf2_._x
let x be Real; ::_thesis: ( x in dom Intf1 implies Intf1 . x = Intf2 . x )
assume A9: x in dom Intf1 ; ::_thesis: Intf1 . x = Intf2 . x
hence Intf1 . x = integral (f,a,x) by A4
.= Intf2 . x by A3, A6, A7, A9 ;
::_thesis: verum
end;
hence L1 = L2 by A3, A5, A6, A8, PARTFUN1:5; ::_thesis: verum
end;
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: :: 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
consider Intf being PartFunc of REAL,REAL such that
A2: ( 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 ) by A1, Def6;
take lim_in-infty Intf ; ::_thesis: 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 & lim_in-infty Intf = lim_in-infty Intf )
thus 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 & lim_in-infty Intf = lim_in-infty Intf ) by A2; ::_thesis: verum
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
let L1, L2 be Real; ::_thesis: ( 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 & L1 = 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 & L2 = lim_in-infty Intf ) implies L1 = L2 )
assume ex Intf1 being PartFunc of REAL,REAL st
( dom Intf1 = left_closed_halfline b & ( for x being Real st x in dom Intf1 holds
Intf1 . x = integral (f,x,b) ) & Intf1 is convergent_in-infty & L1 = lim_in-infty Intf1 ) ; ::_thesis: ( for Intf being PartFunc of REAL,REAL holds
( not dom Intf = left_closed_halfline b or ex x being Real st
( x in dom Intf & not Intf . x = integral (f,x,b) ) or not Intf is convergent_in-infty or not L2 = lim_in-infty Intf ) or L1 = L2 )
then consider Intf1 being PartFunc of REAL,REAL such that
A3: dom Intf1 = left_closed_halfline b and
A4: for x being Real st x in dom Intf1 holds
Intf1 . x = integral (f,x,b) and
Intf1 is convergent_in-infty and
A5: L1 = lim_in-infty Intf1 ;
assume ex Intf2 being PartFunc of REAL,REAL st
( dom Intf2 = left_closed_halfline b & ( for x being Real st x in dom Intf2 holds
Intf2 . x = integral (f,x,b) ) & Intf2 is convergent_in-infty & L2 = lim_in-infty Intf2 ) ; ::_thesis: L1 = L2
then consider Intf2 being PartFunc of REAL,REAL such that
A6: dom Intf2 = left_closed_halfline b and
A7: for x being Real st x in dom Intf2 holds
Intf2 . x = integral (f,x,b) and
Intf2 is convergent_in-infty and
A8: L2 = lim_in-infty Intf2 ;
now__::_thesis:_for_x_being_Real_st_x_in_dom_Intf1_holds_
Intf1_._x_=_Intf2_._x
let x be Real; ::_thesis: ( x in dom Intf1 implies Intf1 . x = Intf2 . x )
assume A9: x in dom Intf1 ; ::_thesis: Intf1 . x = Intf2 . x
hence Intf1 . x = integral (f,x,b) by A4
.= Intf2 . x by A3, A6, A7, A9 ;
::_thesis: verum
end;
hence L1 = L2 by A3, A5, A6, A8, PARTFUN1:5; ::_thesis: verum
end;
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 ) );
definition
let f be PartFunc of REAL,REAL;
attrf 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_:_
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
(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)) is Real ;
end;
:: 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 :: 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
let f, g be PartFunc of REAL,REAL; ::_thesis: 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)) )
let a, b be Real; ::_thesis: ( 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 implies ( 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)) ) )
assume that
A1: a < b and
A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) and
A3: f is_right_ext_Riemann_integrable_on a,b and
A4: g is_right_ext_Riemann_integrable_on a,b ; ::_thesis: ( 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)) )
consider Intg being PartFunc of REAL,REAL such that
A5: dom Intg = [.a,b.[ and
A6: for x being Real st x in dom Intg holds
Intg . x = integral (g,a,x) and
A7: Intg is_left_convergent_in b and
A8: ext_right_integral (g,a,b) = lim_left (Intg,b) by A4, Def3;
consider Intf being PartFunc of REAL,REAL such that
A9: dom Intf = [.a,b.[ and
A10: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
A11: Intf is_left_convergent_in b and
A12: ext_right_integral (f,a,b) = lim_left (Intf,b) by A3, Def3;
set Intfg = Intf + Intg;
A13: ( dom (Intf + Intg) = [.a,b.[ & ( for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),a,x) ) )
proof
A14: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
thus A15: dom (Intf + Intg) = (dom Intf) /\ (dom Intg) by VALUED_1:def_1
.= [.a,b.[ by A9, A5 ; ::_thesis: for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),a,x)
let x be Real; ::_thesis: ( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),a,x) )
assume A16: x in dom (Intf + Intg) ; ::_thesis: (Intf + Intg) . x = integral ((f + g),a,x)
then A17: x < b by A15, XXREAL_1:3;
then A18: [.a,x.] c= [.a,b.] by XXREAL_1:34;
A19: a <= x by A15, A16, XXREAL_1:3;
then A20: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A3, A17, Def1;
['a,x'] = [.a,x.] by A19, INTEGRA5:def_3;
then A21: ( ['a,x'] c= dom f & ['a,x'] c= dom g ) by A2, A14, A18, XBOOLE_1:1;
A22: ( g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A4, A19, A17, Def1;
thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by A16, VALUED_1:def_1
.= (integral (f,a,x)) + (Intg . x) by A9, A10, A15, A16
.= (integral (f,a,x)) + (integral (g,a,x)) by A5, A6, A15, A16
.= integral ((f + g),a,x) by A19, A21, A20, A22, INTEGRA6:12 ; ::_thesis: verum
end;
A23: for r being Element of REAL st r < b holds
ex g being Element of REAL st
( r < g & g < b & g in dom (Intf + Intg) )
proof
let r be Real; ::_thesis: ( r < b implies ex g being Element of REAL st
( r < g & g < b & g in dom (Intf + Intg) ) )
assume A24: r < b ; ::_thesis: ex g being Element of REAL st
( r < g & g < b & g in dom (Intf + Intg) )
percases ( r < a or not r < a ) ;
supposeA25: r < a ; ::_thesis: ex g being Element of REAL st
( r < g & g < b & g in dom (Intf + Intg) )
reconsider g = a as Real ;
take g ; ::_thesis: ( r < g & g < b & g in dom (Intf + Intg) )
thus ( r < g & g < b & g in dom (Intf + Intg) ) by A1, A13, A25, XXREAL_1:3; ::_thesis: verum
end;
suppose not r < a ; ::_thesis: ex g being Element of REAL st
( r < g & g < b & g in dom (Intf + Intg) )
then A26: a - a <= r - a by XREAL_1:9;
reconsider g = r + ((b - r) / 2) as Real ;
take g ; ::_thesis: ( r < g & g < b & g in dom (Intf + Intg) )
A27: 0 < b - r by A24, XREAL_1:50;
then (b - r) / 2 < b - r by XREAL_1:216;
then A28: ((b - r) / 2) + r < (b - r) + r by XREAL_1:8;
r < g by A27, XREAL_1:29, XREAL_1:215;
then A29: r - (r - a) < g - 0 by A26, XREAL_1:14;
0 < (b - r) / 2 by A27, XREAL_1:215;
hence ( r < g & g < b & g in dom (Intf + Intg) ) by A13, A29, A28, XREAL_1:8, XXREAL_1:3; ::_thesis: verum
end;
end;
end;
then A30: Intf + Intg is_left_convergent_in b by A11, A7, LIMFUNC2:45;
for d being Real st a <= d & d < b holds
( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded )
proof
let d be Real; ::_thesis: ( a <= d & d < b implies ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded ) )
assume A31: ( a <= d & d < b ) ; ::_thesis: ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded )
then A32: ( ['a,d'] = [.a,d.] & [.a,d.] c= [.a,b.] ) by INTEGRA5:def_3, XXREAL_1:34;
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A33: ( ['a,d'] c= dom f & ['a,d'] c= dom g ) by A2, A32, XBOOLE_1:1;
A34: ( f is_integrable_on ['a,d'] & g is_integrable_on ['a,d'] ) by A3, A4, A31, Def1;
A35: ( f | ['a,d'] is bounded & g | ['a,d'] is bounded ) by A3, A4, A31, Def1;
then (f + g) | (['a,d'] /\ ['a,d']) is bounded by RFUNCT_1:83;
hence ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded ) by A33, A34, A35, INTEGRA6:11; ::_thesis: verum
end;
hence A36: f + g is_right_ext_Riemann_integrable_on a,b by A13, A30, Def1; ::_thesis: ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b))
lim_left ((Intf + Intg),b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) by A11, A12, A7, A8, A23, LIMFUNC2:45;
hence ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) by A13, A30, A36, Def3; ::_thesis: verum
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
let f be PartFunc of REAL,REAL; ::_thesis: 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)) )
let a, b be Real; ::_thesis: ( a < b & ['a,b'] c= dom f & f is_right_ext_Riemann_integrable_on a,b implies 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)) ) )
assume that
A1: a < b and
A2: ['a,b'] c= dom f and
A3: f is_right_ext_Riemann_integrable_on a,b ; ::_thesis: 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 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
let r be Real; ::_thesis: ( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) )
consider Intf being PartFunc of REAL,REAL such that
A4: dom Intf = [.a,b.[ and
A5: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
A6: Intf is_left_convergent_in b and
A7: ext_right_integral (f,a,b) = lim_left (Intf,b) by A3, Def3;
set Intfg = r (#) Intf;
A8: r (#) Intf is_left_convergent_in b by A6, LIMFUNC2:43;
A9: ( dom (r (#) Intf) = [.a,b.[ & ( for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),a,x) ) )
proof
A10: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
thus A11: dom (r (#) Intf) = [.a,b.[ by A4, VALUED_1:def_5; ::_thesis: for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),a,x)
let x be Real; ::_thesis: ( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),a,x) )
assume A12: x in dom (r (#) Intf) ; ::_thesis: (r (#) Intf) . x = integral ((r (#) f),a,x)
then A13: a <= x by A11, XXREAL_1:3;
then A14: ['a,x'] = [.a,x.] by INTEGRA5:def_3;
A15: x < b by A11, A12, XXREAL_1:3;
then A16: [.a,x.] c= [.a,b.] by XXREAL_1:34;
A17: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A3, A13, A15, Def1;
thus (r (#) Intf) . x = r * (Intf . x) by A12, VALUED_1:def_5
.= r * (integral (f,a,x)) by A4, A5, A11, A12
.= integral ((r (#) f),a,x) by A2, A13, A14, A10, A16, A17, INTEGRA6:10, XBOOLE_1:1 ; ::_thesis: verum
end;
for d being Real st a <= d & d < b holds
( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded )
proof
let d be Real; ::_thesis: ( a <= d & d < b implies ( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded ) )
assume A18: ( a <= d & d < b ) ; ::_thesis: ( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded )
then A19: ( ['a,d'] = [.a,d.] & [.a,d.] c= [.a,b.] ) by INTEGRA5:def_3, XXREAL_1:34;
A20: ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A3, A18, Def1;
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then ['a,d'] c= dom f by A2, A19, XBOOLE_1:1;
hence ( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded ) by A20, INTEGRA6:9, RFUNCT_1:80; ::_thesis: verum
end;
hence A21: r (#) f is_right_ext_Riemann_integrable_on a,b by A9, A8, Def1; ::_thesis: ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b))
lim_left ((r (#) Intf),b) = r * (ext_right_integral (f,a,b)) by A6, A7, LIMFUNC2:43;
hence ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) by A9, A8, A21, Def3; ::_thesis: verum
end;
hence 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)) ) ; ::_thesis: verum
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
let f, g be PartFunc of REAL,REAL; ::_thesis: 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)) )
let a, b be Real; ::_thesis: ( 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 implies ( 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)) ) )
assume that
A1: a < b and
A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) and
A3: f is_left_ext_Riemann_integrable_on a,b and
A4: g is_left_ext_Riemann_integrable_on a,b ; ::_thesis: ( 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)) )
consider Intg being PartFunc of REAL,REAL such that
A5: dom Intg = ].a,b.] and
A6: for x being Real st x in dom Intg holds
Intg . x = integral (g,x,b) and
A7: Intg is_right_convergent_in a and
A8: ext_left_integral (g,a,b) = lim_right (Intg,a) by A4, Def4;
consider Intf being PartFunc of REAL,REAL such that
A9: dom Intf = ].a,b.] and
A10: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A11: Intf is_right_convergent_in a and
A12: ext_left_integral (f,a,b) = lim_right (Intf,a) by A3, Def4;
set Intfg = Intf + Intg;
A13: ( dom (Intf + Intg) = ].a,b.] & ( for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),x,b) ) )
proof
A14: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
thus A15: dom (Intf + Intg) = (dom Intf) /\ (dom Intg) by VALUED_1:def_1
.= ].a,b.] by A9, A5 ; ::_thesis: for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),x,b)
let x be Real; ::_thesis: ( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),x,b) )
assume A16: x in dom (Intf + Intg) ; ::_thesis: (Intf + Intg) . x = integral ((f + g),x,b)
then A17: a < x by A15, XXREAL_1:2;
then A18: [.x,b.] c= [.a,b.] by XXREAL_1:34;
A19: x <= b by A15, A16, XXREAL_1:2;
then A20: ( f is_integrable_on ['x,b'] & f | ['x,b'] is bounded ) by A3, A17, Def2;
['x,b'] = [.x,b.] by A19, INTEGRA5:def_3;
then A21: ( ['x,b'] c= dom f & ['x,b'] c= dom g ) by A2, A14, A18, XBOOLE_1:1;
A22: ( g is_integrable_on ['x,b'] & g | ['x,b'] is bounded ) by A4, A17, A19, Def2;
thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by A16, VALUED_1:def_1
.= (integral (f,x,b)) + (Intg . x) by A9, A10, A15, A16
.= (integral (f,x,b)) + (integral (g,x,b)) by A5, A6, A15, A16
.= integral ((f + g),x,b) by A19, A21, A20, A22, INTEGRA6:12 ; ::_thesis: verum
end;
A23: for r being Element of REAL st a < r holds
ex g being Element of REAL st
( g < r & a < g & g in dom (Intf + Intg) )
proof
let r be Real; ::_thesis: ( a < r implies ex g being Element of REAL st
( g < r & a < g & g in dom (Intf + Intg) ) )
assume A24: a < r ; ::_thesis: ex g being Element of REAL st
( g < r & a < g & g in dom (Intf + Intg) )
percases ( b < r or not b < r ) ;
supposeA25: b < r ; ::_thesis: ex g being Element of REAL st
( g < r & a < g & g in dom (Intf + Intg) )
reconsider g = b as Real ;
take g ; ::_thesis: ( g < r & a < g & g in dom (Intf + Intg) )
thus ( g < r & a < g & g in dom (Intf + Intg) ) by A1, A13, A25, XXREAL_1:2; ::_thesis: verum
end;
supposeA26: not b < r ; ::_thesis: ex g being Element of REAL st
( g < r & a < g & g in dom (Intf + Intg) )
reconsider g = r - ((r - a) / 2) as Real ;
take g ; ::_thesis: ( g < r & a < g & g in dom (Intf + Intg) )
A27: 0 < r - a by A24, XREAL_1:50;
then (r - a) / 2 < r - a by XREAL_1:216;
then A28: ((r - a) / 2) + (a - ((r - a) / 2)) < (r - a) + (a - ((r - a) / 2)) by XREAL_1:8;
A29: 0 < (r - a) / 2 by A27, XREAL_1:215;
then r - ((r - a) / 2) < b - 0 by A26, XREAL_1:15;
hence ( g < r & a < g & g in dom (Intf + Intg) ) by A13, A29, A28, XREAL_1:44, XXREAL_1:2; ::_thesis: verum
end;
end;
end;
then A30: Intf + Intg is_right_convergent_in a by A11, A7, LIMFUNC2:54;
for d being Real st a < d & d <= b holds
( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded )
proof
let d be Real; ::_thesis: ( a < d & d <= b implies ( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded ) )
assume A31: ( a < d & d <= b ) ; ::_thesis: ( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded )
then A32: ( ['d,b'] = [.d,b.] & [.d,b.] c= [.a,b.] ) by INTEGRA5:def_3, XXREAL_1:34;
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then A33: ( ['d,b'] c= dom f & ['d,b'] c= dom g ) by A2, A32, XBOOLE_1:1;
A34: ( f is_integrable_on ['d,b'] & g is_integrable_on ['d,b'] ) by A3, A4, A31, Def2;
A35: ( f | ['d,b'] is bounded & g | ['d,b'] is bounded ) by A3, A4, A31, Def2;
then (f + g) | (['d,b'] /\ ['d,b']) is bounded by RFUNCT_1:83;
hence ( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded ) by A33, A34, A35, INTEGRA6:11; ::_thesis: verum
end;
hence A36: f + g is_left_ext_Riemann_integrable_on a,b by A13, A30, Def2; ::_thesis: ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b))
lim_right ((Intf + Intg),a) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) by A11, A12, A7, A8, A23, LIMFUNC2:54;
hence ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) by A13, A30, A36, Def4; ::_thesis: verum
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
let f be PartFunc of REAL,REAL; ::_thesis: 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)) )
let a, b be Real; ::_thesis: ( a < b & ['a,b'] c= dom f & f is_left_ext_Riemann_integrable_on a,b implies 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)) ) )
assume that
A1: a < b and
A2: ['a,b'] c= dom f and
A3: f is_left_ext_Riemann_integrable_on a,b ; ::_thesis: 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 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
let r be Real; ::_thesis: ( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) )
consider Intf being PartFunc of REAL,REAL such that
A4: dom Intf = ].a,b.] and
A5: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A6: Intf is_right_convergent_in a and
A7: ext_left_integral (f,a,b) = lim_right (Intf,a) by A3, Def4;
set Intfg = r (#) Intf;
A8: r (#) Intf is_right_convergent_in a by A6, LIMFUNC2:52;
A9: ( dom (r (#) Intf) = ].a,b.] & ( for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),x,b) ) )
proof
A10: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
thus A11: dom (r (#) Intf) = ].a,b.] by A4, VALUED_1:def_5; ::_thesis: for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),x,b)
let x be Real; ::_thesis: ( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),x,b) )
assume A12: x in dom (r (#) Intf) ; ::_thesis: (r (#) Intf) . x = integral ((r (#) f),x,b)
then A13: a < x by A11, XXREAL_1:2;
then A14: [.x,b.] c= [.a,b.] by XXREAL_1:34;
A15: x <= b by A11, A12, XXREAL_1:2;
then A16: ['x,b'] = [.x,b.] by INTEGRA5:def_3;
A17: ( f is_integrable_on ['x,b'] & f | ['x,b'] is bounded ) by A3, A13, A15, Def2;
thus (r (#) Intf) . x = r * (Intf . x) by A12, VALUED_1:def_5
.= r * (integral (f,x,b)) by A4, A5, A11, A12
.= integral ((r (#) f),x,b) by A2, A15, A16, A10, A14, A17, INTEGRA6:10, XBOOLE_1:1 ; ::_thesis: verum
end;
for d being Real st a < d & d <= b holds
( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded )
proof
let d be Real; ::_thesis: ( a < d & d <= b implies ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded ) )
assume A18: ( a < d & d <= b ) ; ::_thesis: ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded )
then A19: ( ['d,b'] = [.d,b.] & [.d,b.] c= [.a,b.] ) by INTEGRA5:def_3, XXREAL_1:34;
A20: ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A3, A18, Def2;
['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
then ['d,b'] c= dom f by A2, A19, XBOOLE_1:1;
hence ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded ) by A20, INTEGRA6:9, RFUNCT_1:80; ::_thesis: verum
end;
hence A21: r (#) f is_left_ext_Riemann_integrable_on a,b by A9, A8, Def2; ::_thesis: ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b))
lim_right ((r (#) Intf),a) = r * (ext_left_integral (f,a,b)) by A6, A7, LIMFUNC2:52;
hence ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) by A9, A8, A21, Def4; ::_thesis: verum
end;
hence 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)) ) ; ::_thesis: verum
end;
theorem Th8: :: INTEGR10:8
for f, g being PartFunc of REAL,REAL
for a being real number 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
let f, g be PartFunc of REAL,REAL; ::_thesis: for a being real number 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)) )
let a be real number ; ::_thesis: ( 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 implies ( 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)) ) )
assume that
A1: ( right_closed_halfline a c= dom f & right_closed_halfline a c= dom g ) and
A2: f is_+infty_ext_Riemann_integrable_on a and
A3: g is_+infty_ext_Riemann_integrable_on a ; ::_thesis: ( 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)) )
consider Intg being PartFunc of REAL,REAL such that
A4: dom Intg = right_closed_halfline a and
A5: for x being Real st x in dom Intg holds
Intg . x = integral (g,a,x) and
A6: Intg is convergent_in+infty and
A7: infty_ext_right_integral (g,a) = lim_in+infty Intg by A3, Def7;
consider Intf being PartFunc of REAL,REAL such that
A8: dom Intf = right_closed_halfline a and
A9: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
A10: Intf is convergent_in+infty and
A11: infty_ext_right_integral (f,a) = lim_in+infty Intf by A2, Def7;
set Intfg = Intf + Intg;
A12: ( dom (Intf + Intg) = right_closed_halfline a & ( for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),a,x) ) )
proof
thus A13: dom (Intf + Intg) = (dom Intf) /\ (dom Intg) by VALUED_1:def_1
.= right_closed_halfline a by A8, A4 ; ::_thesis: for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),a,x)
let x be Real; ::_thesis: ( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),a,x) )
assume A14: x in dom (Intf + Intg) ; ::_thesis: (Intf + Intg) . x = integral ((f + g),a,x)
then A15: a <= x by A13, XXREAL_1:236;
then A16: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A2, Def5;
A17: [.a,x.] c= right_closed_halfline a by XXREAL_1:251;
['a,x'] = [.a,x.] by A15, INTEGRA5:def_3;
then A18: ( ['a,x'] c= dom f & ['a,x'] c= dom g ) by A1, A17, XBOOLE_1:1;
A19: ( g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A3, A15, Def5;
thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by A14, VALUED_1:def_1
.= (integral (f,a,x)) + (Intg . x) by A8, A9, A13, A14
.= (integral (f,a,x)) + (integral (g,a,x)) by A4, A5, A13, A14
.= integral ((f + g),a,x) by A15, A18, A16, A19, INTEGRA6:12 ; ::_thesis: verum
end;
A20: for r being Element of REAL ex g being Element of REAL st
( r < g & g in dom (Intf + Intg) )
proof
let r be Real; ::_thesis: ex g being Element of REAL st
( r < g & g in dom (Intf + Intg) )
percases ( r < a or not r < a ) ;
supposeA21: r < a ; ::_thesis: ex g being Element of REAL st
( r < g & g in dom (Intf + Intg) )
reconsider g = a as Real by XREAL_0:def_1;
take g ; ::_thesis: ( r < g & g in dom (Intf + Intg) )
thus ( r < g & g in dom (Intf + Intg) ) by A12, A21, XXREAL_1:236; ::_thesis: verum
end;
supposeA22: not r < a ; ::_thesis: ex g being Element of REAL st
( r < g & g in dom (Intf + Intg) )
reconsider g = r + 1 as Real ;
take g ; ::_thesis: ( r < g & g in dom (Intf + Intg) )
A23: r + 0 < r + 1 by XREAL_1:8;
then a <= g by A22, XXREAL_0:2;
hence ( r < g & g in dom (Intf + Intg) ) by A12, A23, XXREAL_1:236; ::_thesis: verum
end;
end;
end;
then A24: Intf + Intg is convergent_in+infty by A10, A6, LIMFUNC1:82;
for b being Real st a <= b holds
( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded )
proof
let b be Real; ::_thesis: ( a <= b implies ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) )
A25: [.a,b.] c= right_closed_halfline a by XXREAL_1:251;
assume A26: a <= b ; ::_thesis: ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded )
then A27: ( f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] ) by A2, A3, Def5;
['a,b'] = [.a,b.] by A26, INTEGRA5:def_3;
then A28: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) by A1, A25, XBOOLE_1:1;
A29: ( f | ['a,b'] is bounded & g | ['a,b'] is bounded ) by A2, A3, A26, Def5;
then (f + g) | (['a,b'] /\ ['a,b']) is bounded by RFUNCT_1:83;
hence ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) by A28, A27, A29, INTEGRA6:11; ::_thesis: verum
end;
hence A30: f + g is_+infty_ext_Riemann_integrable_on a by A12, A24, Def5; ::_thesis: infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a))
lim_in+infty (Intf + Intg) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) by A10, A11, A6, A7, A20, LIMFUNC1:82;
hence infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) by A12, A24, A30, Def7; ::_thesis: verum
end;
theorem Th9: :: INTEGR10:9
for f being PartFunc of REAL,REAL
for a being real number 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
let f be PartFunc of REAL,REAL; ::_thesis: for a being real number 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)) )
let a be real number ; ::_thesis: ( right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a implies 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)) ) )
assume that
A1: right_closed_halfline a c= dom f and
A2: f is_+infty_ext_Riemann_integrable_on a ; ::_thesis: 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 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
let r be Real; ::_thesis: ( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) )
consider Intf being PartFunc of REAL,REAL such that
A3: dom Intf = right_closed_halfline a and
A4: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
A5: Intf is convergent_in+infty and
A6: infty_ext_right_integral (f,a) = lim_in+infty Intf by A2, Def7;
set Intfg = r (#) Intf;
A7: r (#) Intf is convergent_in+infty by A5, LIMFUNC1:80;
A8: ( dom (r (#) Intf) = right_closed_halfline a & ( for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),a,x) ) )
proof
thus A9: dom (r (#) Intf) = right_closed_halfline a by A3, VALUED_1:def_5; ::_thesis: for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),a,x)
let x be Real; ::_thesis: ( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),a,x) )
assume A10: x in dom (r (#) Intf) ; ::_thesis: (r (#) Intf) . x = integral ((r (#) f),a,x)
then A11: a <= x by A9, XXREAL_1:236;
then A12: ( ['a,x'] = [.a,x.] & f is_integrable_on ['a,x'] ) by A2, Def5, INTEGRA5:def_3;
A13: ( [.a,x.] c= right_closed_halfline a & f | ['a,x'] is bounded ) by A2, A11, Def5, XXREAL_1:251;
thus (r (#) Intf) . x = r * (Intf . x) by A10, VALUED_1:def_5
.= r * (integral (f,a,x)) by A3, A4, A9, A10
.= integral ((r (#) f),a,x) by A1, A11, A12, A13, INTEGRA6:10, XBOOLE_1:1 ; ::_thesis: verum
end;
for b being Real st a <= b holds
( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded )
proof
let b be Real; ::_thesis: ( a <= b implies ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) )
A14: [.a,b.] c= right_closed_halfline a by XXREAL_1:251;
assume A15: a <= b ; ::_thesis: ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded )
then A16: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A2, Def5;
['a,b'] = [.a,b.] by A15, INTEGRA5:def_3;
then ['a,b'] c= dom f by A1, A14, XBOOLE_1:1;
hence ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) by A16, INTEGRA6:9, RFUNCT_1:80; ::_thesis: verum
end;
hence A17: r (#) f is_+infty_ext_Riemann_integrable_on a by A8, A7, Def5; ::_thesis: infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a))
lim_in+infty (r (#) Intf) = r * (infty_ext_right_integral (f,a)) by A5, A6, LIMFUNC1:80;
hence infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) by A8, A7, A17, Def7; ::_thesis: verum
end;
hence 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)) ) ; ::_thesis: verum
end;
theorem :: INTEGR10:10
for f, g being PartFunc of REAL,REAL
for b being real number 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
let f, g be PartFunc of REAL,REAL; ::_thesis: for b being real number 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)) )
let b be real number ; ::_thesis: ( 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 implies ( 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)) ) )
assume that
A1: ( left_closed_halfline b c= dom f & left_closed_halfline b c= dom g ) and
A2: f is_-infty_ext_Riemann_integrable_on b and
A3: g is_-infty_ext_Riemann_integrable_on b ; ::_thesis: ( 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)) )
consider Intg being PartFunc of REAL,REAL such that
A4: dom Intg = left_closed_halfline b and
A5: for x being Real st x in dom Intg holds
Intg . x = integral (g,x,b) and
A6: Intg is convergent_in-infty and
A7: infty_ext_left_integral (g,b) = lim_in-infty Intg by A3, Def8;
consider Intf being PartFunc of REAL,REAL such that
A8: dom Intf = left_closed_halfline b and
A9: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A10: Intf is convergent_in-infty and
A11: infty_ext_left_integral (f,b) = lim_in-infty Intf by A2, Def8;
set Intfg = Intf + Intg;
A12: ( dom (Intf + Intg) = left_closed_halfline b & ( for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),x,b) ) )
proof
thus A13: dom (Intf + Intg) = (dom Intf) /\ (dom Intg) by VALUED_1:def_1
.= left_closed_halfline b by A8, A4 ; ::_thesis: for x being Real st x in dom (Intf + Intg) holds
(Intf + Intg) . x = integral ((f + g),x,b)
let x be Real; ::_thesis: ( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),x,b) )
assume A14: x in dom (Intf + Intg) ; ::_thesis: (Intf + Intg) . x = integral ((f + g),x,b)
then A15: x <= b by A13, XXREAL_1:234;
then A16: ( f is_integrable_on ['x,b'] & f | ['x,b'] is bounded ) by A2, Def6;
A17: [.x,b.] c= left_closed_halfline b by XXREAL_1:265;
['x,b'] = [.x,b.] by A15, INTEGRA5:def_3;
then A18: ( ['x,b'] c= dom f & ['x,b'] c= dom g ) by A1, A17, XBOOLE_1:1;
A19: ( g is_integrable_on ['x,b'] & g | ['x,b'] is bounded ) by A3, A15, Def6;
thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by A14, VALUED_1:def_1
.= (integral (f,x,b)) + (Intg . x) by A8, A9, A13, A14
.= (integral (f,x,b)) + (integral (g,x,b)) by A4, A5, A13, A14
.= integral ((f + g),x,b) by A15, A18, A16, A19, INTEGRA6:12 ; ::_thesis: verum
end;
A20: for r being Element of REAL ex g being Element of REAL st
( g < r & g in dom (Intf + Intg) )
proof
let r be Real; ::_thesis: ex g being Element of REAL st
( g < r & g in dom (Intf + Intg) )
percases ( b < r or not b < r ) ;
supposeA21: b < r ; ::_thesis: ex g being Element of REAL st
( g < r & g in dom (Intf + Intg) )
reconsider g = b as Real by XREAL_0:def_1;
take g ; ::_thesis: ( g < r & g in dom (Intf + Intg) )
thus ( g < r & g in dom (Intf + Intg) ) by A12, A21, XXREAL_1:234; ::_thesis: verum
end;
supposeA22: not b < r ; ::_thesis: ex g being Element of REAL st
( g < r & g in dom (Intf + Intg) )
reconsider g = r - 1 as Real ;
take g ; ::_thesis: ( g < r & g in dom (Intf + Intg) )
A23: r - 1 < r - 0 by XREAL_1:15;
then g <= b by A22, XXREAL_0:2;
hence ( g < r & g in dom (Intf + Intg) ) by A12, A23, XXREAL_1:234; ::_thesis: verum
end;
end;
end;
then A24: Intf + Intg is convergent_in-infty by A10, A6, LIMFUNC1:91;
for a being Real st a <= b holds
( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded )
proof
let a be Real; ::_thesis: ( a <= b implies ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) )
A25: [.a,b.] c= left_closed_halfline b by XXREAL_1:265;
assume A26: a <= b ; ::_thesis: ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded )
then A27: ( f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] ) by A2, A3, Def6;
['a,b'] = [.a,b.] by A26, INTEGRA5:def_3;
then A28: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) by A1, A25, XBOOLE_1:1;
A29: ( f | ['a,b'] is bounded & g | ['a,b'] is bounded ) by A2, A3, A26, Def6;
then (f + g) | (['a,b'] /\ ['a,b']) is bounded by RFUNCT_1:83;
hence ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) by A28, A27, A29, INTEGRA6:11; ::_thesis: verum
end;
hence A30: f + g is_-infty_ext_Riemann_integrable_on b by A12, A24, Def6; ::_thesis: infty_ext_left_integral ((f + g),b) = (infty_ext_left_integral (f,b)) + (infty_ext_left_integral (g,b))
lim_in-infty (Intf + Intg) = (infty_ext_left_integral (f,b)) + (infty_ext_left_integral (g,b)) by A10, A11, A6, A7, A20, LIMFUNC1:91;
hence infty_ext_left_integral ((f + g),b) = (infty_ext_left_integral (f,b)) + (infty_ext_left_integral (g,b)) by A12, A24, A30, Def8; ::_thesis: verum
end;
theorem :: INTEGR10:11
for f being PartFunc of REAL,REAL
for b being real number 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
let f be PartFunc of REAL,REAL; ::_thesis: for b being real number 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)) )
let b be real number ; ::_thesis: ( left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b implies 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)) ) )
assume that
A1: left_closed_halfline b c= dom f and
A2: f is_-infty_ext_Riemann_integrable_on b ; ::_thesis: 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 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
let r be Real; ::_thesis: ( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) )
consider Intf being PartFunc of REAL,REAL such that
A3: dom Intf = left_closed_halfline b and
A4: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A5: Intf is convergent_in-infty and
A6: infty_ext_left_integral (f,b) = lim_in-infty Intf by A2, Def8;
set Intfg = r (#) Intf;
A7: r (#) Intf is convergent_in-infty by A5, LIMFUNC1:89;
A8: ( dom (r (#) Intf) = left_closed_halfline b & ( for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),x,b) ) )
proof
thus A9: dom (r (#) Intf) = left_closed_halfline b by A3, VALUED_1:def_5; ::_thesis: for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),x,b)
let x be Real; ::_thesis: ( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),x,b) )
assume A10: x in dom (r (#) Intf) ; ::_thesis: (r (#) Intf) . x = integral ((r (#) f),x,b)
then A11: x <= b by A9, XXREAL_1:234;
then A12: ( ['x,b'] = [.x,b.] & f is_integrable_on ['x,b'] ) by A2, Def6, INTEGRA5:def_3;
A13: ( [.x,b.] c= left_closed_halfline b & f | ['x,b'] is bounded ) by A2, A11, Def6, XXREAL_1:265;
thus (r (#) Intf) . x = r * (Intf . x) by A10, VALUED_1:def_5
.= r * (integral (f,x,b)) by A3, A4, A9, A10
.= integral ((r (#) f),x,b) by A1, A11, A12, A13, INTEGRA6:10, XBOOLE_1:1 ; ::_thesis: verum
end;
for a being Real st a <= b holds
( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded )
proof
let a be Real; ::_thesis: ( a <= b implies ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) )
A14: [.a,b.] c= left_closed_halfline b by XXREAL_1:265;
assume A15: a <= b ; ::_thesis: ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded )
then A16: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A2, Def6;
['a,b'] = [.a,b.] by A15, INTEGRA5:def_3;
then ['a,b'] c= dom f by A1, A14, XBOOLE_1:1;
hence ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) by A16, INTEGRA6:9, RFUNCT_1:80; ::_thesis: verum
end;
hence A17: r (#) f is_-infty_ext_Riemann_integrable_on b by A8, A7, Def6; ::_thesis: infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b))
lim_in-infty (r (#) Intf) = r * (infty_ext_left_integral (f,b)) by A5, A6, LIMFUNC1:89;
hence infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) by A8, A7, A17, Def8; ::_thesis: verum
end;
hence 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)) ) ; ::_thesis: verum
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
let f be PartFunc of REAL,REAL; ::_thesis: 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)
let a, b be Real; ::_thesis: ( a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies ext_right_integral (f,a,b) = integral (f,a,b) )
assume that
A1: a < b and
A2: ['a,b'] c= dom f and
A3: f is_integrable_on ['a,b'] and
A4: f | ['a,b'] is bounded ; ::_thesis: ext_right_integral (f,a,b) = integral (f,a,b)
reconsider AB = [.a,b.[ as non empty Subset of REAL by A1, XXREAL_1:3;
deffunc H1( Element of AB) -> Element of REAL = integral (f,a,$1);
consider Intf being Function of AB,REAL such that
A5: for x being Element of AB holds Intf . x = H1(x) from FUNCT_2:sch_4();
A6: dom Intf = AB by FUNCT_2:def_1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
consider M0 being real number such that
A7: for x being set st x in ['a,b'] /\ (dom f) holds
abs (f . x) <= M0 by A4, RFUNCT_1:73;
reconsider M = M0 + 1 as Real ;
A8: for x being Real st x in ['a,b'] holds
abs (f . x) < M
proof
A9: ['a,b'] /\ (dom f) = ['a,b'] by A2, XBOOLE_1:28;
let x be Real; ::_thesis: ( x in ['a,b'] implies abs (f . x) < M )
assume x in ['a,b'] ; ::_thesis: abs (f . x) < M
hence abs (f . x) < M by A7, A9, XREAL_1:39; ::_thesis: verum
end;
a in { r where r is Real : ( a <= r & r <= b ) } by A1;
then a in [.a,b.] by RCOMP_1:def_1;
then a in ['a,b'] by A1, INTEGRA5:def_3;
then abs (f . a) < M by A8;
then A10: 0 < M by COMPLEX1:46;
A11: for g1 being Real st 0 < g1 holds
ex r being Real st
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ) )
proof
let g1 be Real; ::_thesis: ( 0 < g1 implies ex r being Real st
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ) ) )
assume 0 < g1 ; ::_thesis: ex r being Real st
( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ) )
then consider r being Real such that
A12: a < r and
A13: r < b and
A14: (b - r) * M < g1 by A1, A10, Th1;
take r ; ::_thesis: ( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ) )
thus r < b by A13; ::_thesis: for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1
now__::_thesis:_for_r1_being_Real_st_r_<_r1_&_r1_<_b_&_r1_in_dom_Intf_holds_
abs_((Intf_._r1)_-_(integral_(f,a,b)))_<_g1
let r1 be Real; ::_thesis: ( r < r1 & r1 < b & r1 in dom Intf implies abs ((Intf . r1) - (integral (f,a,b))) < g1 )
assume that
A15: r < r1 and
A16: r1 < b and
A17: r1 in dom Intf ; ::_thesis: abs ((Intf . r1) - (integral (f,a,b))) < g1
A18: Intf . r1 = integral (f,a,r1) by A5, A6, A17;
A19: a <= r1 by A12, A15, XXREAL_0:2;
then r1 in [.a,b.] by A16, XXREAL_1:1;
then A20: r1 in ['a,b'] by A1, INTEGRA5:def_3;
b - r1 < b - r by A15, XREAL_1:15;
then A21: M * (b - r1) < M * (b - r) by A10, XREAL_1:68;
A22: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
[.r1,b.] = ['r1,b'] by A16, INTEGRA5:def_3;
then ['r1,b'] c= ['a,b'] by A22, A19, XXREAL_1:34;
then A23: for x being real number st x in ['r1,b'] holds
abs (f . x) <= M by A8;
b in ['a,b'] by A1, A22, XXREAL_1:1;
then abs (integral (f,r1,b)) <= M * (b - r1) by A1, A2, A3, A4, A16, A20, A23, INTEGRA6:23;
then A24: abs (integral (f,r1,b)) < M * (b - r) by A21, XXREAL_0:2;
abs ((Intf . r1) - (integral (f,a,b))) = abs ((integral (f,a,b)) - (Intf . r1)) by COMPLEX1:60
.= abs (((integral (f,a,r1)) + (integral (f,r1,b))) - (integral (f,a,r1))) by A1, A2, A3, A4, A18, A20, INTEGRA6:17
.= abs (integral (f,r1,b)) ;
hence abs ((Intf . r1) - (integral (f,a,b))) < g1 by A14, A24, XXREAL_0:2; ::_thesis: verum
end;
hence for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ; ::_thesis: verum
end;
A25: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) by A5, A6;
for r being Real st r < b holds
ex g being Real st
( r < g & g < b & g in dom Intf )
proof
let r be Element of REAL ; ::_thesis: ( r < b implies ex g being Real st
( r < g & g < b & g in dom Intf ) )
assume A26: r < b ; ::_thesis: ex g being Real st
( r < g & g < b & g in dom Intf )
percases ( r < a or not r < a ) ;
supposeA27: r < a ; ::_thesis: ex g being Real st
( r < g & g < b & g in dom Intf )
reconsider g = a as Real ;
take g ; ::_thesis: ( r < g & g < b & g in dom Intf )
thus ( r < g & g < b & g in dom Intf ) by A1, A6, A27, XXREAL_1:3; ::_thesis: verum
end;
suppose not r < a ; ::_thesis: ex g being Real st
( r < g & g < b & g in dom Intf )
then A28: a - a <= r - a by XREAL_1:9;
reconsider g = r + ((b - r) / 2) as Real ;
take g ; ::_thesis: ( r < g & g < b & g in dom Intf )
A29: 0 < b - r by A26, XREAL_1:50;
then (b - r) / 2 < b - r by XREAL_1:216;
then A30: ((b - r) / 2) + r < (b - r) + r by XREAL_1:8;
r < g by A29, XREAL_1:29, XREAL_1:215;
then A31: r - (r - a) < g - 0 by A28, XREAL_1:14;
0 < (b - r) / 2 by A29, XREAL_1:215;
hence ( r < g & g < b & g in dom Intf ) by A6, A31, A30, XREAL_1:8, XXREAL_1:3; ::_thesis: verum
end;
end;
end;
then A32: Intf is_left_convergent_in b by A11, LIMFUNC2:7;
then A33: integral (f,a,b) = lim_left (Intf,b) by A11, LIMFUNC2:41;
for d being Real st a <= d & d < b holds
( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A2, A3, A4, INTEGRA6:18;
then f is_right_ext_Riemann_integrable_on a,b by A6, A25, A32, Def1;
hence ext_right_integral (f,a,b) = integral (f,a,b) by A6, A25, A32, A33, Def3; ::_thesis: verum
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
let f be PartFunc of REAL,REAL; ::_thesis: 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)
let a, b be Real; ::_thesis: ( a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies ext_left_integral (f,a,b) = integral (f,a,b) )
assume that
A1: a < b and
A2: ['a,b'] c= dom f and
A3: f is_integrable_on ['a,b'] and
A4: f | ['a,b'] is bounded ; ::_thesis: ext_left_integral (f,a,b) = integral (f,a,b)
reconsider AB = ].a,b.] as non empty Subset of REAL by A1, XXREAL_1:2;
deffunc H1( Element of AB) -> Element of REAL = integral (f,$1,b);
consider Intf being Function of AB,REAL such that
A5: for x being Element of AB holds Intf . x = H1(x) from FUNCT_2:sch_4();
A6: dom Intf = AB by FUNCT_2:def_1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
consider M0 being real number such that
A7: for x being set st x in ['a,b'] /\ (dom f) holds
abs (f . x) <= M0 by A4, RFUNCT_1:73;
reconsider M = M0 + 1 as Real ;
A8: for x being Real st x in ['a,b'] holds
abs (f . x) < M
proof
A9: ['a,b'] /\ (dom f) = ['a,b'] by A2, XBOOLE_1:28;
let x be Real; ::_thesis: ( x in ['a,b'] implies abs (f . x) < M )
assume x in ['a,b'] ; ::_thesis: abs (f . x) < M
hence abs (f . x) < M by A7, A9, XREAL_1:39; ::_thesis: verum
end;
a in { r where r is Real : ( a <= r & r <= b ) } by A1;
then a in [.a,b.] by RCOMP_1:def_1;
then a in ['a,b'] by A1, INTEGRA5:def_3;
then abs (f . a) < M by A8;
then A10: 0 < M by COMPLEX1:46;
A11: for g1 being Real st 0 < g1 holds
ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ) )
proof
let g1 be Real; ::_thesis: ( 0 < g1 implies ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ) ) )
assume 0 < g1 ; ::_thesis: ex r being Real st
( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ) )
then consider r being Real such that
A12: a < r and
A13: r < b and
A14: (r - a) * M < g1 by A1, A10, Th2;
take r ; ::_thesis: ( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ) )
thus a < r by A12; ::_thesis: for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1
now__::_thesis:_for_r1_being_Real_st_a_<_r1_&_r1_<_r_&_r1_in_dom_Intf_holds_
abs_((Intf_._r1)_-_(integral_(f,a,b)))_<_g1
let r1 be Real; ::_thesis: ( a < r1 & r1 < r & r1 in dom Intf implies abs ((Intf . r1) - (integral (f,a,b))) < g1 )
assume that
A15: a < r1 and
A16: r1 < r and
A17: r1 in dom Intf ; ::_thesis: abs ((Intf . r1) - (integral (f,a,b))) < g1
A18: Intf . r1 = integral (f,r1,b) by A5, A6, A17;
r1 - a < r - a by A16, XREAL_1:14;
then A19: M * (r1 - a) < M * (r - a) by A10, XREAL_1:68;
A20: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3;
A21: r1 <= b by A13, A16, XXREAL_0:2;
then A22: r1 in ['a,b'] by A15, A20, XXREAL_1:1;
[.a,r1.] = ['a,r1'] by A15, INTEGRA5:def_3;
then ['a,r1'] c= ['a,b'] by A20, A21, XXREAL_1:34;
then A23: for x being real number st x in ['a,r1'] holds
abs (f . x) <= M by A8;
a in ['a,b'] by A1, A20, XXREAL_1:1;
then abs (integral (f,a,r1)) <= M * (r1 - a) by A1, A2, A3, A4, A15, A22, A23, INTEGRA6:23;
then A24: abs (integral (f,a,r1)) < M * (r - a) by A19, XXREAL_0:2;
abs ((Intf . r1) - (integral (f,a,b))) = abs ((integral (f,a,b)) - (Intf . r1)) by COMPLEX1:60
.= abs (((integral (f,a,r1)) + (integral (f,r1,b))) - (integral (f,r1,b))) by A1, A2, A3, A4, A18, A22, INTEGRA6:17
.= abs (integral (f,a,r1)) ;
hence abs ((Intf . r1) - (integral (f,a,b))) < g1 by A14, A24, XXREAL_0:2; ::_thesis: verum
end;
hence for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds
abs ((Intf . r1) - (integral (f,a,b))) < g1 ; ::_thesis: verum
end;
A25: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) by A5, A6;
for r being Real st a < r holds
ex g being Real st
( g < r & a < g & g in dom Intf )
proof
let r be Element of REAL ; ::_thesis: ( a < r implies ex g being Real st
( g < r & a < g & g in dom Intf ) )
assume A26: a < r ; ::_thesis: ex g being Real st
( g < r & a < g & g in dom Intf )
percases ( b < r or not b < r ) ;
supposeA27: b < r ; ::_thesis: ex g being Real st
( g < r & a < g & g in dom Intf )
reconsider g = b as Real ;
take g ; ::_thesis: ( g < r & a < g & g in dom Intf )
g in ].a,b.] by A1, XXREAL_1:2;
hence ( g < r & a < g & g in dom Intf ) by A1, A27, FUNCT_2:def_1; ::_thesis: verum
end;
supposeA28: not b < r ; ::_thesis: ex g being Real st
( g < r & a < g & g in dom Intf )
reconsider g = a + ((r - a) / 2) as Real ;
take g ; ::_thesis: ( g < r & a < g & g in dom Intf )
A29: 0 < r - a by A26, XREAL_1:50;
then A30: a < g by XREAL_1:29, XREAL_1:215;
(r - a) / 2 < r - a by A29, XREAL_1:216;
then A31: ((r - a) / 2) + a < (r - a) + a by XREAL_1:8;
then g < b by A28, XXREAL_0:2;
hence ( g < r & a < g & g in dom Intf ) by A6, A30, A31, XXREAL_1:2; ::_thesis: verum
end;
end;
end;
then A32: Intf is_right_convergent_in a by A11, LIMFUNC2:10;
then A33: integral (f,a,b) = lim_right (Intf,a) by A11, LIMFUNC2:42;
for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A2, A3, A4, INTEGRA6:18;
then f is_left_ext_Riemann_integrable_on a,b by A6, A25, A32, Def2;
hence ext_left_integral (f,a,b) = integral (f,a,b) by A6, A25, A32, A33, Def4; ::_thesis: verum
end;
begin
definition
let s be real number ;
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
deffunc H1( Real) -> Element of REAL = exp_R . (- (s * $1));
consider g being Function of REAL,REAL such that
A1: for x being Element of REAL holds g . x = H1(x) from FUNCT_2:sch_4();
take g ; ::_thesis: for t being Real holds g . t = exp_R . (- (s * t))
thus for t being Real holds g . t = exp_R . (- (s * t)) by A1; ::_thesis: verum
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
let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for t being Real holds f1 . t = exp_R . (- (s * t)) ) & ( for t being Real holds f2 . t = exp_R . (- (s * t)) ) implies f1 = f2 )
assume that
A2: for d being Real holds f1 . d = exp_R . (- (s * d)) and
A3: for d being Real holds f2 . d = exp_R . (- (s * d)) ; ::_thesis: f1 = f2
for d being Element of REAL holds f1 . d = f2 . d
proof
let d be Element of REAL ; ::_thesis: f1 . d = f2 . d
thus f1 . d = exp_R . (- (s * d)) by A2
.= f2 . d by A3 ; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: 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)) );
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) ) );
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 (#) (exp*- s)),0) ) )
proof
defpred S1[ Element of REAL , Element of REAL ] means ( $1 in right_open_halfline 0 & $2 = infty_ext_right_integral ((f (#) (exp*- $1)),0) );
consider g being PartFunc of REAL,REAL such that
A1: ( ( for d being Element of REAL holds
( d in dom g iff ex c being Element of REAL st S1[d,c] ) ) & ( for d being Element of REAL st d in dom g holds
S1[d,g /. d] ) ) from PARTFUN2:sch_1();
A2: dom g = right_open_halfline 0
proof
let s1 be real number ; :: according to MEMBERED:def_15 ::_thesis: ( ( not s1 in dom g or s1 in right_open_halfline 0 ) & ( not s1 in right_open_halfline 0 or s1 in dom g ) )
reconsider s = s1 as Real by XREAL_0:def_1;
( s in right_open_halfline 0 implies s in dom g )
proof
assume s in right_open_halfline 0 ; ::_thesis: s in dom g
then ex y being Element of REAL st
( s in right_open_halfline 0 & y = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ;
hence s in dom g by A1; ::_thesis: verum
end;
hence ( ( not s1 in dom g or s1 in right_open_halfline 0 ) & ( not s1 in right_open_halfline 0 or s1 in dom g ) ) by A1; ::_thesis: verum
end;
take g ; ::_thesis: ( dom g = right_open_halfline 0 & ( for s being Real st s in dom g holds
g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) )
for s being Real st s in dom g holds
g . s = infty_ext_right_integral ((f (#) (exp*- s)),0)
proof
let s be Real; ::_thesis: ( s in dom g implies g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) )
assume A3: s in dom g ; ::_thesis: g . s = infty_ext_right_integral ((f (#) (exp*- s)),0)
then g /. s = infty_ext_right_integral ((f (#) (exp*- s)),0) by A1;
hence g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) by A3, PARTFUN1:def_6; ::_thesis: verum
end;
hence ( dom g = right_open_halfline 0 & ( for s being Real st s in dom g holds
g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ) by A2; ::_thesis: verum
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 (#) (exp*- s)),0) ) & 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) ) holds
b1 = b2
proof
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( dom f1 = right_open_halfline 0 & ( for s being Real st s in dom f1 holds
f1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) & dom f2 = right_open_halfline 0 & ( for s being Real st s in dom f2 holds
f2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) implies f1 = f2 )
assume that
A4: dom f1 = right_open_halfline 0 and
A5: for s being Real st s in dom f1 holds
f1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ; ::_thesis: ( not dom f2 = right_open_halfline 0 or ex s being Real st
( s in dom f2 & not f2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) or f1 = f2 )
assume that
A6: dom f2 = right_open_halfline 0 and
A7: for s being Real st s in dom f2 holds
f2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ; ::_thesis: f1 = f2
for s being Element of REAL st s in dom f1 holds
f1 . s = f2 . s
proof
let s be Element of REAL ; ::_thesis: ( s in dom f1 implies f1 . s = f2 . s )
assume A8: s in dom f1 ; ::_thesis: f1 . s = f2 . s
f1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) by A5, A8;
hence f1 . s = f2 . s by A4, A6, A7, A8; ::_thesis: verum
end;
hence f1 = f2 by A4, A6, PARTFUN1:5; ::_thesis: verum
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 (#) (exp*- s)),0) ) ) );
begin
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
let f, g be PartFunc of REAL,REAL; ::_thesis: ( 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 ) implies ( ( 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) ) )
assume that
A1: dom f = right_closed_halfline 0 and
A2: dom g = right_closed_halfline 0 and
A3: ( ( 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 ) ) ; ::_thesis: ( ( 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) )
set Intg = One-sided_Laplace_transform g;
set Intf = One-sided_Laplace_transform f;
set F = (One-sided_Laplace_transform f) + (One-sided_Laplace_transform g);
A4: dom ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) = (dom (One-sided_Laplace_transform f)) /\ (dom (One-sided_Laplace_transform g)) by VALUED_1:def_1
.= (right_open_halfline 0) /\ (dom (One-sided_Laplace_transform g)) by Def12
.= (right_open_halfline 0) /\ (right_open_halfline 0) by Def12
.= right_open_halfline 0 ;
A5: for s being Real st s in right_open_halfline 0 holds
( (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((f + g) (#) (exp*- s)),0) = (infty_ext_right_integral ((f (#) (exp*- s)),0)) + (infty_ext_right_integral ((g (#) (exp*- s)),0)) )
proof
let s be Real; ::_thesis: ( s in right_open_halfline 0 implies ( (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((f + g) (#) (exp*- s)),0) = (infty_ext_right_integral ((f (#) (exp*- s)),0)) + (infty_ext_right_integral ((g (#) (exp*- s)),0)) ) )
A6: (f + g) (#) (exp*- s) = (f (#) (exp*- s)) + (g (#) (exp*- s)) by RFUNCT_1:10;
A7: dom (g (#) (exp*- s)) = (dom g) /\ (dom (exp*- s)) by VALUED_1:def_4
.= (right_closed_halfline 0) /\ REAL by A2, FUNCT_2:def_1
.= right_closed_halfline 0 by XBOOLE_1:28 ;
assume s in right_open_halfline 0 ; ::_thesis: ( (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((f + g) (#) (exp*- s)),0) = (infty_ext_right_integral ((f (#) (exp*- s)),0)) + (infty_ext_right_integral ((g (#) (exp*- s)),0)) )
then A8: ( f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & g (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) by A3;
dom (f (#) (exp*- s)) = (dom f) /\ (dom (exp*- s)) by VALUED_1:def_4
.= (right_closed_halfline 0) /\ REAL by A1, FUNCT_2:def_1
.= right_closed_halfline 0 by XBOOLE_1:28 ;
hence ( (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((f + g) (#) (exp*- s)),0) = (infty_ext_right_integral ((f (#) (exp*- s)),0)) + (infty_ext_right_integral ((g (#) (exp*- s)),0)) ) by A8, A6, A7, Th8; ::_thesis: verum
end;
for s being Real st s in dom ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) holds
((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s = infty_ext_right_integral (((f + g) (#) (exp*- s)),0)
proof
let s be Real; ::_thesis: ( s in dom ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) implies ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s = infty_ext_right_integral (((f + g) (#) (exp*- s)),0) )
assume A9: s in dom ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) ; ::_thesis: ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s = infty_ext_right_integral (((f + g) (#) (exp*- s)),0)
then A10: s in dom (One-sided_Laplace_transform f) by A4, Def12;
A11: s in dom (One-sided_Laplace_transform g) by A4, A9, Def12;
thus infty_ext_right_integral (((f + g) (#) (exp*- s)),0) = (infty_ext_right_integral ((f (#) (exp*- s)),0)) + (infty_ext_right_integral ((g (#) (exp*- s)),0)) by A5, A4, A9
.= ((One-sided_Laplace_transform f) . s) + (infty_ext_right_integral ((g (#) (exp*- s)),0)) by A10, Def12
.= ((One-sided_Laplace_transform f) . s) + ((One-sided_Laplace_transform g) . s) by A11, Def12
.= ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s by A9, VALUED_1:def_1 ; ::_thesis: verum
end;
hence ( ( 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) ) by A5, A4, Def12; ::_thesis: verum
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
let f be PartFunc of REAL,REAL; ::_thesis: 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) )
let a be Real; ::_thesis: ( 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 ) implies ( ( 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) ) )
assume that
A1: dom f = right_closed_halfline 0 and
A2: for s being Real st s in right_open_halfline 0 holds
f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ; ::_thesis: ( ( 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) )
set Intf = One-sided_Laplace_transform f;
set F = a (#) (One-sided_Laplace_transform f);
A3: dom (a (#) (One-sided_Laplace_transform f)) = dom (One-sided_Laplace_transform f) by VALUED_1:def_5
.= right_open_halfline 0 by Def12 ;
A4: for s being Real st s in right_open_halfline 0 holds
( (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) = a * (infty_ext_right_integral ((f (#) (exp*- s)),0)) )
proof
let s be Real; ::_thesis: ( s in right_open_halfline 0 implies ( (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) = a * (infty_ext_right_integral ((f (#) (exp*- s)),0)) ) )
A5: (a (#) f) (#) (exp*- s) = a (#) (f (#) (exp*- s)) by RFUNCT_1:12;
assume s in right_open_halfline 0 ; ::_thesis: ( (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) = a * (infty_ext_right_integral ((f (#) (exp*- s)),0)) )
then A6: f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 by A2;
dom (f (#) (exp*- s)) = (dom f) /\ (dom (exp*- s)) by VALUED_1:def_4
.= (right_closed_halfline 0) /\ REAL by A1, FUNCT_2:def_1
.= right_closed_halfline 0 by XBOOLE_1:28 ;
hence ( (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) = a * (infty_ext_right_integral ((f (#) (exp*- s)),0)) ) by A6, A5, Th9; ::_thesis: verum
end;
for s being Real st s in dom (a (#) (One-sided_Laplace_transform f)) holds
(a (#) (One-sided_Laplace_transform f)) . s = infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0)
proof
let s be Real; ::_thesis: ( s in dom (a (#) (One-sided_Laplace_transform f)) implies (a (#) (One-sided_Laplace_transform f)) . s = infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) )
assume A7: s in dom (a (#) (One-sided_Laplace_transform f)) ; ::_thesis: (a (#) (One-sided_Laplace_transform f)) . s = infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0)
then A8: s in dom (One-sided_Laplace_transform f) by A3, Def12;
thus infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) = a * (infty_ext_right_integral ((f (#) (exp*- s)),0)) by A4, A3, A7
.= a * ((One-sided_Laplace_transform f) . s) by A8, Def12
.= (a (#) (One-sided_Laplace_transform f)) . s by VALUED_1:6 ; ::_thesis: verum
end;
hence ( ( 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) ) by A4, A3, Def12; ::_thesis: verum
end;