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;
set a = Integral (M,f);
0 < |.(Integral (M,f)).| by A3, COMPLEX1:47;
then A5: |.(Integral (M,f)).| / |.(Integral (M,f)).| = 1 by XCMPLX_1:60;
set h = f (#) (|.f.| ");
set b = (Integral (M,f)) / |.(Integral (M,f)).|;
A6: dom |.f.| = dom f by VALUED_1:def 11;
|.((Integral (M,f)) / |.(Integral (M,f)).|).| * |.(((Integral (M,f)) / |.(Integral (M,f)).|) *').| = |.(((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *')).| by COMPLEX1:65;
then |.((Integral (M,f)) / |.(Integral (M,f)).|).| * |.(((Integral (M,f)) / |.(Integral (M,f)).|) *').| = |.(((Integral (M,f)) / |.(Integral (M,f)).|) * ((Integral (M,f)) / |.(Integral (M,f)).|)).| by COMPLEX1:69;
then A7: |.((Integral (M,f)) / |.(Integral (M,f)).|).| * |.(((Integral (M,f)) / |.(Integral (M,f)).|) *').| = |.((Integral (M,f)) / |.(Integral (M,f)).|).| * |.((Integral (M,f)) / |.(Integral (M,f)).|).| by COMPLEX1:65;
A8: f (#) (|.f.| ") = f /" |.f.| ;
then A9: dom (f (#) (|.f.| ")) = (dom f) /\ (dom |.f.|) by VALUED_1:16;
then A10: dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) = dom f by A6, VALUED_1:def 5;
then A11: dom (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) = (dom f) /\ (dom f) by A6, VALUED_1:def 4;
then A12: dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) = dom f by COMSEQ_3:def 3;
A13: dom (|.f.| (#) (f (#) (|.f.| "))) = (dom |.f.|) /\ (dom (f (#) (|.f.| "))) by VALUED_1:def 4;
then A14: dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) = dom f by A6, A9, VALUED_1:def 5;
now :: thesis: for x being object st x in dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) holds
((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x
let x be object ; :: thesis: ( x in dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) implies ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x )
assume A15: x in dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) ; :: thesis: ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x
then x in dom (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) by A6, A9, A13, A11, VALUED_1:def 5;
then (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = (|.f.| . x) * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by VALUED_1:def 4;
then (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = |.(f . x).| * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A14, A15, VALUED_1:def 11;
then A16: (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = ((((Integral (M,f)) / |.(Integral (M,f)).|) *') * ((f (#) (|.f.| ")) . x)) * |.(f . x).| by A14, A10, A15, VALUED_1:def 5;
((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (((Integral (M,f)) / |.(Integral (M,f)).|) *') * ((|.f.| (#) (f (#) (|.f.| "))) . x) by A15, VALUED_1:def 5;
then ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (((Integral (M,f)) / |.(Integral (M,f)).|) *') * ((|.f.| . x) * ((f (#) (|.f.| ")) . x)) by A6, A9, A13, A14, A15, VALUED_1:def 4;
then ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (((Integral (M,f)) / |.(Integral (M,f)).|) *') * (|.(f . x).| * ((f (#) (|.f.| ")) . x)) by A6, A14, A15, VALUED_1:def 11;
hence ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x by A16; :: thesis: verum
end;
then A17: (((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| "))) = |.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) by A14, A11, FUNCT_1:2;
A18: |.((Integral (M,f)) / |.(Integral (M,f)).|).| = |.(Integral (M,f)).| / |.|.(Integral (M,f)).|.| by COMPLEX1:67;
now :: thesis: for x being set st x in (dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) /\ (dom |.f.|) holds
(Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x <= |.f.| . x
let x be set ; :: thesis: ( x in (dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) /\ (dom |.f.|) implies (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . b1 <= |.f.| . b1 )
A19: (f (#) (|.f.| ")) . x = (f . x) / (|.f.| . x) by A8, VALUED_1:17;
assume A20: x in (dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) /\ (dom |.f.|) ; :: thesis: (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . b1 <= |.f.| . b1
then |.f.| . x = |.(f . x).| by A6, A12, VALUED_1:def 11;
then A21: |.((f (#) (|.f.| ")) . x).| = |.(f . x).| / |.|.(f . x).|.| by A19, COMPLEX1:67;
per cases ( f . x <> 0 or f . x = 0 ) ;
suppose A22: f . x <> 0 ; :: thesis: (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . b1 <= |.f.| . b1
A23: Re ((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x) = (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x by A6, A12, A20, COMSEQ_3:def 3;
(|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = (|.f.| . x) * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A11, A12, A20, VALUED_1:def 4;
then (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = |.(f . x).| * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A12, A20, VALUED_1:def 11;
then A24: |.((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x).| = |.|.(f . x).|.| * |.(((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x).| by COMPLEX1:65;
x in dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) by A9, A12, A20, VALUED_1:def 5;
then ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x = (((Integral (M,f)) / |.(Integral (M,f)).|) *') * ((f (#) (|.f.| ")) . x) by VALUED_1:def 5;
then A25: |.(((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x).| = |.(((Integral (M,f)) / |.(Integral (M,f)).|) *').| * |.((f (#) (|.f.| ")) . x).| by COMPLEX1:65;
0 < |.(f . x).| by A22, COMPLEX1:47;
then |.(f . x).| / |.(f . x).| = 1 by XCMPLX_1:60;
then Re ((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x) <= |.(f . x).| by A7, A18, A5, A21, A25, A24, COMPLEX1:54;
hence (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x <= |.f.| . x by A6, A12, A20, A23, VALUED_1:def 11; :: thesis: verum
end;
suppose A26: f . x = 0 ; :: thesis: (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . b1 <= |.f.| . b1
(|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = (|.f.| . x) * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A11, A12, A20, VALUED_1:def 4;
then (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = |.(f . x).| * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A12, A20, VALUED_1:def 11;
then A27: |.((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x).| = |.|.(f . x).|.| * |.(((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x).| by COMPLEX1:65;
((Re (f . x)) ^2) + ((Im (f . x)) ^2) = 0 by A26, COMPLEX1:5;
then A28: Re ((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x) <= |.(f . x).| by A27, COMPLEX1:54, SQUARE_1:17;
Re ((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x) = (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x by A6, A12, A20, COMSEQ_3:def 3;
hence (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x <= |.f.| . x by A6, A12, A20, A28, VALUED_1:def 11; :: thesis: verum
end;
end;
end;
then A29: |.f.| - (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) is nonnegative by MESFUNC6:58;
set F = Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))));
reconsider b1 = (Integral (M,f)) / |.(Integral (M,f)).| as Element of COMPLEX by XCMPLX_0:def 2;
A30: Re (b1 * (b1 *')) = ((Re b1) ^2) + ((Im b1) ^2) by COMPLEX1:40;
consider A being Element of S such that
A31: A = dom f and
A32: f is A -measurable by A1;
A33: |.f.| is A -measurable by A31, A32, Th30;
A34: now :: thesis: for x being object st x in dom f holds
f . x = (|.f.| (#) (f (#) (|.f.| "))) . x
let x be object ; :: thesis: ( x in dom f implies f . b1 = (|.f.| (#) (f (#) (|.f.| "))) . b1 )
A35: (f (#) (|.f.| ")) . x = (f . x) / (|.f.| . x) by A8, VALUED_1:17;
assume A36: x in dom f ; :: thesis: f . b1 = (|.f.| (#) (f (#) (|.f.| "))) . b1
then A37: |.f.| . x = |.(f . x).| by A6, VALUED_1:def 11;
A38: (|.f.| (#) (f (#) (|.f.| "))) . x = (|.f.| . x) * ((f (#) (|.f.| ")) . x) by A6, A9, A13, A36, VALUED_1:def 4;
per cases ( f . x <> 0 or f . x = 0 ) ;
suppose f . x <> 0 ; :: thesis: f . b1 = (|.f.| (#) (f (#) (|.f.| "))) . b1
then 0 < |.(f . x).| by COMPLEX1:47;
hence f . x = (|.f.| (#) (f (#) (|.f.| "))) . x by A38, A37, A35, XCMPLX_1:87; :: thesis: verum
end;
suppose A39: f . x = 0 ; :: thesis: f . b1 = (|.f.| (#) (f (#) (|.f.| "))) . b1
then ((Re (f . x)) ^2) + ((Im (f . x)) ^2) = 0 by COMPLEX1:5;
then f . x = ((f (#) (|.f.| ")) . x) * |.(f . x).| by A39, SQUARE_1:17;
hence f . x = (|.f.| (#) (f (#) (|.f.| "))) . x by A6, A36, A38, VALUED_1:def 11; :: thesis: verum
end;
end;
end;
then A40: f = |.f.| (#) (f (#) (|.f.| ")) by A6, A9, A13, FUNCT_1:2;
then A41: (((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| "))) is_integrable_on M by A2, Th40;
then consider R1, I1 being Real such that
A42: R1 = Integral (M,(Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) and
I1 = Integral (M,(Im (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) and
A43: Integral (M,(|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) = R1 + (I1 * <i>) by A17, Def3;
A44: Im (b1 * (b1 *')) = 0 by COMPLEX1:40;
reconsider aa = |.(Integral (M,f)).| as Element of REAL by XREAL_0:def 1;
((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *') = (Re (((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *'))) + ((Im (((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *'))) * <i>) by COMPLEX1:13;
then ((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *') = |.(((Integral (M,f)) / |.(Integral (M,f)).|) * ((Integral (M,f)) / |.(Integral (M,f)).|)).| by A30, A44, COMPLEX1:68;
then ((((Integral (M,f)) / |.(Integral (M,f)).|) *') * (Integral (M,f))) / |.(Integral (M,f)).| = 1 by A7, A18, A5, COMPLEX1:65;
then A45: (((Integral (M,f)) / |.(Integral (M,f)).|) *') * (Integral (M,f)) = |.(Integral (M,f)).| by XCMPLX_1:58;
Re (R1 + (I1 * <i>)) = R1 by COMPLEX1:12;
then Re |.aa.| = R1 by A2, A45, A40, A17, A43, Th40;
then A46: |.aa.| = Integral (M,(Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) by A42, COMPLEX1:def 1;
|.f.| (#) (f (#) (|.f.| ")) is A -measurable by A32, A6, A9, A13, A34, FUNCT_1:2;
then (((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| "))) is A -measurable by A31, A6, A9, A13, Th17;
then A47: Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) is A -measurable by A17;
Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) is_integrable_on M by A17, A41;
then consider E being Element of S such that
A48: E = (dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) /\ (dom |.f.|) and
A49: Integral (M,((Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) | E)) <= Integral (M,(|.f.| | E)) by A4, A31, A6, A33, A47, A12, A29, Th42;
thus |.(Integral (M,f)).| <= Integral (M,|.f.|) by A6, A46, A12, A48, A49; :: thesis: verum