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 E -measurable & g is E -measurable holds
f (#) g is E -measurable
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 E -measurable & g is E -measurable holds
f (#) g is E -measurable
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 E -measurable & g is E -measurable holds
f (#) g is E -measurable
let E be Element of S; ( (dom f) /\ (dom g) = E & f is real-valued & g is real-valued & f is E -measurable & g is E -measurable implies f (#) g is E -measurable )
assume that
A1:
(dom f) /\ (dom g) = E
and
A2:
f is real-valued
and
A3:
g is real-valued
and
A4:
f is E -measurable
and
A5:
g is E -measurable
; f (#) g is E -measurable
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 Def4;
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 Def4;
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
Element of
REAL by A19, EXTREAL1:41;
(f . x) + (g . x) = c1 + c2
by SUPINF_2:1;
then
|.((f . x) + (g . x)).| = |.(c1 + c2).|
by EXTREAL1:12;
then A20:
|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).| = |.(c1 + c2).| * |.(c1 + c2).|
by EXTREAL1:1;
(|.(f + g).| |^ 2) . x = (|.(f + g).| . x) |^ (1 + 1)
by A18, Def4;
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 EXTREAL1:19
.=
|.(((f . x) + (g . x)) * ((f . x) + (g . x))).|
.=
|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|
by EXTREAL1:19
;
hence
|.((|.(f + g).| |^ 2) . x).| < +infty
by A20, XXREAL_0:9, XREAL_0:def 1;
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:10;
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
Element of
REAL by A26, EXTREAL1:41;
(f . x) + (g . x) = c1 + c2
by SUPINF_2:1;
then
|.((f . x) + (g . x)).| = |.(c1 + c2).|
by EXTREAL1:12;
then A27:
|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).| = |.(c1 + c2).| * |.(c1 + c2).|
by EXTREAL1:1;
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (1 / 4) * ((|.(f + g).| |^ 2) . x)
by A15, A6, A7, A25, MESFUNC1:def 6;
then
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (1 / 4) * ((|.(f + g).| . x) |^ (1 + 1))
by A15, A6, A25, Def4;
then A28:
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (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 = (1 / 4) * (|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|)
by A29, A28, Th9;
then A30:
((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (1 / 4) * (|.(c1 + c2).| * |.(c1 + c2).|)
by A27, EXTREAL1:1;
|.(c1 - c2).| * |.(c1 - c2).| = |.(c1 - c2).| ^2
;
then A31:
|.(c1 - c2).| * |.(c1 - c2).| = (c1 - c2) ^2
by COMPLEX1:75;
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (1 / 4) * ((|.(f - g).| |^ 2) . x)
by A10, A6, A12, A25, MESFUNC1:def 6;
then
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (1 / 4) * ((|.(f - g).| . x) |^ (1 + 1))
by A10, A6, A25, Def4;
then A32:
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (1 / 4) * (((|.(f - g).| . x) |^ 1) * (|.(f - g).| . x))
by Th10;
(f . x) - (g . x) = c1 - c2
by SUPINF_2:3;
then
|.((f . x) - (g . x)).| = |.(c1 - c2).|
by EXTREAL1:12;
then A33:
|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).| = |.(c1 - c2).| * |.(c1 - c2).|
by EXTREAL1:1;
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 = (1 / 4) * (|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|)
by A34, A32, Th9;
then A35:
((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (1 / 4) * (|.(c1 - c2).| * |.(c1 - c2).|)
by A33, EXTREAL1:1;
|.(c1 + c2).| * |.(c1 + c2).| = |.(c1 + c2).| ^2
;
then
|.(c1 + c2).| * |.(c1 + c2).| = (c1 + c2) ^2
by COMPLEX1:75;
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:3
.=
c1 * c2
.=
(f . x) * (g . x)
by EXTREAL1:1
.=
(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:5;
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
Element of
REAL by A39, EXTREAL1:41;
(f . x) - (g . x) = c1 - c2
by SUPINF_2:3;
then
|.((f . x) - (g . x)).| = |.(c1 - c2).|
by EXTREAL1:12;
then A40:
|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).| = |.(c1 - c2).| * |.(c1 - c2).|
by EXTREAL1:1;
(|.(f - g).| |^ 2) . x = (|.(f - g).| . x) |^ (1 + 1)
by A38, Def4;
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 EXTREAL1:19
.=
|.(((f . x) - (g . x)) * ((f . x) - (g . x))).|
.=
|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|
by EXTREAL1:19
;
hence
|.((|.(f - g).| |^ 2) . x).| < +infty
by A40, XXREAL_0:9, XREAL_0:def 1;
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:10;
f + g is E -measurable
by A2, A3, A4, A5, MESFUNC2:7;
then
|.(f + g).| |^ 2 is E -measurable
by A1, A14, A15, Th14;
then A43:
(jj / 4) (#) (|.(f + g).| |^ 2) is E -measurable
by A1, A15, MESFUNC5:49;
f - g is E -measurable
by A1, A2, A3, A4, A5, MESFUNC2:11, XBOOLE_1:17;
then
|.(f - g).| |^ 2 is E -measurable
by A1, A9, A10, Th14;
then
(jj / 4) (#) (|.(f - g).| |^ 2) is E -measurable
by A1, A10, MESFUNC5:49;
hence
f (#) g is E -measurable
by A1, A10, A12, A23, A42, A36, A43, MESFUNC2:11; verum