:: 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-2021 Association of Mizar Users

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 V153() V154() V155() nonnegative [#] Sigma -measurable for Element of bool [:Omega,REAL:];

existence
ex b₁ being Real-Valued-Random-Variable of Sigma st b₁ 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) -> 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 b₁ being 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 & b₁ = Integral ((P2M P),((abs Y) to_power 2)) );
uniqueness
for b₁, b₂ being 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 & b₁ = 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 & b₂ = Integral ((P2M P),((abs Y) to_power 2)) ) holds
b₁ = b₂;

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 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)) ) );

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;

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)) by BHSP_5:def 5;

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;

reconsider jj = 1 as R_eal by XXREAL_0:def 1;

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 b₁ 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 b₁ . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) )

proof end;

uniqueness
for b₁, b₂ 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 b₁ . 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 b₂ . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) holds
b₁ = b₂

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 b₅ being Probability of Trivial-SigmaField [:Omega1,Omega2:] holds
( b₅ = 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 b₅ . 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;

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;