:: Improper Integral, Part {I}
:: by Noboru Endou
::
:: Copyright (c) 2021 Association of Mizar Users

Lm1: for f being PartFunc of REAL,REAL
for a, b, c being Real st a < b & b < c & ['a,c'] c= dom f & f | ['a,b'] is bounded & f | ['b,c'] is bounded & f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] holds
f is_integrable_on ['a,c']

proof end;

theorem Th1: :: INTEGR24:1
for f being PartFunc of REAL,REAL
for a, b, c being Real st a <= b & b <= c & ['a,c'] c= dom f & f | ['a,b'] is bounded & f | ['b,c'] is bounded & f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] holds
( f is_integrable_on ['a,c'] & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) )
proof end;

theorem Th2: :: INTEGR24:2
for seq being Real_Sequence st seq is divergent_to+infty holds
( not seq is divergent_to-infty & not seq is convergent )
proof end;

theorem Th3: :: INTEGR24:3
for seq being Real_Sequence st seq is divergent_to-infty holds
( not seq is divergent_to+infty & not seq is convergent )
proof end;

theorem Th4: :: INTEGR24:4
for f being PartFunc of REAL,REAL
for x0 being Real st ( f is_left_convergent_in x0 or f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0 ) holds
ex seq being Real_Sequence st
( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ () )
proof end;

theorem Th5: :: INTEGR24:5
for f being PartFunc of REAL,REAL
for x0 being Real st ( f is_right_convergent_in x0 or f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) holds
ex seq being Real_Sequence st
( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ () )
proof end;

theorem Th6: :: INTEGR24:6
for f being PartFunc of REAL,REAL
for x0 being Real st f is_left_divergent_to+infty_in x0 holds
( not f is_left_divergent_to-infty_in x0 & not f is_left_convergent_in x0 )
proof end;

theorem Th7: :: INTEGR24:7
for f being PartFunc of REAL,REAL
for x0 being Real st f is_left_divergent_to-infty_in x0 holds
( not f is_left_divergent_to+infty_in x0 & not f is_left_convergent_in x0 )
proof end;

theorem Th8: :: INTEGR24:8
for f being PartFunc of REAL,REAL
for x0 being Real st f is_right_divergent_to+infty_in x0 holds
( not f is_right_divergent_to-infty_in x0 & not f is_right_convergent_in x0 )
proof end;

theorem Th9: :: INTEGR24:9
for f being PartFunc of REAL,REAL
for x0 being Real st f is_right_divergent_to-infty_in x0 holds
( not f is_right_divergent_to+infty_in x0 & not f is_right_convergent_in x0 )
proof end;

theorem Th10: :: INTEGR24:10
for f being PartFunc of REAL,REAL
for x0 being Real st f is_right_convergent_in x0 holds
( ex r being Real st
( 0 < r & f | ].x0,(x0 + r).[ is bounded_below ) & ex r being Real st
( 0 < r & f | ].x0,(x0 + r).[ is bounded_above ) )
proof end;

theorem Th11: :: INTEGR24:11
for f being PartFunc of REAL,REAL
for x0 being Real st f is_left_convergent_in x0 holds
( ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_below ) & ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_above ) )
proof end;

theorem Th12: :: INTEGR24:12
for f being PartFunc of REAL,REAL
for x0 being Real st f is_right_divergent_to+infty_in x0 holds
ex r being Real st
( 0 < r & f | ].x0,(x0 + r).[ is bounded_below )
proof end;

theorem Th13: :: INTEGR24:13
for f being PartFunc of REAL,REAL
for x0 being Real st f is_right_divergent_to-infty_in x0 holds
ex r being Real st
( 0 < r & f | ].x0,(x0 + r).[ is bounded_above )
proof end;

theorem Th14: :: INTEGR24:14
for f being PartFunc of REAL,REAL
for x0 being Real st f is_left_divergent_to+infty_in x0 holds
ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_below )
proof end;

theorem Th15: :: INTEGR24:15
for f being PartFunc of REAL,REAL
for x0 being Real st f is_left_divergent_to-infty_in x0 holds
ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_above )
proof end;

