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_measurable_on A ) & 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_measurable_on A ) & 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_measurable_on A ) & 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_measurable_on A ) & 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_measurable_on A ) 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:133;
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:151;
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:155;
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:151;
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 Def1;
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
let x be set ; :: 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:9;
A18: |.((Integral M,f) / |.(Integral M,f).|).| = |.(Integral M,f).| / |.|.(Integral M,f).|.| by COMPLEX1:153;
now
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:153;
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, Def1;
(|.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:151;
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:151;
0 < |.(f . x).| by A22, COMPLEX1:133;
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:140;
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:151;
((Re (f . x)) ^2 ) + ((Im (f . x)) ^2 ) = 0 by A26, COMPLEX1:13;
then A28: Re ((|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) . x) <= |.(f . x).| by A27, COMPLEX1:140, SQUARE_1:82;
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, Def1;
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 ;
A30: Re (b1 * (b1 *' )) = ((Re b1) ^2 ) + ((Im b1) ^2 ) by COMPLEX1:126;
consider A being Element of S such that
A31: A = dom f and
A32: f is_measurable_on A by A1;
A33: |.f.| is_measurable_on A by A31, A32, Th30;
A34: now
let x be set ; :: 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:133;
hence f . x = (|.f.| (#) (f (#) (|.f.| " ))) . x by A38, A37, A35, XCMPLX_1:88; :: 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:13;
then f . x = ((f (#) (|.f.| " )) . x) * |.(f . x).| by A39, SQUARE_1:82;
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:9;
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, Def5;
A44: Im (b1 * (b1 *' )) = 0 by COMPLEX1:126;
((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:29;
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:154;
then ((((Integral M,f) / |.(Integral M,f).|) *' ) * (Integral M,f)) / |.(Integral M,f).| = 1 by A7, A18, A5, COMPLEX1:151;
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:28;
then Re |.(Integral M,f).| = R1 by A2, A45, A40, A17, A43, Th40;
then A46: |.(Integral M,f).| = Integral M,(Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))))) by A42, COMPLEX1:def 2;
|.f.| (#) (f (#) (|.f.| " )) is_measurable_on A by A32, A6, A9, A13, A34, FUNCT_1:9;
then (((Integral M,f) / |.(Integral M,f).|) *' ) (#) (|.f.| (#) (f (#) (|.f.| " ))) is_measurable_on A by A31, A6, A9, A13, Th17;
then A47: Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) is_measurable_on A by A17, Def3;
Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) is_integrable_on M by A17, A41, Def4;
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;
|.f.| | E = |.f.| by A6, A12, A48, RELAT_1:97;
hence |.(Integral M,f).| <= Integral M,|.f.| by A6, A46, A12, A48, A49, RELAT_1:97; :: thesis: verum