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 ) & f is_integrable_on M & Integral (M,f) = 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
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 ) & f is_integrable_on M & Integral (M,f) = 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
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 ) & f is_integrable_on M & Integral (M,f) = 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
let f be PartFunc of X,COMPLEX; :: thesis: ( ex A being Element of S st
( A = dom f & f is A -measurable ) & f is_integrable_on M & Integral (M,f) = 0 implies |.(Integral (M,f)).| <= Integral (M,|.f.|) )
assume that
A1: ex A being Element of S st
( A = dom f & f is A -measurable ) and
A2: f is_integrable_on M and
A3: Integral (M,f) = 0 ; :: thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|)
A4: |.f.| is_integrable_on M by A1, A2, Th31;
consider R, I being Real such that
A5: R = Integral (M,(Re f)) and
I = Integral (M,(Im f)) and
A6: Integral (M,f) = R + (I * <i>) by A2, Def3;
R = 0 by A3, A6, COMPLEX1:4, COMPLEX1:12;
then A7: |.(Integral (M,(Re f))).| = 0 by A5, EXTREAL1:16;
Re f is_integrable_on M by A2;
then A8: |.(Integral (M,(Re f))).| <= Integral (M,|.(Re f).|) by MESFUNC6:95;
A9: dom |.f.| = dom f by VALUED_1:def 11;
consider A being Element of S such that
A10: A = dom f and
A11: f is A -measurable by A1;
A12: dom (Re f) = A by A10, COMSEQ_3:def 3;
A13: 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 )
assume A14: x in dom (Re f) ; :: thesis: |.((Re f) . x).| <= |.f.| . x
then A15: (Re f) . x = Re (f . x) by COMSEQ_3:def 3;
|.f.| . x = |.(f . x).| by A10, A12, A9, A14, VALUED_1:def 11;
hence |.((Re f) . x).| <= |.f.| . x by A15, COMPLEX1:79; :: thesis: verum
end;
Re f is A -measurable by A11;
hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A3, A4, A8, A10, A12, A9, A13, A7, COMPLEX1:44, MESFUNC6:96; :: thesis: verum