Lm2: for r, g, r1 being Real st 0 < g & r <= r1 holds
( r - g < r1 & r < r1 + g )

proof end;

theorem Th16: :: INTEGR24:16
for f1, f2 being PartFunc of REAL,REAL
for x0 being Real st f1 is_right_divergent_to-infty_in x0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (f1 + f2) ) ) & ex r being Real st
( 0 < r & f2 | ].x0,(x0 + r).[ is bounded_above ) holds
f1 + f2 is_right_divergent_to-infty_in x0
proof end;

theorem Th17: :: INTEGR24:17
for f1, f2 being PartFunc of REAL,REAL
for x0 being Real st f1 is_left_divergent_to-infty_in x0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 + f2) ) ) & ex r being Real st
( 0 < r & f2 | ].(x0 - r),x0.[ is bounded_above ) holds
f1 + f2 is_left_divergent_to-infty_in x0
proof end;

theorem Th18: :: INTEGR24:18
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
( f is_left_ext_Riemann_integrable_on a,b & ext_left_integral (f,a,b) = integral (f,a,b) )
proof end;

theorem Th19: :: INTEGR24:19
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
( f is_right_ext_Riemann_integrable_on a,b & ext_right_integral (f,a,b) = integral (f,a,b) )
proof end;

theorem Th20: :: INTEGR24:20
for f being PartFunc of REAL,REAL
for a, b, c being Real st a < b & b <= c & ].a,c.] c= dom f & f | ['b,c'] is bounded & f is_integrable_on ['b,c'] & f is_left_ext_Riemann_integrable_on a,b holds
( f is_left_ext_Riemann_integrable_on a,c & ext_left_integral (f,a,c) = (ext_left_integral (f,a,b)) + (integral (f,b,c)) )
proof end;

theorem Th21: :: INTEGR24:21
for f being PartFunc of REAL,REAL
for a, b, c being Real st a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & f is_right_ext_Riemann_integrable_on b,c holds
( f is_right_ext_Riemann_integrable_on a,c & ext_right_integral (f,a,c) = (integral (f,a,b)) + (ext_right_integral (f,b,c)) )
proof end;

Lm3: 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
( f is_left_ext_Riemann_integrable_on a,b & ext_left_integral (f,a,b) = integral (f,a,b) )

proof end;

Lm4: for f being PartFunc of REAL,REAL
for a, b being Real st ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b holds
for c being Real st a <= c & c < b holds
f is_left_ext_Riemann_integrable_on c,b

proof end;

theorem Th22: :: INTEGR24:22
for f being PartFunc of REAL,REAL
for a, b being Real st ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b holds
for d being Real st a < d & d <= b holds
( f is_left_ext_Riemann_integrable_on a,d & ext_left_integral (f,a,b) = (ext_left_integral (f,a,d)) + (integral (f,d,b)) )
proof end;

theorem :: INTEGR24:23
for f being PartFunc of REAL,REAL
for a, b being Real st ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b holds
for c, d being Real st a <= c & c < d & d <= b holds
( f is_left_ext_Riemann_integrable_on c,d & ( a < c implies ext_left_integral (f,c,d) = integral (f,c,d) ) )
proof end;

theorem :: INTEGR24:24
for f being PartFunc of REAL,REAL
for a, b being Real st ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b holds
for c, d being Real st a < c & c < d & d <= b holds
( f is_right_ext_Riemann_integrable_on c,d & ext_right_integral (f,c,d) = integral (f,c,d) )
proof end;

Lm5: 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
( f is_right_ext_Riemann_integrable_on a,b & ext_right_integral (f,a,b) = integral (f,a,b) )

proof end;

