:: deftheorem Def1 defines variance RANDOM_2:def 1 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for X being Real-Valued-Random-Variable of Sigma st X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds
for b₅ being Real holds
( b₅ = variance (X,P) iff 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 & b₅ = Integral ((P2M P),((abs Y) to_power 2)) ) );