:: Improper Integral, Part {II}
:: by Noboru Endou
::
:: Received December 8, 2021
:: Copyright (c) 2021 Association of Mizar Users


theorem Th1: :: INTEGR25:1
for f being PartFunc of REAL,REAL st f is divergent_in-infty_to+infty holds
( not f is convergent_in-infty & not f is divergent_in-infty_to-infty )
proof end;

theorem Th2: :: INTEGR25:2
for f being PartFunc of REAL,REAL st f is divergent_in-infty_to-infty holds
( not f is convergent_in-infty & not f is divergent_in-infty_to+infty )
proof end;

theorem Th3: :: INTEGR25:3
for f being PartFunc of REAL,REAL st f is divergent_in+infty_to+infty holds
( not f is convergent_in+infty & not f is divergent_in+infty_to-infty )
proof end;

theorem Th4: :: INTEGR25:4
for f being PartFunc of REAL,REAL st f is divergent_in+infty_to-infty holds
( not f is convergent_in+infty & not f is divergent_in+infty_to+infty )
proof end;

theorem Th5: :: INTEGR25:5
for f being PartFunc of REAL,REAL st f is convergent_in-infty holds
( ex r being Real st f | (left_open_halfline r) is bounded_below & ex r being Real st f | (left_open_halfline r) is bounded_above )
proof end;

theorem Th6: :: INTEGR25:6
for f being PartFunc of REAL,REAL st f is convergent_in+infty holds
( ex r being Real st f | (right_open_halfline r) is bounded_below & ex r being Real st f | (right_open_halfline r) is bounded_above )
proof end;

theorem Th7: :: INTEGR25:7
for f being PartFunc of REAL,REAL st f is divergent_in-infty_to+infty holds
ex r being Real st f | (left_open_halfline r) is bounded_below
proof end;

theorem Th8: :: INTEGR25:8
for f being PartFunc of REAL,REAL st f is divergent_in-infty_to-infty holds
ex r being Real st f | (left_open_halfline r) is bounded_above
proof end;

theorem Th9: :: INTEGR25:9
for f being PartFunc of REAL,REAL st f is divergent_in+infty_to+infty holds
ex r being Real st f | (right_open_halfline r) is bounded_below
proof end;

theorem Th10: :: INTEGR25:10
for f being PartFunc of REAL,REAL st f is divergent_in+infty_to-infty holds
ex r being Real st f | (right_open_halfline r) is bounded_above
proof end;

Lm1: for seq being Real_Sequence
for f1, f2 being PartFunc of REAL,REAL st rng seq c= dom (f1 + f2) holds
( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 )

proof end;

theorem Th11: :: INTEGR25:11
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st
( g < r & g in dom (f1 + f2) ) ) & ex r being Real st f2 | (left_open_halfline r) is bounded_above holds
f1 + f2 is divergent_in-infty_to-infty
proof end;

theorem Th12: :: INTEGR25:12
for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 + f2) ) ) & ex r being Real st f2 | (right_open_halfline r) is bounded_above holds
f1 + f2 is divergent_in+infty_to-infty
proof end;

theorem :: INTEGR25:13
for f being PartFunc of REAL,REAL
for d being Real st left_closed_halfline d c= dom f & f is_-infty_ext_Riemann_integrable_on d holds
for b, c being Real st b < c & c <= d holds
( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c )
proof end;

theorem :: INTEGR25:14
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 b, c being Real st a <= b & b < c holds
( f is_right_ext_Riemann_integrable_on b,c & f is_left_ext_Riemann_integrable_on b,c )
proof end;

theorem Th15: :: INTEGR25:15
for f being PartFunc of REAL,REAL
for a being Real st left_closed_halfline a c= dom f & f is_-infty_ext_Riemann_integrable_on a holds
for b being Real st b <= a holds
f is_-infty_ext_Riemann_integrable_on b
proof end;

theorem Th16: :: INTEGR25:16
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 b being Real st a <= b holds
f is_+infty_ext_Riemann_integrable_on b
proof end;

