:: by Hiroyuki Okazaki and Yasunari Shidama

::

:: Received March 17, 2009

:: Copyright (c) 2009-2016 Association of Mizar Users

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

a * (M . E) <= Integral (M,(f | E))

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

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

a * (M . E) <= Integral (M,(f | E)) by Th1;

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

a * (M . E) <= Integral (M,(f | E)) by Th1;

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)) <= a * (M . E)

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)) <= 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)) <= a * (M . E) by Th3;

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)) <= a * (M . E) by Th3;

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 object 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 = (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 real-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 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

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;

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;
:: original: Trivial-SigmaField

redefine func Trivial-SigmaField E -> SigmaField of E;

correctness

coherence

Trivial-SigmaField E is SigmaField of E;

by PROB_1:40;

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

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 )

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

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 )

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;

reconsider jj = 1 as Real ;

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

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 = (f . (s . n)) * (M . {(s . n)}) ) holds

Integral (M,f) = Sum x

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 = (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 = (f . (s . n)) * (M . {(s . n)}) ) & Integral (M,f) = Sum x )

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 = (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

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 )

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 Nat st

for m being Nat st N <= m holds

ASeq . N = ASeq . m

for ASeq being SetSequence of E st ASeq is non-ascending holds

ex N being Nat st

for m being 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 Nat st

for m being Nat st N <= m holds

Intersection ASeq = ASeq . m

for ASeq being SetSequence of E st ASeq is non-ascending holds

ex N being Nat st

for m being 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 Nat st

for m being Nat st N <= m holds

ASeq . N = ASeq . m

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

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

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;

definition

let E be non empty finite set ;

ex b_{1} being Probability of Trivial-SigmaField E st

for A being Event of E holds b_{1} . A = prob A

for b_{1}, b_{2} being Probability of Trivial-SigmaField E st ( for A being Event of E holds b_{1} . A = prob A ) & ( for A being Event of E holds b_{2} . A = prob A ) holds

b_{1} = b_{2}

end;
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 for A being Event of E holds it . A = prob A;

ex b

for A being Event of E holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Trivial-Probability RANDOM_1:def 1 :

for E being non empty finite set

for b_{2} being Probability of Trivial-SigmaField E holds

( b_{2} = Trivial-Probability E iff for A being Event of E holds b_{2} . A = prob A );

for E being non empty finite set

for b

( b

:: Real-Valued-Random-Variable

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

existence

ex b_{1} being Function of Omega,REAL ex X being Element of Sigma st

( X = Omega & b_{1} is_measurable_on X );

end;
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 ex X being Element of Sigma st

( X = Omega & it is_measurable_on X );

existence

ex b

( X = Omega & b

proof 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_{3} being Function of Omega,REAL holds

( b_{3} is Real-Valued-Random-Variable of Sigma iff ex X being Element of Sigma st

( X = Omega & b_{3} is_measurable_on X ) );

for Omega being non empty set

for Sigma being SigmaField of Omega

for b

( b

( X = Omega & b

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

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

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

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

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

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

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)

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

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

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 st 0 <= r & f is nonnegative holds

f to_power r is Real-Valued-Random-Variable of Sigma

for Sigma being SigmaField of Omega

for f being Real-Valued-Random-Variable of Sigma

for r being Real st 0 <= r & f is nonnegative holds

f to_power r is Real-Valued-Random-Variable of Sigma

proof end;

Lm12: 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

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

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 st 0 <= r holds

(abs f) to_power r is Real-Valued-Random-Variable of Sigma

for Sigma being SigmaField of Omega

for f being Real-Valued-Random-Variable of Sigma

for r being Real st 0 <= r holds

(abs f) to_power r is Real-Valued-Random-Variable of Sigma

proof end;

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

end;
let Sigma be SigmaField of Omega;

let f be Real-Valued-Random-Variable of Sigma;

let P be Probability of Sigma;

:: deftheorem 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 );

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 ;

correctness

coherence

Integral ((P2M P),f) is Real;

end;
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 ;

correctness

coherence

Integral ((P2M P),f) is Real;

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

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

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 Sigma being SigmaField of Omega

for P being Probability of Sigma

for f being Real-Valued-Random-Variable of Sigma

for r being Real st f is_integrable_on P holds

expect ((r (#) f),P) = r * (expect (f,P))

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for f being Real-Valued-Random-Variable of Sigma

for r being Real 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))

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

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

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

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 )

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 )

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)

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

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;

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

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;