Lm6: for f being PartFunc of REAL,REAL
for a, b being Real st [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b holds
for d being Real st a < d & d <= b holds
f is_right_ext_Riemann_integrable_on a,d

proof end;

theorem Th25: :: INTEGR24:25
for f being PartFunc of REAL,REAL
for a, b being Real st [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b holds
for c being Real st a <= c & c < b holds
( f is_right_ext_Riemann_integrable_on c,b & ext_right_integral (f,a,b) = (integral (f,a,c)) + (ext_right_integral (f,c,b)) )
proof end;

theorem :: INTEGR24:26
for f being PartFunc of REAL,REAL
for a, b being Real st [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b holds
for c, d being Real st a <= c & c < d & d <= b holds
( f is_right_ext_Riemann_integrable_on c,d & ( d < b implies ext_right_integral (f,c,d) = integral (f,c,d) ) )
proof end;

theorem :: INTEGR24:27
for f being PartFunc of REAL,REAL
for a, b being Real st [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b holds
for c, d being Real st a <= c & c < d & d < b holds
( f is_left_ext_Riemann_integrable_on c,d & ext_left_integral (f,c,d) = integral (f,c,d) )
proof end;

theorem Th28: :: INTEGR24:28
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 end;

theorem Th29: :: INTEGR24:29
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 end;

theorem Th30: :: INTEGR24:30
for f being PartFunc of REAL,REAL
for a, b being Real st ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b holds
for r being Real holds
( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) )
proof end;

theorem Th31: :: INTEGR24:31
for f being PartFunc of REAL,REAL
for a, b being Real st [.a,b.[ c= dom f & f is_right_ext_Riemann_integrable_on a,b holds
for r being Real holds
( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) )
proof end;

definition
let f be PartFunc of REAL,REAL;
let a, b be Real;
pred f is_left_improper_integrable_on a,b means :: INTEGR24:def 1
( ( 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 or Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) ) );
end;

:: deftheorem defines is_left_improper_integrable_on INTEGR24:def 1 :
for f being PartFunc of REAL,REAL
for a, b being Real holds
( f is_left_improper_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 or Intf is_right_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) ) ) );

definition
let f be PartFunc of REAL,REAL;
let a, b be Real;
pred f is_right_improper_integrable_on a,b means :: INTEGR24:def 2
( ( 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 or Intf is_left_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) ) );
end;

:: deftheorem defines is_right_improper_integrable_on INTEGR24:def 2 :
for f being PartFunc of REAL,REAL
for a, b being Real holds
( f is_right_improper_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 or Intf is_left_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) ) ) );

definition
let f be PartFunc of REAL,REAL;
let a, b be Real;
assume A1: f is_left_improper_integrable_on a,b ;
func left_improper_integral (f,a,b) -> ExtReal means :Def3: :: INTEGR24: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,x,b) ) & ( ( Intf is_right_convergent_in a & it = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & it = +infty ) or ( Intf is_right_divergent_to-infty_in a & it = -infty ) ) );
existence
ex b1 being ExtReal 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) ) or ( Intf is_right_divergent_to+infty_in a & b1 = +infty ) or ( Intf is_right_divergent_to-infty_in a & b1 = -infty ) ) )
proof end;
uniqueness
for b1, b2 being ExtReal 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) ) or ( Intf is_right_divergent_to+infty_in a & b1 = +infty ) or ( Intf is_right_divergent_to-infty_in a & b1 = -infty ) ) ) & 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) ) or ( Intf is_right_divergent_to+infty_in a & b2 = +infty ) or ( Intf is_right_divergent_to-infty_in a & b2 = -infty ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines left_improper_integral INTEGR24:def 3 :
for f being PartFunc of REAL,REAL
for a, b being Real st f is_left_improper_integrable_on a,b holds
for b4 being ExtReal holds
( b4 = left_improper_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) ) or ( Intf is_right_divergent_to+infty_in a & b4 = +infty ) or ( Intf is_right_divergent_to-infty_in a & b4 = -infty ) ) ) );

