let X be non empty set ; :: thesis: for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for E being Element of S st (dom f) /\ (dom g) = E & f is real-valued & g is real-valued & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,ExtREAL
for E being Element of S st (dom f) /\ (dom g) = E & f is real-valued & g is real-valued & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let f, g be PartFunc of X,ExtREAL ; :: thesis: for E being Element of S st (dom f) /\ (dom g) = E & f is real-valued & g is real-valued & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let E be Element of S; :: thesis: ( (dom f) /\ (dom g) = E & f is real-valued & g is real-valued & f is_measurable_on E & g is_measurable_on E implies f (#) g is_measurable_on E )
assume A1:
( (dom f) /\ (dom g) = E & f is real-valued & g is real-valued & f is_measurable_on E & g is_measurable_on E )
; :: thesis: f (#) g is_measurable_on E
A2:
( dom (|.(f + g).| |^ 2) = dom |.(f + g).| & dom (|.(f - g).| |^ 2) = dom |.(f - g).| )
by Def5;
then A3:
( dom (|.(f + g).| |^ 2) = dom (f + g) & dom (|.(f - g).| |^ 2) = dom (f - g) )
by MESFUNC1:def 10;
then A4:
( dom (|.(f + g).| |^ 2) = (dom f) /\ (dom g) & dom (|.(f - g).| |^ 2) = (dom f) /\ (dom g) )
by A1, MESFUNC2:2;
then A5:
( dom (|.(f + g).| |^ 2) c= dom f & dom (|.(f + g).| |^ 2) c= dom g & dom (|.(f - g).| |^ 2) c= dom f & dom (|.(f - g).| |^ 2) c= dom g )
by XBOOLE_1:17;
A6:
dom (f (#) g) = (dom f) /\ (dom g)
by MESFUNC1:def 5;
A7:
( dom ((1 / 4) (#) (|.(f + g).| |^ 2)) = dom (|.(f + g).| |^ 2) & dom ((1 / 4) (#) (|.(f - g).| |^ 2)) = dom (|.(f - g).| |^ 2) )
by MESFUNC1:def 6;
A8:
for x being Element of X st x in dom (|.(f + g).| |^ 2) holds
|.((|.(f + g).| |^ 2) . x).| < +infty
proof
let x be
Element of
X;
:: thesis: ( x in dom (|.(f + g).| |^ 2) implies |.((|.(f + g).| |^ 2) . x).| < +infty )
assume A9:
x in dom (|.(f + g).| |^ 2)
;
:: thesis: |.((|.(f + g).| |^ 2) . x).| < +infty
then
(
|.(f . x).| < +infty &
|.(g . x).| < +infty )
by A1, A5, MESFUNC2:def 1;
then reconsider c1 =
f . x,
c2 =
g . x as
Real by EXTREAL2:102;
(|.(f + g).| |^ 2) . x = (|.(f + g).| . x) |^ (1 + 1)
by A9, Def5;
then A10:
(|.(f + g).| |^ 2) . x = ((|.(f + g).| . x) |^ 1) * (|.(f + g).| . x)
by Th10;
(f . x) + (g . x) = c1 + c2
by SUPINF_2:1;
then
|.((f . x) + (g . x)).| = abs (c1 + c2)
by EXTREAL2:49;
then A11:
|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).| = (abs (c1 + c2)) * (abs (c1 + c2))
by EXTREAL1:13;
(
|.(f + g).| . x = |.((f + g) . x).| &
|.((f + g) . x).| = |.((f . x) + (g . x)).| )
by A2, A3, A9, MESFUNC1:def 3, MESFUNC1:def 10;
then |.((|.(f + g).| |^ 2) . x).| =
|.(|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|).|
by A10, Th9
.=
|.|.(((f . x) + (g . x)) * ((f . x) + (g . x))).|.|
by EXTREAL2:56
.=
|.(((f . x) + (g . x)) * ((f . x) + (g . x))).|
by EXTREAL2:70
.=
|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|
by EXTREAL2:56
;
hence
|.((|.(f + g).| |^ 2) . x).| < +infty
by A11, XXREAL_0:9;
:: thesis: verum
end;
for x being Element of X st x in dom (|.(f - g).| |^ 2) holds
|.((|.(f - g).| |^ 2) . x).| < +infty
proof
let x be
Element of
X;
:: thesis: ( x in dom (|.(f - g).| |^ 2) implies |.((|.(f - g).| |^ 2) . x).| < +infty )
assume A12:
x in dom (|.(f - g).| |^ 2)
;
:: thesis: |.((|.(f - g).| |^ 2) . x).| < +infty
then
(
|.(f . x).| < +infty &
|.(g . x).| < +infty )
by A1, A5, MESFUNC2:def 1;
then reconsider c1 =
f . x,
c2 =
g . x as
Real by EXTREAL2:102;
(|.(f - g).| |^ 2) . x = (|.(f - g).| . x) |^ (1 + 1)
by A12, Def5;
then A13:
(|.(f - g).| |^ 2) . x = ((|.(f - g).| . x) |^ 1) * (|.(f - g).| . x)
by Th10;
(f . x) - (g . x) = c1 - c2
by SUPINF_2:5;
then
|.((f . x) - (g . x)).| = abs (c1 - c2)
by EXTREAL2:49;
then A14:
|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).| = (abs (c1 - c2)) * (abs (c1 - c2))
by EXTREAL1:13;
|.(f - g).| . x = |.((f - g) . x).|
by A2, A12, MESFUNC1:def 10;
then
|.(f - g).| . x = |.((f . x) - (g . x)).|
by A3, A12, MESFUNC1:def 4;
then |.((|.(f - g).| |^ 2) . x).| =
|.(|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|).|
by A13, Th9
.=
|.|.(((f . x) - (g . x)) * ((f . x) - (g . x))).|.|
by EXTREAL2:56
.=
|.(((f . x) - (g . x)) * ((f . x) - (g . x))).|
by EXTREAL2:70
.=
|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|
by EXTREAL2:56
;
hence
|.((|.(f - g).| |^ 2) . x).| < +infty
by A14, XXREAL_0:9;
:: thesis: verum
end;
then
( |.(f + g).| |^ 2 is real-valued & |.(f - g).| |^ 2 is real-valued )
by A8, MESFUNC2:def 1;
then A15:
( (1 / 4) (#) (|.(f + g).| |^ 2) is real-valued & (1 / 4) (#) (|.(f - g).| |^ 2) is real-valued )
by MESFUNC2:12;
A16:
f (#) g = ((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))
proof
A17:
dom (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) = (dom ((1 / 4) (#) (|.(f + g).| |^ 2))) /\ (dom ((1 / 4) (#) (|.(f - g).| |^ 2)))
by A15, MESFUNC2:2;
for
x being
Element of
X st
x in dom (f (#) g) holds
(f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x
proof
let x be
Element of
X;
:: thesis: ( x in dom (f (#) g) implies (f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x )
assume A18:
x in dom (f (#) g)
;
:: thesis: (f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x
then A19:
(
|.((f + g) . x).| = |.((f . x) + (g . x)).| &
|.((f - g) . x).| = |.((f . x) - (g . x)).| &
|.(f + g).| . x = |.((f + g) . x).| &
|.(f - g).| . x = |.((f - g) . x).| )
by A2, A3, A4, A6, MESFUNC1:def 3, MESFUNC1:def 4, MESFUNC1:def 10;
(
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f + g).| |^ 2) . x) &
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f - g).| |^ 2) . x) )
by A4, A6, A7, A18, MESFUNC1:def 6;
then
(
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f + g).| . x) |^ (1 + 1)) &
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f - g).| . x) |^ (1 + 1)) )
by A4, A6, A18, Def5;
then
(
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * (((|.(f + g).| . x) |^ 1) * (|.(f + g).| . x)) &
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * (((|.(f - g).| . x) |^ 1) * (|.(f - g).| . x)) )
by Th10;
then A20:
(
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * (|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|) &
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * (|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|) )
by A19, Th9;
(
|.(f . x).| < +infty &
|.(g . x).| < +infty )
by A1, A4, A5, A6, A18, MESFUNC2:def 1;
then reconsider c1 =
f . x,
c2 =
g . x as
Real by EXTREAL2:102;
(
(f . x) + (g . x) = c1 + c2 &
(f . x) - (g . x) = c1 - c2 )
by SUPINF_2:1, SUPINF_2:5;
then
(
|.((f . x) + (g . x)).| = abs (c1 + c2) &
|.((f . x) - (g . x)).| = abs (c1 - c2) )
by EXTREAL2:49;
then
(
|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).| = (abs (c1 + c2)) * (abs (c1 + c2)) &
|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).| = (abs (c1 - c2)) * (abs (c1 - c2)) )
by EXTREAL1:13;
then A21:
(
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (1 / 4) * ((abs (c1 + c2)) * (abs (c1 + c2))) &
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (1 / 4) * ((abs (c1 - c2)) * (abs (c1 - c2))) )
by A20, EXTREAL1:13;
(
(abs (c1 + c2)) * (abs (c1 + c2)) = (abs (c1 + c2)) ^2 &
(abs (c1 - c2)) * (abs (c1 - c2)) = (abs (c1 - c2)) ^2 )
;
then
(
(abs (c1 + c2)) * (abs (c1 + c2)) = (c1 + c2) ^2 &
(abs (c1 - c2)) * (abs (c1 - c2)) = (c1 - c2) ^2 )
by COMPLEX1:161;
then
(
(abs (c1 + c2)) * (abs (c1 + c2)) = ((c1 ^2 ) + ((2 * c1) * c2)) + (c2 ^2 ) &
(abs (c1 - c2)) * (abs (c1 - c2)) = ((c1 ^2 ) - ((2 * c1) * c2)) + (c2 ^2 ) )
;
then (((1 / 4) (#) (|.(f + g).| |^ 2)) . x) - (((1 / 4) (#) (|.(f - g).| |^ 2)) . x) =
((1 / 4) * (((c1 ^2 ) + ((2 * c1) * c2)) + (c2 ^2 ))) - ((1 / 4) * (((c1 ^2 ) - ((2 * c1) * c2)) + (c2 ^2 )))
by A21, SUPINF_2:5
.=
c1 * c2
.=
(f . x) * (g . x)
by EXTREAL1:13
.=
(f (#) g) . x
by A18, MESFUNC1:def 5
;
hence
(f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x
by A4, A6, A7, A17, A18, MESFUNC1:def 4;
:: thesis: verum
end;
hence
f (#) g = ((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))
by A4, A6, A7, A17, PARTFUN1:34;
:: thesis: verum
end;
( f + g is_measurable_on E & f - g is_measurable_on E )
by A1, A4, A5, MESFUNC2:7, MESFUNC2:13;
then
( |.(f + g).| |^ 2 is_measurable_on E & |.(f - g).| |^ 2 is_measurable_on E )
by A1, A3, A4, Th14;
then
( (1 / 4) (#) (|.(f + g).| |^ 2) is_measurable_on E & (1 / 4) (#) (|.(f - g).| |^ 2) is_measurable_on E )
by A1, A4, MESFUNC5:55;
hence
f (#) g is_measurable_on E
by A1, A4, A7, A15, A16, MESFUNC2:13; :: thesis: verum