let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
ex F being sequence of S st
( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) )
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
ex F being sequence of S st
( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) )
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
ex F being sequence of S st
( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) )
let f be PartFunc of X,ExtREAL; ( f is_integrable_on M implies ex F being sequence of S st
( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) ) )
assume A1:
f is_integrable_on M
; ex F being sequence of S st
( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) )
then consider E being Element of S such that
A2:
E = dom f
and
A3:
f is E -measurable
;
defpred S1[ Element of NAT , set ] means $2 = E /\ (great_eq_dom (|.f.|,(1 / ($1 + 1))));
A4:
dom |.f.| = E
by A2, MESFUNC1:def 10;
now for x being object st x in E \ (eq_dom (f,0.)) holds
x in E /\ (great_dom (|.f.|,0.))let x be
object ;
( x in E \ (eq_dom (f,0.)) implies x in E /\ (great_dom (|.f.|,0.)) )assume A5:
x in E \ (eq_dom (f,0.))
;
x in E /\ (great_dom (|.f.|,0.))then reconsider z =
x as
Element of
X ;
reconsider y =
f . z as
R_eal ;
A6:
x in E
by A5, XBOOLE_0:def 5;
then A7:
x in dom |.f.|
by A2, MESFUNC1:def 10;
not
x in eq_dom (
f,
0.)
by A5, XBOOLE_0:def 5;
then
not
y = 0.
by A2, A6, MESFUNC1:def 15;
then
0. < |.(f . z).|
by EXTREAL1:15;
then
0. < |.f.| . z
by A7, MESFUNC1:def 10;
then
x in great_dom (
|.f.|,
0.)
by A7, MESFUNC1:def 13;
hence
x in E /\ (great_dom (|.f.|,0.))
by A6, XBOOLE_0:def 4;
verum end;
then A8:
E \ (eq_dom (f,0.)) c= E /\ (great_dom (|.f.|,0.))
;
now for x being object st x in E /\ (great_dom (|.f.|,0.)) holds
x in E \ (eq_dom (f,0.))let x be
object ;
( x in E /\ (great_dom (|.f.|,0.)) implies x in E \ (eq_dom (f,0.)) )assume A9:
x in E /\ (great_dom (|.f.|,0.))
;
x in E \ (eq_dom (f,0.))then reconsider z =
x as
Element of
X ;
x in great_dom (
|.f.|,
0.)
by A9, XBOOLE_0:def 4;
then A10:
0. < |.f.| . z
by MESFUNC1:def 13;
A11:
x in E
by A9, XBOOLE_0:def 4;
then
x in dom |.f.|
by A2, MESFUNC1:def 10;
then A12:
0. < |.(f . z).|
by A10, MESFUNC1:def 10;
not
x in eq_dom (
f,
0.)
hence
x in E \ (eq_dom (f,0.))
by A11, XBOOLE_0:def 5;
verum end;
then A13:
E /\ (great_dom (|.f.|,0.)) c= E \ (eq_dom (f,0.))
;
A14:
|.f.| is E -measurable
by A2, A3, MESFUNC2:27;
A15:
for n being Element of NAT ex Z being Element of S st S1[n,Z]
proof
let n be
Element of
NAT ;
ex Z being Element of S st S1[n,Z]
take
E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))
;
( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] )
thus
(
E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is
Element of
S &
S1[
n,
E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] )
by A14, A4, MESFUNC1:27;
verum
end;
consider F being sequence of S such that
A16:
for n being Element of NAT holds S1[n,F . n]
from FUNCT_2:sch 3(A15);
A17:
for n being Element of NAT holds
( F . n in S & M . (F . n) < +infty )
proof
let n be
Element of
NAT ;
( F . n in S & M . (F . n) < +infty )
set d = 1
/ (n + 1);
set En =
F . n;
set g =
|.f.| | (F . n);
A18:
|.f.| | (F . n) is
nonnegative
by MESFUNC5:15;
set z = 1
/ (n + 1);
A19:
|.f.| | E = |.f.|
by A4, RELAT_1:69;
A20:
F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))
by A16;
then A21:
dom (|.f.| | (F . n)) = F . n
by A4, RELAT_1:62, XBOOLE_1:17;
(dom |.f.|) /\ (F . n) = E /\ (F . n)
by A2, MESFUNC1:def 10;
then A22:
(dom |.f.|) /\ (F . n) = F . n
by A20, XBOOLE_1:17, XBOOLE_1:28;
|.f.| is
F . n -measurable
by A14, A20, MESFUNC1:30, XBOOLE_1:17;
then A23:
|.f.| | (F . n) is
F . n -measurable
by A22, MESFUNC5:42;
then A24:
integral+ (
M,
(|.f.| | (F . n)))
= Integral (
M,
(|.f.| | (F . n)))
by A21, MESFUNC5:15, MESFUNC5:88;
|.f.| is_integrable_on M
by A1, MESFUNC5:100;
then A25:
Integral (
M,
|.f.|)
< +infty
by MESFUNC5:96;
A26:
((1 / (n + 1)) * (M . (F . n))) / (1 / (n + 1)) = M . (F . n)
by XXREAL_3:88;
F . n c= E
by A20, XBOOLE_1:17;
then A27:
Integral (
M,
(|.f.| | (F . n)))
<= Integral (
M,
|.f.|)
by A2, A3, A4, A19, MESFUNC2:27, MESFUNC5:93;
consider nf being
PartFunc of
X,
ExtREAL such that A28:
nf is_simple_func_in S
and A29:
dom nf = F . n
and A30:
for
x being
object st
x in F . n holds
nf . x = 1
/ (n + 1)
by MESFUNC5:41;
for
x being
object st
x in dom nf holds
nf . x >= 0
by A29, A30;
then A31:
nf is
nonnegative
by SUPINF_2:52;
then A32:
Integral (
M,
nf)
= integral' (
M,
nf)
by A28, MESFUNC5:89;
A33:
F . n c= great_eq_dom (
|.f.|,
(1 / (n + 1)))
by A20, XBOOLE_1:17;
A34:
for
x being
Element of
X st
x in dom nf holds
nf . x <= (|.f.| | (F . n)) . x
nf is
F . n -measurable
by A28, MESFUNC2:34;
then
integral+ (
M,
nf)
<= integral+ (
M,
(|.f.| | (F . n)))
by A21, A23, A18, A29, A31, A34, MESFUNC5:85;
then A37:
integral+ (
M,
nf)
<= Integral (
M,
|.f.|)
by A24, A27, XXREAL_0:2;
A38:
+infty / (1 / (n + 1)) = +infty
by XXREAL_3:83;
integral+ (
M,
nf)
= Integral (
M,
nf)
by A28, A31, MESFUNC5:89;
then
integral+ (
M,
nf)
= (1 / (n + 1)) * (M . (F . n))
by A29, A30, A32, MESFUNC5:104;
then
(1 / (n + 1)) * (M . (F . n)) < +infty
by A25, A37, XXREAL_0:2;
hence
(
F . n in S &
M . (F . n) < +infty )
by A26, A38, XXREAL_3:80;
verum
end;
take
F
; ( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) )
for n being Element of NAT holds F . n = E /\ (great_eq_dom (|.f.|,(0 + (1 / (n + 1)))))
by A16;
then
E /\ (great_dom (|.f.|,0)) = union (rng F)
by MESFUNC1:22;
hence
( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds
( F . n in S & M . (F . n) < +infty ) ) )
by A2, A16, A13, A8, A17, XBOOLE_0:def 10; verum