definition
let f be PartFunc of REAL,REAL;
let a, b be Real;
assume A1: f is_right_improper_integrable_on a,b ;
func right_improper_integral (f,a,b) -> ExtReal means :Def4: :: INTEGR24: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,a,x) ) & ( ( Intf is_left_convergent_in b & it = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & it = +infty ) or ( Intf is_left_divergent_to-infty_in b & it = -infty ) ) );
existence
ex b1 being ExtReal 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) ) or ( Intf is_left_divergent_to+infty_in b & b1 = +infty ) or ( Intf is_left_divergent_to-infty_in b & b1 = -infty ) ) )
proof end;
uniqueness
for b1, b2 being ExtReal 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) ) or ( Intf is_left_divergent_to+infty_in b & b1 = +infty ) or ( Intf is_left_divergent_to-infty_in b & b1 = -infty ) ) ) & 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) ) or ( Intf is_left_divergent_to+infty_in b & b2 = +infty ) or ( Intf is_left_divergent_to-infty_in b & b2 = -infty ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines right_improper_integral INTEGR24:def 4 :
for f being PartFunc of REAL,REAL
for a, b being Real st f is_right_improper_integrable_on a,b holds
for b4 being ExtReal holds
( b4 = right_improper_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) ) or ( Intf is_left_divergent_to+infty_in b & b4 = +infty ) or ( Intf is_left_divergent_to-infty_in b & b4 = -infty ) ) ) );

theorem Th32: :: INTEGR24:32
for f being PartFunc of REAL,REAL
for a, b being Real st f is_left_ext_Riemann_integrable_on a,b holds
f is_left_improper_integrable_on a,b
proof end;

theorem Th33: :: INTEGR24:33
for f being PartFunc of REAL,REAL
for a, b being Real st f is_right_ext_Riemann_integrable_on a,b holds
f is_right_improper_integrable_on a,b
proof end;

theorem Th34: :: INTEGR24:34
for f being PartFunc of REAL,REAL
for a, b being Real holds
( not f is_left_improper_integrable_on a,b or ( f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) ) or ( not f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = +infty ) or ( not f is_left_ext_Riemann_integrable_on a,b & left_improper_integral (f,a,b) = -infty ) )
proof end;

theorem Th35: :: INTEGR24:35
for f being PartFunc of REAL,REAL
for a, b 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_divergent_to+infty_in a or Intf is_right_divergent_to-infty_in a ) ) holds
not f is_left_ext_Riemann_integrable_on a,b
proof end;

theorem :: INTEGR24:36
for f, Intf being PartFunc of REAL,REAL
for a, b being Real st f is_left_improper_integrable_on a,b & dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a holds
left_improper_integral (f,a,b) = lim_right (Intf,a)
proof end;

Lm7: for f being PartFunc of REAL,REAL
for a, c being Real st ].a,c.] c= dom f & f is_left_improper_integrable_on a,c holds
for b being Real st a < b & b <= c holds
for d being Real st a < d & d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )

proof end;

Lm8: for f being PartFunc of REAL,REAL
for a, c being Real st ].a,c.] c= dom f & f is_left_improper_integrable_on a,c & left_improper_integral (f,a,c) = ext_left_integral (f,a,c) holds
for b being Real st a < b & b <= c holds
( f is_left_improper_integrable_on a,b & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) )

proof end;

Lm9: for f being PartFunc of REAL,REAL
for a, c being Real st ].a,c.] c= dom f & f is_left_improper_integrable_on a,c & left_improper_integral (f,a,c) = +infty holds
for b being Real st a < b & b <= c holds
( f is_left_improper_integrable_on a,b & left_improper_integral (f,a,b) = +infty )

proof end;

Lm10: for f being PartFunc of REAL,REAL
for a, c being Real st ].a,c.] c= dom f & f is_left_improper_integrable_on a,c & left_improper_integral (f,a,c) = -infty holds
for b being Real st a < b & b <= c holds
( f is_left_improper_integrable_on a,b & left_improper_integral (f,a,b) = -infty )

proof end;