theorem Th17: :: INTEGR25:17
for f being PartFunc of REAL,REAL
for a, b being Real st a <= b & left_closed_halfline b c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & f is_-infty_ext_Riemann_integrable_on a holds
( f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral (f,b) = (infty_ext_left_integral (f,a)) + (integral (f,a,b)) )
proof end;

theorem Th18: :: INTEGR25:18
for f being PartFunc of REAL,REAL
for a, b being Real st a <= b & right_closed_halfline a c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & f is_+infty_ext_Riemann_integrable_on b holds
( f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral (f,a) = (infty_ext_right_integral (f,b)) + (integral (f,a,b)) )
proof end;

theorem :: INTEGR25:19
for f being PartFunc of REAL,REAL st dom f = REAL holds
( f is infty_ext_Riemann_integrable iff for a being Real holds
( f is_+infty_ext_Riemann_integrable_on a & f is_-infty_ext_Riemann_integrable_on a ) )
proof end;

definition
let f be PartFunc of REAL,REAL;
let b be Real;
pred f is_-infty_improper_integrable_on b means :: INTEGR25:def 1
( ( 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 or Intf is divergent_in-infty_to+infty or Intf is divergent_in-infty_to-infty ) ) );
end;

:: deftheorem defines is_-infty_improper_integrable_on INTEGR25:def 1 :
for f being PartFunc of REAL,REAL
for b being Real holds
( f is_-infty_improper_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 or Intf is divergent_in-infty_to+infty or Intf is divergent_in-infty_to-infty ) ) ) );

definition
let f be PartFunc of REAL,REAL;
let a be Real;
pred f is_+infty_improper_integrable_on a means :: INTEGR25:def 2
( ( 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 or Intf is divergent_in+infty_to+infty or Intf is divergent_in+infty_to-infty ) ) );
end;

:: deftheorem defines is_+infty_improper_integrable_on INTEGR25:def 2 :
for f being PartFunc of REAL,REAL
for a being Real holds
( f is_+infty_improper_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 or Intf is divergent_in+infty_to+infty or Intf is divergent_in+infty_to-infty ) ) ) );

definition
let f be PartFunc of REAL,REAL;
let b be Real;
assume A1: f is_-infty_improper_integrable_on b ;
func improper_integral_-infty (f,b) -> ExtReal means :Def3: :: INTEGR25:def 3
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 ) or ( Intf is divergent_in-infty_to+infty & it = +infty ) or ( Intf is divergent_in-infty_to-infty & it = -infty ) ) );
existence
ex b1 being ExtReal 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 ) or ( Intf is divergent_in-infty_to+infty & b1 = +infty ) or ( Intf is divergent_in-infty_to-infty & b1 = -infty ) ) )
proof end;
uniqueness
for b1, b2 being ExtReal 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 ) or ( Intf is divergent_in-infty_to+infty & b1 = +infty ) or ( Intf is divergent_in-infty_to-infty & b1 = -infty ) ) ) & 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 ) or ( Intf is divergent_in-infty_to+infty & b2 = +infty ) or ( Intf is divergent_in-infty_to-infty & b2 = -infty ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines improper_integral_-infty INTEGR25:def 3 :
for f being PartFunc of REAL,REAL
for b being Real st f is_-infty_improper_integrable_on b holds
for b3 being ExtReal holds
( b3 = improper_integral_-infty (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 ) or ( Intf is divergent_in-infty_to+infty & b3 = +infty ) or ( Intf is divergent_in-infty_to-infty & b3 = -infty ) ) ) );

