:: by Hiroyuki Okazaki and Yasunari Shidama

::

:: Received March 16, 2010

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

theorem Th1: :: RANDOM_2:1

for f being one-to-one Function

for A, B being Subset of (dom f) st A misses B holds

rng (f | A) misses rng (f | B)

for A, B being Subset of (dom f) st A misses B holds

rng (f | A) misses rng (f | B)

proof end;

registration

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

ex b_{1} being Real-Valued-Random-Variable of Sigma st b_{1} is nonnegative

end;
let Sigma be SigmaField of Omega;

cluster Relation-like Omega -defined REAL -valued Function-like non empty total quasi_total V153() V154() V155() nonnegative for Real-Valued-Random-Variable of Sigma;

existence ex b

proof end;

registration

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

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

coherence

abs X is nonnegative

end;
let Sigma be SigmaField of Omega;

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

coherence

abs X is nonnegative

proof end;

theorem Th4: :: RANDOM_2:4

for Omega being non empty set

for r being Real

for Sigma being SigmaField of Omega holds Omega --> r is Real-Valued-Random-Variable of Sigma

for r being Real

for Sigma being SigmaField of Omega holds Omega --> r is Real-Valued-Random-Variable of Sigma

proof end;

theorem Th5: :: RANDOM_2:5

for X being non empty set

for f being PartFunc of X,REAL holds

( f to_power 2 = (- f) to_power 2 & f to_power 2 = (abs f) to_power 2 )

for f being PartFunc of X,REAL holds

( f to_power 2 = (- f) to_power 2 & f to_power 2 = (abs f) to_power 2 )

proof end;

theorem Th6: :: RANDOM_2:6

for X being non empty set

for f, g being PartFunc of X,REAL holds

( (f + g) to_power 2 = ((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2) & (f - g) to_power 2 = ((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2) )

for f, g being PartFunc of X,REAL holds

( (f + g) to_power 2 = ((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2) & (f - g) to_power 2 = ((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2) )

proof end;

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

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

assume A1: ( X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P ) ;

existence

ex b_{1} being Real ex Y, E being Real-Valued-Random-Variable of Sigma st

( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b_{1} = Integral ((P2M P),((abs Y) to_power 2)) );

uniqueness

for b_{1}, b_{2} being Real st ex Y, E being Real-Valued-Random-Variable of Sigma st

( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b_{1} = Integral ((P2M P),((abs Y) to_power 2)) ) & ex Y, E being Real-Valued-Random-Variable of Sigma st

( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b_{2} = Integral ((P2M P),((abs Y) to_power 2)) ) holds

b_{1} = b_{2};

end;
let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

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

assume A1: ( X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P ) ;

func variance (X,P) -> Real means :Def1: :: RANDOM_2:def 1

ex Y, E being Real-Valued-Random-Variable of Sigma st

( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & it = Integral ((P2M P),((abs Y) to_power 2)) );

correctness ex Y, E being Real-Valued-Random-Variable of Sigma st

( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & it = Integral ((P2M P),((abs Y) to_power 2)) );

existence

ex b

( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b

uniqueness

for b

( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b

( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b

b

proof end;

:: deftheorem Def1 defines variance RANDOM_2:def 1 :

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for X being Real-Valued-Random-Variable of Sigma st X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds

for b_{5} being Real holds

( b_{5} = variance (X,P) iff ex Y, E being Real-Valued-Random-Variable of Sigma st

( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b_{5} = Integral ((P2M P),((abs Y) to_power 2)) ) );

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for X being Real-Valued-Random-Variable of Sigma st X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds

for b

( b

( E = Omega --> (expect (X,P)) & Y = X - E & Y is_integrable_on P & (abs Y) to_power 2 is_integrable_on P2M P & b

theorem :: RANDOM_2:7

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for r being Real

for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds

P . { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } <= (variance (X,P)) / (r to_power 2)

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for r being Real

for X being Real-Valued-Random-Variable of Sigma st 0 < r & X is nonnegative & X is_integrable_on P & (abs X) to_power 2 is_integrable_on P2M P holds

P . { t where t is Element of Omega : r <= |.((X . t) - (expect (X,P))).| } <= (variance (X,P)) / (r to_power 2)

proof end;

theorem Th8: :: RANDOM_2:8

for Omega being non empty finite set

for f being Function of Omega,REAL

for P being Function of (bool Omega),REAL st ( for x being set st x c= Omega holds

( 0 <= P . x & P . x <= 1 ) ) & P . Omega = 1 & ( for z being finite Subset of Omega holds P . z = setopfunc (z,Omega,REAL,f,addreal) ) holds

P is Probability of Trivial-SigmaField Omega

for f being Function of Omega,REAL

for P being Function of (bool Omega),REAL st ( for x being set st x c= Omega holds

( 0 <= P . x & P . x <= 1 ) ) & P . Omega = 1 & ( for z being finite Subset of Omega holds P . z = setopfunc (z,Omega,REAL,f,addreal) ) holds

P is Probability of Trivial-SigmaField Omega

proof end;

Lm1: for Omega1, Omega2 being non empty finite set

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2 ex Q being Function of [:Omega1,Omega2:],REAL st

for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y})

proof end;

Lm2: for Omega1, Omega2 being non empty finite set

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2

for Q1, Q2 being Function of [:Omega1,Omega2:],REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds

Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for x, y being set st x in Omega1 & y in Omega2 holds

Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) holds

Q1 = Q2

proof end;

Lm3: for Omega1, Omega2 being non empty finite set

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2

for Q being Function of [:Omega1,Omega2:],REAL ex P being Function of (bool [:Omega1,Omega2:]),REAL st

for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)

proof end;

Lm4: for Omega1, Omega2 being non empty finite set

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2

for Q being Function of [:Omega1,Omega2:],REAL

for P1, P2 being Function of (bool [:Omega1,Omega2:]),REAL st ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds

P1 = P2

proof end;

Lm5: for DK, DX being non empty set

for F being Function of DX,DK

for p, q being FinSequence of DX

for fp, fq being FinSequence of DK st fp = F * p & fq = F * q holds

F * (p ^ q) = fp ^ fq

proof end;

theorem Th9: :: RANDOM_2:9

for DX being non empty set

for F being Function of DX,REAL

for Y being finite Subset of DX ex p being FinSequence of DX st

( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) )

for F being Function of DX,REAL

for Y being finite Subset of DX ex p being FinSequence of DX st

( p is one-to-one & rng p = Y & setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p)) )

proof end;

theorem Th10: :: RANDOM_2:10

for DX being non empty set

for F being Function of DX,REAL

for Y being finite Subset of DX

for p being FinSequence of DX st p is one-to-one & rng p = Y holds

setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p))

