:: Probability on Finite Set and Real Valued Random Variables
:: by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received March 17, 2009
:: Copyright (c) 2009-2011 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))

proof end;

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))

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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 ) )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

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 ) )

proof end;

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 ) )

proof end;

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 )

proof end;

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

proof end;

Lm8: for Omega being non empty finite set
for f being PartFunc of Omega,REAL holds f * (canFS (dom f)) is FinSequence of REAL

proof end;

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))

proof end;

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 )

proof end;

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 )

proof end;

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 ) )

proof end;

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

proof end;

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 )

proof end;

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 )

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 b₁ being Probability of Trivial-SigmaField E st
for A being Event of E holds b₁ . A = prob A by Lm12;
uniqueness
for b₁, b₂ being Probability of Trivial-SigmaField E st ( for A being Event of E holds b₁ . A = prob A ) & ( for A being Event of E holds b₂ . A = prob A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Trivial-Probability RANDOM_1:def 1 :
for E being non empty finite set
for b₂ being Probability of Trivial-SigmaField E holds
( b₂ = Trivial-Probability E iff for A being Event of E holds b₂ . A = prob A );

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 b₁ being Function of Omega,REAL ex X being Element of Sigma st
( X = Omega & b₁ is_measurable_on X );

proof end;

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 b₃ being Function of Omega,REAL holds
( b₃ is Real-Valued-Random-Variable of Sigma iff ex X being Element of Sigma st
( X = Omega & b₃ 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

proof end;

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 func f + 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

proof end;

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 func f - 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

proof end;

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 func r (#) 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)

proof end;

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

proof end;

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 func f (#) 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

proof end;

Lm13: for X being non empty set
for f being PartFunc of X,REAL holds abs f is nonnegative

proof end;

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

proof end;

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

proof end;

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;
pred f 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 ;

proof end;

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))

proof end;

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))

proof end;

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))

proof end;

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

proof end;

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

proof end;

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

proof end;

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 )

proof end;

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 )

proof end;

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)

proof end;

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) )

proof end;

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

proof end;