:: Probability on Finite Set and Real Valued Random Variables :: by Hiroyuki Okazaki and Yasunari Shidama :: :: Received March 17, 2009 :: Copyright (c) 2009-2012 Association of Mizar Users begin theorem Th1: :: RANDOM_1:1 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,ExtREAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) holds (R_EAL a) * (M . E) <= Integral (M,(f | E)) proofend; theorem Th2: :: RANDOM_1:2 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds a <= f . x ) holds (R_EAL a) * (M . E) <= Integral (M,(f | E)) proofend; theorem Th3: :: RANDOM_1:3 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,ExtREAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) holds Integral (M,(f | E)) <= (R_EAL a) * (M . E) proofend; theorem :: RANDOM_1:4 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for E being Element of S for a being Real st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds f . x <= a ) holds Integral (M,(f | E)) <= (R_EAL a) * (M . E) proofend; Lm1: for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for M being sigma_Measure of S for F being Finite_Sep_Sequence of S for a being FinSequence of REAL for x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds Integral (M,f) = Sum x proofend; Lm2: for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of REAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) proofend; Lm3: for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL st f is_simple_func_in S holds rng f is real-bounded proofend; Lm4: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL st dom f <> {} & rng f is real-bounded & M . (dom f) < +infty & ex E being Element of S st ( E = dom f & f is_measurable_on E ) holds f is_integrable_on M proofend; Lm5: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL st f is_simple_func_in S & dom f <> {} & dom f in S & M . (dom f) < +infty holds f is_integrable_on M proofend; begin notation let E be non empty set ; synonym Trivial-SigmaField E for bool E; end; definition let E be non empty set ; :: original:Trivial-SigmaField redefine func Trivial-SigmaField E -> SigmaField of E; correctness coherence Trivial-SigmaField E is SigmaField of E; by PROB_1:40; end; Lm6: for Omega being non empty finite set for f being PartFunc of Omega,REAL ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega st ( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being Nat st k in dom F holds F . k = {((canFS (dom f)) . k)} ) & ( for n being Nat for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ) proofend; theorem :: RANDOM_1:5 for Omega being non empty finite set for f being PartFunc of Omega,REAL ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex s being FinSequence of dom f st ( dom f = union (rng F) & dom F = dom s & s is one-to-one & rng s = dom f & len s = card (dom f) & ( for k being Nat st k in dom F holds F . k = {(s . k)} ) & ( for n being Nat for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ) proofend; theorem Th6: :: RANDOM_1:6 for Omega being non empty finite set for f being PartFunc of Omega,REAL holds ( f is_simple_func_in Trivial-SigmaField Omega & dom f is Element of Trivial-SigmaField Omega ) proofend; theorem :: RANDOM_1:7 for Omega being non empty finite set for M being sigma_Measure of (Trivial-SigmaField Omega) for f being PartFunc of Omega,REAL st dom f <> {} & M . (dom f) < +infty holds f is_integrable_on M by Lm5, Th6; Lm7: for Omega being non empty set for Sigma being SigmaField of Omega for M being sigma_Measure of Sigma for A, B being set st A in Sigma & B in Sigma & A c= B & M . B < +infty holds M . A in REAL proofend; Lm8: for Omega being non empty finite set for f being PartFunc of Omega,REAL holds f * (canFS (dom f)) is FinSequence of REAL proofend; Lm9: for Omega being non empty finite set for f being PartFunc of Omega,REAL holds dom (f * (canFS (dom f))) = dom (canFS (dom f)) proofend; theorem Th8: :: RANDOM_1:8 for Omega being non empty finite set for f being PartFunc of Omega,REAL ex X being Element of Trivial-SigmaField Omega st ( dom f = X & f is_measurable_on X ) proofend; Lm10: for Omega being non empty finite set for M being sigma_Measure of (Trivial-SigmaField Omega) for f being Function of Omega,REAL st M . Omega < +infty holds ex x being FinSequence of ExtREAL st ( len x = card Omega & ( for n being Nat st n in dom x holds x . n = (R_EAL (f . ((canFS Omega) . n))) * (M . {((canFS Omega) . n)}) ) & Integral (M,f) = Sum x ) proofend; theorem Th9: :: RANDOM_1:9 for Omega being non empty finite set for M being sigma_Measure of (Trivial-SigmaField Omega) for f being Function of Omega,REAL for x being FinSequence of ExtREAL for s being FinSequence of Omega st s is one-to-one & rng s = Omega holds ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega ex a being FinSequence of REAL st ( dom f = union (rng F) & dom a = dom s & dom F = dom s & ( for k being Nat st k in dom F holds F . k = {(s . k)} ) & ( for n being Nat for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ) proofend; theorem Th10: :: RANDOM_1:10 for Omega being non empty finite set for M being sigma_Measure of (Trivial-SigmaField Omega) for f being Function of Omega,REAL for x being FinSequence of ExtREAL for s being FinSequence of Omega st M . Omega < +infty & len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds x . n = (R_EAL (f . (s . n))) * (M . {(s . n)}) ) holds Integral (M,f) = Sum x proofend; theorem :: RANDOM_1:11 for Omega being non empty finite set for M being sigma_Measure of (Trivial-SigmaField Omega) for f being Function of Omega,REAL st M . Omega < +infty holds ex x being FinSequence of ExtREAL ex s being FinSequence of Omega st ( len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds x . n = (R_EAL (f . (s . n))) * (M . {(s . n)}) ) & Integral (M,f) = Sum x ) proofend; Lm11: for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for f being Function of Omega,REAL ex F being FinSequence of REAL st ( len F = card Omega & ( for n being Nat st n in dom F holds F . n = (f . ((canFS Omega) . n)) * (P . {((canFS Omega) . n)}) ) & Integral ((P2M P),f) = Sum F ) proofend; theorem Th12: :: RANDOM_1:12 for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for f being Function of Omega,REAL for x being FinSequence of REAL for s being FinSequence of Omega st len x = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom x holds x . n = (f . (s . n)) * (P . {(s . n)}) ) holds Integral ((P2M P),f) = Sum x proofend; theorem Th13: :: RANDOM_1:13 for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for f being Function of Omega,REAL ex F being FinSequence of REAL ex s being FinSequence of Omega st ( len F = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom F holds F . n = (f . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),f) = Sum F ) proofend; theorem Th14: :: RANDOM_1:14 for E being non empty finite set for ASeq being SetSequence of E st ASeq is non-ascending holds ex N being Element of NAT st for m being Element of NAT st N <= m holds ASeq . N = ASeq . m proofend; theorem Th15: :: RANDOM_1:15 for E being non empty finite set for ASeq being SetSequence of E st ASeq is non-ascending holds ex N being Element of NAT st for m being Element of NAT st N <= m holds Intersection ASeq = ASeq . m proofend; theorem Th16: :: RANDOM_1:16 for E being non empty finite set for ASeq being SetSequence of E st ASeq is non-descending holds ex N being Element of NAT st for m being Element of NAT st N <= m holds ASeq . N = ASeq . m proofend; theorem :: RANDOM_1:17 for E being non empty finite set for ASeq being SetSequence of E st ASeq is non-descending holds ex N being Nat st for m being Nat st N <= m holds Union ASeq = ASeq . m proofend; definition let E be non empty finite set ; func Trivial-Probability E -> Probability of Trivial-SigmaField E means :Def1: :: RANDOM_1:def 1 for A being Event of E holds it . A = prob A; existence ex b1 being Probability of Trivial-SigmaField E st for A being Event of E holds b1 . A = prob A proofend; uniqueness for b1, b2 being Probability of Trivial-SigmaField E st ( for A being Event of E holds b1 . A = prob A ) & ( for A being Event of E holds b2 . A = prob A ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines Trivial-Probability RANDOM_1:def_1_:_ for E being non empty finite set for b2 being Probability of Trivial-SigmaField E holds ( b2 = Trivial-Probability E iff for A being Event of E holds b2 . A = prob A ); :: Real-Valued-Random-Variable definition let Omega be non empty set ; let Sigma be SigmaField of Omega; mode Real-Valued-Random-Variable of Sigma -> Function of Omega,REAL means :Def2: :: RANDOM_1:def 2 ex X being Element of Sigma st ( X = Omega & it is_measurable_on X ); correctness existence ex b1 being Function of Omega,REAL ex X being Element of Sigma st ( X = Omega & b1 is_measurable_on X ); proofend; end; :: deftheorem Def2 defines Real-Valued-Random-Variable RANDOM_1:def_2_:_ for Omega being non empty set for Sigma being SigmaField of Omega for b3 being Function of Omega,REAL holds ( b3 is Real-Valued-Random-Variable of Sigma iff ex X being Element of Sigma st ( X = Omega & b3 is_measurable_on X ) ); theorem Th18: :: RANDOM_1:18 for Omega being non empty set for Sigma being SigmaField of Omega for f, g being Real-Valued-Random-Variable of Sigma holds f + g is Real-Valued-Random-Variable of Sigma proofend; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let f, g be Real-Valued-Random-Variable of Sigma; :: original:+ redefine funcf + g -> Real-Valued-Random-Variable of Sigma; correctness coherence f + g is Real-Valued-Random-Variable of Sigma; by Th18; end; theorem Th19: :: RANDOM_1:19 for Omega being non empty set for Sigma being SigmaField of Omega for f, g being Real-Valued-Random-Variable of Sigma holds f - g is Real-Valued-Random-Variable of Sigma proofend; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let f, g be Real-Valued-Random-Variable of Sigma; :: original:- redefine funcf - g -> Real-Valued-Random-Variable of Sigma; correctness coherence f - g is Real-Valued-Random-Variable of Sigma; by Th19; end; theorem Th20: :: RANDOM_1:20 for Omega being non empty set for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma for r being Real holds r (#) f is Real-Valued-Random-Variable of Sigma proofend; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let f be Real-Valued-Random-Variable of Sigma; let r be Real; :: original:(#) redefine funcr (#) f -> Real-Valued-Random-Variable of Sigma; correctness coherence r (#) f is Real-Valued-Random-Variable of Sigma; by Th20; end; theorem Th21: :: RANDOM_1:21 for Omega being non empty set for f, g being PartFunc of Omega,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) proofend; theorem Th22: :: RANDOM_1:22 for Omega being non empty set for Sigma being SigmaField of Omega for f, g being Real-Valued-Random-Variable of Sigma holds f (#) g is Real-Valued-Random-Variable of Sigma proofend; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let f, g be Real-Valued-Random-Variable of Sigma; :: original:(#) redefine funcf (#) g -> Real-Valued-Random-Variable of Sigma; correctness coherence f (#) g is Real-Valued-Random-Variable of Sigma; by Th22; end; theorem Th23: :: RANDOM_1:23 for Omega being non empty set for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma for r being real number st 0 <= r & f is nonnegative holds f to_power r is Real-Valued-Random-Variable of Sigma proofend; Lm12: for X being non empty set for f being PartFunc of X,REAL holds abs f is nonnegative proofend; theorem Th24: :: RANDOM_1:24 for Omega being non empty set for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma holds abs f is Real-Valued-Random-Variable of Sigma proofend; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let f be Real-Valued-Random-Variable of Sigma; :: original:|. redefine func abs f -> Real-Valued-Random-Variable of Sigma; correctness coherence |.f.| is Real-Valued-Random-Variable of Sigma; by Th24; end; theorem :: RANDOM_1:25 for Omega being non empty set for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma for r being real number st 0 <= r holds (abs f) to_power r is Real-Valued-Random-Variable of Sigma proofend; :: Definition of the Expectations definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let f be Real-Valued-Random-Variable of Sigma; let P be Probability of Sigma; predf is_integrable_on P means :Def3: :: RANDOM_1:def 3 f is_integrable_on P2M P; end; :: deftheorem Def3 defines is_integrable_on RANDOM_1:def_3_:_ for Omega being non empty set for Sigma being SigmaField of Omega for f being Real-Valued-Random-Variable of Sigma for P being Probability of Sigma holds ( f is_integrable_on P iff f is_integrable_on P2M P ); definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let P be Probability of Sigma; let f be Real-Valued-Random-Variable of Sigma; assume A1: f is_integrable_on P ; func expect (f,P) -> Element of REAL equals :Def4: :: RANDOM_1:def 4 Integral ((P2M P),f); correctness coherence Integral ((P2M P),f) is Element of REAL ; proofend; end; :: deftheorem Def4 defines expect RANDOM_1:def_4_:_ for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for f being Real-Valued-Random-Variable of Sigma st f is_integrable_on P holds expect (f,P) = Integral ((P2M P),f); theorem Th26: :: RANDOM_1:26 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for f, g being Real-Valued-Random-Variable of Sigma st f is_integrable_on P & g is_integrable_on P holds expect ((f + g),P) = (expect (f,P)) + (expect (g,P)) proofend; theorem Th27: :: RANDOM_1:27 for Omega being non empty set for r being Real for Sigma being SigmaField of Omega for P being Probability of Sigma for f being Real-Valued-Random-Variable of Sigma st f is_integrable_on P holds expect ((r (#) f),P) = r * (expect (f,P)) proofend; theorem :: RANDOM_1:28 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for f, g being Real-Valued-Random-Variable of Sigma st f is_integrable_on P & g is_integrable_on P holds expect ((f - g),P) = (expect (f,P)) - (expect (g,P)) proofend; theorem :: RANDOM_1:29 for Omega being non empty finite set for f being Function of Omega,REAL holds f is Real-Valued-Random-Variable of Trivial-SigmaField Omega proofend; theorem Th30: :: RANDOM_1:30 for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega holds X is_integrable_on P proofend; theorem Th31: :: RANDOM_1:31 for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega for F being FinSequence of REAL for s being FinSequence of Omega st len F = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom F holds F . n = (X . (s . n)) * (P . {(s . n)}) ) holds expect (X,P) = Sum F proofend; theorem :: RANDOM_1:32 for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex F being FinSequence of REAL ex s being FinSequence of Omega st ( len F = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom F holds F . n = (X . (s . n)) * (P . {(s . n)}) ) & expect (X,P) = Sum F ) proofend; theorem Th33: :: RANDOM_1:33 for Omega being non empty finite set for P being Probability of Trivial-SigmaField Omega for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex F being FinSequence of REAL ex s being FinSequence of Omega st ( len F = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom F holds F . n = (X . (s . n)) * (P . {(s . n)}) ) & expect (X,P) = Sum F ) proofend; theorem :: RANDOM_1:34 for Omega being non empty finite set for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega for G being FinSequence of REAL for s being FinSequence of Omega st len G = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom G holds G . n = X . (s . n) ) holds expect (X,(Trivial-Probability Omega)) = (Sum G) / (card Omega) proofend; theorem :: RANDOM_1:35 for Omega being non empty finite set for X being Real-Valued-Random-Variable of Trivial-SigmaField Omega ex G being FinSequence of REAL ex s being FinSequence of Omega st ( len G = card Omega & s is one-to-one & rng s = Omega & len s = card Omega & ( for n being Nat st n in dom G holds G . n = X . (s . n) ) & expect (X,(Trivial-Probability Omega)) = (Sum G) / (card Omega) ) proofend; :: Markov's Theorem theorem :: RANDOM_1:36 for Omega being non empty set for r being Real for Sigma being SigmaField of Omega for P being Probability of Sigma for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P holds P . { t where t is Element of Omega : r <= X . t } <= (expect (X,P)) / r proofend;