theorem Th37: :: INTEGR24:37
for f being PartFunc of REAL,REAL
for a, b, c being Real st a < b & b <= c & ].a,c.] c= dom f & f is_left_improper_integrable_on a,c holds
( f is_left_improper_integrable_on a,b & ( left_improper_integral (f,a,c) = ext_left_integral (f,a,c) implies left_improper_integral (f,a,b) = ext_left_integral (f,a,b) ) & ( left_improper_integral (f,a,c) = +infty implies left_improper_integral (f,a,b) = +infty ) & ( left_improper_integral (f,a,c) = -infty implies left_improper_integral (f,a,b) = -infty ) )
proof end;

Lm11: for f being PartFunc of REAL,REAL
for a, b, c being Real st a < b & b <= c & ].a,c.] c= dom f & f | ['b,c'] is bounded & f is_left_improper_integrable_on a,b & f is_integrable_on ['b,c'] holds
for d being Real st a < d & d <= c holds
( f is_integrable_on ['d,c'] & f | ['d,c'] is bounded )

proof end;

Lm12: for f being PartFunc of REAL,REAL
for a, b, c being Real st a < b & b <= c & ].a,c.] c= dom f & f | ['b,c'] is bounded & f is_left_improper_integrable_on a,b & f is_integrable_on ['b,c'] & left_improper_integral (f,a,b) = ext_left_integral (f,a,b) holds
( f is_left_improper_integrable_on a,c & left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) )

proof end;

Lm13: for f being PartFunc of REAL,REAL
for a, b, c being Real st a < b & b <= c & ].a,c.] c= dom f & f | ['b,c'] is bounded & f is_left_improper_integrable_on a,b & f is_integrable_on ['b,c'] & left_improper_integral (f,a,b) = +infty holds
( f is_left_improper_integrable_on a,c & left_improper_integral (f,a,c) = +infty )

proof end;

Lm14: for f being PartFunc of REAL,REAL
for a, b, c being Real st a < b & b <= c & ].a,c.] c= dom f & f | ['b,c'] is bounded & f is_left_improper_integrable_on a,b & f is_integrable_on ['b,c'] & left_improper_integral (f,a,b) = -infty holds
( f is_left_improper_integrable_on a,c & left_improper_integral (f,a,c) = -infty )

proof end;

theorem Th38: :: INTEGR24:38
for f being PartFunc of REAL,REAL
for a, b, c being Real st a < b & b <= c & ].a,c.] c= dom f & f | ['b,c'] is bounded & f is_left_improper_integrable_on a,b & f is_integrable_on ['b,c'] holds
( f is_left_improper_integrable_on a,c & ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) implies left_improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (integral (f,b,c)) ) & ( left_improper_integral (f,a,b) = +infty implies left_improper_integral (f,a,c) = +infty ) & ( left_improper_integral (f,a,b) = -infty implies left_improper_integral (f,a,c) = -infty ) )
proof end;

theorem Th39: :: INTEGR24:39
for f being PartFunc of REAL,REAL
for a, b being Real holds
( not f is_right_improper_integrable_on a,b or ( f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = ext_right_integral (f,a,b) ) or ( not f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = +infty ) or ( not f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = -infty ) )
proof end;

theorem Th40: :: INTEGR24:40
for f being PartFunc of REAL,REAL
for a, b 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_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) ) holds
not f is_right_ext_Riemann_integrable_on a,b
proof end;

theorem :: INTEGR24:41
for f, Intf being PartFunc of REAL,REAL
for a, b being Real st f is_right_improper_integrable_on a,b & dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b holds
right_improper_integral (f,a,b) = lim_left (Intf,b)
proof end;

