:: Probability on Finite Set and Real Valued Random Variables
:: by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received March 17, 2009
:: Copyright (c) 2009 Association of Mizar Users
theorem Th1: :: RANDOM_1:1
theorem Th2: :: RANDOM_1:2
theorem Th3: :: RANDOM_1:3
theorem :: RANDOM_1:4
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
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 ) )
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 bounded
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 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
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
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 ) )
theorem :: RANDOM_1:5
theorem Th6: :: RANDOM_1:6
theorem :: RANDOM_1:7
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
Lm8:
for Omega being non empty finite set
for f being PartFunc of Omega,REAL holds f * (canFS (dom f)) is FinSequence of REAL
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))
theorem Th8: :: RANDOM_1:8
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 )
theorem Th9: :: RANDOM_1:9
theorem Th10: :: RANDOM_1:10
theorem :: RANDOM_1:11
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 )
theorem Th12: :: RANDOM_1:12
theorem Th13: :: RANDOM_1:13
theorem Th14: :: RANDOM_1:14
theorem Th15: :: RANDOM_1:15
theorem Th16: :: RANDOM_1:16
theorem :: RANDOM_1:17
Lm12:
for E being non empty finite set ex EP being Probability of Trivial-SigmaField E st
for A being Event of E holds EP . A = prob A
:: deftheorem Def1 defines Trivial-Probability RANDOM_1:def 1 :
:: deftheorem Def2 defines Real-Valued-Random-Variable RANDOM_1:def 2 :
theorem Th18: :: RANDOM_1:18
theorem Th19: :: RANDOM_1:19
theorem Th20: :: RANDOM_1:20
theorem Th21: :: RANDOM_1:21
theorem Th22: :: RANDOM_1:22
theorem Th23: :: RANDOM_1:23
Lm13:
for X being non empty set
for f being PartFunc of X,REAL holds abs f is nonnegative
theorem Th24: :: RANDOM_1:24
theorem :: RANDOM_1:25
:: deftheorem Def3 defines is_integrable_on RANDOM_1:def 3 :
:: deftheorem Def4 defines expect RANDOM_1:def 4 :
theorem Th26: :: RANDOM_1:26
theorem Th27: :: RANDOM_1:27
theorem :: RANDOM_1:28
theorem :: RANDOM_1:29
theorem Th30: :: RANDOM_1:30
theorem Th31: :: RANDOM_1:31
theorem :: RANDOM_1:32
theorem Th33: :: RANDOM_1:33
theorem :: RANDOM_1:34
theorem :: RANDOM_1:35
theorem :: RANDOM_1:36