let f be 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 ) )
let a, b be Real; ( 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 ) )
assume A1:
f is_right_improper_integrable_on a,b
; ( ( 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 ) )
then consider Intf being PartFunc of REAL,REAL such that
A2:
( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) & ( Intf is_left_convergent_in b or Intf is_left_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b ) )
;
per cases
( Intf is_left_convergent_in b or Intf is_left_divergent_to+infty_in b or Intf is_left_divergent_to-infty_in b )
by A2;
suppose A3:
Intf is_left_convergent_in b
;
( ( 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 ) )then A4:
f is_right_ext_Riemann_integrable_on a,
b
by A1, A2, INTEGR10:def 1;
right_improper_integral (
f,
a,
b) =
lim_left (
Intf,
b)
by A1, A2, A3, Def4
.=
ext_right_integral (
f,
a,
b)
by A2, A3, A4, INTEGR10:def 3
;
hence
( (
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 ) )
by A3, A1, A2, INTEGR10:def 1;
verum end; suppose A5:
Intf is_left_divergent_to+infty_in b
;
( ( 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 ) )
for
I being
PartFunc of
REAL,
REAL st
dom I = [.a,b.[ & ( for
x being
Real st
x in dom I holds
I . x = integral (
f,
a,
x) ) holds
not
I is_left_convergent_in b
proof
let I be
PartFunc of
REAL,
REAL;
( dom I = [.a,b.[ & ( for x being Real st x in dom I holds
I . x = integral (f,a,x) ) implies not I is_left_convergent_in b )
assume that A6:
dom I = [.a,b.[
and A7:
for
x being
Real st
x in dom I holds
I . x = integral (
f,
a,
x)
;
not I is_left_convergent_in b
then
Intf = I
by A2, A6, PARTFUN1:5;
hence
not
I is_left_convergent_in b
by A5, Th6;
verum
end; hence
( (
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 ) )
by A1, Def4, INTEGR10:def 1;
verum end; suppose A9:
Intf is_left_divergent_to-infty_in b
;
( ( 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 ) )
for
I being
PartFunc of
REAL,
REAL st
dom I = [.a,b.[ & ( for
x being
Real st
x in dom I holds
I . x = integral (
f,
a,
x) ) holds
not
I is_left_convergent_in b
proof
let I be
PartFunc of
REAL,
REAL;
( dom I = [.a,b.[ & ( for x being Real st x in dom I holds
I . x = integral (f,a,x) ) implies not I is_left_convergent_in b )
assume that A10:
dom I = [.a,b.[
and A11:
for
x being
Real st
x in dom I holds
I . x = integral (
f,
a,
x)
;
not I is_left_convergent_in b
then
Intf = I
by A2, A10, PARTFUN1:5;
hence
not
I is_left_convergent_in b
by A9, Th7;
verum
end; hence
( (
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 ) )
by A1, Def4, INTEGR10:def 1;
verum end; end;