:: Probability Measure on Discrete Spaces and Algebra of Real Valued Random Variables
:: by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received March 16, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

theorem Th1: :: RANDOM_2:1
for f being one-to-one Function
for A, B being Subset of (dom f) st A misses B holds
rng (f | A) misses rng (f | B)
proof end;

theorem Th2: :: RANDOM_2:2
for f, g being Function holds rng (f * g) c= rng (f | (rng g))
proof end;

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
cluster Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V146() V147() V148() nonnegative for Real-Valued-Random-Variable of Sigma;
existence
ex b1 being Real-Valued-Random-Variable of Sigma st b1 is nonnegative
proof end;
end;

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let X be Real-Valued-Random-Variable of Sigma;
cluster |.X.| -> nonnegative ;
coherence
abs X is nonnegative
proof end;
end;

theorem Th3: :: RANDOM_2:3
for Omega being non empty set holds Omega --> 1 = chi (Omega,Omega)
proof end;

theorem Th4: :: RANDOM_2:4
for Omega being non empty set
for r being Real
for Sigma being SigmaField of Omega holds Omega --> r is Real-Valued-Random-Variable of Sigma
proof end;

theorem Th5: :: RANDOM_2:5
for X being non empty set
for f being PartFunc of X,REAL holds
( f to_power 2 = (- f) to_power 2 & f to_power 2 = (abs f) to_power 2 )
proof end;

theorem Th6: :: RANDOM_2:6
for X being non empty set
for f, g being PartFunc of X,REAL holds
( (f + g) to_power 2 = ((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2) & (f - g) to_power 2 = ((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2) )
proof end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let X be Real-Valued-Random-Variable of Sigma;
assume A1: ( X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P ) ;
func variance (X,P) -> Element of REAL means :Def1: :: RANDOM_2:def 1
 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 & it = Integral ((P2M P),((abs Y) to_power 2)) );
correctness
existence
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)) );
uniqueness
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;
proof end;
end;

:: 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 b5 being Element of REAL holds
( b5 = 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 & b5 = Integral ((P2M P),((abs Y) to_power 2)) ) );

begin

theorem :: RANDOM_2:7
for Omega being 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)
proof end;

begin

theorem Th8: :: RANDOM_2:8
for Omega being non empty finite set
for f being Function of Omega,REAL
for P being Function of (bool Omega),REAL st ( for x being set st x c= Omega holds
( 0 <= P . x & P . x <= 1 ) ) & P . Omega = 1 & ( for z being finite Subset of Omega holds P . z = setopfunc (z,Omega,REAL,f,addreal) ) holds
P is Probability of Trivial-SigmaField Omega
proof end;

Lm1: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2 ex Q being Function of [:Omega1,Omega2:],REAL st
for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y})
proof end;

Lm2: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q1, Q2 being Function of [:Omega1,Omega2:],REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) holds
Q1 = Q2
proof end;

Lm3: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL ex P being Function of (bool [:Omega1,Omega2:]),REAL st
for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
proof end;

Lm4: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P1, P2 being Function of (bool [:Omega1,Omega2:]),REAL st ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P1 = P2
proof end;

Lm5: for DK, DX being non empty set
for F being Function of DX,DK
for p, q being FinSequence of DX
for fp, fq being FinSequence of DK st fp = F * p & fq = F * q holds
F * (p ^ q) = fp ^ fq
proof end;

theorem Th9: :: RANDOM_2:9
for DX being non empty set
for F being Function of DX,REAL
for Y being finite Subset of DX ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) )
proof end;

theorem Th10: :: RANDOM_2:10
for DX being non empty set
for F being Function of DX,REAL
for Y being finite Subset of DX
for p being FinSequence of DX st p is one-to-one & rng p = Y holds
setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p))
proof end;

Lm6: for p being Function st dom p = Seg 1 holds
p = <*(p . 1)*>
proof end;

theorem Th11: :: RANDOM_2:11
for DX1, DX2 being non empty set
for F1 being Function of DX1,REAL
for F2 being Function of DX2,REAL
for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for p1 being FinSequence of DX1 st p1 is one-to-one & rng p1 = Y1 holds
for p2 being FinSequence of DX2
for p3 being FinSequence of [:DX1,DX2:]
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))
proof end;

theorem Th12: :: RANDOM_2:12
for DX1, DX2 being non empty set
for F1 being Function of DX1,REAL
for F2 being Function of DX2,REAL
for G being Function of [:DX1,DX2:],REAL
for Y1 being non empty finite Subset of DX1
for Y2 being non empty finite Subset of DX2
for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds
G . (x,y) = (F1 . x) * (F2 . y) ) holds
setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal))
proof end;

