set S = [#] Sigma;
A3: 1 in REAL by XREAL_0:def 1;
(P2M P) . ([#] Sigma) <= 1 by PROB_1:35;
then A4: (P2M P) . ([#] Sigma) < +infty by XXREAL_0:2, XXREAL_0:9, A3;
set r = expect (X,P);
set E0 = Omega --> 1;
set E = Omega --> (expect (X,P));
A5: ( 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;
A6: R_EAL E0 = chi (([#] Sigma),Omega) by Th3;
A7: dom (Omega --> (expect (X,P))) = dom E0 by A5, FUNCT_2:def 1;
now :: thesis: for x being object st x in dom (Omega --> (expect (X,P))) holds
(Omega --> (expect (X,P))) . x = (expect (X,P)) * (E0 . x)
let x be object ; :: thesis: ( x in dom (Omega --> (expect (X,P))) implies (Omega --> (expect (X,P))) . x = (expect (X,P)) * (E0 . x) )
assume A8: 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 A8, FUNCOP_1:7 ;
:: thesis: verum
end;
then A9: Omega --> (expect (X,P)) = (expect (X,P)) (#) E0 by A7, 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 (([#] Sigma),Omega) is_integrable_on P2M P by A4, MESFUNC7:24;
then A10: E0 is_integrable_on P2M P by A6, MESFUNC6:def 4;
then A11: (expect (X,P)) (#) E0 is_integrable_on P2M P by MESFUNC6:102;
A12: (- 1) (#) ((expect (X,P)) (#) E0) is_integrable_on P2M P by A11, MESFUNC6:102;
A13: X is_integrable_on P2M P by A1, RANDOM_1:def 2;
then Y is_integrable_on P2M P by A9, A12, MESFUNC6:100;
then A14: Y is_integrable_on P by RANDOM_1:def 2;
(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 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 A5, VALUED_1:def 5 ;
A19: dom (((expect (X,P)) (#) E0) to_power 2) = dom ((expect (X,P)) (#) E0) by MESFUN6C:def 4
.= Omega by A5, VALUED_1:def 5 ;
A20: dom (((expect (X,P)) * (expect (X,P))) (#) E0) = Omega by A5, 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, A9
.= ((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 A10, 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 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 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