:: Random Variables and Product of Probability Spaces
:: by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 1, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users


theorem Th1: :: RANDOM_3:1
for B being non empty set
for f being Function holds f " (union B) = union { (f " Y) where Y is Element of B : verum }
proof end;

theorem Th2: :: RANDOM_3:2
for Omega1, Omega2 being non empty set
for f being Function of Omega1,Omega2
for B being SetSequence of Omega2
for D being SetSequence of Omega1 st ( for n being Element of NAT holds D . n = f " (B . n) ) holds
f " (Union B) = Union D
proof end;

theorem Th3: :: RANDOM_3:3
for Omega1, Omega2 being non empty set
for f being Function of Omega1,Omega2
for B being SetSequence of Omega2
for D being SetSequence of Omega1 st ( for n being Element of NAT holds D . n = f " (B . n) ) holds
f " (Intersection B) = Intersection D
proof end;

theorem Th4: :: RANDOM_3:4
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being Function of Omega,REAL
for r being Real st F is Real-Valued-Random-Variable of Sigma holds
F " ].-infty,r.[ in Sigma
proof end;

theorem Th5: :: RANDOM_3:5
for Omega being non empty set
for Sigma being SigmaField of Omega
for F being Function of Omega,REAL st F is Real-Valued-Random-Variable of Sigma holds
{ x where x is Element of Borel_Sets : F " x is Element of Sigma } is SigmaField of REAL
proof end;

theorem Th6: :: RANDOM_3:6
for Omega being non empty set
for Sigma being SigmaField of Omega
for f being Function of Omega,REAL st f is Real-Valued-Random-Variable of Sigma holds
{ x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets
proof end;

theorem Th7: :: RANDOM_3:7
for Omega being non empty set
for Sigma being SigmaField of Omega
for f being Function of Omega,REAL holds
( f is Sigma, Borel_Sets -random_variable-like iff f is Real-Valued-Random-Variable of Sigma )
proof end;

theorem :: RANDOM_3:8
for Omega being non empty set
for Sigma being SigmaField of Omega
for f being Function of Omega,REAL holds set_of_random_variables_on (Sigma,Borel_Sets) = Real-Valued-Random-Variables-Set Sigma
proof end;

definition
end;

:: deftheorem RANDOM_3:def 1 :
canceled;

registration
let Omega1, Omega2 be non empty set ;
let S1 be SigmaField of Omega1;
let S2 be SigmaField of Omega2;
cluster Relation-like Omega1 -defined Omega2 -valued non empty Function-like total quasi_total S1,S2 -random_variable-like for Element of bool [:Omega1,Omega2:];
existence
ex b1 being Function of Omega1,Omega2 st b1 is S1,S2 -random_variable-like
proof end;
end;

definition
let Omega1, Omega2 be non empty set ;
let S1 be SigmaField of Omega1;
let S2 be SigmaField of Omega2;
mode random_variable of S1,S2 is S1,S2 -random_variable-like Function of Omega1,Omega2;
end;

theorem :: RANDOM_3:9
for Omega being non empty set
for Sigma being SigmaField of Omega
for f being Function of Omega,REAL holds
( f is random_variable of Sigma, Borel_Sets iff f is Real-Valued-Random-Variable of Sigma ) by Th7;

definition
let F be Function;
attr F is random_variable_family-like means :Def2: :: RANDOM_3:def 2
for x being set st x in dom F holds
ex Omega1, Omega2 being non empty set ex S1 being SigmaField of Omega1 ex S2 being SigmaField of Omega2 ex f being random_variable of S1,S2 st F . x = f;
end;

:: deftheorem Def2 defines random_variable_family-like RANDOM_3:def 2 :
for F being Function holds
( F is random_variable_family-like iff for x being set st x in dom F holds
ex Omega1, Omega2 being non empty set ex S1 being SigmaField of Omega1 ex S2 being SigmaField of Omega2 ex f being random_variable of S1,S2 st F . x = f );

registration
cluster Relation-like Function-like random_variable_family-like for set ;
existence
ex b1 being Function st b1 is random_variable_family-like
proof end;
end;

definition
mode random_variable_family is random_variable_family-like Function;
end;

definition
let Y be non empty set ;
let S be SigmaField of Y;
let F be Function;
attr F is S -Measure_valued means :Def3: :: RANDOM_3:def 3
for x being set st x in dom F holds
ex M being sigma_Measure of S st F . x = M;
end;

:: deftheorem Def3 defines -Measure_valued RANDOM_3:def 3 :
for Y being non empty set
for S being SigmaField of Y
for F being Function holds
( F is S -Measure_valued iff for x being set st x in dom F holds
ex M being sigma_Measure of S st F . x = M );

registration
let Y be non empty set ;
let S be SigmaField of Y;
cluster Relation-like Function-like S -Measure_valued for set ;
existence
ex b1 being Function st b1 is S -Measure_valued
proof end;
end;

definition
let Y be non empty set ;
let S be SigmaField of Y;
let F be Function;
attr F is S -Probability_valued means :Def4: :: RANDOM_3:def 4
for x being set st x in dom F holds
ex P being Probability of S st F . x = P;
end;

:: deftheorem Def4 defines -Probability_valued RANDOM_3:def 4 :
for Y being non empty set
for S being SigmaField of Y
for F being Function holds
( F is S -Probability_valued iff for x being set st x in dom F holds
ex P being Probability of S st F . x = P );

registration
let Y be non empty set ;
let S be SigmaField of Y;
cluster Relation-like Function-like S -Probability_valued for set ;
existence
ex b1 being Function st b1 is S -Probability_valued
proof end;
end;

Lm1: for X, Y being non empty set
for S being SigmaField of Y
for M being Probability of S holds X --> M is S -Probability_valued

by FUNCOP_1:7;

registration
let X, Y be non empty set ;
let S be SigmaField of Y;
cluster Relation-like X -defined Function-like S -Probability_valued for set ;
existence
ex b1 being S -Probability_valued Function st b1 is X -defined
proof end;
end;

registration
let X, Y be non empty set ;
let S be SigmaField of Y;
cluster Relation-like X -defined Function-like total S -Probability_valued for set ;
existence
ex b1 being X -defined S -Probability_valued Function st b1 is total
proof end;
end;

registration
let Y be non empty set ;
let S be SigmaField of Y;
cluster Relation-like Function-like S -Probability_valued -> S -Measure_valued for set ;
coherence
for b1 being Function st b1 is S -Probability_valued holds
b1 is S -Measure_valued
proof end;
end;

definition
let Y be non empty set ;
let S be SigmaField of Y;
let F be Function;
attr F is S -Random-Variable-Family means :Def5: :: RANDOM_3:def 5
for x being set st x in dom F holds
ex Z being Real-Valued-Random-Variable of S st F . x = Z;
end;

:: deftheorem Def5 defines -Random-Variable-Family RANDOM_3:def 5 :
for Y being non empty set
for S being SigmaField of Y
for F being Function holds
( F is S -Random-Variable-Family iff for x being set st x in dom F holds
ex Z being Real-Valued-Random-Variable of S st F . x = Z );

registration
let Y be non empty set ;
let S be SigmaField of Y;
cluster Relation-like Function-like S -Random-Variable-Family for set ;
existence
ex b1 being Function st b1 is S -Random-Variable-Family
proof end;
end;

theorem :: RANDOM_3:10
for Omega1, Omega2 being non empty set
for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for F being random_variable of S1,S2
for y being Element of S2 st y <> {} holds
{ z where z is Element of Omega1 : F . z is Element of y } = F " y
proof end;

theorem :: RANDOM_3:11
for Omega1, Omega2 being non empty set
for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for F being random_variable of S1,S2 holds
( { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } c= S1 & { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } is SigmaField of Omega1 )
proof end;

Lm2: for Omega1, Omega2 being non empty set
for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for M being Measure of S1
for F being random_variable of S1,S2 ex N being Measure of S2 st
for y being Element of S2 holds N . y = M . (F " y)

proof end;

definition
let Omega1, Omega2 be non empty set ;
let S1 be SigmaField of Omega1;
let S2 be SigmaField of Omega2;
let M be Measure of S1;
let F be random_variable of S1,S2;
func image_measure (F,M) -> Measure of S2 means :Def6: :: RANDOM_3:def 6
for y being Element of S2 holds it . y = M . (F " y);
existence
ex b1 being Measure of S2 st
for y being Element of S2 holds b1 . y = M . (F " y)
by Lm2;
uniqueness
for b1, b2 being Measure of S2 st ( for y being Element of S2 holds b1 . y = M . (F " y) ) & ( for y being Element of S2 holds b2 . y = M . (F " y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines image_measure RANDOM_3:def 6 :
for Omega1, Omega2 being non empty set
for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for M being Measure of S1
for F being random_variable of S1,S2
for b7 being Measure of S2 holds
( b7 = image_measure (F,M) iff for y being Element of S2 holds b7 . y = M . (F " y) );

registration
let Omega1, Omega2 be non empty set ;
let S1 be SigmaField of Omega1;
let S2 be SigmaField of Omega2;
let M be sigma_Measure of S1;
let F be random_variable of S1,S2;
cluster image_measure (F,M) -> sigma-additive ;
coherence
image_measure (F,M) is sigma-additive
proof end;
end;

theorem Th12: :: RANDOM_3:12
for Omega1, Omega2 being non empty set
for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for P being Probability of S1
for F being random_variable of S1,S2 holds (image_measure (F,(P2M P))) . Omega2 = 1
proof end;

definition
let Omega1, Omega2 be non empty set ;
let S1 be SigmaField of Omega1;
let S2 be SigmaField of Omega2;
let P be Probability of S1;
let F be random_variable of S1,S2;
func probability (F,P) -> Probability of S2 equals :: RANDOM_3:def 7
M2P (image_measure (F,(P2M P)));
coherence
M2P (image_measure (F,(P2M P))) is Probability of S2
;
end;

:: deftheorem defines probability RANDOM_3:def 7 :
for Omega1, Omega2 being non empty set
for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for P being Probability of S1
for F being random_variable of S1,S2 holds probability (F,P) = M2P (image_measure (F,(P2M P)));

theorem Th13: :: RANDOM_3:13
for Omega1, Omega2 being non empty set
for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for P being Probability of S1
for F being random_variable of S1,S2 holds probability (F,P) = image_measure (F,(P2M P))
proof end;

theorem Th14: :: RANDOM_3:14
for Omega1, Omega2 being non empty set
for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for P being Probability of S1
for F being random_variable of S1,S2
for y being set st y in S2 holds
(probability (F,P)) . y = P . (F " y)
proof end;

theorem Th15: :: RANDOM_3:15
for Omega1, Omega2 being non empty set
for F being Function of Omega1,Omega2 holds F is random_variable of Trivial-SigmaField Omega1, Trivial-SigmaField Omega2
proof end;

theorem Th16: :: RANDOM_3:16
for S being non empty set
for F being non empty FinSequence of S holds F is random_variable of Trivial-SigmaField (Seg (len F)), Trivial-SigmaField S
proof end;

theorem Th17: :: RANDOM_3:17
for V, S being non empty finite set
for G being random_variable of Trivial-SigmaField V, Trivial-SigmaField S
for y being set st y in Trivial-SigmaField S holds
(probability (G,(Trivial-Probability V))) . y = (card (G " y)) / (card V)
proof end;

theorem :: RANDOM_3:18
for S being non empty finite set
for s being non empty FinSequence of S ex G being random_variable of Trivial-SigmaField (Seg (len s)), Trivial-SigmaField S st
( G = s & ( for x being set st x in S holds
(probability (G,(Trivial-Probability (Seg (len s))))) . {x} = FDprobability (x,s) ) )
proof end;

registration
let D be non-empty ManySortedSet of NAT ;
let n be Nat;
cluster D . n -> non empty ;
correctness
coherence
not D . n is empty
;
proof end;
end;

definition
let S, F be ManySortedSet of NAT ;
attr F is S -SigmaField_sequence-like means :Def8: :: RANDOM_3:def 8
for n being Nat holds F . n is SigmaField of (S . n);
end;

:: deftheorem Def8 defines -SigmaField_sequence-like RANDOM_3:def 8 :
for S, F being ManySortedSet of NAT holds
( F is S -SigmaField_sequence-like iff for n being Nat holds F . n is SigmaField of (S . n) );

registration
let S be ManySortedSet of NAT ;
cluster Relation-like NAT -defined non empty Function-like total S -SigmaField_sequence-like for set ;
existence
ex b1 being ManySortedSet of NAT st b1 is S -SigmaField_sequence-like
proof end;
end;

definition
let D be ManySortedSet of NAT ;
mode SigmaField_sequence of D is D -SigmaField_sequence-like ManySortedSet of NAT ;
end;

definition
let D be ManySortedSet of NAT ;
let S be SigmaField_sequence of D;
let n be Nat;
:: original: .
redefine func S . n -> SigmaField of (D . n);
correctness
coherence
S . n is SigmaField of (D . n)
;
by Def8;
end;

definition
let D be non-empty ManySortedSet of NAT ;
let S be SigmaField_sequence of D;
let M be ManySortedSet of NAT ;
attr M is S -Probability_sequence-like means :Def9: :: RANDOM_3:def 9
for n being Nat holds M . n is Probability of S . n;
end;

:: deftheorem Def9 defines -Probability_sequence-like RANDOM_3:def 9 :
for D being non-empty ManySortedSet of NAT
for S being SigmaField_sequence of D
for M being ManySortedSet of NAT holds
( M is S -Probability_sequence-like iff for n being Nat holds M . n is Probability of S . n );

registration
let D be non-empty ManySortedSet of NAT ;
let S be SigmaField_sequence of D;
cluster Relation-like NAT -defined non empty Function-like total S -Probability_sequence-like for set ;
existence
ex b1 being ManySortedSet of NAT st b1 is S -Probability_sequence-like
proof end;
end;

definition
let D be non-empty ManySortedSet of NAT ;
let S be SigmaField_sequence of D;
mode Probability_sequence of S is S -Probability_sequence-like ManySortedSet of NAT ;
end;

definition
let D be non-empty ManySortedSet of NAT ;
let S be SigmaField_sequence of D;
let P be Probability_sequence of S;
let n be Nat;
:: original: .
redefine func P . n -> Probability of S . n;
correctness
coherence
P . n is Probability of S . n
;
by Def9;
end;

definition
let D be ManySortedSet of NAT ;
func Product_dom D -> ManySortedSet of NAT means :Def10: :: RANDOM_3:def 10
( it . 0 = D . 0 & ( for i being Nat holds it . (i + 1) = [:(it . i),(D . (i + 1)):] ) );
existence
ex b1 being ManySortedSet of NAT st
( b1 . 0 = D . 0 & ( for i being Nat holds b1 . (i + 1) = [:(b1 . i),(D . (i + 1)):] ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of NAT st b1 . 0 = D . 0 & ( for i being Nat holds b1 . (i + 1) = [:(b1 . i),(D . (i + 1)):] ) & b2 . 0 = D . 0 & ( for i being Nat holds b2 . (i + 1) = [:(b2 . i),(D . (i + 1)):] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines Product_dom RANDOM_3:def 10 :
for D, b2 being ManySortedSet of NAT holds
( b2 = Product_dom D iff ( b2 . 0 = D . 0 & ( for i being Nat holds b2 . (i + 1) = [:(b2 . i),(D . (i + 1)):] ) ) );

theorem Th19: :: RANDOM_3:19
for D being ManySortedSet of NAT holds
( (Product_dom D) . 0 = D . 0 & (Product_dom D) . 1 = [:(D . 0),(D . 1):] & (Product_dom D) . 2 = [:(D . 0),(D . 1),(D . 2):] & (Product_dom D) . 3 = [:(D . 0),(D . 1),(D . 2),(D . 3):] )
proof end;

registration
let D be non-empty ManySortedSet of NAT ;
cluster Product_dom D -> non-empty ;
correctness
coherence
Product_dom D is non-empty
;
proof end;
end;

registration
let D be V26() ManySortedSet of NAT ;
cluster Product_dom D -> V26() ;
correctness
coherence
Product_dom D is finite-yielding
;
proof end;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be set ;
assume A1: P is Probability of Sigma ;
func modetrans (P,Sigma) -> Probability of Sigma equals :Def11: :: RANDOM_3:def 11
P;
correctness
coherence
P is Probability of Sigma
;
by A1;
end;

:: deftheorem Def11 defines modetrans RANDOM_3:def 11 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being set st P is Probability of Sigma holds
modetrans (P,Sigma) = P;

definition
let D be non-empty V26() ManySortedSet of NAT ;
func Trivial-SigmaField_sequence D -> SigmaField_sequence of D means :Def12: :: RANDOM_3:def 12
for n being Nat holds it . n = Trivial-SigmaField (D . n);
existence
ex b1 being SigmaField_sequence of D st
for n being Nat holds b1 . n = Trivial-SigmaField (D . n)
proof end;
uniqueness
for b1, b2 being SigmaField_sequence of D st ( for n being Nat holds b1 . n = Trivial-SigmaField (D . n) ) & ( for n being Nat holds b2 . n = Trivial-SigmaField (D . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines Trivial-SigmaField_sequence RANDOM_3:def 12 :
for D being non-empty V26() ManySortedSet of NAT
for b2 being SigmaField_sequence of D holds
( b2 = Trivial-SigmaField_sequence D iff for n being Nat holds b2 . n = Trivial-SigmaField (D . n) );

definition
let D be non-empty V26() ManySortedSet of NAT ;
let P be Probability_sequence of Trivial-SigmaField_sequence D;
let n be Nat;
:: original: .
redefine func P . n -> Probability of Trivial-SigmaField (D . n);
coherence
P . n is Probability of Trivial-SigmaField (D . n)
proof end;
end;

definition
let D be non-empty V26() ManySortedSet of NAT ;
let P be Probability_sequence of Trivial-SigmaField_sequence D;
func Product-Probability (P,D) -> ManySortedSet of NAT means :Def13: :: RANDOM_3:def 13
( it . 0 = P . 0 & ( for i being Nat holds it . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((it . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) );
existence
ex b1 being ManySortedSet of NAT st
( b1 . 0 = P . 0 & ( for i being Nat holds b1 . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b1 . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of NAT st b1 . 0 = P . 0 & ( for i being Nat holds b1 . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b1 . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) & b2 . 0 = P . 0 & ( for i being Nat holds b2 . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b2 . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines Product-Probability RANDOM_3:def 13 :
for D being non-empty V26() ManySortedSet of NAT
for P being Probability_sequence of Trivial-SigmaField_sequence D
for b3 being ManySortedSet of NAT holds
( b3 = Product-Probability (P,D) iff ( b3 . 0 = P . 0 & ( for i being Nat holds b3 . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b3 . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) ) );

theorem Th20: :: RANDOM_3:20
for D being non-empty V26() ManySortedSet of NAT
for P being Probability_sequence of Trivial-SigmaField_sequence D
for n being Nat holds (Product-Probability (P,D)) . n is Probability of Trivial-SigmaField ((Product_dom D) . n)
proof end;

theorem Th21: :: RANDOM_3:21
for D being non-empty V26() ManySortedSet of NAT
for P being Probability_sequence of Trivial-SigmaField_sequence D
for n being Nat ex Pn being Probability of Trivial-SigmaField ((Product_dom D) . n) st
( Pn = (Product-Probability (P,D)) . n & (Product-Probability (P,D)) . (n + 1) = Product-Probability (((Product_dom D) . n),(D . (n + 1)),Pn,(P . (n + 1))) )
proof end;

theorem :: RANDOM_3:22
for D being non-empty V26() ManySortedSet of NAT
for P being Probability_sequence of Trivial-SigmaField_sequence D holds
( (Product-Probability (P,D)) . 0 = P . 0 & (Product-Probability (P,D)) . 1 = Product-Probability ((D . 0),(D . 1),(P . 0),(P . 1)) & ex P1 being Probability of Trivial-SigmaField [:(D . 0),(D . 1):] st
( P1 = (Product-Probability (P,D)) . 1 & (Product-Probability (P,D)) . 2 = Product-Probability ([:(D . 0),(D . 1):],(D . 2),P1,(P . 2)) ) & ex P2 being Probability of Trivial-SigmaField [:(D . 0),(D . 1),(D . 2):] st
( P2 = (Product-Probability (P,D)) . 2 & (Product-Probability (P,D)) . 3 = Product-Probability ([:(D . 0),(D . 1),(D . 2):],(D . 3),P2,(P . 3)) ) & ex P3 being Probability of Trivial-SigmaField [:(D . 0),(D . 1),(D . 2),(D . 3):] st
( P3 = (Product-Probability (P,D)) . 3 & (Product-Probability (P,D)) . 4 = Product-Probability ([:(D . 0),(D . 1),(D . 2),(D . 3):],(D . 4),P3,(P . 4)) ) )
proof end;