let X be non empty set ; 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; 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 ; 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; ( (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 that
A1:
(dom f) /\ (dom g) = E
and
A2:
f is real-valued
and
A3:
g is real-valued
and
A4:
f is_measurable_on E
and
A5:
g is_measurable_on E
; f (#) g is_measurable_on E
A6:
dom (f (#) g) = (dom f) /\ (dom g)
by MESFUNC1:def 5;
A7:
dom ((1 / 4) (#) (|.(f + g).| |^ 2)) = dom (|.(f + g).| |^ 2)
by MESFUNC1:def 6;
A8:
dom (|.(f - g).| |^ 2) = dom |.(f - g).|
by Def5;
then A9:
dom (|.(f - g).| |^ 2) = dom (f - g)
by MESFUNC1:def 10;
then A10:
dom (|.(f - g).| |^ 2) = (dom f) /\ (dom g)
by A2, MESFUNC2:2;
then A11:
dom (|.(f - g).| |^ 2) c= dom g
by XBOOLE_1:17;
A12:
dom ((1 / 4) (#) (|.(f - g).| |^ 2)) = dom (|.(f - g).| |^ 2)
by MESFUNC1:def 6;
A13:
dom (|.(f + g).| |^ 2) = dom |.(f + g).|
by Def5;
then A14:
dom (|.(f + g).| |^ 2) = dom (f + g)
by MESFUNC1:def 10;
then A15:
dom (|.(f + g).| |^ 2) = (dom f) /\ (dom g)
by A2, MESFUNC2:2;
then A16:
dom (|.(f + g).| |^ 2) c= dom g
by XBOOLE_1:17;
A17:
dom (|.(f + g).| |^ 2) c= dom f
by A15, XBOOLE_1:17;
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;
( x in dom (|.(f + g).| |^ 2) implies |.((|.(f + g).| |^ 2) . x).| < +infty )
assume A18:
x in dom (|.(f + g).| |^ 2)
;
|.((|.(f + g).| |^ 2) . x).| < +infty
then A19:
|.(g . x).| < +infty
by A3, A16, MESFUNC2:def 1;
|.(f . x).| < +infty
by A2, A17, A18, MESFUNC2:def 1;
then reconsider c1 =
f . x,
c2 =
g . x as
Real by A19, EXTREAL2:102;
(f . x) + (g . x) = c1 + c2
by SUPINF_2:1;
then
|.((f . x) + (g . x)).| = abs (c1 + c2)
by EXTREAL2:49;
then A20:
|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).| = (abs (c1 + c2)) * (abs (c1 + c2))
by EXTREAL1:13;
(|.(f + g).| |^ 2) . x = (|.(f + g).| . x) |^ (1 + 1)
by A18, Def5;
then A21:
(|.(f + g).| |^ 2) . x = ((|.(f + g).| . x) |^ 1) * (|.(f + g).| . x)
by Th10;
A22:
|.((f + g) . x).| = |.((f . x) + (g . x)).|
by A14, A18, MESFUNC1:def 3;
|.(f + g).| . x = |.((f + g) . x).|
by A13, A18, MESFUNC1:def 10;
then |.((|.(f + g).| |^ 2) . x).| =
|.(|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|).|
by A21, A22, 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 A20, XXREAL_0:9;
verum
end;
then
|.(f + g).| |^ 2 is real-valued
by MESFUNC2:def 1;
then A23:
(1 / 4) (#) (|.(f + g).| |^ 2) is real-valued
by MESFUNC2:12;
then A24:
dom (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) = (dom ((1 / 4) (#) (|.(f + g).| |^ 2))) /\ (dom ((1 / 4) (#) (|.(f - g).| |^ 2)))
by 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;
( x in dom (f (#) g) implies (f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x )
assume A25:
x in dom (f (#) g)
;
(f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x
then A26:
|.(g . x).| < +infty
by A3, A15, A16, A6, MESFUNC2:def 1;
|.(f . x).| < +infty
by A2, A15, A17, A6, A25, MESFUNC2:def 1;
then reconsider c1 =
f . x,
c2 =
g . x as
Real by A26, EXTREAL2:102;
(f . x) + (g . x) = c1 + c2
by SUPINF_2:1;
then
|.((f . x) + (g . x)).| = abs (c1 + c2)
by EXTREAL2:49;
then A27:
|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).| = (abs (c1 + c2)) * (abs (c1 + c2))
by EXTREAL1:13;
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f + g).| |^ 2) . x)
by A15, A6, A7, A25, MESFUNC1:def 6;
then
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f + g).| . x) |^ (1 + 1))
by A15, A6, A25, Def5;
then A28:
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * (((|.(f + g).| . x) |^ 1) * (|.(f + g).| . x))
by Th10;
A29:
|.(f + g).| . x = |.((f + g) . x).|
by A13, A15, A6, A25, MESFUNC1:def 10;
|.((f + g) . x).| = |.((f . x) + (g . x)).|
by A14, A15, A6, A25, MESFUNC1:def 3;
then
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * (|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|)
by A29, A28, Th9;
then A30:
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (1 / 4) * ((abs (c1 + c2)) * (abs (c1 + c2)))
by A27, EXTREAL1:13;
(abs (c1 - c2)) * (abs (c1 - c2)) = (abs (c1 - c2)) ^2
;
then A31:
(abs (c1 - c2)) * (abs (c1 - c2)) = (c1 - c2) ^2
by COMPLEX1:161;
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f - g).| |^ 2) . x)
by A10, A6, A12, A25, MESFUNC1:def 6;
then
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f - g).| . x) |^ (1 + 1))
by A10, A6, A25, Def5;
then A32:
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * (((|.(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 A33:
|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).| = (abs (c1 - c2)) * (abs (c1 - c2))
by EXTREAL1:13;
A34:
|.(f - g).| . x = |.((f - g) . x).|
by A8, A10, A6, A25, MESFUNC1:def 10;
|.((f - g) . x).| = |.((f . x) - (g . x)).|
by A9, A10, A6, A25, MESFUNC1:def 4;
then
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * (|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|)
by A34, A32, Th9;
then A35:
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (1 / 4) * ((abs (c1 - c2)) * (abs (c1 - c2)))
by A33, EXTREAL1:13;
(abs (c1 + c2)) * (abs (c1 + c2)) = (abs (c1 + c2)) ^2
;
then
(abs (c1 + c2)) * (abs (c1 + c2)) = (c1 + c2) ^2
by COMPLEX1:161;
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 A30, A35, A31, SUPINF_2:5
.=
c1 * c2
.=
(f . x) * (g . x)
by EXTREAL1:13
.=
(f (#) g) . x
by A25, MESFUNC1:def 5
;
hence
(f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x
by A15, A10, A6, A7, A12, A24, A25, MESFUNC1:def 4;
verum
end;
then A36:
f (#) g = ((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))
by A15, A10, A6, A7, A12, A24, PARTFUN1:34;
A37:
dom (|.(f - g).| |^ 2) c= dom f
by A10, XBOOLE_1:17;
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;
( x in dom (|.(f - g).| |^ 2) implies |.((|.(f - g).| |^ 2) . x).| < +infty )
assume A38:
x in dom (|.(f - g).| |^ 2)
;
|.((|.(f - g).| |^ 2) . x).| < +infty
then A39:
|.(g . x).| < +infty
by A3, A11, MESFUNC2:def 1;
|.(f . x).| < +infty
by A2, A37, A38, MESFUNC2:def 1;
then reconsider c1 =
f . x,
c2 =
g . x as
Real by A39, EXTREAL2:102;
(f . x) - (g . x) = c1 - c2
by SUPINF_2:5;
then
|.((f . x) - (g . x)).| = abs (c1 - c2)
by EXTREAL2:49;
then A40:
|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).| = (abs (c1 - c2)) * (abs (c1 - c2))
by EXTREAL1:13;
(|.(f - g).| |^ 2) . x = (|.(f - g).| . x) |^ (1 + 1)
by A38, Def5;
then A41:
(|.(f - g).| |^ 2) . x = ((|.(f - g).| . x) |^ 1) * (|.(f - g).| . x)
by Th10;
|.(f - g).| . x = |.((f - g) . x).|
by A8, A38, MESFUNC1:def 10;
then
|.(f - g).| . x = |.((f . x) - (g . x)).|
by A9, A38, MESFUNC1:def 4;
then |.((|.(f - g).| |^ 2) . x).| =
|.(|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|).|
by A41, 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 A40, XXREAL_0:9;
verum
end;
then
|.(f - g).| |^ 2 is real-valued
by MESFUNC2:def 1;
then A42:
(1 / 4) (#) (|.(f - g).| |^ 2) is real-valued
by MESFUNC2:12;
f + g is_measurable_on E
by A2, A3, A4, A5, MESFUNC2:7;
then
|.(f + g).| |^ 2 is_measurable_on E
by A1, A14, A15, Th14;
then A43:
(1 / 4) (#) (|.(f + g).| |^ 2) is_measurable_on E
by A1, A15, MESFUNC5:55;
f - g is_measurable_on E
by A1, A2, A3, A4, A5, MESFUNC2:13, XBOOLE_1:17;
then
|.(f - g).| |^ 2 is_measurable_on E
by A1, A9, A10, Th14;
then
(1 / 4) (#) (|.(f - g).| |^ 2) is_measurable_on E
by A1, A10, MESFUNC5:55;
hence
f (#) g is_measurable_on E
by A1, A10, A12, A23, A42, A36, A43, MESFUNC2:13; verum