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