definition
let f be PartFunc of REAL,REAL;
let a be Real;
assume A1: f is_+infty_improper_integrable_on a ;
func improper_integral_+infty (f,a) -> ExtReal means :Def4: :: INTEGR25:def 4
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 ) or ( Intf is divergent_in+infty_to+infty & it = +infty ) or ( Intf is divergent_in+infty_to-infty & it = -infty ) ) );
existence
ex b1 being ExtReal 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 ) or ( Intf is divergent_in+infty_to+infty & b1 = +infty ) or ( Intf is divergent_in+infty_to-infty & b1 = -infty ) ) )
proof end;
uniqueness
for b1, b2 being ExtReal 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 ) or ( Intf is divergent_in+infty_to+infty & b1 = +infty ) or ( Intf is divergent_in+infty_to-infty & b1 = -infty ) ) ) & 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 ) or ( Intf is divergent_in+infty_to+infty & b2 = +infty ) or ( Intf is divergent_in+infty_to-infty & b2 = -infty ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines improper_integral_+infty INTEGR25:def 4 :
for f being PartFunc of REAL,REAL
for a being Real st f is_+infty_improper_integrable_on a holds
for b3 being ExtReal holds
( b3 = improper_integral_+infty (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 ) or ( Intf is divergent_in+infty_to+infty & b3 = +infty ) or ( Intf is divergent_in+infty_to-infty & b3 = -infty ) ) ) );

theorem Th20: :: INTEGR25:20
for f being PartFunc of REAL,REAL
for b being Real st f is_-infty_ext_Riemann_integrable_on b holds
f is_-infty_improper_integrable_on b
proof end;

theorem Th21: :: INTEGR25:21
for f being PartFunc of REAL,REAL
for a being Real st f is_+infty_ext_Riemann_integrable_on a holds
f is_+infty_improper_integrable_on a
proof end;

theorem Th22: :: INTEGR25:22
for f being PartFunc of REAL,REAL
for b being Real holds
( not f is_-infty_improper_integrable_on b or ( f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) or ( not f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty (f,b) = +infty ) or ( not f is_-infty_ext_Riemann_integrable_on b & improper_integral_-infty (f,b) = -infty ) )
proof end;

theorem Th23: :: INTEGR25:23
for f being PartFunc of REAL,REAL
for b 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 divergent_in-infty_to+infty or Intf is divergent_in-infty_to-infty ) ) holds
not f is_-infty_ext_Riemann_integrable_on b
proof end;

theorem :: INTEGR25:24
for f, Intf being PartFunc of REAL,REAL
for b being Real st f is_-infty_improper_integrable_on 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 holds
improper_integral_-infty (f,b) = lim_in-infty Intf
proof end;

Lm2: for f being PartFunc of REAL,REAL
for c being Real st left_closed_halfline c c= dom f & f is_-infty_improper_integrable_on c holds
for b being Real st b <= c holds
for d being Real st d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )

proof end;

Lm3: for f being PartFunc of REAL,REAL
for c being Real st left_closed_halfline c c= dom f & f is_-infty_improper_integrable_on c & improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) holds
for b being Real st b <= c holds
( f is_-infty_improper_integrable_on b & improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) )

proof end;

Lm4: for f being PartFunc of REAL,REAL
for c being Real st left_closed_halfline c c= dom f & f is_-infty_improper_integrable_on c & improper_integral_-infty (f,c) = +infty holds
for b being Real st b <= c holds
( f is_-infty_improper_integrable_on b & improper_integral_-infty (f,b) = +infty )

proof end;

Lm5: for f being PartFunc of REAL,REAL
for c being Real st left_closed_halfline c c= dom f & f is_-infty_improper_integrable_on c & improper_integral_-infty (f,c) = -infty holds
for b being Real st b <= c holds
( f is_-infty_improper_integrable_on b & improper_integral_-infty (f,b) = -infty )

proof end;

theorem Th25: :: INTEGR25:25
for f being PartFunc of REAL,REAL
for b, c being Real st b <= c & left_closed_halfline c c= dom f & f is_-infty_improper_integrable_on c holds
( f is_-infty_improper_integrable_on b & ( improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) implies improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) & ( improper_integral_-infty (f,c) = +infty implies improper_integral_-infty (f,b) = +infty ) & ( improper_integral_-infty (f,c) = -infty implies improper_integral_-infty (f,b) = -infty ) )
proof end;

Lm6: for f being PartFunc of REAL,REAL
for b, c being Real st b <= c & left_closed_halfline c c= dom f & f | ['b,c'] is bounded & f is_-infty_improper_integrable_on b & f is_integrable_on ['b,c'] holds
for d being Real st d <= c holds
( f is_integrable_on ['d,c'] & f | ['d,c'] is bounded )

