let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for r being Real
for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds
P . { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } <= (variance X,P) / (r to_power 2)
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for r being Real
for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds
P . { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } <= (variance X,P) / (r to_power 2)
let P be Probability of Sigma; :: thesis: for r being Real
for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds
P . { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } <= (variance X,P) / (r to_power 2)
let r be Real; :: thesis: for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds
P . { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } <= (variance X,P) / (r to_power 2)
let X be Real-Valued-Random-Variable of Sigma; :: thesis: ( 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P implies P . { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } <= (variance X,P) / (r to_power 2) )
assume AS: ( 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P ) ; :: thesis: P . { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } <= (variance X,P) / (r to_power 2)
CC1: { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } c= { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 }

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } or s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 } )
assume s in { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } ; :: thesis: s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 }
then AC1: ex ss being Element of Omega st
( s = ss & r <= |.((X . ss) - (expect X,P)).| ) ;
AC2: ( r ^2 = r to_power 2 & (abs ((X . s) - (expect X,P))) ^2 = (abs ((X . s) - (expect X,P))) to_power 2 ) by POWER:53;
r ^2 <= (abs ((X . s) - (expect X,P))) ^2 by SQUARE_1:77, AS, AC1;
hence s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 } by AC1, AC2; :: thesis: verum

end;

{ t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 } c= { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| }

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 } or s in { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } )
assume s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 } ; :: thesis: s in { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| }
then AC1: ex ss being Element of Omega st
( s = ss & r to_power 2 <= (abs ((X . ss) - (expect X,P))) to_power 2 ) ;
AC4: 0 <= abs ((X . s) - (expect X,P)) by COMPLEX1:132;
( r ^2 = r to_power 2 & (abs ((X . s) - (expect X,P))) ^2 = (abs ((X . s) - (expect X,P))) to_power 2 ) by POWER:53;
then r <= abs ((X . s) - (expect X,P)) by SQUARE_1:117, AC4, AC1;
hence s in { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } by AC1; :: thesis: verum

end;

then P1: { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } = { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 } by CC1, XBOOLE_0:def 10;
consider Y, E being Real-Valued-Random-Variable of Sigma such that
P2: ( E = Omega --> (expect X,P) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & variance X,P = Integral (P2M P),((abs Y) to_power 2) ) by defvar, AS;
reconsider Z = (abs Y) to_power 2 as Real-Valued-Random-Variable of Sigma by RANDOM_1:23;
Q3: Z is_integrable_on P by P2, RANDOM_1:def 3;
then Q4: P . { t where t is Element of Omega : r to_power 2 <= Z . t } <= (expect Z,P) / (r to_power 2) by AS, POWER:39, RANDOM_1:36;
V1: expect Z,P = variance X,P by P2, Q3, RANDOM_1:def 4;
AC5: dom X = Omega by FUNCT_2:def 1;
AC6: dom (Omega --> (expect X,P)) = Omega by FUNCOP_1:19;
AC7: dom (X - (Omega --> (expect X,P))) = (dom X) /\ (dom (Omega --> (expect X,P))) by VALUED_1:12
.= Omega by AC5, AC6 ;
then AC8: dom (abs (X - (Omega --> (expect X,P)))) = Omega by VALUED_1:def 11;
then AC9: dom ((abs (X - (Omega --> (expect X,P)))) to_power 2) = Omega by MESFUN6C:def 6;
CC2: { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 } c= { t where t is Element of Omega : r to_power 2 <= Z . t }

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 } or s in { t where t is Element of Omega : r to_power 2 <= Z . t } )
assume s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 } ; :: thesis: s in { t where t is Element of Omega : r to_power 2 <= Z . t }
then AC3: ex ss being Element of Omega st
( s = ss & r to_power 2 <= (abs ((X . ss) - (expect X,P))) to_power 2 ) ;
then Z . s = ((abs (X - (Omega --> (expect X,P)))) . s) to_power 2 by MESFUN6C:def 6, AC9, P2
.= (abs ((X - (Omega --> (expect X,P))) . s)) to_power 2 by AC8, AC3, VALUED_1:def 11
.= (abs ((X . s) - ((Omega --> (expect X,P)) . s))) to_power 2 by AC7, AC3, VALUED_1:13
.= (abs ((X . s) - (expect X,P))) to_power 2 by AC3, FUNCOP_1:13 ;
hence s in { t where t is Element of Omega : r to_power 2 <= Z . t } by AC3; :: thesis: verum

end;

{ t where t is Element of Omega : r to_power 2 <= Z . t } c= { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 }

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in { t where t is Element of Omega : r to_power 2 <= Z . t } or s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 } )
assume s in { t where t is Element of Omega : r to_power 2 <= Z . t } ; :: thesis: s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 }
then AC3: ex ss being Element of Omega st
( s = ss & r to_power 2 <= Z . ss ) ;
then Z . s = ((abs (X - (Omega --> (expect X,P)))) . s) to_power 2 by MESFUN6C:def 6, AC9, P2
.= (abs ((X - (Omega --> (expect X,P))) . s)) to_power 2 by AC8, AC3, VALUED_1:def 11
.= (abs ((X . s) - ((Omega --> (expect X,P)) . s))) to_power 2 by AC7, AC3, VALUED_1:13
.= (abs ((X . s) - (expect X,P))) to_power 2 by AC3, FUNCOP_1:13 ;
hence s in { t where t is Element of Omega : r to_power 2 <= (abs ((X . t) - (expect X,P))) to_power 2 } by AC3; :: thesis: verum

end;

hence P . { t where t is Element of Omega : r <= |.((X . t) - (expect X,P)).| } <= (variance X,P) / (r to_power 2) by V1, Q4, P1, CC2, XBOOLE_0:def 10; :: thesis: verum