:: 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 b₁ 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 & b₁ = lim_in-infty Intf ) or ( Intf is divergent_in-infty_to+infty & b₁ = +infty ) or ( Intf is divergent_in-infty_to-infty & b₁ = -infty ) ) )

proof end;

uniqueness
for b₁, b₂ 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 & b₁ = lim_in-infty Intf ) or ( Intf is divergent_in-infty_to+infty & b₁ = +infty ) or ( Intf is divergent_in-infty_to-infty & b₁ = -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 & b₂ = lim_in-infty Intf ) or ( Intf is divergent_in-infty_to+infty & b₂ = +infty ) or ( Intf is divergent_in-infty_to-infty & b₂ = -infty ) ) ) holds
b₁ = b₂

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 b₃ being ExtReal holds
( b₃ = 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 & b₃ = lim_in-infty Intf ) or ( Intf is divergent_in-infty_to+infty & b₃ = +infty ) or ( Intf is divergent_in-infty_to-infty & b₃ = -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 b₁ 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 & b₁ = lim_in+infty Intf ) or ( Intf is divergent_in+infty_to+infty & b₁ = +infty ) or ( Intf is divergent_in+infty_to-infty & b₁ = -infty ) ) )

proof end;

uniqueness
for b₁, b₂ 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 & b₁ = lim_in+infty Intf ) or ( Intf is divergent_in+infty_to+infty & b₁ = +infty ) or ( Intf is divergent_in+infty_to-infty & b₁ = -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 & b₂ = lim_in+infty Intf ) or ( Intf is divergent_in+infty_to+infty & b₂ = +infty ) or ( Intf is divergent_in+infty_to-infty & b₂ = -infty ) ) ) holds
b₁ = b₂

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 b₃ being ExtReal holds
( b₃ = 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 & b₃ = lim_in+infty Intf ) or ( Intf is divergent_in+infty_to+infty & b₃ = +infty ) or ( Intf is divergent_in+infty_to-infty & b₃ = -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 b₁ being ExtReal ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & b₁ = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) )

proof end;

uniqueness
for b₁, b₂ being ExtReal st ex c being Real st
( f is_-infty_improper_integrable_on c & f is_+infty_improper_integrable_on c & b₁ = (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 & b₂ = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) ) holds
b₁ = b₂ 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 b₂ being ExtReal holds
( b₂ = 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 & b₂ = (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;