:: 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 b₁ being Function of Omega1,Omega2 st b₁ 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 b₁ being Function st b₁ 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 b₁ being Function st b₁ 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 b₁ being Function st b₁ 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 b₁ being S -Probability_valued Function st b₁ 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 b₁ being X -defined S -Probability_valued Function st b₁ 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 b₁ being Function st b₁ is S -Probability_valued holds
b₁ 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 b₁ being Function st b₁ 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 b₁ being Measure of S2 st
for y being Element of S2 holds b₁ . y = M . (F " y) by Lm2;
uniqueness
for b₁, b₂ being Measure of S2 st ( for y being Element of S2 holds b₁ . y = M . (F " y) ) & ( for y being Element of S2 holds b₂ . y = M . (F " y) ) holds
b₁ = b₂

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 b₇ being Measure of S2 holds
( b₇ = image_measure (F,M) iff for y being Element of S2 holds b₇ . 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 b₁ being ManySortedSet of NAT st b₁ 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 b₁ being ManySortedSet of NAT st b₁ 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 b₁ being ManySortedSet of NAT st
( b₁ . 0 = D . 0 & ( for i being Nat holds b₁ . (i + 1) = [:(b₁ . i),(D . (i + 1)):] ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of NAT st b₁ . 0 = D . 0 & ( for i being Nat holds b₁ . (i + 1) = [:(b₁ . i),(D . (i + 1)):] ) & b₂ . 0 = D . 0 & ( for i being Nat holds b₂ . (i + 1) = [:(b₂ . i),(D . (i + 1)):] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines Product_dom RANDOM_3:def 10 :
for D, b₂ being ManySortedSet of NAT holds
( b₂ = Product_dom D iff ( b₂ . 0 = D . 0 & ( for i being Nat holds b₂ . (i + 1) = [:(b₂ . 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 b₁ being SigmaField_sequence of D st
for n being Nat holds b₁ . n = Trivial-SigmaField (D . n)

proof end;

uniqueness
for b₁, b₂ being SigmaField_sequence of D st ( for n being Nat holds b₁ . n = Trivial-SigmaField (D . n) ) & ( for n being Nat holds b₂ . n = Trivial-SigmaField (D . n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines Trivial-SigmaField_sequence RANDOM_3:def 12 :
for D being non-empty V26() ManySortedSet of NAT
for b₂ being SigmaField_sequence of D holds
( b₂ = Trivial-SigmaField_sequence D iff for n being Nat holds b₂ . 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 b₁ being ManySortedSet of NAT st
( b₁ . 0 = P . 0 & ( for i being Nat holds b₁ . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b₁ . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of NAT st b₁ . 0 = P . 0 & ( for i being Nat holds b₁ . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b₁ . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) & b₂ . 0 = P . 0 & ( for i being Nat holds b₂ . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b₂ . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) holds
b₁ = b₂

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 b₃ being ManySortedSet of NAT holds
( b₃ = Product-Probability (P,D) iff ( b₃ . 0 = P . 0 & ( for i being Nat holds b₃ . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b₃ . 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;