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.|
Y1: |.f.| is_integrable_on M by A1, A2, Th94;
set a = Integral M,f;
set b = (Integral M,f) / |.(Integral M,f).|;
|.((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 A4: |.((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;
A5: |.((Integral M,f) / |.(Integral M,f).|).| = |.(Integral M,f).| / |.|.(Integral M,f).|.| by COMPLEX1:153;
0 < |.(Integral M,f).| by A3, COMPLEX1:133;
then A6: |.(Integral M,f).| / |.(Integral M,f).| = 1 by XCMPLX_1:60;
A81: ((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;
reconsider b1 = (Integral M,f) / |.(Integral M,f).| as Element of COMPLEX ;
( Re (b1 * (b1 *' )) = ((Re b1) ^2 ) + ((Im b1) ^2 ) & Im (b1 * (b1 *' )) = 0 ) by COMPLEX1:126;
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 A81, COMPLEX1:154;
then ((((Integral M,f) / |.(Integral M,f).|) *' ) * (Integral M,f)) / |.(Integral M,f).| = 1 by A6, A4, A5, COMPLEX1:151;
then A8: (((Integral M,f) / |.(Integral M,f).|) *' ) * (Integral M,f) = |.(Integral M,f).| by XCMPLX_1:58;
consider A being Element of S such that
B1: ( A = dom f & f is_measurable_on A ) by A1;
B4: dom |.f.| = dom f by VALUED_1:def 11;
set h = f (#) (|.f.| " );
E1: f (#) (|.f.| " ) = f /" |.f.| ;
then E0: dom (f (#) (|.f.| " )) = (dom f) /\ (dom |.f.|) by VALUED_1:16;
G0: dom (|.f.| (#) (f (#) (|.f.| " ))) = (dom |.f.|) /\ (dom (f (#) (|.f.| " ))) by VALUED_1:def 4;
Z0: now
let x be set ; :: thesis: ( x in dom f implies f . b1 = (|.f.| (#) (f (#) (|.f.| " ))) . b1 )
assume P01: x in dom f ; :: thesis: f . b1 = (|.f.| (#) (f (#) (|.f.| " ))) . b1
then P11: (|.f.| (#) (f (#) (|.f.| " ))) . x = (|.f.| . x) * ((f (#) (|.f.| " )) . x) by G0, B4, E0, VALUED_1:def 4;
P12: |.f.| . x = |.(f . x).| by P01, B4, VALUED_1:def 11;
P03: (f (#) (|.f.| " )) . x = (f . x) / (|.f.| . x) by E1, VALUED_1:17;
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 P11, P03, P12, XCMPLX_1:88; :: thesis: verum
end;
suppose X1: 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 X1, SQUARE_1:82;
hence f . x = (|.f.| (#) (f (#) (|.f.| " ))) . x by P11, P01, B4, VALUED_1:def 11; :: thesis: verum
end;
end;
end;
then Z1: f = |.f.| (#) (f (#) (|.f.| " )) by G0, B4, E0, FUNCT_1:9;
Z2: |.f.| (#) (f (#) (|.f.| " )) is_measurable_on A by Z0, B1, G0, B4, E0, FUNCT_1:9;
E3: dom ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (|.f.| (#) (f (#) (|.f.| " )))) = dom f by G0, B4, E0, VALUED_1:def 5;
E4: dom ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))) = dom f by E0, B4, VALUED_1:def 5;
then E5: dom (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) = (dom f) /\ (dom f) by B4, VALUED_1:def 4;
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 P01: 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 ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (|.f.| (#) (f (#) (|.f.| " )))) . x = (((Integral M,f) / |.(Integral M,f).|) *' ) * ((|.f.| (#) (f (#) (|.f.| " ))) . x) by 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 P01, E3, G0, B4, E0, VALUED_1:def 4;
then Q01: ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (|.f.| (#) (f (#) (|.f.| " )))) . x = (((Integral M,f) / |.(Integral M,f).|) *' ) * (|.(f . x).| * ((f (#) (|.f.| " )) . x)) by P01, E3, B4, VALUED_1:def 11;
x in dom (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) by P01, E5, G0, B4, E0, 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 P01, E3, B4, VALUED_1:def 11;
then (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) . x = ((((Integral M,f) / |.(Integral M,f).|) *' ) * ((f (#) (|.f.| " )) . x)) * |.(f . x).| by P01, E3, E4, VALUED_1:def 5;
hence ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (|.f.| (#) (f (#) (|.f.| " )))) . x = (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) . x by Q01; :: thesis: verum
end;
then Z4: (((Integral M,f) / |.(Integral M,f).|) *' ) (#) (|.f.| (#) (f (#) (|.f.| " ))) = |.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))) by E5, E3, FUNCT_1:9;
Y2: |.f.| is_measurable_on A by B1, MES648;
(((Integral M,f) / |.(Integral M,f).|) *' ) (#) (|.f.| (#) (f (#) (|.f.| " ))) is_measurable_on A by G0, B4, E0, B1, Z2, Th21;
then F1: Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) is_measurable_on A by Z4, Def3;
F21: (((Integral M,f) / |.(Integral M,f).|) *' ) (#) (|.f.| (#) (f (#) (|.f.| " ))) is_integrable_on M by Z1, A2, Th102;
then F2: Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) is_integrable_on M by Z4, Def4;
consider R1, I1 being Real such that
Y32: ( R1 = Integral M,(Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))))) & I1 = Integral M,(Im (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))))) & Integral M,(|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) = R1 + (I1 * <i> ) ) by F21, Z4, Def5;
Re (R1 + (I1 * <i> )) = R1 by COMPLEX1:28;
then Re |.(Integral M,f).| = R1 by A8, Z1, Z4, A2, Th102, Y32;
then Y3: |.(Integral M,f).| = Integral M,(Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))))) by Y32, COMPLEX1:def 2;
F3: dom (Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))))) = dom f by E5, Def1;
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 )
assume P02: 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 P11: |.f.| . x = |.(f . x).| by F3, B4, VALUED_1:def 11;
(f (#) (|.f.| " )) . x = (f . x) / (|.f.| . x) by E1, VALUED_1:17;
then P12: |.((f (#) (|.f.| " )) . x).| = |.(f . x).| / |.|.(f . x).|.| by P11, COMPLEX1:153;
per cases ( f . x <> 0 or f . x = 0 ) ;
suppose f . x <> 0 ; :: thesis: (Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))))) . b1 <= |.f.| . b1
then 0 < |.(f . x).| by COMPLEX1:133;
then P13: |.(f . x).| / |.(f . x).| = 1 by XCMPLX_1:60;
x in dom ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))) by P02, F3, E0, 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 P14: |.(((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))) . x).| = |.(((Integral M,f) / |.(Integral M,f).|) *' ).| * |.((f (#) (|.f.| " )) . x).| by COMPLEX1:151;
(|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) . x = (|.f.| . x) * (((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))) . x) by P02, F3, B4, E5, 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 P02, F3, B4, VALUED_1:def 11;
then |.((|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) . x).| = |.|.(f . x).|.| * |.(((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))) . x).| by COMPLEX1:151;
then P16: Re ((|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) . x) <= |.(f . x).| by P14, A4, A5, A6, P13, P12, COMPLEX1:140;
Re ((|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) . x) = (Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))))) . x by P02, F3, B4, Def1;
hence (Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))))) . x <= |.f.| . x by P16, P02, F3, B4, VALUED_1:def 11; :: thesis: verum
end;
suppose f . x = 0 ; :: thesis: (Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))))) . b1 <= |.f.| . b1
then R01: ((Re (f . x)) ^2 ) + ((Im (f . x)) ^2 ) = 0 by COMPLEX1:13;
(|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) . x = (|.f.| . x) * (((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))) . x) by P02, F3, B4, E5, 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 P02, F3, B4, VALUED_1:def 11;
then |.((|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) . x).| = |.|.(f . x).|.| * |.(((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))) . x).| by COMPLEX1:151;
then P16: Re ((|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))) . x) <= |.(f . x).| by R01, 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 P02, F3, B4, Def1;
hence (Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))))) . x <= |.f.| . x by P16, P02, F3, B4, VALUED_1:def 11; :: thesis: verum
end;
end;
end;
then F5: |.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.| " ))));
consider E being Element of S such that
F6: ( E = (dom (Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " )))))) /\ (dom |.f.|) & Integral M,((Re (|.f.| (#) ((((Integral M,f) / |.(Integral M,f).|) *' ) (#) (f (#) (|.f.| " ))))) | E) <= Integral M,(|.f.| | E) ) by B1, F3, B4, F1, F2, F5, Y1, Y2, MES73;
|.f.| | E = |.f.| by B4, F3, F6, RELAT_1:97;
hence |.(Integral M,f).| <= Integral M,|.f.| by Y3, F6, F3, B4, RELAT_1:97; :: thesis: verum