let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is A -measurable ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is A -measurable ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is A -measurable ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
let f be PartFunc of X,COMPLEX; :: thesis: ( ex A being Element of S st
( A = dom f & f is A -measurable ) implies ( f is_integrable_on M iff |.f.| is_integrable_on M ) )
A1: dom (|.(Re f).| + |.(Im f).|) = (dom |.(Re f).|) /\ (dom |.(Im f).|) by VALUED_1:def 1;
A2: dom |.(Re f).| = dom (Re f) by VALUED_1:def 11;
A3: dom |.(Im f).| = dom (Im f) by VALUED_1:def 11;
A4: dom |.f.| = dom f by VALUED_1:def 11;
assume ex A being Element of S st
( A = dom f & f is A -measurable ) ; :: thesis: ( f is_integrable_on M iff |.f.| is_integrable_on M )
then consider A being Element of S such that
A5: A = dom f and
A6: f is A -measurable ;
A7: dom (Re f) = A by A5, COMSEQ_3:def 3;
A8: Im f is A -measurable by A6;
A9: Re f is A -measurable by A6;
A10: dom (Im f) = A by A5, COMSEQ_3:def 4;
A11: |.f.| is A -measurable by A5, A6, Th30;
hereby :: thesis: ( |.f.| is_integrable_on M implies f is_integrable_on M )
A12: now :: thesis: for x being Element of X st x in dom |.f.| holds
|.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x
let x be Element of X; :: thesis: ( x in dom |.f.| implies |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x )
assume A13: x in dom |.f.| ; :: thesis: |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x
then A14: |.f.| . x = |.(f . x).| by VALUED_1:def 11;
A15: |.((Im f) . x).| = |.(Im f).| . x by A5, A10, A3, A4, A13, VALUED_1:def 11;
A16: |.((Re f) . x).| = |.(Re f).| . x by A5, A7, A2, A4, A13, VALUED_1:def 11;
A17: (Im f) . x = Im (f . x) by A5, A10, A4, A13, COMSEQ_3:def 4;
A18: (Re f) . x = Re (f . x) by A5, A7, A4, A13, COMSEQ_3:def 3;
(|.(Re f).| + |.(Im f).|) . x = (|.(Re f).| . x) + (|.(Im f).| . x) by A5, A7, A10, A1, A2, A3, A4, A13, VALUED_1:def 1;
hence |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x by A18, A17, A14, A16, A15, COMPLEX1:78; :: thesis: verum
end;
assume A19: f is_integrable_on M ; :: thesis: |.f.| is_integrable_on M
then Im f is_integrable_on M ;
then A20: |.(Im f).| is_integrable_on M by A10, A8, MESFUNC6:94;
Re f is_integrable_on M by A19;
then |.(Re f).| is_integrable_on M by A7, A9, MESFUNC6:94;
then |.(Re f).| + |.(Im f).| is_integrable_on M by A20, MESFUNC6:100;
hence |.f.| is_integrable_on M by A5, A7, A10, A1, A2, A3, A4, A11, A12, MESFUNC6:96; :: thesis: verum
end;
hereby :: thesis: verum
assume A21: |.f.| is_integrable_on M ; :: thesis: f is_integrable_on M
now :: thesis: for x being Element of X st x in dom (Im f) holds
|.((Im f) . x).| <= |.f.| . x
let x be Element of X; :: thesis: ( x in dom (Im f) implies |.((Im f) . x).| <= |.f.| . x )
A22: |.(Im (f . x)).| <= |.(f . x).| by COMPLEX1:79;
assume A23: x in dom (Im f) ; :: thesis: |.((Im f) . x).| <= |.f.| . x
then |.f.| . x = |.(f . x).| by A5, A10, A4, VALUED_1:def 11;
hence |.((Im f) . x).| <= |.f.| . x by A23, A22, COMSEQ_3:def 4; :: thesis: verum
end;
then A24: Im f is_integrable_on M by A5, A10, A8, A4, A21, MESFUNC6:96;
now :: thesis: for x being Element of X st x in dom (Re f) holds
|.((Re f) . x).| <= |.f.| . x
let x be Element of X; :: thesis: ( x in dom (Re f) implies |.((Re f) . x).| <= |.f.| . x )
A25: |.(Re (f . x)).| <= |.(f . x).| by COMPLEX1:79;
assume A26: x in dom (Re f) ; :: thesis: |.((Re f) . x).| <= |.f.| . x
then |.f.| . x = |.(f . x).| by A5, A7, A4, VALUED_1:def 11;
hence |.((Re f) . x).| <= |.f.| . x by A26, A25, COMSEQ_3:def 3; :: thesis: verum
end;
then Re f is_integrable_on M by A5, A7, A9, A4, A21, MESFUNC6:96;
hence f is_integrable_on M by A24; :: thesis: verum
end;