let f be 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 )
let b, c be Real; ( 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 implies ( f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = -infty ) )
assume that
A1:
b >= c
and
A2:
right_closed_halfline c c= dom f
and
A3:
f | ['c,b'] is bounded
and
A4:
f is_+infty_improper_integrable_on b
and
A5:
f is_integrable_on ['c,b']
and
A6:
improper_integral_+infty (f,b) = -infty
; ( f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = -infty )
consider I being PartFunc of REAL,REAL such that
A7:
dom I = right_closed_halfline b
and
A8:
for x being Real st x in dom I holds
I . x = integral (f,b,x)
and
A9:
( I is convergent_in+infty or I is divergent_in+infty_to+infty or I is divergent_in+infty_to-infty )
by A4;
improper_integral_+infty (f,b) <> infty_ext_right_integral (f,b)
by A6;
then A10:
not f is_+infty_ext_Riemann_integrable_on b
by A4, Th27;
+infty > c
by XREAL_0:def 1, XXREAL_0:9;
then reconsider AC = [.c,+infty.[ as non empty Subset of REAL by XXREAL_1:3;
deffunc H1( Element of AC) -> Element of REAL = In ((integral (f,c,$1)),REAL);
consider Intf being Function of AC,REAL such that
A11:
for x being Element of AC holds Intf . x = H1(x)
from FUNCT_2:sch 4();
A12:
dom Intf = AC
by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
A13:
for x being Real st x in dom Intf holds
Intf . x = integral (f,c,x)
proof
let x be
Real;
( x in dom Intf implies Intf . x = integral (f,c,x) )
assume
x in dom Intf
;
Intf . x = integral (f,c,x)
then
Intf . x = In (
(integral (f,c,x)),
REAL)
by A11, A12;
hence
Intf . x = integral (
f,
c,
x)
;
verum
end;
A14:
for r being Real ex g being Real st
( g > r & g in dom Intf )
proof
let r be
Real;
ex g being Real st
( g > r & g in dom Intf )
consider g being
Real such that A15:
(
g > r &
g in dom I )
by A10, A6, A7, Def4, INTEGR10:def 5, A4, LIMFUNC1:47;
[.b,+infty.[ c= [.c,+infty.[
by A1, XXREAL_1:38;
hence
ex
g being
Real st
(
g > r &
g in dom Intf )
by A15, A7, A12;
verum
end;
A16:
for g1 being Real ex r being Real st
for r1 being Real st r1 > r & r1 in dom Intf holds
g1 > Intf . r1
proof
let g1 be
Real;
ex r being Real st
for r1 being Real st r1 > r & r1 in dom Intf holds
g1 > Intf . r1
consider r being
Real such that A17:
for
r1 being
Real st
r1 > r &
r1 in dom I holds
g1 - (integral (f,c,b)) > I . r1
by A10, A9, A4, A6, A7, A8, Def4, INTEGR10:def 5, LIMFUNC1:47;
set R =
max (
b,
r);
take
max (
b,
r)
;
for r1 being Real st r1 > max (b,r) & r1 in dom Intf holds
g1 > Intf . r1
thus
for
r1 being
Real st
r1 > max (
b,
r) &
r1 in dom Intf holds
g1 > Intf . r1
verumproof
let r1 be
Real;
( r1 > max (b,r) & r1 in dom Intf implies g1 > Intf . r1 )
assume A18:
(
r1 > max (
b,
r) &
r1 in dom Intf )
;
g1 > Intf . r1
A19:
(
max (
b,
r)
>= b &
max (
b,
r)
>= r )
by XXREAL_0:25;
then A20:
(
r1 > b &
r1 > r )
by A18, XXREAL_0:2;
then A21:
r1 > c
by A1, XXREAL_0:2;
r1 in dom I
by A7, A19, A18, XXREAL_0:2, XXREAL_1:236;
then
g1 - (integral (f,c,b)) > I . r1
by A17, A20;
then A22:
g1 - (integral (f,c,b)) > integral (
f,
b,
r1)
by A8, A20, A7, XXREAL_1:236;
A23:
(
f is_integrable_on ['c,r1'] &
f | ['c,r1'] is
bounded )
by A21, A1, A2, A3, A4, A5, Lm14;
A24:
['c,r1'] = [.c,r1.]
by A20, A1, XXREAL_0:2, INTEGRA5:def 3;
then
['c,r1'] c= [.c,+infty.[
by XXREAL_1:251;
then A25:
['c,r1'] c= dom f
by A2;
b in ['c,r1']
by A24, A20, A1, XXREAL_1:1;
then
integral (
f,
c,
r1)
= (integral (f,b,r1)) + (integral (f,c,b))
by A21, A23, A25, INTEGRA6:17;
then
integral (
f,
b,
r1)
= (integral (f,c,r1)) - (integral (f,c,b))
;
then
g1 > integral (
f,
c,
r1)
by A22, XREAL_1:9;
hence
g1 > Intf . r1
by A13, A18;
verum
end;
end;
hence A26:
f is_+infty_improper_integrable_on c
by A12, A13, A14, A1, A2, A3, A4, A5, Lm14, LIMFUNC1:47; improper_integral_+infty (f,c) = -infty
Intf is divergent_in+infty_to-infty
by A14, A16, LIMFUNC1:47;
hence
improper_integral_+infty (f,c) = -infty
by A12, A13, A26, Def4; verum