theorem Th13: :: RANDOM_2:13
for DX being non empty set
for F being Function of DX,REAL
for Y being finite Subset of DX st ( for x being set st x in Y holds
0 <= F . x ) holds
0 <= setopfunc (Y,DX,REAL,F,addreal)
proof end;

theorem Th14: :: RANDOM_2:14
for DX being non empty set
for F being Function of DX,REAL
for Y1, Y2 being finite Subset of DX st Y1 c= Y2 & ( for x being set st x in Y2 holds
0 <= F . x ) holds
setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal)
proof end;

theorem Th15: :: RANDOM_2:15
for Omega being non empty finite set
for P being Probability of Trivial-SigmaField Omega
for Y being non empty finite Subset of Omega
for f being Function of Omega,REAL ex G being FinSequence of REAL ex s being FinSequence of Y st
( len G = card Y & s is one-to-one & rng s = Y & len s = card Y & ( for n being Nat st n in dom G holds
G . n = (f . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),(f | Y)) = Sum G )
proof end;

Lm7: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
proof end;

Lm8: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
P . [:Omega1,Omega2:] = 1
proof end;

Lm9: for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
proof end;

definition
let Omega1, Omega2 be non empty finite set ;
let P1 be Probability of Trivial-SigmaField Omega1;
let P2 be Probability of Trivial-SigmaField Omega2;
func Product-Probability (Omega1,Omega2,P1,P2) -> Probability of Trivial-SigmaField [:Omega1,Omega2:] means :Def2: :: RANDOM_2:def 2
 ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds it . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) );
existence
ex b1 being Probability of Trivial-SigmaField [:Omega1,Omega2:] ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) )
proof end;
uniqueness
for b1, b2 being Probability of Trivial-SigmaField [:Omega1,Omega2:] st ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) & ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Product-Probability RANDOM_2:def 2 :
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for b5 being Probability of Trivial-SigmaField [:Omega1,Omega2:] holds
( b5 = Product-Probability (Omega1,Omega2,P1,P2) iff ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b5 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) );

theorem Th16: :: RANDOM_2:16
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Y1 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 holds (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)
proof end;

theorem :: RANDOM_2:17
for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for y1, y2 being set st y1 in Omega1 & y2 in Omega2 holds
(Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})
proof end;

begin

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
func Real-Valued-Random-Variables-Set Sigma -> non empty Subset of (RAlgebra Omega) equals :: RANDOM_2:def 3
 { f where f is Real-Valued-Random-Variable of Sigma : verum } ;
correctness
coherence
{ f where f is Real-Valued-Random-Variable of Sigma : verum } is non empty Subset of (RAlgebra Omega);
proof end;
end;

:: deftheorem defines Real-Valued-Random-Variables-Set RANDOM_2:def 3 :
for Omega being non empty set
for Sigma being SigmaField of Omega holds Real-Valued-Random-Variables-Set Sigma = { f where f is Real-Valued-Random-Variable of Sigma : verum } ;

Lm10: for Omega being non empty set
for Sigma being SigmaField of Omega holds
( Real-Valued-Random-Variables-Set Sigma is additively-linearly-closed & Real-Valued-Random-Variables-Set Sigma is multiplicatively-closed )
proof end;

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
cluster Real-Valued-Random-Variables-Set Sigma -> non empty multiplicatively-closed additively-linearly-closed ;
coherence
( Real-Valued-Random-Variables-Set Sigma is additively-linearly-closed & Real-Valued-Random-Variables-Set Sigma is multiplicatively-closed ) by Lm10;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
func R_Algebra_of_Real-Valued-Random-Variables Sigma -> Algebra equals :: RANDOM_2:def 4
 AlgebraStr(# (Real-Valued-Random-Variables-Set Sigma),(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #);
coherence
AlgebraStr(# (Real-Valued-Random-Variables-Set Sigma),(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #) is Algebra by C0SP1:6;
end;

:: deftheorem defines R_Algebra_of_Real-Valued-Random-Variables RANDOM_2:def 4 :
for Omega being non empty set
for Sigma being SigmaField of Omega holds R_Algebra_of_Real-Valued-Random-Variables Sigma = AlgebraStr(# (Real-Valued-Random-Variables-Set Sigma),(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #);

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
cluster R_Algebra_of_Real-Valued-Random-Variables Sigma -> scalar-unital ;
coherence
R_Algebra_of_Real-Valued-Random-Variables Sigma is scalar-unital
proof end;
end;