proof end;

Lm7: for f being PartFunc of REAL,REAL
for b, c being Real st b <= c & left_closed_halfline c c= dom f & f | ['b,c'] is bounded & f is_-infty_improper_integrable_on b & f is_integrable_on ['b,c'] & improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) holds
( f is_-infty_improper_integrable_on c & improper_integral_-infty (f,c) = (improper_integral_-infty (f,b)) + (integral (f,b,c)) )

proof end;

Lm8: for f being PartFunc of REAL,REAL
for b, c being Real st b <= c & left_closed_halfline c c= dom f & f | ['b,c'] is bounded & f is_-infty_improper_integrable_on b & f is_integrable_on ['b,c'] & improper_integral_-infty (f,b) = +infty holds
( f is_-infty_improper_integrable_on c & improper_integral_-infty (f,c) = +infty )

proof end;

Lm9: for f being PartFunc of REAL,REAL
for b, c being Real st b <= c & left_closed_halfline c c= dom f & f | ['b,c'] is bounded & f is_-infty_improper_integrable_on b & f is_integrable_on ['b,c'] & improper_integral_-infty (f,b) = -infty holds
( f is_-infty_improper_integrable_on c & improper_integral_-infty (f,c) = -infty )

proof end;

theorem Th26: :: INTEGR25:26
for f being PartFunc of REAL,REAL
for b, c being Real st b <= c & left_closed_halfline c c= dom f & f | ['b,c'] is bounded & f is_-infty_improper_integrable_on b & f is_integrable_on ['b,c'] holds
( f is_-infty_improper_integrable_on c & ( improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) implies improper_integral_-infty (f,c) = (improper_integral_-infty (f,b)) + (integral (f,b,c)) ) & ( improper_integral_-infty (f,b) = +infty implies improper_integral_-infty (f,c) = +infty ) & ( improper_integral_-infty (f,b) = -infty implies improper_integral_-infty (f,c) = -infty ) )
proof end;

theorem Th27: :: INTEGR25:27
for f being PartFunc of REAL,REAL
for b being Real holds
( not f is_+infty_improper_integrable_on b or ( f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or ( not f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = +infty ) or ( not f is_+infty_ext_Riemann_integrable_on b & improper_integral_+infty (f,b) = -infty ) )
proof end;

theorem Th28: :: INTEGR25:28
for f being PartFunc of REAL,REAL
for b being Real st ex Intf being PartFunc of REAL,REAL st
( dom Intf = right_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,b,x) ) & ( Intf is divergent_in+infty_to+infty or Intf is divergent_in+infty_to-infty ) ) holds
not f is_+infty_ext_Riemann_integrable_on b
proof end;

theorem :: INTEGR25:29
for f, Intf being PartFunc of REAL,REAL
for b being Real st f is_+infty_improper_integrable_on b & dom Intf = right_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,b,x) ) & Intf is convergent_in+infty holds
improper_integral_+infty (f,b) = lim_in+infty Intf
proof end;

Lm10: for f being PartFunc of REAL,REAL
for c being Real st right_closed_halfline c c= dom f & f is_+infty_improper_integrable_on c holds
for b being Real st b >= c holds
for d being Real st d >= b holds
( f is_integrable_on ['b,d'] & f | ['b,d'] is bounded )

proof end;

Lm11: for f being PartFunc of REAL,REAL
for c being Real st right_closed_halfline c c= dom f & f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = infty_ext_right_integral (f,c) holds
for b being Real st b >= c holds
( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) )

proof end;

Lm12: for f being PartFunc of REAL,REAL
for c being Real st right_closed_halfline c c= dom f & f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = +infty holds
for b being Real st b >= c holds
( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = +infty )

proof end;

Lm13: for f being PartFunc of REAL,REAL
for c being Real st right_closed_halfline c c= dom f & f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = -infty holds
for b being Real st b >= c holds
( f is_+infty_improper_integrable_on b & improper_integral_+infty (f,b) = -infty )