for F being Function of DX,REAL

for Y being finite Subset of DX

for p being FinSequence of DX st p is one-to-one & rng p = Y holds

setopfunc (Y,DX,REAL,F,addreal) = Sum (Func_Seq (F,p))

proof end;

Lm6: for p being Function st dom p = Seg 1 holds

p = <*(p . 1)*>

proof end;

theorem Th11: :: RANDOM_2:11

for DX1, DX2 being non empty set

for F1 being Function of DX1,REAL

for F2 being Function of DX2,REAL

for G being Function of [:DX1,DX2:],REAL

for Y1 being non empty finite Subset of DX1

for p1 being FinSequence of DX1 st p1 is one-to-one & rng p1 = Y1 holds

for p2 being FinSequence of DX2

for p3 being FinSequence of [:DX1,DX2:]

for Y2 being non empty finite Subset of DX2

for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds

G . (x,y) = (F1 . x) * (F2 . y) ) holds

Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))

for F1 being Function of DX1,REAL

for F2 being Function of DX2,REAL

for G being Function of [:DX1,DX2:],REAL

for Y1 being non empty finite Subset of DX1

for p1 being FinSequence of DX1 st p1 is one-to-one & rng p1 = Y1 holds

for p2 being FinSequence of DX2

for p3 being FinSequence of [:DX1,DX2:]

for Y2 being non empty finite Subset of DX2

for Y3 being finite Subset of [:DX1,DX2:] st p2 is one-to-one & rng p2 = Y2 & p3 is one-to-one & rng p3 = Y3 & Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds

G . (x,y) = (F1 . x) * (F2 . y) ) holds

Sum (Func_Seq (G,p3)) = (Sum (Func_Seq (F1,p1))) * (Sum (Func_Seq (F2,p2)))

proof end;

theorem Th12: :: RANDOM_2:12

for DX1, DX2 being non empty set

for F1 being Function of DX1,REAL

for F2 being Function of DX2,REAL

for G being Function of [:DX1,DX2:],REAL

for Y1 being non empty finite Subset of DX1

for Y2 being non empty finite Subset of DX2

for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds

G . (x,y) = (F1 . x) * (F2 . y) ) holds

setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal))

for F1 being Function of DX1,REAL

for F2 being Function of DX2,REAL

for G being Function of [:DX1,DX2:],REAL

for Y1 being non empty finite Subset of DX1

for Y2 being non empty finite Subset of DX2

for Y3 being finite Subset of [:DX1,DX2:] st Y3 = [:Y1,Y2:] & ( for x, y being set st x in Y1 & y in Y2 holds

G . (x,y) = (F1 . x) * (F2 . y) ) holds

