let f be PartFunc of REAL,REAL; for a being Real
for A being non empty Subset of REAL st dom f = REAL & f is_improper_integrable_on_REAL & f is nonnegative holds
( improper_integral_on_REAL f = Integral (L-Meas,f) & ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = +infty ) )
let a be Real; for A being non empty Subset of REAL st dom f = REAL & f is_improper_integrable_on_REAL & f is nonnegative holds
( improper_integral_on_REAL f = Integral (L-Meas,f) & ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = +infty ) )
let A be non empty Subset of REAL; ( dom f = REAL & f is_improper_integrable_on_REAL & f is nonnegative implies ( improper_integral_on_REAL f = Integral (L-Meas,f) & ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = +infty ) ) )
assume that
A1:
dom f = REAL
and
A2:
f is_improper_integrable_on_REAL
and
A3:
f is nonnegative
; ( improper_integral_on_REAL f = Integral (L-Meas,f) & ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = +infty ) )
consider c being Real such that
A4:
f is_-infty_improper_integrable_on c
and
A5:
f is_+infty_improper_integrable_on c
and
A6:
improper_integral_on_REAL f = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c))
by A1, A2, INTEGR25:def 6;
A7:
( -infty < c & c < +infty )
by XREAL_0:def 1, XXREAL_0:9, XXREAL_0:12;
then reconsider A = ].-infty,c.] as non empty Subset of REAL by XXREAL_1:32;
reconsider B = [.c,+infty.[ as non empty Subset of REAL by A7, XXREAL_1:31;
A8:
A = left_closed_halfline c
by LIMFUNC1:def 1;
then A9:
improper_integral_-infty (f,c) = Integral (L-Meas,(f | A))
by A4, A1, A3, Th47;
A10:
B = right_closed_halfline c
by LIMFUNC1:def 2;
REAL = ].-infty,+infty.[
by XXREAL_1:224;
then reconsider E = REAL as Element of L-Field by MEASUR10:5, MEASUR12:75;
A11:
f is E -measurable
by A1, A2, Th38;
reconsider A1 = A as Element of L-Field by MEASUR10:5, MEASUR12:75;
reconsider B1 = B as Element of L-Field by MEASUR10:5, MEASUR12:75;
A12:
f is A1 -measurable
by A1, A2, Th38;
set C = {c};
A13:
{c} = [.c,c.]
by XXREAL_1:17;
reconsider C = {c} as Element of L-Field by Th28;
A14: L-Meas . C =
c - c
by A13, MESFUN14:5
.=
0
;
A15:
dom (f | A) = A
by A1, RELAT_1:62;
then
A1 = (dom f) /\ A1
by RELAT_1:61;
then A16: Integral (L-Meas,(f | A)) =
Integral (L-Meas,((f | A) | (A \ C)))
by A12, A14, A15, MESFUNC6:76, MESFUNC6:89
.=
Integral (L-Meas,(f | (A \ C)))
by XBOOLE_1:36, RELAT_1:74
;
A17:
( -infty < c & c < +infty )
by XREAL_0:def 1, XXREAL_0:12, XXREAL_0:9;
then A18:
A1 \ C = ].-infty,c.[
by XXREAL_1:137;
A \/ B = ].-infty,+infty.[
by A17, XXREAL_1:172;
then A19:
f | (A \/ B) = f
by XXREAL_1:224;
(A1 \ C) \/ B1 = ].-infty,+infty.[
by A17, A18, XXREAL_1:173;
then
f = f | ((A1 \ C) \/ B1)
by XXREAL_1:224;
then
Integral (L-Meas,f) = (Integral (L-Meas,(f | A1))) + (Integral (L-Meas,(f | B1)))
by A16, A1, A11, A3, A18, XXREAL_1:94, MESFUNC6:85;
hence
improper_integral_on_REAL f = Integral (L-Meas,f)
by A10, A6, A9, A5, A1, A3, Th49; ( ( f is infty_ext_Riemann_integrable implies f is_integrable_on L-Meas ) & ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = +infty ) )
hereby ( not f is infty_ext_Riemann_integrable implies Integral (L-Meas,f) = +infty )
assume
f is
infty_ext_Riemann_integrable
;
f is_integrable_on L-Meas then
(
f is_+infty_ext_Riemann_integrable_on c &
f is_-infty_ext_Riemann_integrable_on c )
by A1, INTEGR25:19;
then
(
f | A1 is_integrable_on L-Meas &
f | B1 is_integrable_on L-Meas )
by A1, A3, A4, A5, A8, A10, Th47, Th49;
hence
f is_integrable_on L-Meas
by A19, A1, Th53;
verum
end;
hereby verum
assume
not
f is
infty_ext_Riemann_integrable
;
Integral (L-Meas,f) = +infty then consider d being
Real such that A20:
( not
f is_+infty_ext_Riemann_integrable_on d or not
f is_-infty_ext_Riemann_integrable_on d )
by A1, INTEGR25:19;
A21:
(
f is_-infty_improper_integrable_on d &
f is_+infty_improper_integrable_on d &
improper_integral_on_REAL f = (improper_integral_-infty (f,d)) + (improper_integral_+infty (f,d)) )
by A1, A2, INTEGR25:36;
A22:
d in REAL
by XREAL_0:def 1;
then
not
].-infty,d.] is
empty
by XXREAL_0:12, XXREAL_1:32;
then reconsider A1 =
left_closed_halfline d as non
empty Subset of
REAL by LIMFUNC1:def 1;
not
[.d,+infty.[ is
empty
by A22, XXREAL_0:9, XXREAL_1:31;
then reconsider B1 =
right_closed_halfline d as non
empty Subset of
REAL by LIMFUNC1:def 2;
A1 = ].-infty,d.]
by LIMFUNC1:def 1;
then reconsider A1 =
A1 as
Element of
L-Field by MEASUR10:5, MEASUR12:75;
B1 = [.d,+infty.[
by LIMFUNC1:def 2;
then reconsider B1 =
B1 as
Element of
L-Field by MEASUR10:5, MEASUR12:75;
per cases
( not f is_+infty_ext_Riemann_integrable_on d or not f is_-infty_ext_Riemann_integrable_on d )
by A20;
suppose
not
f is_+infty_ext_Riemann_integrable_on d
;
Integral (L-Meas,f) = +infty then A23:
Integral (
L-Meas,
(f | B1))
= +infty
by A21, A3, A1, Th49;
Integral (
L-Meas,
(f | B1))
<= Integral (
L-Meas,
(f | E))
by A1, A3, A2, Th38, MESFUNC6:87;
hence
Integral (
L-Meas,
f)
= +infty
by A23, XXREAL_0:4;
verum end; suppose
not
f is_-infty_ext_Riemann_integrable_on d
;
Integral (L-Meas,f) = +infty then A24:
Integral (
L-Meas,
(f | A1))
= +infty
by A21, A3, A1, Th47;
Integral (
L-Meas,
(f | A1))
<= Integral (
L-Meas,
(f | E))
by A1, A3, A2, Th38, MESFUNC6:87;
hence
Integral (
L-Meas,
f)
= +infty
by A24, XXREAL_0:4;
verum end;
end;