consider S being Element of Sigma such that
A0: ( S = Omega & X is_measurable_on S ) by RANDOM_1:def 2;
(P2M P) . S <= 1 by PROB_1:71;
then A1: (P2M P) . S < +infty by XXREAL_0:9, XXREAL_0:2;
set r = expect (X,P);
set E0 = Omega --> 1;
set E = Omega --> (expect (X,P));
A100: ( dom (Omega --> 1) = Omega & rng (Omega --> 1) c= {1} ) by FUNCOP_1:19;
reconsider E0 = Omega --> 1 as Real-Valued-Random-Variable of Sigma by CHILM1;
K21: R_EAL E0 = chi (S,Omega) by A0, CHILM0;
K221: dom (Omega --> (expect (X,P))) = dom E0 by A100, 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 AS1: 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:13
.= (expect (X,P)) * (E0 . x) by AS1, FUNCOP_1:13 ;
:: thesis: verum
end;
then K0: Omega --> (expect (X,P)) = (expect (X,P)) (#) E0 by K221, VALUED_1:def 5;
reconsider E = Omega --> (expect (X,P)) as Real-Valued-Random-Variable of Sigma by CHILM1;
set Y = X - E;
reconsider Y = X - E as Real-Valued-Random-Variable of Sigma ;
chi (S,Omega) is_integrable_on P2M P by MESFUNC7:24, A1;
then K2: E0 is_integrable_on P2M P by K21, MESFUNC6:def 9;
then KK2: (expect (X,P)) (#) E0 is_integrable_on P2M P by MESFUNC6:102;
KK5: - 1 is Real by XREAL_0:def 1;
then KK3: (- 1) (#) ((expect (X,P)) (#) E0) is_integrable_on P2M P by KK2, MESFUNC6:102;
KK4: X is_integrable_on P2M P by AS, RANDOM_1:def 3;
then Y is_integrable_on P2M P by K0, KK3, MESFUNC6:100;
then KK: Y is_integrable_on P by RANDOM_1:def 3;
(2 * (expect (X,P))) (#) X is_integrable_on P2M P by KK4, MESFUNC6:102;
then (- 1) (#) ((2 * (expect (X,P))) (#) X) is_integrable_on P2M P by KK5, MESFUNC6:102;
then K11: ((abs X) to_power 2) - ((2 * (expect (X,P))) (#) X) is_integrable_on P2M P by AS, MESFUNC6:100;
DK0: ((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
DK0L1: dom (X to_power 2) = dom X by MESFUN6C:def 6;
DK0L2: 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 A100, VALUED_1:def 5 ;
DK0L22: dom (((expect (X,P)) (#) E0) to_power 2) = dom ((expect (X,P)) (#) E0) by MESFUN6C:def 6
.= Omega by A100, VALUED_1:def 5 ;
DK0L3: dom (((expect (X,P)) * (expect (X,P))) (#) E0) = Omega by A100, VALUED_1:def 5;
DK0L33: dom ((2 * (expect (X,P))) (#) X) = dom X by VALUED_1:def 5;
DK0L4: dom ((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) = (dom X) /\ (Omega /\ (dom X)) by DK0L1, DK0L2, VALUED_1:12
.= ((dom X) /\ (dom X)) /\ Omega by XBOOLE_1:16
.= (dom X) /\ Omega ;
DK0L44: 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 DK0L1, DK0L33 ;
DK0L5: 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 XBOOLE_1:16, DK0L22, DK0L4
.= (dom X) /\ Omega ;
then DK0L6: 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 DK0L3, DK0L44, 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 CAS: 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 CAS2: ( x in dom X & x in Omega ) by XBOOLE_0:def 4, DK0L5;
DK: (((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 VALUED_1:def 1, CAS
.= (((X to_power 2) . x) - ((2 (#) (((expect (X,P)) (#) E0) (#) X)) . x)) + ((((expect (X,P)) (#) E0) to_power 2) . x) by VALUED_1:13, DK0L4, DK0L5, CAS
.= (((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:13
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + ((((expect (X,P)) (#) E0) . x) to_power 2) by MESFUN6C:def 6, DK0L22
.= (((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:13
.= (((X to_power 2) . x) - ((2 * (expect (X,P))) * (X . x))) + ((expect (X,P)) ^2) by POWER:53
.= (((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 VALUED_1:def 1, CAS, DK0L6
.= (((X to_power 2) . x) - (((2 * (expect (X,P))) (#) X) . x)) + ((((expect (X,P)) * (expect (X,P))) (#) E0) . x) by DK0L44, CAS2, 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:13
.= (((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 DK; :: 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 PARTFUN1:34, DK0L6; :: thesis: verum
end;
K5: (abs Y) to_power 2 = (X - ((expect (X,P)) (#) E0)) to_power 2 by THSQE, K0
.= ((X to_power 2) - (2 (#) (((expect (X,P)) (#) E0) (#) X))) + (((expect (X,P)) (#) E0) to_power 2) by THSQ
.= (((abs X) to_power 2) - ((2 * (expect (X,P))) (#) X)) + (((expect (X,P)) * (expect (X,P))) (#) E0) by THSQE, DK0 ;
K17: ((expect (X,P)) * (expect (X,P))) (#) E0 is_integrable_on P2M P by K2, MESFUNC6:102;
then (abs Y) to_power 2 is_integrable_on P2M P by K11, K5, 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 K17, K11, K5, MESFUNC6:100, KK; :: thesis: verum