let f be 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)) )
let a, r be Real; ( right_closed_halfline a c= dom f & f is_+infty_improper_integrable_on a implies ( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) ) )
assume that
A1:
right_closed_halfline a c= dom f
and
A2:
f is_+infty_improper_integrable_on a
; ( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )
A3:
for d being Real st a <= d holds
( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded )
proof
let d be
Real;
( a <= d implies ( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded ) )
assume A4:
a <= d
;
( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded )
[.a,d.] c= [.a,+infty.[
by XXREAL_1:251;
then
[.a,d.] c= dom f
by A1;
then A5:
['a,d'] c= dom f
by A4, INTEGRA5:def 3;
A6:
(
f is_integrable_on ['a,d'] &
f | ['a,d'] is
bounded )
by A2, A4;
hence
r (#) f is_integrable_on ['a,d']
by A5, INTEGRA6:9;
(r (#) f) | ['a,d'] is bounded
thus
(r (#) f) | ['a,d'] is
bounded
by A6, RFUNCT_1:80;
verum
end;
per cases
( f is_+infty_ext_Riemann_integrable_on a or not f is_+infty_ext_Riemann_integrable_on a )
;
suppose A7:
f is_+infty_ext_Riemann_integrable_on a
;
( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )then A8:
improper_integral_+infty (
f,
a)
= infty_ext_right_integral (
f,
a)
by A2, Th27;
A9:
(
r (#) f is_+infty_ext_Riemann_integrable_on a &
infty_ext_right_integral (
(r (#) f),
a)
= r * (infty_ext_right_integral (f,a)) )
by A1, A7, INTEGR10:9;
thus
r (#) f is_+infty_improper_integrable_on a
by A1, A7, INTEGR10:9, Th21;
improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a))then
improper_integral_+infty (
(r (#) f),
a)
= infty_ext_right_integral (
(r (#) f),
a)
by A9, Th27;
hence
improper_integral_+infty (
(r (#) f),
a)
= r * (improper_integral_+infty (f,a))
by A8, A9, XXREAL_3:def 5;
verum end; suppose A10:
not
f is_+infty_ext_Riemann_integrable_on a
;
( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )consider Intf being
PartFunc of
REAL,
REAL such that A11:
dom Intf = right_closed_halfline a
and A12:
for
x being
Real st
x in dom Intf holds
Intf . x = integral (
f,
a,
x)
by A2;
A13:
dom (r (#) Intf) = right_closed_halfline a
by A11, VALUED_1:def 5;
A14:
for
x being
Real st
x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral (
(r (#) f),
a,
x)
proof
let x be
Real;
( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),a,x) )
assume A15:
x in dom (r (#) Intf)
;
(r (#) Intf) . x = integral ((r (#) f),a,x)
then A16:
(r (#) Intf) . x =
r * (Intf . x)
by VALUED_1:def 5
.=
r * (integral (f,a,x))
by A15, A13, A12, A11
;
A17:
a <= x
by A13, A15, XXREAL_1:3;
[.a,x.] c= [.a,+infty.[
by XXREAL_1:251;
then
[.a,x.] c= dom f
by A1;
then A18:
['a,x'] c= dom f
by A17, INTEGRA5:def 3;
(
f is_integrable_on ['a,x'] &
f | ['a,x'] is
bounded )
by A2, A17;
hence
(r (#) Intf) . x = integral (
(r (#) f),
a,
x)
by A16, A17, A18, INTEGRA6:10;
verum
end; per cases
( improper_integral_+infty (f,a) = +infty or improper_integral_+infty (f,a) = -infty )
by A2, A10, Th27;
suppose A19:
improper_integral_+infty (
f,
a)
= +infty
;
( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )then A20:
Intf is
divergent_in+infty_to+infty
by A2, A11, A12, Th39;
per cases
( r > 0 or r < 0 or r = 0 )
;
suppose A21:
r > 0
;
( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )then A22:
r (#) Intf is
divergent_in+infty_to+infty
by A19, A2, A11, A12, Th39, LIMFUNC1:58;
thus
r (#) f is_+infty_improper_integrable_on a
by A3, A13, A14, A21, A20, LIMFUNC1:58;
improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a))then
improper_integral_+infty (
(r (#) f),
a)
= +infty
by A13, A14, A22, Def4;
hence
improper_integral_+infty (
(r (#) f),
a)
= r * (improper_integral_+infty (f,a))
by A19, A21, XXREAL_3:def 5;
verum end; suppose A23:
r < 0
;
( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )then A24:
r (#) Intf is
divergent_in+infty_to-infty
by A19, A2, A11, A12, Th39, LIMFUNC1:58;
thus
r (#) f is_+infty_improper_integrable_on a
by A3, A13, A14, A23, A20, LIMFUNC1:58;
improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a))then
improper_integral_+infty (
(r (#) f),
a)
= -infty
by A13, A14, A24, Def4;
hence
improper_integral_+infty (
(r (#) f),
a)
= r * (improper_integral_+infty (f,a))
by A19, A23, XXREAL_3:def 5;
verum end; suppose A25:
r = 0
;
( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )A26:
for
R being
Real ex
g being
Real st
(
R < g &
g in dom (r (#) Intf) )
by A11, A13, A20, LIMFUNC1:46;
A27:
for
g1 being
Real st
0 < g1 holds
ex
R being
Real st
for
r1 being
Real st
R < r1 &
r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1
then A29:
r (#) Intf is
convergent_in+infty
by A26, LIMFUNC1:44;
then A30:
lim_in+infty (r (#) Intf) = 0
by A27, LIMFUNC1:79;
thus
r (#) f is_+infty_improper_integrable_on a
by A3, A13, A14, A27, A26, LIMFUNC1:44;
improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a))then
improper_integral_+infty (
(r (#) f),
a)
= 0
by A13, A14, A29, A30, Def4;
hence
improper_integral_+infty (
(r (#) f),
a)
= r * (improper_integral_+infty (f,a))
by A25;
verum end; end; end; suppose A31:
improper_integral_+infty (
f,
a)
= -infty
;
( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )then A32:
Intf is
divergent_in+infty_to-infty
by A2, A11, A12, Th40;
per cases
( r > 0 or r < 0 or r = 0 )
;
suppose A33:
r > 0
;
( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )then A34:
r (#) Intf is
divergent_in+infty_to-infty
by A31, A2, A11, A12, Th40, LIMFUNC1:58;
thus
r (#) f is_+infty_improper_integrable_on a
by A3, A13, A14, A33, A32, LIMFUNC1:58;
improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a))then
improper_integral_+infty (
(r (#) f),
a)
= -infty
by A13, A14, A34, Def4;
hence
improper_integral_+infty (
(r (#) f),
a)
= r * (improper_integral_+infty (f,a))
by A31, A33, XXREAL_3:def 5;
verum end; suppose A35:
r < 0
;
( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )then A36:
r (#) Intf is
divergent_in+infty_to+infty
by A31, A2, A11, A12, Th40, LIMFUNC1:58;
thus
r (#) f is_+infty_improper_integrable_on a
by A3, A13, A14, A35, A32, LIMFUNC1:58;
improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a))then
improper_integral_+infty (
(r (#) f),
a)
= +infty
by A13, A14, A36, Def4;
hence
improper_integral_+infty (
(r (#) f),
a)
= r * (improper_integral_+infty (f,a))
by A31, A35, XXREAL_3:def 5;
verum end; suppose A37:
r = 0
;
( r (#) f is_+infty_improper_integrable_on a & improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) )A38:
for
R being
Real ex
g being
Real st
(
R < g &
g in dom (r (#) Intf) )
by A11, A13, A32, LIMFUNC1:47;
A39:
for
g1 being
Real st
0 < g1 holds
ex
R being
Real st
for
r1 being
Real st
R < r1 &
r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1
then A41:
r (#) Intf is
convergent_in+infty
by A38, LIMFUNC1:44;
then A42:
lim_in+infty (r (#) Intf) = 0
by A39, LIMFUNC1:79;
thus
r (#) f is_+infty_improper_integrable_on a
by A3, A13, A14, A39, A38, LIMFUNC1:44;
improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a))then
improper_integral_+infty (
(r (#) f),
a)
= 0
by A13, A14, A41, A42, Def4;
hence
improper_integral_+infty (
(r (#) f),
a)
= r * (improper_integral_+infty (f,a))
by A37;
verum end; end; end; end; end; end;