proof end;

theorem Th30: :: INTEGR25:30
for f being PartFunc of REAL,REAL
for b, c being Real st b >= c & right_closed_halfline c c= dom f & f is_+infty_improper_integrable_on c holds
( f is_+infty_improper_integrable_on b & ( improper_integral_+infty (f,c) = infty_ext_right_integral (f,c) implies improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) & ( improper_integral_+infty (f,c) = +infty implies improper_integral_+infty (f,b) = +infty ) & ( improper_integral_+infty (f,c) = -infty implies improper_integral_+infty (f,b) = -infty ) )
proof end;

Lm14: for f being PartFunc of REAL,REAL
for b, c being Real st b >= c & right_closed_halfline c c= dom f & f | ['c,b'] is bounded & f is_+infty_improper_integrable_on b & f is_integrable_on ['c,b'] holds
for d being Real st d >= c holds
( f is_integrable_on ['c,d'] & f | ['c,d'] is bounded )

proof end;

Lm15: for f being PartFunc of REAL,REAL
for b, c being Real st b >= c & right_closed_halfline c c= dom f & f | ['c,b'] is bounded & f is_+infty_improper_integrable_on b & f is_integrable_on ['c,b'] & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) holds
( f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = (improper_integral_+infty (f,b)) + (integral (f,c,b)) )

proof end;

Lm16: for f being PartFunc of REAL,REAL
for b, c being Real st b >= c & right_closed_halfline c c= dom f & f | ['c,b'] is bounded & f is_+infty_improper_integrable_on b & f is_integrable_on ['c,b'] & improper_integral_+infty (f,b) = +infty holds
( f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = +infty )

proof end;

Lm17: for f being PartFunc of REAL,REAL
for b, c being Real st b >= c & right_closed_halfline c c= dom f & f | ['c,b'] is bounded & f is_+infty_improper_integrable_on b & f is_integrable_on ['c,b'] & improper_integral_+infty (f,b) = -infty holds
( f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = -infty )

proof end;

theorem Th31: :: INTEGR25:31
for f being PartFunc of REAL,REAL
for b, c being Real st b >= c & right_closed_halfline c c= dom f & f | ['c,b'] is bounded & f is_+infty_improper_integrable_on b & f is_integrable_on ['c,b'] holds
( f is_+infty_improper_integrable_on c & ( improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) implies improper_integral_+infty (f,c) = (improper_integral_+infty (f,b)) + (integral (f,c,b)) ) & ( improper_integral_+infty (f,b) = +infty implies improper_integral_+infty (f,c) = +infty ) & ( improper_integral_+infty (f,b) = -infty implies improper_integral_+infty (f,c) = -infty ) )
proof end;

definition
let f be PartFunc of REAL,REAL;
pred f is_improper_integrable_on_REAL means :: INTEGR25:def 5
ex r being Real st
( f is_-infty_improper_integrable_on r & f is_+infty_improper_integrable_on r & ( not improper_integral_-infty (f,r) = -infty or not improper_integral_+infty (f,r) = +infty ) & ( not improper_integral_-infty (f,r) = +infty or not improper_integral_+infty (f,r) = -infty ) );
end;

:: deftheorem defines is_improper_integrable_on_REAL INTEGR25:def 5 :
for f being PartFunc of REAL,REAL holds
( f is_improper_integrable_on_REAL iff ex r being Real st
( f is_-infty_improper_integrable_on r & f is_+infty_improper_integrable_on r & ( not improper_integral_-infty (f,r) = -infty or not improper_integral_+infty (f,r) = +infty ) & ( not improper_integral_-infty (f,r) = +infty or not improper_integral_+infty (f,r) = -infty ) ) );