setopfunc (Y3,[:DX1,DX2:],REAL,G,addreal) = (setopfunc (Y1,DX1,REAL,F1,addreal)) * (setopfunc (Y2,DX2,REAL,F2,addreal))

proof end;

theorem Th13: :: RANDOM_2:13

for DX being non empty set

for F being Function of DX,REAL

for Y being finite Subset of DX st ( for x being set st x in Y holds

0 <= F . x ) holds

0 <= setopfunc (Y,DX,REAL,F,addreal)

for F being Function of DX,REAL

for Y being finite Subset of DX st ( for x being set st x in Y holds

0 <= F . x ) holds

0 <= setopfunc (Y,DX,REAL,F,addreal)

proof end;

theorem Th14: :: RANDOM_2:14

for DX being non empty set

for F being Function of DX,REAL

for Y1, Y2 being finite Subset of DX st Y1 c= Y2 & ( for x being set st x in Y2 holds

0 <= F . x ) holds

setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal)

for F being Function of DX,REAL

for Y1, Y2 being finite Subset of DX st Y1 c= Y2 & ( for x being set st x in Y2 holds

0 <= F . x ) holds

setopfunc (Y1,DX,REAL,F,addreal) <= setopfunc (Y2,DX,REAL,F,addreal)

proof end;

theorem Th15: :: RANDOM_2:15

for Omega being non empty finite set

for P being Probability of Trivial-SigmaField Omega

for Y being non empty finite Subset of Omega

for f being Function of Omega,REAL ex G being FinSequence of REAL ex s being FinSequence of Y st

( len G = card Y & s is one-to-one & rng s = Y & len s = card Y & ( for n being Nat st n in dom G holds

G . n = (f . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),(f | Y)) = Sum G )

for P being Probability of Trivial-SigmaField Omega

for Y being non empty finite Subset of Omega

for f being Function of Omega,REAL ex G being FinSequence of REAL ex s being FinSequence of Y st

( len G = card Y & s is one-to-one & rng s = Y & len s = card Y & ( for n being Nat st n in dom G holds

G . n = (f . (s . n)) * (P . {(s . n)}) ) & Integral ((P2M P),(f | Y)) = Sum G )

proof end;

reconsider jj = 1 as R_eal by XXREAL_0:def 1;

Lm7: for Omega1, Omega2 being non empty finite set

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2

for Q being Function of [:Omega1,Omega2:],REAL

for P being Function of (bool [:Omega1,Omega2:]),REAL

for Y1 being non empty finite Subset of Omega1

for Y2 being non empty finite Subset of Omega2 st ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds

P . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)

proof end;

Lm8: for Omega1, Omega2 being non empty finite set

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2

for Q being Function of [:Omega1,Omega2:],REAL

for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds

P . [:Omega1,Omega2:] = 1

proof end;

Lm9: for Omega1, Omega2 being non empty finite set

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2

for Q being Function of [:Omega1,Omega2:],REAL

for P being Function of (bool [:Omega1,Omega2:]),REAL st ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds

for x being set st x c= [:Omega1,Omega2:] holds

( 0 <= P . x & P . x <= 1 )

proof end;

definition

let Omega1, Omega2 be non empty finite set ;

let P1 be Probability of Trivial-SigmaField Omega1;

let P2 be Probability of Trivial-SigmaField Omega2;

ex b_{1} being Probability of Trivial-SigmaField [:Omega1,Omega2:] ex Q being Function of [:Omega1,Omega2:],REAL st

( ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b_{1} . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) )

for b_{1}, b_{2} being Probability of Trivial-SigmaField [:Omega1,Omega2:] st ex Q being Function of [:Omega1,Omega2:],REAL st

( ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b_{1} . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) & ex Q being Function of [:Omega1,Omega2:],REAL st

( ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b_{2} . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) holds

b_{1} = b_{2}

end;
let P1 be Probability of Trivial-SigmaField Omega1;

let P2 be Probability of Trivial-SigmaField Omega2;

func Product-Probability (Omega1,Omega2,P1,P2) -> Probability of Trivial-SigmaField [:Omega1,Omega2:] means :Def2: :: RANDOM_2:def 2

ex Q being Function of [:Omega1,Omega2:],REAL st

( ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds it . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) );

existence ex Q being Function of [:Omega1,Omega2:],REAL st

( ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds it . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) );

ex b

( ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b

proof end;

uniqueness for b

( ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b

( ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b

b

proof end;

:: deftheorem Def2 defines Product-Probability RANDOM_2:def 2 :

for Omega1, Omega2 being non empty finite set

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2

for b_{5} being Probability of Trivial-SigmaField [:Omega1,Omega2:] holds

( b_{5} = Product-Probability (Omega1,Omega2,P1,P2) iff ex Q being Function of [:Omega1,Omega2:],REAL st

( ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b_{5} . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) );

for Omega1, Omega2 being non empty finite set

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2

for b

( b

( ( for x, y being set st x in Omega1 & y in Omega2 holds

Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b

theorem Th16: :: RANDOM_2:16

for Omega1, Omega2 being non empty finite set

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2

for Y1 being non empty finite Subset of Omega1

for Y2 being non empty finite Subset of Omega2 holds (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2

for Y1 being non empty finite Subset of Omega1

for Y2 being non empty finite Subset of Omega2 holds (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)

proof end;

theorem :: RANDOM_2:17

for Omega1, Omega2 being non empty finite set

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2

for y1, y2 being set st y1 in Omega1 & y2 in Omega2 holds

(Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})

for P1 being Probability of Trivial-SigmaField Omega1

for P2 being Probability of Trivial-SigmaField Omega2

for y1, y2 being set st y1 in Omega1 & y2 in Omega2 holds

(Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})

proof end;

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

coherence

{ f where f is Real-Valued-Random-Variable of Sigma : verum } is non empty Subset of (RAlgebra Omega);

end;
let Sigma be SigmaField of Omega;

func Real-Valued-Random-Variables-Set Sigma -> non empty Subset of (RAlgebra Omega) equals :: RANDOM_2:def 3

{ f where f is Real-Valued-Random-Variable of Sigma : verum } ;

correctness { f where f is Real-Valued-Random-Variable of Sigma : verum } ;

coherence

{ f where f is Real-Valued-Random-Variable of Sigma : verum } is non empty Subset of (RAlgebra Omega);

proof end;

:: deftheorem defines Real-Valued-Random-Variables-Set RANDOM_2:def 3 :

for Omega being non empty set

for Sigma being SigmaField of Omega holds Real-Valued-Random-Variables-Set Sigma = { f where f is Real-Valued-Random-Variable of Sigma : verum } ;

for Omega being non empty set

for Sigma being SigmaField of Omega holds Real-Valued-Random-Variables-Set Sigma = { f where f is Real-Valued-Random-Variable of Sigma : verum } ;

Lm10: for Omega being non empty set

for Sigma being SigmaField of Omega holds

( Real-Valued-Random-Variables-Set Sigma is additively-linearly-closed & Real-Valued-Random-Variables-Set Sigma is multiplicatively-closed )

proof end;

registration

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

( Real-Valued-Random-Variables-Set Sigma is additively-linearly-closed & Real-Valued-Random-Variables-Set Sigma is multiplicatively-closed ) by Lm10;

end;
let Sigma be SigmaField of Omega;

cluster Real-Valued-Random-Variables-Set Sigma -> non empty multiplicatively-closed additively-linearly-closed ;

coherence ( Real-Valued-Random-Variables-Set Sigma is additively-linearly-closed & Real-Valued-Random-Variables-Set Sigma is multiplicatively-closed ) by Lm10;

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

AlgebraStr(# (Real-Valued-Random-Variables-Set Sigma),(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #) is Algebra by C0SP1:6;

end;
let Sigma be SigmaField of Omega;

func R_Algebra_of_Real-Valued-Random-Variables Sigma -> Algebra equals :: RANDOM_2:def 4

AlgebraStr(# (Real-Valued-Random-Variables-Set Sigma),(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #);

coherence AlgebraStr(# (Real-Valued-Random-Variables-Set Sigma),(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #);

AlgebraStr(# (Real-Valued-Random-Variables-Set Sigma),(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #) is Algebra by C0SP1:6;

:: deftheorem defines R_Algebra_of_Real-Valued-Random-Variables RANDOM_2:def 4 :

for Omega being non empty set

for Sigma being SigmaField of Omega holds R_Algebra_of_Real-Valued-Random-Variables Sigma = AlgebraStr(# (Real-Valued-Random-Variables-Set Sigma),(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #);

for Omega being non empty set

for Sigma being SigmaField of Omega holds R_Algebra_of_Real-Valued-Random-Variables Sigma = AlgebraStr(# (Real-Valued-Random-Variables-Set Sigma),(mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Add_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Mult_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(One_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))),(Zero_ ((Real-Valued-Random-Variables-Set Sigma),(RAlgebra Omega))) #);

registration

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

coherence

R_Algebra_of_Real-Valued-Random-Variables Sigma is scalar-unital

end;
let Sigma be SigmaField of Omega;

coherence

R_Algebra_of_Real-Valued-Random-Variables Sigma is scalar-unital

proof end;