RANDOM_2: Probability Measure on Discrete Spaces and Algebra of Real Valued RandomVariables

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

begin

theorem TRNG01: :: 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 TRNG02: :: 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 Function-like non empty total quasi_total V138() V139() V140() nonnegative Real-Valued-Random-Variable of Sigma;
existence

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

proof end;

end;

theorem CHILM0: :: RANDOM_2:3

for Omega being non empty set holds Omega --> 1 = chi Omega,Omega

proof end;

theorem CHILM1: :: 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 THSQE: :: 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 THSQ: :: 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 AS: ( X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P ) ;
func variance X,P -> Element of REAL means :defvar: :: 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

proof end;

end;

:: deftheorem defvar defines variance RANDOM_2:def 1 :

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 LMXY03: :: 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;

LMXY04: 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;

LMXY05: 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;

LMXY07: 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;

LMXY08: 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;

LMXXX1: 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 LMXY092: :: 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 LMXY092A: :: 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;

THL1FS2: for p being Function st dom p = Seg 1 holds
p = <*(p . 1)*>

proof end;

theorem LMXY090A: :: 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 LMXY090: :: 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 LMXY093: :: 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 LMXY094: :: 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 RANDOM113: :: 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;

LMXY10A: 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;

LMXY10: 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;

LMXY09: 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 :DefPRD: :: 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

proof end;

uniqueness

proof end;

end;

:: deftheorem DefPRD defines Product-Probability RANDOM_2:def 2 :

theorem XX1: :: 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

proof end;

end;

:: deftheorem defines Real-Valued-Random-Variables-Set RANDOM_2:def 3 :

Th9: 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 by Th9;

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 by C0SP1:6;

end;

:: deftheorem defines R_Algebra_of_Real-Valued-Random-Variables RANDOM_2:def 4 :

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

proof end;

end;