Lm15: for f being PartFunc of REAL,REAL
for a, c being Real st [.a,c.[ c= dom f & f is_right_improper_integrable_on a,c holds
for b being Real st a <= b & b < c holds
for d being Real st b <= d & d < c holds
( f is_integrable_on ['b,d'] & f | ['b,d'] is bounded )

proof end;

Lm16: for f being PartFunc of REAL,REAL
for a, c being Real st [.a,c.[ c= dom f & f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = ext_right_integral (f,a,c) holds
for b being Real st a <= b & b < c holds
( f is_right_improper_integrable_on b,c & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) )

proof end;

Lm17: for f being PartFunc of REAL,REAL
for a, c being Real st [.a,c.[ c= dom f & f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = +infty holds
for b being Real st a <= b & b < c holds
( f is_right_improper_integrable_on b,c & right_improper_integral (f,b,c) = +infty )

proof end;

Lm18: for f being PartFunc of REAL,REAL
for a, c being Real st [.a,c.[ c= dom f & f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = -infty holds
for b being Real st a <= b & b < c holds
( f is_right_improper_integrable_on b,c & right_improper_integral (f,b,c) = -infty )

proof end;

theorem Th42: :: INTEGR24:42
for f being PartFunc of REAL,REAL
for a, b, c being Real st a <= b & b < c & [.a,c.[ c= dom f & f is_right_improper_integrable_on a,c holds
( f is_right_improper_integrable_on b,c & ( right_improper_integral (f,a,c) = ext_right_integral (f,a,c) implies right_improper_integral (f,b,c) = ext_right_integral (f,b,c) ) & ( right_improper_integral (f,a,c) = +infty implies right_improper_integral (f,b,c) = +infty ) & ( right_improper_integral (f,a,c) = -infty implies right_improper_integral (f,b,c) = -infty ) )
proof end;

Lm19: for f being PartFunc of REAL,REAL
for a, b, c being Real st a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_right_improper_integrable_on b,c & f is_integrable_on ['a,b'] holds
for d being Real st a <= d & d < c holds
( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded )

proof end;

Lm20: for f being PartFunc of REAL,REAL
for a, b, c being Real st a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_right_improper_integrable_on b,c & f is_integrable_on ['a,b'] & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) holds
( f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) )

proof end;

Lm21: for f being PartFunc of REAL,REAL
for a, b, c being Real st a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_right_improper_integrable_on b,c & f is_integrable_on ['a,b'] & right_improper_integral (f,b,c) = +infty holds
( f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = +infty )

proof end;

Lm22: for f being PartFunc of REAL,REAL
for a, b, c being Real st a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_right_improper_integrable_on b,c & f is_integrable_on ['a,b'] & right_improper_integral (f,b,c) = -infty holds
( f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = -infty )

proof end;

theorem Th43: :: INTEGR24:43
for f being PartFunc of REAL,REAL
for a, b, c being Real st a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_right_improper_integrable_on b,c & f is_integrable_on ['a,b'] holds
( f is_right_improper_integrable_on a,c & ( right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) & ( right_improper_integral (f,b,c) = +infty implies right_improper_integral (f,a,c) = +infty ) & ( right_improper_integral (f,b,c) = -infty implies right_improper_integral (f,a,c) = -infty ) )
proof end;

definition
let f be PartFunc of REAL,REAL;
let a, c be Real;
pred f is_improper_integrable_on a,c means :: INTEGR24:def 5
ex b being Real st
( a < b & b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) & ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) );
end;

:: deftheorem defines is_improper_integrable_on INTEGR24:def 5 :
for f being PartFunc of REAL,REAL
for a, c being Real holds
( f is_improper_integrable_on a,c iff ex b being Real st
( a < b & b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) & ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) ) );

theorem :: INTEGR24:44
for f being PartFunc of REAL,REAL
for a, c being Real st f is_improper_integrable_on a,c holds
ex b being Real st
( a < b & b < c & ( ( left_improper_integral (f,a,b) = ext_left_integral (f,a,b) & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) ) or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = +infty or (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = -infty ) )
proof end;

theorem Th45: :: INTEGR24:45
for f being PartFunc of REAL,REAL
for a, b, c being Real st ].a,c.[ c= dom f & a < b & b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) & ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) holds
for b1 being Real st a < b1 & b1 <= b holds
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
proof end;

theorem Th46: :: INTEGR24:46
for f being PartFunc of REAL,REAL
for a, b, c being Real st ].a,c.[ c= dom f & a < b & b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) & ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) holds
for b2 being Real st b <= b2 & b2 < c holds
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c))
proof end;

