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 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; 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; 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; ( 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 )
; ( 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 ( |.f.| is_integrable_on M implies f is_integrable_on M )
A12:
now for x being Element of X st x in dom |.f.| holds
|.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . xlet x be
Element of
X;
( x in dom |.f.| implies |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x )assume A13:
x in dom |.f.|
;
|.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . xthen 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;
verum end; assume A19:
f is_integrable_on M
;
|.f.| is_integrable_on Mthen
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;
verum
end;
hereby verum
assume A21:
|.f.| is_integrable_on M
;
f is_integrable_on Mthen A24:
Im f is_integrable_on M
by A5, A10, A8, A4, A21, MESFUNC6:96;
then
Re f is_integrable_on M
by A5, A7, A9, A4, A21, MESFUNC6:96;
hence
f is_integrable_on M
by A24;
verum
end;