consider S being Element of Sigma such that
A2: ( S = Omega & X is_measurable_on S ) by RANDOM_1:def 2;
(P2M P) . S <= 1 by PROB_1:35;
then A3: (P2M P) . S < +infty by XXREAL_0:2, XXREAL_0:9;
set r = expect (X,P);
set E0 = Omega --> 1;
set E = Omega --> (expect (X,P));
A4: ( dom (Omega --> 1) = Omega & rng (Omega --> 1) c= {1} ) by FUNCOP_1:13;
reconsider E0 = Omega --> 1 as Real-Valued-Random-Variable of Sigma by Th4;
A5: R_EAL E0 = chi (S,Omega) by A2, Th3;
A6: dom (Omega --> (expect (X,P))) = dom E0 by A4, FUNCT_2:def 1;
now
let x be set ; :: thesis: ( x in dom (Omega --> (expect (X,P))) implies (Omega --> (expect (X,P))) . x = (expect (X,P)) * (E0 . x) )
assume A7: x in dom (Omega --> (expect (X,P))) ; :: thesis: (Omega --> (expect (X,P))) . x = (expect (X,P)) * (E0 . x)
hence (Omega --> (expect (X,P))) . x = (expect (X,P)) * 1 by FUNCOP_1:7
.= (expect (X,P)) * (E0 . x) by A7, FUNCOP_1:7 ;
:: thesis: verum
end;
then A8: Omega --> (expect (X,P)) = (expect (X,P)) (#) E0 by A6, VALUED_1:def 5;
reconsider E = Omega --> (expect (X,P)) as Real-Valued-Random-Variable of Sigma by Th4;
set Y = X - E;
reconsider Y = X - E as Real-Valued-Random-Variable of Sigma ;
chi (S,Omega) is_integrable_on P2M P by A3, MESFUNC7:24;
then A9: E0 is_integrable_on P2M P by A5, MESFUNC6:def 4;
then A10: (expect (X,P)) (#) E0 is_integrable_on P2M P by MESFUNC6:102;
A11: - 1 is Real by XREAL_0:def 1;
then A12: (- 1) (#) ((expect (X,P)) (#) E0) is_integrable_on P2M P by A10, MESFUNC6:102;
A13: X is_integrable_on P2M P by A1, RANDOM_1:def 3;
then Y is_integrable_on P2M P by A8, A12, MESFUNC6:100;
then A14: Y is_integrable_on P by RANDOM_1:def 3;
(2 * (expect (X,P))) (#) X is_integrable_on P2M P by A13, MESFUNC6:102;
then (- 1) (#) ((2 * (expect (X,P))) (#) X) is_integrable_on P2M P by A11, MESFUNC6:102;
then A15: ((abs X) to_power 2) - ((2 * (expect (X,P))) (#) X) is_integrable_on P2M P by A1, MESFUNC6:100;
A16: ((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2) = ((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)
proof
A17: dom (X to_power 2) = dom X by MESFUN6C:def 4;
A18: dom (2 (#) (((expect (X,P)) (#) E0) (#) X)) = dom (((expect (X,P)) (#) E0) (#) X) by VALUED_1:def 5
.= (dom ((expect (X,P)) (#) E0)) /\ (dom X) by VALUED_1:def 4
.= Omega /\ (dom X) by A4, VALUED_1:def 5 ;
A19: dom (((expect (X,P)) (#) E0) to_power 2) = dom ((expect (X,P)) (#) E0) by MESFUN6C:def 4
.= Omega by A4, VALUED_1:def 5 ;
A20: dom (((expect (X,P)) * (expect (X,P))) (#) E0) = Omega by A4, VALUED_1:def 5;
A21: dom ((2 * (expect (X,P))) (#) X) = dom X by VALUED_1:def 5;
A22: dom ((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) = (dom X) /\ (Omega /\ (dom X)) by A17, A18, VALUED_1:12
.= ((dom X) /\ (dom X)) /\ Omega by XBOOLE_1:16
.= (dom X) /\ Omega ;
A23: dom ((X to_power 2) - ((2 * (expect (X,P))) (#) X)) = (dom (X to_power 2)) /\ (dom ((2 * (expect (X,P))) (#) X)) by VALUED_1:12
.= dom X by A17, A21 ;
A24: dom (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) = (dom ((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X)))) /\ (dom (((expect (X,P)) (#) E0) to_power 2)) by VALUED_1:def 1
.= (dom X) /\ (Omega /\ Omega) by A19, A22, XBOOLE_1:16
.= (dom X) /\ Omega ;
then A25: dom (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) = dom (((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)) by A20, A23, VALUED_1:def 1;
for x being Element of Omega st x in dom (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) holds
(((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) . x = (((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)) . x
proof
let x be Element of Omega; :: thesis: ( x in dom (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) implies (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) . x = (((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)) . x )
assume A26: x in dom (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) ; :: thesis: (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) . x = (((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)) . x
then A27: ( x in dom X & x in Omega ) by A24, XBOOLE_0:def 4;
A28: (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) . x = (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) . x) + ((((expect (X,P)) (#) E0) to_power 2) . x) by A26, VALUED_1:def 1
.= (((X to_power 2) . x) - ((2 (#) (((expect (X,P)) (#) E0) (#) X)) . x)) + ((((expect (X,P)) (#) E0) to_power 2) . x) by A22, A24, A26, VALUED_1:13
.= (((X to_power 2) . x) - (2 * ((((expect (X,P)) (#) E0) (#) X) . x))) + ((((expect (X,P)) (#) E0) to_power 2) . x) by VALUED_1:6
.= (((X to_power 2) . x) - (2 * ((((expect (X,P)) (#) E0) . x) * (X . x)))) + ((((expect (X,P)) (#) E0) to_power 2) . x) by VALUED_1:5
.= (((X to_power 2) . x) - (2 * (((expect (X,P)) * (E0 . x)) * (X . x)))) + ((((expect (X,P)) (#) E0) to_power 2) . x) by VALUED_1:6
.= (((X to_power 2) . x) - (2 * (((expect (X,P)) * 1) * (X . x)))) + ((((expect (X,P)) (#) E0) to_power 2) . x) by FUNCOP_1:7
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + ((((expect (X,P)) (#) E0) . x) to_power 2) by A19, MESFUN6C:def 4
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + (((expect (X,P)) * (E0 . x)) to_power 2) by VALUED_1:6
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + (((expect (X,P)) * 1) to_power 2) by FUNCOP_1:7
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + ((expect (X,P)) ^2) by POWER:46
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + ((expect (X,P)) * (expect (X,P))) ;
(((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)) . x = (((X to_power 2) - ((2 * (expect (X,P))) (#) X)) . x) + ((((expect (X,P)) * (expect (X,P))) (#) E0) . x) by A26, A25, VALUED_1:def 1
.= (((X to_power 2) . x) - (((2 * (expect (X,P))) (#) X) . x)) + ((((expect (X,P)) * (expect (X,P))) (#) E0) . x) by A23, A27, VALUED_1:13
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + ((((expect (X,P)) * (expect (X,P))) (#) E0) . x) by VALUED_1:6
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + (((expect (X,P)) * (expect (X,P))) * (E0 . x)) by VALUED_1:6
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + (((expect (X,P)) * (expect (X,P))) * 1) by FUNCOP_1:7
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + ((expect (X,P)) * (expect (X,P))) ;
hence (((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2)) . x = (((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0)) . x by A28; :: thesis: verum
end;
hence ((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2) = ((X to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0) by A25, PARTFUN1:5; :: thesis: verum
end;
A29: (abs Y) to_power 2 = (X - ((expect (X,P)) (#) E0)) to_power 2 by Th5, A8
.= ((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2) by Th6
.= (((abs X) to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0) by Th5, A16 ;
A30: ((expect (X,P)) * (expect (X,P))) (#) E0 is_integrable_on P2M P by A9, MESFUNC6:102;
then (abs Y) to_power 2 is_integrable_on P2M P by A15, A29, MESFUNC6:100;
then ( -infty < Integral ((P2M P),((abs Y) to_power 2)) & Integral ((P2M P),((abs Y) to_power 2)) < +infty ) by MESFUNC6:90;
then Integral ((P2M P),((abs Y) to_power 2)) is Element of REAL by XXREAL_0:14;
hence ( ex b1 being Element of REAL ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b1 = Integral ((P2M P),((abs Y) to_power 2)) ) & ( for b1, b2 being Element of REAL st ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b1 = Integral ((P2M P),((abs Y) to_power 2)) ) & ex Y, E being Real-Valued-Random-Variable of Sigma st
( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b2 = Integral ((P2M P),((abs Y) to_power 2)) ) holds
b1 = b2 ) ) by A30, A15, A29, A14, MESFUNC6:100; :: thesis: verum