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,COMPLEX st f is_integrable_on M holds
ex F being sequence of S st
( ( for n being 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 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,COMPLEX st f is_integrable_on M holds
ex F being sequence of S st
( ( for n being 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 Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
let M be sigma_Measure of S; for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
ex F being sequence of S st
( ( for n being 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 Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
let f be PartFunc of X,COMPLEX; ( f is_integrable_on M implies ex F being sequence of S st
( ( for n being 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 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 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 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
by Th35;
defpred S1[ Element of NAT , set ] means $2 = E /\ (great_eq_dom (|.f.|,(1 / ($1 + 1))));
A4:
dom |.f.| = E
by A2, VALUED_1:def 11;
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)) )reconsider y =
|.f.| . x as
Real ;
assume A5:
x in E \ (eq_dom (|.f.|,0))
;
x in E /\ (great_dom (|.f.|,0))then A6:
x in E
by XBOOLE_0:def 5;
then A7:
x in dom |.f.|
by A2, VALUED_1:def 11;
not
x in eq_dom (
|.f.|,
0)
by A5, XBOOLE_0:def 5;
then
not
y = 0
by A7, MESFUNC6:7;
then
not
|.(f . x).| = 0
by A7, VALUED_1:def 11;
then
f . x <> 0
by COMPLEX1:5, SQUARE_1:17;
then
0 < |.(f . x).|
by COMPLEX1:47;
then
0 < |.f.| . x
by A7, VALUED_1:def 11;
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))
;
then A11:
E /\ (great_dom (|.f.|,0)) c= E \ (eq_dom (|.f.|,0))
;
A12:
|.f.| is E -measurable
by A2, A3, MESFUN6C:30;
A13:
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 A12, A4, MESFUNC6:13;
verum
end;
consider F being sequence of S such that
A14:
for n being Element of NAT holds S1[n,F . n]
from FUNCT_2:sch 3(A13);
A15:
for n being Nat holds
( F . n in S & M . (F . n) < +infty )
proof
|.f.| is_integrable_on M
by A1, Th35;
then A16:
Integral (
M,
|.f.|)
< +infty
by MESFUNC6:90;
let n be
Nat;
( F . n in S & M . (F . n) < +infty )
reconsider n1 =
n as
Element of
NAT by ORDINAL1:def 12;
set z = 1
/ (n + 1);
A17:
F . n1 = E /\ (great_eq_dom (|.f.|,(1 / (n1 + 1))))
by A14;
then reconsider En =
F . n as
Element of
S ;
set h =
|.f.| | En;
consider nf being
PartFunc of
X,
REAL such that A18:
nf is_simple_func_in S
and A19:
dom nf = En
and A20:
for
x being
object st
x in En holds
nf . x = 1
/ (n + 1)
by MESFUNC6:75;
A21:
dom (|.f.| | En) = En
by A4, A17, RELAT_1:62, XBOOLE_1:17;
A22:
F . n c= great_eq_dom (
|.f.|,
(1 / (n + 1)))
by A17, XBOOLE_1:17;
A23:
for
x being
Element of
X st
x in dom nf holds
nf . x <= (|.f.| | En) . x
(dom |.f.|) /\ En = E /\ En
by A2, VALUED_1:def 11;
then A25:
(dom |.f.|) /\ En = En
by A17, XBOOLE_1:17, XBOOLE_1:28;
|.f.| is
En -measurable
by A12, A17, MESFUNC6:16, XBOOLE_1:17;
then A26:
|.f.| | En is
En -measurable
by A25, MESFUNC6:76;
A27:
|.f.| | En is
nonnegative
by Lm1, MESFUNC6:55;
for
x being
object st
x in dom nf holds
nf . x >= 0
by A19, A20;
then A28:
nf is
nonnegative
by MESFUNC6:52;
(
|.f.| is
nonnegative &
|.f.| | E = |.f.| )
by A4, Lm1;
then A29:
Integral (
M,
(|.f.| | En))
<= Integral (
M,
|.f.|)
by A12, A4, A17, MESFUNC6:87, XBOOLE_1:17;
nf is
En -measurable
by A18, MESFUNC6:50;
then
Integral (
M,
nf)
<= Integral (
M,
(|.f.| | En))
by A21, A26, A27, A19, A28, A23, Th34;
then A30:
Integral (
M,
nf)
<= Integral (
M,
|.f.|)
by A29, XXREAL_0:2;
A31:
(
((1 / (n + 1)) * (M . En)) / (1 / (n + 1)) = M . En &
+infty / (1 / (n + 1)) = +infty )
by XXREAL_3:83, XXREAL_3:88;
Integral (
M,
nf)
= (1 / (n + 1)) * (M . En)
by A19, A20, MESFUNC6:97;
then
(1 / (n + 1)) * (M . En) < +infty
by A16, A30, XXREAL_0:2;
hence
(
F . n in S &
M . (F . n) < +infty )
by A31, XXREAL_3:80;
verum
end;
take
F
; ( ( for n being 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 Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
A32:
for n being Nat holds F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))
then
for n being Nat holds F . n = E /\ (great_eq_dom (|.f.|,(0 + (1 / (n + 1)))))
;
then
E /\ (great_dom (|.f.|,0)) = union (rng F)
by MESFUNC6:11;
hence
( ( for n being 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 Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
by A2, A32, A11, A8, A15; verum