let Omega be non empty set ; 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; 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; 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; 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; ( 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 A1:
( 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P )
; P . { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } <= (variance (X,P)) / (r to_power 2)
A2:
{ 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 <= |.((X . t) - (expect (X,P))).| to_power 2 }
proof
let s be
object ;
TARSKI:def 3 ( 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 <= |.((X . t) - (expect (X,P))).| to_power 2 } )
assume
s in { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| }
;
s in { t where t is Element of Omega : r to_power 2 <= |.((X . t) - (expect (X,P))).| to_power 2 }
then A3:
ex
ss being
Element of
Omega st
(
s = ss &
r <= |.((X . ss) - (expect (X,P))).| )
;
A4:
(
r ^2 = r to_power 2 &
|.((X . s) - (expect (X,P))).| ^2 = |.((X . s) - (expect (X,P))).| to_power 2 )
by POWER:46;
r ^2 <= |.((X . s) - (expect (X,P))).| ^2
by A1, A3, SQUARE_1:15;
hence
s in { t where t is Element of Omega : r to_power 2 <= |.((X . t) - (expect (X,P))).| to_power 2 }
by A3, A4;
verum
end;
{ t where t is Element of Omega : r to_power 2 <= |.((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
object ;
TARSKI:def 3 ( not s in { t where t is Element of Omega : r to_power 2 <= |.((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 <= |.((X . t) - (expect (X,P))).| to_power 2 }
;
s in { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| }
then A5:
ex
ss being
Element of
Omega st
(
s = ss &
r to_power 2
<= |.((X . ss) - (expect (X,P))).| to_power 2 )
;
A6:
0 <= |.((X . s) - (expect (X,P))).|
by COMPLEX1:46;
(
r ^2 = r to_power 2 &
|.((X . s) - (expect (X,P))).| ^2 = |.((X . s) - (expect (X,P))).| to_power 2 )
by POWER:46;
then
r <= |.((X . s) - (expect (X,P))).|
by A6, A5, SQUARE_1:47;
hence
s in { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| }
by A5;
verum
end;
then A7:
{ t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } = { t where t is Element of Omega : r to_power 2 <= |.((X . t) - (expect (X,P))).| to_power 2 }
by A2, XBOOLE_0:def 10;
consider Y, E being Real-Valued-Random-Variable of Sigma such that
A8:
( 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 Def1, A1;
reconsider Z = (abs Y) to_power 2 as Real-Valued-Random-Variable of Sigma by RANDOM_1:23;
A9:
Z is_integrable_on P
by A8, RANDOM_1:def 2;
then A10:
P . { t where t is Element of Omega : r to_power 2 <= Z . t } <= (expect (Z,P)) / (r to_power 2)
by A1, POWER:34, RANDOM_1:36;
A11:
expect (Z,P) = variance (X,P)
by A8, A9, RANDOM_1:def 3;
A12:
dom X = Omega
by FUNCT_2:def 1;
A13:
dom (Omega --> (expect (X,P))) = Omega
by FUNCOP_1:13;
A14: dom (X - (Omega --> (expect (X,P)))) =
(dom X) /\ (dom (Omega --> (expect (X,P))))
by VALUED_1:12
.=
Omega
by A12, A13
;
then A15:
dom |.(X - (Omega --> (expect (X,P)))).| = Omega
by VALUED_1:def 11;
then A16:
dom (|.(X - (Omega --> (expect (X,P)))).| to_power 2) = Omega
by MESFUN6C:def 4;
A17:
{ t where t is Element of Omega : r to_power 2 <= |.((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
object ;
TARSKI:def 3 ( not s in { t where t is Element of Omega : r to_power 2 <= |.((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 <= |.((X . t) - (expect (X,P))).| to_power 2 }
;
s in { t where t is Element of Omega : r to_power 2 <= Z . t }
then A18:
ex
ss being
Element of
Omega st
(
s = ss &
r to_power 2
<= |.((X . ss) - (expect (X,P))).| to_power 2 )
;
then Z . s =
(|.(X - (Omega --> (expect (X,P)))).| . s) to_power 2
by A16, A8, MESFUN6C:def 4
.=
|.((X - (Omega --> (expect (X,P)))) . s).| to_power 2
by A15, A18, VALUED_1:def 11
.=
|.((X . s) - ((Omega --> (expect (X,P))) . s)).| to_power 2
by A14, A18, VALUED_1:13
.=
|.((X . s) - (expect (X,P))).| to_power 2
by A18, FUNCOP_1:7
;
hence
s in { t where t is Element of Omega : r to_power 2 <= Z . t }
by A18;
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 <= |.((X . t) - (expect (X,P))).| to_power 2 }
proof
let s be
object ;
TARSKI:def 3 ( 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 <= |.((X . t) - (expect (X,P))).| to_power 2 } )
assume
s in { t where t is Element of Omega : r to_power 2 <= Z . t }
;
s in { t where t is Element of Omega : r to_power 2 <= |.((X . t) - (expect (X,P))).| to_power 2 }
then A19:
ex
ss being
Element of
Omega st
(
s = ss &
r to_power 2
<= Z . ss )
;
then Z . s =
(|.(X - (Omega --> (expect (X,P)))).| . s) to_power 2
by A16, A8, MESFUN6C:def 4
.=
|.((X - (Omega --> (expect (X,P)))) . s).| to_power 2
by A15, A19, VALUED_1:def 11
.=
|.((X . s) - ((Omega --> (expect (X,P))) . s)).| to_power 2
by A14, A19, VALUED_1:13
.=
|.((X . s) - (expect (X,P))).| to_power 2
by A19, FUNCOP_1:7
;
hence
s in { t where t is Element of Omega : r to_power 2 <= |.((X . t) - (expect (X,P))).| to_power 2 }
by A19;
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 A11, A10, A7, A17, XBOOLE_0:def 10; verum