:: by Hiroyuki Okazaki and Yasunari Shidama

::

:: Received December 1, 2012

:: Copyright (c) 2012-2018 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 }

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

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

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

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

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

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_random_variable_on Sigma, Borel_Sets iff f is Real-Valued-Random-Variable of Sigma )

for Sigma being SigmaField of Omega

for f being Function of Omega,REAL holds

( f is_random_variable_on Sigma, Borel_Sets 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

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

let Omega1, Omega2 be non empty set ;

let S1 be SigmaField of Omega1;

let S2 be SigmaField of Omega2;

let F be Function of Omega1,Omega2;

end;
let S1 be SigmaField of Omega1;

let S2 be SigmaField of Omega2;

let F be Function of Omega1,Omega2;

:: deftheorem Def1 defines -random_variable-like RANDOM_3:def 1 :

for Omega1, Omega2 being non empty set

for S1 being SigmaField of Omega1

for S2 being SigmaField of Omega2

for F being Function of Omega1,Omega2 holds

( F is S1,S2 -random_variable-like iff F is_random_variable_on S1,S2 );

for Omega1, Omega2 being non empty set

for S1 being SigmaField of Omega1

for S2 being SigmaField of Omega2

for F being Function of Omega1,Omega2 holds

( F is S1,S2 -random_variable-like iff F is_random_variable_on S1,S2 );

registration

let Omega1, Omega2 be non empty set ;

let S1 be SigmaField of Omega1;

let S2 be SigmaField of Omega2;

ex b_{1} being Function of Omega1,Omega2 st b_{1} is S1,S2 -random_variable-like

end;
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 Function of ,;

existence ex b

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

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

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

definition

let F be Function;

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

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;

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

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

definition

let Y be non empty set ;

let S be SigmaField of Y;

let F be Function;

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

for x being set st x in dom F holds

ex M being sigma_Measure of S st F . x = M;

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

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;

existence

ex b_{1} being Function st b_{1} is S -Measure_valued

end;
let S be SigmaField of Y;

existence

ex b

proof end;

definition

let Y be non empty set ;

let S be SigmaField of Y;

let F be Function;

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

for x being set st x in dom F holds

ex P being Probability of S st F . x = P;

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

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;

existence

ex b_{1} being Function st b_{1} is S -Probability_valued

end;
let S be SigmaField of Y;

existence

ex b

proof 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

proof end;

registration

let X, Y be non empty set ;

let S be SigmaField of Y;

existence

ex b_{1} being S -Probability_valued Function st b_{1} is X -defined

end;
let S be SigmaField of Y;

existence

ex b

proof end;

registration

let X, Y be non empty set ;

let S be SigmaField of Y;

existence

ex b_{1} being X -defined S -Probability_valued Function st b_{1} is total

end;
let S be SigmaField of Y;

existence

ex b

proof end;

registration

let Y be non empty set ;

let S be SigmaField of Y;

coherence

for b_{1} being Function st b_{1} is S -Probability_valued holds

b_{1} is S -Measure_valued

end;
let S be SigmaField of Y;

coherence

for b

b

proof end;

definition

let Y be non empty set ;

let S be SigmaField of Y;

let F be Function;

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

for x being set st x in dom F holds

ex Z being Real-Valued-Random-Variable of S st F . x = Z;

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

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;

existence

ex b_{1} being Function st b_{1} is S -Random-Variable-Family

end;
let S be SigmaField of Y;

existence

ex b

proof 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

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 )

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;

ex b_{1} being Measure of S2 st