theorem :: INTEGR25:32
for f being PartFunc of REAL,REAL st f is_improper_integrable_on_REAL holds
ex b being Real st
( ( improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ) or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = +infty or (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = -infty )
proof end;

theorem Th33: :: INTEGR25:33
for f being PartFunc of REAL,REAL
for b being Real st dom f = REAL & f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & ( not improper_integral_-infty (f,b) = -infty or not improper_integral_+infty (f,b) = +infty ) & ( not improper_integral_-infty (f,b) = +infty or not improper_integral_+infty (f,b) = -infty ) holds
for b1 being Real st b1 <= b holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
proof end;

theorem Th34: :: INTEGR25:34
for f being PartFunc of REAL,REAL
for b being Real st dom f = REAL & f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & ( not improper_integral_-infty (f,b) = -infty or not improper_integral_+infty (f,b) = +infty ) & ( not improper_integral_-infty (f,b) = +infty or not improper_integral_+infty (f,b) = -infty ) holds
for b2 being Real st b <= b2 holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))
proof end;

theorem Th35: :: INTEGR25:35
for f being PartFunc of REAL,REAL st dom f = REAL & f is_improper_integrable_on_REAL holds
for b1, b2 being Real holds (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))
proof end;

definition
let f be PartFunc of REAL,REAL;
assume A1: ( dom f = REAL & f is_improper_integrable_on_REAL ) ;
func improper_integral_on_REAL f -> ExtReal means :Def6: :: INTEGR25:def 6
ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & it = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) );
existence
ex b1 being ExtReal ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & b1 = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) )
proof end;
uniqueness
for b1, b2 being ExtReal st ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & b1 = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) ) & ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & b2 = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) ) holds
b1 = b2
by A1, Th35;
end;

:: deftheorem Def6 defines improper_integral_on_REAL INTEGR25:def 6 :
for f being PartFunc of REAL,REAL st dom f = REAL & f is_improper_integrable_on_REAL holds
for b2 being ExtReal holds
( b2 = improper_integral_on_REAL f iff ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & b2 = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) ) );

theorem Th36: :: INTEGR25:36
for f being PartFunc of REAL,REAL
for b being Real st dom f = REAL & f is_improper_integrable_on_REAL holds
( f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )
proof end;

theorem Th37: :: INTEGR25:37
for f being PartFunc of REAL,REAL
for b being Real st f is_-infty_improper_integrable_on b & improper_integral_-infty (f,b) = +infty holds
for 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) ) holds
Intf is divergent_in-infty_to+infty
proof end;

theorem Th38: :: INTEGR25:38
for f being PartFunc of REAL,REAL
for b being Real st f is_-infty_improper_integrable_on b & improper_integral_-infty (f,b) = -infty holds
for 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) ) holds
Intf is divergent_in-infty_to-infty
proof end;

theorem Th39: :: INTEGR25:39
for f being PartFunc of REAL,REAL
for a being Real st f is_+infty_improper_integrable_on a & improper_integral_+infty (f,a) = +infty holds
for 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) ) holds
Intf is divergent_in+infty_to+infty
proof end;

theorem Th40: :: INTEGR25:40
for f being PartFunc of REAL,REAL
for a being Real st f is_+infty_improper_integrable_on a & improper_integral_+infty (f,a) = -infty holds
for 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) ) holds
Intf is divergent_in+infty_to-infty
proof end;

