:: Improper Integral, Part {I}
:: by Noboru Endou
::
:: Received September 30, 2021
:: 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) /\ (left_open_halfline x0) )

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) /\ (right_open_halfline x0) )

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 b₁ 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 & b₁ = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & b₁ = +infty ) or ( Intf is_right_divergent_to-infty_in a & b₁ = -infty ) ) )

proof end;

uniqueness
for b₁, b₂ 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 & b₁ = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & b₁ = +infty ) or ( Intf is_right_divergent_to-infty_in a & b₁ = -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 & b₂ = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & b₂ = +infty ) or ( Intf is_right_divergent_to-infty_in a & b₂ = -infty ) ) ) holds
b₁ = b₂

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 b₄ being ExtReal holds
( b₄ = 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 & b₄ = lim_right (Intf,a) ) or ( Intf is_right_divergent_to+infty_in a & b₄ = +infty ) or ( Intf is_right_divergent_to-infty_in a & b₄ = -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 b₁ 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 & b₁ = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & b₁ = +infty ) or ( Intf is_left_divergent_to-infty_in b & b₁ = -infty ) ) )

proof end;

uniqueness
for b₁, b₂ 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 & b₁ = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & b₁ = +infty ) or ( Intf is_left_divergent_to-infty_in b & b₁ = -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 & b₂ = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & b₂ = +infty ) or ( Intf is_left_divergent_to-infty_in b & b₂ = -infty ) ) ) holds
b₁ = b₂

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 b₄ being ExtReal holds
( b₄ = 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 & b₄ = lim_left (Intf,b) ) or ( Intf is_left_divergent_to+infty_in b & b₄ = +infty ) or ( Intf is_left_divergent_to-infty_in b & b₄ = -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 b₁ 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 & b₁ = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) )

proof end;

uniqueness
for b₁, b₂ 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 & b₁ = (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 & b₂ = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) ) holds
b₁ = b₂ by A1, Th47;

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 b₄ being ExtReal holds
( b₄ = 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 & b₄ = (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;