for y being Element of S2 holds b_{1} . y = M . (F " y)
by Lm2;

uniqueness

for b_{1}, b_{2} being Measure of S2 st ( for y being Element of S2 holds b_{1} . y = M . (F " y) ) & ( for y being Element of S2 holds b_{2} . y = M . (F " y) ) holds

b_{1} = b_{2}

end;
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 for y being Element of S2 holds it . y = M . (F " y);

ex b

for y being Element of S2 holds b

uniqueness

for b

b

proof 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_{7} being Measure of S2 holds

( b_{7} = image_measure (F,M) iff for y being Element of S2 holds b_{7} . y = M . (F " y) );

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

( b

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;

coherence

image_measure (F,M) is sigma-additive

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

coherence

image_measure (F,M) is sigma-additive

proof 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

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;

M2P (image_measure (F,(P2M P))) is Probability of S2 ;

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

M2P (image_measure (F,(P2M P))) is Probability of S2 ;

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

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

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)

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

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

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)

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

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;

correctness

coherence

not D . n is empty ;

end;
let n be Nat;

correctness

coherence

not D . n is empty ;

proof end;

definition

let S, F be ManySortedSet of NAT ;

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

for n being Nat holds F . n is SigmaField of (S . n);

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

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 ;

ex b_{1} being ManySortedSet of NAT st b_{1} is S -SigmaField_sequence-like

end;
cluster Relation-like NAT -defined non empty Function-like total S -SigmaField_sequence-like for ManySortedSet of ;

existence ex b

proof end;

definition

let D be ManySortedSet of NAT ;

mode SigmaField_sequence of D is D -SigmaField_sequence-like ManySortedSet of NAT ;

end;
mode SigmaField_sequence of D is D -SigmaField_sequence-like ManySortedSet of NAT ;

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

definition

let D be non-empty ManySortedSet of NAT ;

let S be SigmaField_sequence of D;

let M be ManySortedSet of NAT ;

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

for n being Nat holds M . n is Probability of S . n;

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

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;

ex b_{1} being ManySortedSet of NAT st b_{1} is S -Probability_sequence-like

end;
let S be SigmaField_sequence of D;

cluster Relation-like NAT -defined non empty Function-like total S -Probability_sequence-like for ManySortedSet of ;

existence ex b

proof 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;
let S be SigmaField_sequence of D;

mode Probability_sequence of S is S -Probability_sequence-like ManySortedSet of NAT ;

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

definition

let D be ManySortedSet of NAT ;

ex b_{1} being ManySortedSet of NAT st

( b_{1} . 0 = D . 0 & ( for i being Nat holds b_{1} . (i + 1) = [:(b_{1} . i),(D . (i + 1)):] ) )

for b_{1}, b_{2} being ManySortedSet of NAT st b_{1} . 0 = D . 0 & ( for i being Nat holds b_{1} . (i + 1) = [:(b_{1} . i),(D . (i + 1)):] ) & b_{2} . 0 = D . 0 & ( for i being Nat holds b_{2} . (i + 1) = [:(b_{2} . i),(D . (i + 1)):] ) holds

b_{1} = b_{2}

end;
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 ( it . 0 = D . 0 & ( for i being Nat holds it . (i + 1) = [:(it . i),(D . (i + 1)):] ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines Product_dom RANDOM_3:def 10 :

for D, b_{2} being ManySortedSet of NAT holds

( b_{2} = Product_dom D iff ( b_{2} . 0 = D . 0 & ( for i being Nat holds b_{2} . (i + 1) = [:(b_{2} . i),(D . (i + 1)):] ) ) );

for D, b

( b

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

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

correctness

coherence

Product_dom D is non-empty ;

end;
correctness

coherence

Product_dom D is non-empty ;

proof end;

registration

let D be V26() ManySortedSet of NAT ;

correctness

coherence

Product_dom D is finite-yielding ;

end;
correctness

coherence

Product_dom D is finite-yielding ;

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

correctness

coherence

P is Probability of Sigma;

by A1;

end;
let Sigma be SigmaField of Omega;

let P be set ;

assume A1: P is Probability of Sigma ;

correctness

coherence

P is Probability of Sigma;

by A1;

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

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 ;

ex b_{1} being SigmaField_sequence of D st

for n being Nat holds b_{1} . n = Trivial-SigmaField (D . n)

for b_{1}, b_{2} being SigmaField_sequence of D st ( for n being Nat holds b_{1} . n = Trivial-SigmaField (D . n) ) & ( for n being Nat holds b_{2} . n = Trivial-SigmaField (D . n) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = Trivial-SigmaField (D . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines Trivial-SigmaField_sequence RANDOM_3:def 12 :

for D being non-empty V26() ManySortedSet of NAT

for b_{2} being SigmaField_sequence of D holds

( b_{2} = Trivial-SigmaField_sequence D iff for n being Nat holds b_{2} . n = Trivial-SigmaField (D . n) );

for D being non-empty V26() ManySortedSet of NAT

for b

( b

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)

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

definition

let D be non-empty V26() ManySortedSet of NAT ;

let P be Probability_sequence of Trivial-SigmaField_sequence D;

ex b_{1} being ManySortedSet of NAT st

( b_{1} . 0 = P . 0 & ( for i being Nat holds b_{1} . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b_{1} . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) )

for b_{1}, b_{2} being ManySortedSet of NAT st b_{1} . 0 = P . 0 & ( for i being Nat holds b_{1} . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b_{1} . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) & b_{2} . 0 = P . 0 & ( for i being Nat holds b_{2} . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b_{2} . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) holds

b_{1} = b_{2}

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

ex b

( b

proof end;

uniqueness for b

b

proof 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_{3} being ManySortedSet of NAT holds

( b_{3} = Product-Probability (P,D) iff ( b_{3} . 0 = P . 0 & ( for i being Nat holds b_{3} . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b_{3} . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) ) );

for D being non-empty V26() ManySortedSet of NAT

for P being Probability_sequence of Trivial-SigmaField_sequence D

for b

( b

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)

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

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

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;