theorem Th41: :: INTEGR25:41
for f being PartFunc of REAL,REAL
for b, r being Real st left_closed_halfline b c= dom f & f is_-infty_improper_integrable_on b holds
( r (#) f is_-infty_improper_integrable_on b & improper_integral_-infty ((r (#) f),b) = r * (improper_integral_-infty (f,b)) )
proof end;

theorem Th42: :: INTEGR25:42
for f being PartFunc of REAL,REAL
for a, r being Real st right_closed_halfline a c= dom f & f is_+infty_improper_integrable_on a holds
( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )
proof end;

theorem Th43: :: INTEGR25:43
for f being PartFunc of REAL,REAL
for b being Real st left_closed_halfline b c= dom f & f is_-infty_improper_integrable_on b holds
( - f is_-infty_improper_integrable_on b & improper_integral_-infty ((- f),b) = - (improper_integral_-infty (f,b)) )
proof end;

theorem Th44: :: INTEGR25:44
for f being PartFunc of REAL,REAL
for a being Real st right_closed_halfline a c= dom f & f is_+infty_improper_integrable_on a holds
( - f is_+infty_improper_integrable_on a & improper_integral_+infty ((- f),a) = - (improper_integral_+infty (f,a)) )
proof end;

theorem Th45: :: INTEGR25:45
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_improper_integrable_on b & g is_-infty_improper_integrable_on b & ( not improper_integral_-infty (f,b) = +infty or not improper_integral_-infty (g,b) = -infty ) & ( not improper_integral_-infty (f,b) = -infty or not improper_integral_-infty (g,b) = +infty ) holds
( f + g is_-infty_improper_integrable_on b & improper_integral_-infty ((f + g),b) = (improper_integral_-infty (f,b)) + (improper_integral_-infty (g,b)) )
proof end;

theorem Th46: :: INTEGR25:46
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_improper_integrable_on a & g is_+infty_improper_integrable_on a & ( not improper_integral_+infty (f,a) = +infty or not improper_integral_+infty (g,a) = -infty ) & ( not improper_integral_+infty (f,a) = -infty or not improper_integral_+infty (g,a) = +infty ) holds
( f + g is_+infty_improper_integrable_on a & improper_integral_+infty ((f + g),a) = (improper_integral_+infty (f,a)) + (improper_integral_+infty (g,a)) )
proof end;

theorem :: INTEGR25:47
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_improper_integrable_on b & g is_-infty_improper_integrable_on b & ( not improper_integral_-infty (f,b) = +infty or not improper_integral_-infty (g,b) = +infty ) & ( not improper_integral_-infty (f,b) = -infty or not improper_integral_-infty (g,b) = -infty ) holds
( f - g is_-infty_improper_integrable_on b & improper_integral_-infty ((f - g),b) = (improper_integral_-infty (f,b)) - (improper_integral_-infty (g,b)) )
proof end;

theorem :: INTEGR25:48
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_improper_integrable_on a & g is_+infty_improper_integrable_on a & ( not improper_integral_+infty (f,a) = +infty or not improper_integral_+infty (g,a) = +infty ) & ( not improper_integral_+infty (f,a) = -infty or not improper_integral_+infty (g,a) = -infty ) holds
( f - g is_+infty_improper_integrable_on a & improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) - (improper_integral_+infty (g,a)) )
proof end;

theorem Th49: :: INTEGR25:49
for f being PartFunc of REAL,REAL
for r being Real st dom f = REAL & f is_improper_integrable_on_REAL holds
( r (#) f is_improper_integrable_on_REAL & improper_integral_on_REAL (r (#) f) = r * (improper_integral_on_REAL f) )
proof end;

theorem Th50: :: INTEGR25:50
for f being PartFunc of REAL,REAL
for r being Real st dom f = REAL & f is_improper_integrable_on_REAL holds
( - f is_improper_integrable_on_REAL & improper_integral_on_REAL (- f) = - (improper_integral_on_REAL f) )
proof end;

theorem Th51: :: INTEGR25:51
for f, g being PartFunc of REAL,REAL st dom f = REAL & dom g = REAL & f is_improper_integrable_on_REAL & g is_improper_integrable_on_REAL & ( not improper_integral_on_REAL f = +infty or not improper_integral_on_REAL g = -infty ) & ( not improper_integral_on_REAL f = -infty or not improper_integral_on_REAL g = +infty ) holds
( f + g is_improper_integrable_on_REAL & improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g) )
proof end;

theorem :: INTEGR25:52
for f, g being PartFunc of REAL,REAL st dom f = REAL & dom g = REAL & f is_improper_integrable_on_REAL & g is_improper_integrable_on_REAL & ( not improper_integral_on_REAL f = +infty or not improper_integral_on_REAL g = +infty ) & ( not improper_integral_on_REAL f = -infty or not improper_integral_on_REAL g = -infty ) holds
( f - g is_improper_integrable_on_REAL & improper_integral_on_REAL (f - g) = (improper_integral_on_REAL f) - (improper_integral_on_REAL g) )
proof end;