theorem Th47: :: INTEGR24:47
for f being PartFunc of REAL,REAL
for a, c being Real st ].a,c.[ c= dom f & f is_improper_integrable_on a,c holds
for b1, b2 being Real st a < b1 & b1 < c & a < b2 & b2 < c holds
(left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c))
proof end;

definition
let f be PartFunc of REAL,REAL;
let a, b be Real;
assume A1: ( ].a,b.[ c= dom f & f is_improper_integrable_on a,b ) ;
func improper_integral (f,a,b) -> ExtReal means :Def6: :: INTEGR24:def 6
ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & it = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) );
existence
ex b1 being ExtReal ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & b1 = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) )
proof end;
uniqueness
for b1, b2 being ExtReal st ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & b1 = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) ) & ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & b2 = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) ) holds
b1 = b2
by ;
end;

:: deftheorem Def6 defines improper_integral INTEGR24:def 6 :
for f being PartFunc of REAL,REAL
for a, b being Real st ].a,b.[ c= dom f & f is_improper_integrable_on a,b holds
for b4 being ExtReal holds
( b4 = improper_integral (f,a,b) iff ex c being Real st
( a < c & c < b & f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & b4 = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) ) );

theorem Th48: :: INTEGR24:48
for f being PartFunc of REAL,REAL
for a, c being Real st ].a,c.[ c= dom f & f is_improper_integrable_on a,c holds
for b being Real st a < b & b < c holds
( f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) )
proof end;

theorem Th49: :: INTEGR24:49
for f being PartFunc of REAL,REAL
for a, b being Real st f is_left_improper_integrable_on a,b & left_improper_integral (f,a,b) = +infty holds
for 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) ) holds
Intf is_right_divergent_to+infty_in a
proof end;

theorem Th50: :: INTEGR24:50
for f being PartFunc of REAL,REAL
for a, b being Real st f is_left_improper_integrable_on a,b & left_improper_integral (f,a,b) = -infty holds
for 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) ) holds
Intf is_right_divergent_to-infty_in a
proof end;

theorem Th51: :: INTEGR24:51
for f being PartFunc of REAL,REAL
for a, b being Real st f is_right_improper_integrable_on a,b & right_improper_integral (f,a,b) = +infty holds
for 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) ) holds
Intf is_left_divergent_to+infty_in b
proof end;

theorem Th52: :: INTEGR24:52
for f being PartFunc of REAL,REAL
for a, b being Real st f is_right_improper_integrable_on a,b & right_improper_integral (f,a,b) = -infty holds
for 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) ) holds
Intf is_left_divergent_to-infty_in b
proof end;

