:: 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 LMMarkov1: :: RANDOM_1:1
theorem LMMarkov2: :: RANDOM_1:2
theorem LMMarkov3: :: RANDOM_1:3
theorem :: RANDOM_1:4
MES43:
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
MES33:
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 ) )
Lm9C0:
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
Lm9B0:
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
Lm9A0:
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
Lm6A:
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 Lm6: :: RANDOM_1:6
theorem :: RANDOM_1:7
Lm9A2:
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
LmX1:
for Omega being non empty finite set
for f being PartFunc of Omega,REAL holds f * (canFS (dom f)) is FinSequence of REAL
LmX2:
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 Lm7: :: RANDOM_1:8
Lm9A:
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 Lm9A4: :: RANDOM_1:9
theorem Lm9A3: :: RANDOM_1:10
theorem :: RANDOM_1:11
Lm10A:
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 LMTX1: :: RANDOM_1:12
theorem LMTX2: :: RANDOM_1:13
theorem LME1: :: RANDOM_1:14
theorem LME2: :: RANDOM_1:15
theorem LME3: :: RANDOM_1:16
theorem :: RANDOM_1:17
LME10:
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 defTP defines Trivial-Probability RANDOM_1:def 1 :
:: deftheorem def1 defines Real-Valued-Random-Variable RANDOM_1:def 2 :
theorem FPG: :: RANDOM_1:18
theorem FMG: :: RANDOM_1:19
theorem RF: :: RANDOM_1:20
theorem Cor1: :: RANDOM_1:21
theorem FXG: :: RANDOM_1:22
theorem AF0: :: RANDOM_1:23
Lem02:
for X being non empty set
for f being PartFunc of X,REAL holds abs f is nonnegative
theorem AF1: :: RANDOM_1:24
theorem :: RANDOM_1:25
:: deftheorem defintf defines is_integrable_on RANDOM_1:def 3 :
:: deftheorem def2 defines expect RANDOM_1:def 4 :
theorem EXPFG: :: RANDOM_1:26
theorem EXPRF: :: RANDOM_1:27
theorem :: RANDOM_1:28
theorem :: RANDOM_1:29
theorem LMTX3: :: RANDOM_1:30
theorem LMTX4: :: RANDOM_1:31
theorem :: RANDOM_1:32
theorem LMTX5: :: RANDOM_1:33
theorem :: RANDOM_1:34
theorem :: RANDOM_1:35
theorem :: RANDOM_1:36