:: 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) proofend; theorem Th2: :: RANDOM_2:2 for f, g being Function holds rng (f * g) c= rng (f | (rng g)) proofend; 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 proofend; 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 proofend; end; theorem Th3: :: RANDOM_2:3 for Omega being non empty set holds Omega --> 1 = chi (Omega,Omega) proofend; 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 proofend; 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 ) proofend; 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) ) proofend; 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; proofend; 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) proofend; 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 proofend; 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}) proofend; 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 proofend; 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) proofend; 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 proofend; 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 proofend; 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)) ) proofend; 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)) proofend; Lm6: for p being Function st dom p = Seg 1 holds p = <*(p . 1)*> proofend; 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))) proofend; 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)) proofend; 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) proofend; 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) proofend; 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 ) proofend; 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) proofend; 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 proofend; 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 ) proofend; 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) ) ) proofend; 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 proofend; 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) proofend; 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}) proofend; 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); proofend; 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 ) proofend; 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 proofend; end;