theorem Th53: :: INTEGR24:53
for f being PartFunc of REAL,REAL
for a, b, r being Real st a < b & ].a,b.] c= dom f & f is_left_improper_integrable_on a,b holds
( r (#) f is_left_improper_integrable_on a,b & left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) )
proof end;

theorem Th54: :: INTEGR24:54
for f being PartFunc of REAL,REAL
for a, b, r being Real st a < b & [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b holds
( r (#) f is_right_improper_integrable_on a,b & right_improper_integral ((r (#) f),a,b) = r * (right_improper_integral (f,a,b)) )
proof end;

theorem Th55: :: INTEGR24:55
for f being PartFunc of REAL,REAL
for a, b being Real st a < b & ].a,b.] c= dom f & f is_left_improper_integrable_on a,b holds
( - f is_left_improper_integrable_on a,b & left_improper_integral ((- f),a,b) = - (left_improper_integral (f,a,b)) )
proof end;

theorem Th56: :: INTEGR24:56
for f being PartFunc of REAL,REAL
for a, b being Real st a < b & [.a,b.[ c= dom f & f is_right_improper_integrable_on a,b holds
( - f is_right_improper_integrable_on a,b & right_improper_integral ((- f),a,b) = - (right_improper_integral (f,a,b)) )
proof end;

theorem Th57: :: INTEGR24:57
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_improper_integrable_on a,b & g is_left_improper_integrable_on a,b & ( not left_improper_integral (f,a,b) = +infty or not left_improper_integral (g,a,b) = -infty ) & ( not left_improper_integral (f,a,b) = -infty or not left_improper_integral (g,a,b) = +infty ) holds
( f + g is_left_improper_integrable_on a,b & left_improper_integral ((f + g),a,b) = (left_improper_integral (f,a,b)) + (left_improper_integral (g,a,b)) )
proof end;

theorem Th58: :: INTEGR24:58
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_improper_integrable_on a,b & g is_right_improper_integrable_on a,b & ( not right_improper_integral (f,a,b) = +infty or not right_improper_integral (g,a,b) = -infty ) & ( not right_improper_integral (f,a,b) = -infty or not right_improper_integral (g,a,b) = +infty ) holds
( f + g is_right_improper_integrable_on a,b & right_improper_integral ((f + g),a,b) = (right_improper_integral (f,a,b)) + (right_improper_integral (g,a,b)) )
proof end;

theorem :: INTEGR24:59
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_improper_integrable_on a,b & g is_left_improper_integrable_on a,b & ( not left_improper_integral (f,a,b) = +infty or not left_improper_integral (g,a,b) = +infty ) & ( not left_improper_integral (f,a,b) = -infty or not left_improper_integral (g,a,b) = -infty ) holds
( f - g is_left_improper_integrable_on a,b & left_improper_integral ((f - g),a,b) = (left_improper_integral (f,a,b)) - (left_improper_integral (g,a,b)) )
proof end;

theorem :: INTEGR24:60
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_improper_integrable_on a,b & g is_right_improper_integrable_on a,b & ( not right_improper_integral (f,a,b) = +infty or not right_improper_integral (g,a,b) = +infty ) & ( not right_improper_integral (f,a,b) = -infty or not right_improper_integral (g,a,b) = -infty ) holds
( f - g is_right_improper_integrable_on a,b & right_improper_integral ((f - g),a,b) = (right_improper_integral (f,a,b)) - (right_improper_integral (g,a,b)) )
proof end;

theorem Th61: :: INTEGR24:61
for f being PartFunc of REAL,REAL
for a, b, r being Real st ].a,b.[ c= dom f & f is_improper_integrable_on a,b holds
( r (#) f is_improper_integrable_on a,b & improper_integral ((r (#) f),a,b) = r * (improper_integral (f,a,b)) )
proof end;

theorem Th62: :: INTEGR24:62
for f being PartFunc of REAL,REAL
for a, b, r being Real st ].a,b.[ c= dom f & f is_improper_integrable_on a,b holds
( - f is_improper_integrable_on a,b & improper_integral ((- f),a,b) = - (improper_integral (f,a,b)) )
proof end;

theorem Th63: :: INTEGR24:63
for f, g being PartFunc of REAL,REAL
for a, b being Real st ].a,b.[ c= dom f & ].a,b.[ c= dom g & f is_improper_integrable_on a,b & g is_improper_integrable_on a,b & ( not improper_integral (f,a,b) = +infty or not improper_integral (g,a,b) = -infty ) & ( not improper_integral (f,a,b) = -infty or not improper_integral (g,a,b) = +infty ) holds
( f + g is_improper_integrable_on a,b & improper_integral ((f + g),a,b) = (improper_integral (f,a,b)) + (improper_integral (g,a,b)) )
proof end;

theorem :: INTEGR24:64
for f, g being PartFunc of REAL,REAL
for a, b being Real st ].a,b.[ c= dom f & ].a,b.[ c= dom g & f is_improper_integrable_on a,b & g is_improper_integrable_on a,b & ( not improper_integral (f,a,b) = +infty or not improper_integral (g,a,b) = +infty ) & ( not improper_integral (f,a,b) = -infty or not improper_integral (g,a,b) = -infty ) holds
( f - g is_improper_integrable_on a,b & improper_integral ((f - g),a,b) = (improper_integral (f,a,b)) - (improper_integral (g,a,b)) )
proof end;