:: Random Variables and Product of Probability Spaces
:: by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 1, 2012
:: Copyright (c) 2012-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, PROB_1, MEASURE1, PARTFUN1, SUBSET_1, TARSKI,
RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0, XXREAL_1, LOPBAN_1, FUNCT_2, DIST_1,
MSSUBFAM, VALUED_0, MESFUNC1, SUPINF_2, FINSEQ_1, NAT_1, CARD_3, CARD_1,
ZFMISC_1, RPR_1, FINSET_1, PROB_4, EQREL_1, RANDOM_1, RANDOM_2, RANDOM_3,
FUNCOP_1, FINANCE1, PBOOLE, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, PBOOLE, ENUMSET1,
FINSET_1, CARD_1, NUMBERS,
XXREAL_3, XCMPLX_0, XXREAL_0, XXREAL_1, NAT_1, XREAL_0,
VALUED_0, FINSEQ_1, RPR_1, SUPINF_2, PROB_1, PROB_2, MEASURE1, MEASURE6,
MESFUNC1, PROB_4, MESFUNC6, RANDOM_1, DIST_1, RANDOM_2, FINANCE1;
constructors REAL_1, RPR_1, MESFUNC6, MESFUNC3, DIST_1, MEASURE6, INTEGRA2,
PROB_4, MESFUNC1, RELSET_1, COMSEQ_2, RANDOM_2, FINANCE1, ENUMSET1;
registrations XBOOLE_0, SUBSET_1, NAT_1, XREAL_0, XXREAL_0, ORDINAL1,
MEASURE1, FUNCOP_1, FINANCE1, VALUED_0, FINSEQ_1, FUNCT_2, RELAT_1,
FINSET_1, NUMBERS, PROB_1, PARTFUN1, RELSET_1, CARD_1, PBOOLE, PRE_CIRC;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, FINSET_1;
equalities RPR_1, SUBSET_1, RANDOM_2, PROB_4, PROB_1, RELAT_1, DIST_1,
FINANCE1, CARD_3;
expansions TARSKI, XBOOLE_0, RELAT_1, FINANCE1;
theorems TARSKI, PARTFUN1, FUNCT_1, MESFUNC1, FINSEQ_1, XBOOLE_0, XBOOLE_1,
PROB_2, XXREAL_0, PROB_1, RELAT_1, ZFMISC_1, FUNCT_2, MEASURE1, PROB_4,
MESFUNC6, MEASURE6, ORDINAL1, VALUED_0, RCOMP_1, FUNCOP_1, RANDOM_1,
FINANCE1;
schemes FUNCT_1, FUNCT_2, NAT_1, RECDEF_1;
begin :: Random Variables
reserve Omega, Omega1, Omega2 for non empty set;
reserve Sigma for SigmaField of Omega;
reserve S1 for SigmaField of Omega1;
reserve S2 for SigmaField of Omega2;
theorem Th1:
for B being non empty set, f being Function holds
f " (union B)
= union the set of all f "Y where Y is Element of B
proof
let B be non empty set, f be Function;
set Z = the set of all f "Y where Y is Element of B ;
thus f " (union B) c= union Z
proof
let x be object;
assume A1: x in f " (union B);
then f . x in union B by FUNCT_1:def 7;
then consider Y being set such that
A2: f . x in Y and
A3: Y in B by TARSKI:def 4;
reconsider Y as Element of B by A3;
x in dom f by A1, FUNCT_1:def 7; then
A4: x in f " Y by A2,FUNCT_1:def 7;
f " Y in Z;
hence x in union Z by A4,TARSKI:def 4;
end;
let x be object;
assume x in union Z;
then consider Y being set such that
A5: x in Y and
A6: Y in Z by TARSKI:def 4;
consider D be Element of B such that
A7: Y = f " D by A6;
f " D c= f "(union B) by RELAT_1:143,ZFMISC_1:74;
hence x in f "(union B) by A5,A7;
end;
theorem Th2:
for f be Function of Omega1,Omega2,
B be SetSequence of Omega2,
D be SetSequence of Omega1
st for n be Element of NAT holds D.n = f "(B.n) holds
f"(Union B) = Union D
proof
let f be Function of Omega1,Omega2,
B be SetSequence of Omega2,
D be SetSequence of Omega1;
assume A1: for n be Element of NAT holds D.n = f "(B.n);
set Z = rng D;
set Q = the set of all f "Y where Y is Element of (rng B) ;
for x be object holds x in Z iff x in Q
proof
let x be object;
hereby assume x in Z;
then consider n be Element of NAT such that
A2: x = D.n by FUNCT_2:113;
A3: x = f "(B.n) by A1,A2;
B.n in rng B by FUNCT_2:112;
hence x in Q by A3;
end;
assume x in Q;
then consider Y be Element of (rng B) such that
A4:x =f "Y;
consider n be Element of NAT such that
A5: Y=B.n by FUNCT_2:113;
x =D.n by A1,A4,A5;
hence x in Z by FUNCT_2:112;
end;
then Z = Q by TARSKI:2;
hence thesis by Th1;
end;
theorem Th3:
for f be Function of Omega1,Omega2,
B be SetSequence of Omega2,
D be SetSequence of Omega1
st for n be Element of NAT holds D.n = f "(B.n) holds
f"(Intersection B) = Intersection D
proof
let f be Function of Omega1,Omega2,
B be SetSequence of Omega2,
D be SetSequence of Omega1;
assume A1:for n be Element of NAT holds D.n = f "(B.n);
set Z = the set of all f "(B.n) where n is Element of NAT;
set Q = the set of all f "Y where Y is Element of (rng B) ;
set E = Complement D;
A2: for n be Element of NAT holds E.n = f "((Complement B).n)
proof
let n be Element of NAT;
thus E.n = (D .n)` by PROB_1:def 2
.= (f "(B.n))` by A1
.= f " Omega2 \ (f "(B.n)) by FUNCT_2:40
.= f " ((B.n)` ) by FUNCT_1:69
.= f "((Complement B).n) by PROB_1:def 2;
end;
f"(Intersection B)=f"Omega2 \ f"(union rng (Complement B)) by FUNCT_1:69
.=Omega1 \ f"(Union (Complement B)) by FUNCT_2:40
.=Omega1 \ Union E by Th2,A2
.=Omega1 \ union rng E;
hence thesis;
end;
theorem Th4:
for F being Function of Omega,REAL,
r being Real
st F is Real-Valued-Random-Variable of Sigma
holds F"(].-infty,r.[) in Sigma
proof
let F be Function of Omega,REAL;
let r be Real;
assume F is Real-Valued-Random-Variable of Sigma; then
F is ([#]Sigma)-measurable; then
A2:([#]Sigma) /\ (less_dom (F,r)) in Sigma by MESFUNC6:12;
for z be object holds
z in F"(].-infty,r.[) iff z in ([#]Sigma) /\ (less_dom (F,r))
proof
let z be object;
hereby assume A3: z in F"(].-infty,r.[);
then
A4: z in dom F & F.z in ].-infty,r.[ by FUNCT_1:def 7;
then
F.z in {p where p is Real : -infty<p & p<r } by RCOMP_1:def 2;
then consider w be Real such that
A5: F.z = w & -infty < w & w < r;
z in less_dom (F,r) by A4,A5,MESFUNC1:def 11;
hence z in ([#]Sigma) /\ (less_dom (F,r)) by A3,XBOOLE_0:def 4;
end;
assume z in ([#]Sigma) /\ (less_dom (F,r)); then
A6: z in ([#]Sigma) & z in (less_dom (F,r)) by XBOOLE_0:def 4;
then
A7: z in dom F & F.z < r by MESFUNC1:def 11;
-infty < F.z & F.z < r by XXREAL_0:12,FUNCT_2:5,MESFUNC1:def 11,A6;
then
F.z in {p where p is Real : -infty<p & p<r }; then
F.z in ].-infty,r.[ by RCOMP_1:def 2;
hence z in F"(].-infty,r.[) by A7, FUNCT_1:def 7;
end;
hence thesis by A2,TARSKI:2;
end;
theorem Th5:
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
let F be Function of Omega,REAL;
assume A1: F is Real-Valued-Random-Variable of Sigma;
set S = { x where x is Element of Borel_Sets : F"x is Element of Sigma };
for x be object st x in S holds x in Borel_Sets
proof
let z be object;
assume z in S;
then ex x be Element of Borel_Sets st x=z & F"x is Element of Sigma;
hence z in Borel_Sets;
end; then
A2: S c= Borel_Sets;
set r0 = the Element of REAL;
A3: halfline(r0) in Family_of_halflines;
Family_of_halflines c= sigma(Family_of_halflines) by PROB_1:def 9;
then reconsider y0 = halfline(r0) as Element of Borel_Sets by A3;
F"y0 is Element of Sigma by Th4,A1; then
A4: y0 in S;
A5: for A be Subset of REAL st A in S holds A` in S
proof
let A be Subset of REAL;
assume A in S; then
consider x be Element of Borel_Sets such that
A6: A= x & F"x is Element of Sigma;
A7: F"(REAL \ x) = F"REAL \ F"x by FUNCT_1:69
.= Omega \ F"x by FUNCT_2:40;
REAL is Element of Borel_Sets by PROB_1:5; then
A8: REAL \ x is Element of Borel_Sets by PROB_1:6;
Omega is Element of Sigma by PROB_1:5;
then
Omega \ F"x is Element of Sigma by A6,PROB_1:6;
hence A` in S by A6,A7,A8;
end;
for A1 being SetSequence of REAL
st rng A1 c= S holds Intersection A1 in S
proof
let A1 be SetSequence of REAL;
assume A9: rng A1 c= S;
then A10:
rng A1 c= Borel_Sets by A2; then
A11: Intersection A1 in Borel_Sets by PROB_1:15;
reconsider B1 = Intersection A1
as Element of Borel_Sets by PROB_1:15,A10;
deffunc G(set) = F"(A1.$1);
A12: for n be Element of NAT holds G(n) is Element of Sigma
proof
let n be Element of NAT;
A1.n in rng A1 by FUNCT_2:112; then
A1.n in S by A9; then
ex x be Element of Borel_Sets st
x= A1.n & F"x is Element of Sigma;
hence G(n) is Element of Sigma;
end;
consider D be Function of NAT,Sigma such that
A13:for n be Element of NAT holds D.n = G(n) from FUNCT_2:sch 9(A12);
D in Funcs(NAT,Sigma) by FUNCT_2:8; then
A14:ex f being Function st D = f & dom f = NAT & rng f c= Sigma
by FUNCT_2:def 2;
rng D c= bool Omega;
then reconsider D as SetSequence of Omega by FUNCT_2:6;
A15: Intersection D in Sigma by A14,PROB_1:15;
F"(Intersection A1) = Intersection D by A13,Th3;
hence Intersection A1 in S by A11,A15;
end;
hence S is SigmaField of REAL by PROB_1:15,A4,A5,XBOOLE_1:1,A2;
end;
theorem Th6:
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
let f be Function of Omega,REAL;
assume
A1: f is Real-Valued-Random-Variable of Sigma;
set B
= { x where x is Element of Borel_Sets : f"x is Element of Sigma };
now let z be object;
assume A2: z in Family_of_halflines;
Family_of_halflines c= sigma(Family_of_halflines) by PROB_1:def 9;
then reconsider y = z as Element of Borel_Sets by A2;
consider r be Element of REAL such that
A3: y = halfline(r) by A2;
f"y is Element of Sigma by A1,Th4,A3;
hence z in B;
end; then
A4: Family_of_halflines c= B;
B is SigmaField of REAL by Th5,A1; then
A5: Borel_Sets c= B by A4,PROB_1:def 9;
now let x be object;
assume x in B; then
ex z be Element of Borel_Sets st z=x & f"z is Element of Sigma;
hence x in Borel_Sets;
end;
then B c= Borel_Sets;
hence B= Borel_Sets by A5;
end;
theorem Th7:
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
let f be Function of Omega,REAL;
thus f is (Sigma,Borel_Sets)-random_variable-like implies
f is Real-Valued-Random-Variable of Sigma by FINANCE1:15;
assume
A1: f is Real-Valued-Random-Variable of Sigma;
set B = { x where x is Element of Borel_Sets : f"x is Element of Sigma };
A2:B= Borel_Sets by Th6,A1;
for x being set st x in Borel_Sets holds f"x in Sigma
proof
let x be set;
assume x in Borel_Sets; then
ex z be Element of Borel_Sets st z=x & f"z is Element of Sigma by A2;
hence thesis;
end;
hence thesis;
end;
theorem
for f being Function of Omega,REAL holds
set_of_random_variables_on (Sigma,Borel_Sets) =
Real-Valued-Random-Variables-Set Sigma
proof
let f be Function of Omega,REAL;
for x be object holds x in set_of_random_variables_on (Sigma,Borel_Sets)
iff x in Real-Valued-Random-Variables-Set Sigma
proof
let x be object;
hereby assume x in set_of_random_variables_on (Sigma,Borel_Sets);
then consider f being Function of Omega,REAL such that
A1: x=f & f is (Sigma,Borel_Sets)-random_variable-like;
f is (Sigma,Borel_Sets)-random_variable-like implies
f is Real-Valued-Random-Variable of Sigma by Th7;
hence x in Real-Valued-Random-Variables-Set Sigma by A1;
end;
assume x in Real-Valued-Random-Variables-Set Sigma; then
consider q be Real-Valued-Random-Variable of Sigma such that
A2: x=q;
q is (Sigma,Borel_Sets)-random_variable-like by Th7;
hence x in set_of_random_variables_on (Sigma,Borel_Sets) by A2;
end;
hence thesis by TARSKI:2;
end;
definition
::$CD
end;
registration
let Omega1, Omega2, S1, S2;
cluster (S1,S2)-random_variable-like for Function of Omega1, Omega2;
existence
proof
set F = the Element of set_of_random_variables_on(S1,S2);
F in set_of_random_variables_on(S1,S2);
then ex f be Function of Omega1, Omega2
st F=f & f is (S1,S2)-random_variable-like;
hence thesis;
end;
end;
definition
let Omega1, Omega2, S1, S2;
mode random_variable of S1,S2 is
(S1,S2)-random_variable-like Function of Omega1, Omega2;
end;
theorem
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:
for x be set st x in dom F
ex Omega1, Omega2 be non empty set,
S1 be SigmaField of Omega1, S2 be SigmaField of Omega2,
f be random_variable of S1,S2 st F.x = f;
end;
registration
cluster random_variable_family-like for Function;
existence
proof
set Omega1 = the non empty set;
set S1 = the SigmaField of Omega1;
set M = the random_variable of S1,S1;
set F = {1} --> M;
for x be set st x in dom F holds
ex Omega1, Omega2 be non empty set,
S1 be SigmaField of Omega1, S2 be SigmaField of Omega2,
f be random_variable of S1,S2 st F.x = f by FUNCOP_1:7;
hence thesis by Def2;
end;
end;
definition
mode random_variable_family is random_variable_family-like Function;
end;
reserve F for random_variable of S1,S2;
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:
for x be set st x in dom F ex M being sigma_Measure of S st F.x = M;
end;
registration
let Y be non empty set;
let S be SigmaField of Y;
cluster S-Measure_valued for Function;
existence
proof
set M = the sigma_Measure of S;
set F = {1} --> M;
for x be set st x in dom F holds
ex MM being sigma_Measure of S st F.x = MM by FUNCOP_1:7;
hence thesis by Def3;
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:
for x be set st x in dom F ex P be Probability of S st F.x = P;
end;
registration
let Y be non empty set;
let S be SigmaField of Y;
cluster S-Probability_valued for Function;
existence
proof
set M = the Probability of S;
set F = {1} --> M;
for x be set st x in dom F holds ex P be Probability of S st
F.x = P by FUNCOP_1:7;
hence thesis by Def4;
end;
end;
Lm1: for X,Y be non empty set,
S being SigmaField of Y,
M be 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 X-defined for S-Probability_valued Function;
existence
proof
X --> the Probability of S is S-Probability_valued Function by Lm1;
hence thesis;
end;
end;
registration
let X, Y be non empty set;
let S be SigmaField of Y;
cluster total for X-defined S-Probability_valued Function;
existence
proof
X-->the Probability of S is S-Probability_valued Function by Lm1;
hence thesis;
end;
end;
registration
let Y be non empty set, S be SigmaField of Y;
cluster S-Probability_valued -> S-Measure_valued for Function;
coherence
proof
let F be Function;
assume
A1: F is S-Probability_valued;
let y be set;
assume y in dom F;
then consider P be Probability of S such that
A2: F.y = P by A1;
take P2M(P);
thus thesis by A2;
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:
for x be set st x in dom F
ex Z be Real-Valued-Random-Variable of S st F.x = Z;
end;
registration
let Y be non empty set;
let S be SigmaField of Y;
cluster S-Random-Variable-Family for Function;
existence
proof
set M = the Real-Valued-Random-Variable of S;
set F = {1} --> M;
for x be set st x in dom F holds
ex Z being Real-Valued-Random-Variable of S st F.x = Z by FUNCOP_1:7;
hence thesis by Def5;
end;
end;
theorem
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
let y be Element of S2;
assume A1: y <> {};
set D = {z where z is Element of Omega1: F.z is Element of y};
for x be object holds x in D iff x in F"y
proof
let x be object;
hereby assume x in D;
then consider z be Element of Omega1 such that
A2: x=z & F.z is Element of y;
z in Omega1; then
z in dom F by FUNCT_2:def 1;
hence x in F"y by A2,FUNCT_1:def 7,A1;
end;
assume x in F"y;
then x in dom F & F.x in y by FUNCT_1:def 7;
hence x in D;
end;
hence thesis by TARSKI:2;
end;
theorem
for F be random_variable of S1,S2 holds
{x where x is Subset of Omega1 : ex y be Element of S2 st x =F"y } c= S1 &
{x where x is Subset of Omega1 : ex y be Element of S2 st x =F"y }
is SigmaField of Omega1
proof
let F be random_variable of S1,S2;
set S = {x where x is Subset of Omega1 :
ex y be Element of S2 st x = F"y };
for x be object st x in S holds x in S1
proof
let z be object;
assume z in S;
then consider x be Subset of Omega1 such that
A1: z= x & ex y be Element of S2 st x =F"y;
thus z in S1 by A1,FINANCE1:def 5;
end;
hence A2: S c= S1;
{} is Element of S2 by PROB_1:22; then
A3:F"{} in S;
A4: for A be Subset of Omega1 st A in S holds A` in S
proof
let A be Subset of Omega1;
assume A in S; then
consider x be Subset of Omega1 such that
A5: A= x & ex y be Element of S2 st x =F"y;
consider y be Element of S2 such that
A6: x = F"y by A5;
A7: y` in S2 by PROB_1:def 1;
F"(y`) = F"Omega2 \ F"y by FUNCT_1:69
.= A` by A5,A6,FUNCT_2:40;
hence A` in S by A7;
end;
for A1 being SetSequence of Omega1
st rng A1 c= S holds Intersection A1 in S
proof
let A1 be SetSequence of Omega1;
assume A8: rng A1 c= S;
defpred Q[set,set] means A1.$1 = F"$2 & $2 in S2;
A9: for n be Element of NAT
ex Bn be Element of bool Omega2 st Q[n,Bn]
proof
let n be Element of NAT;
A1.n in rng A1 by FUNCT_2:112; then
A1.n in S by A8; then
consider x be Subset of Omega1 such that
A10: A1.n= x & ex y be Element of S2 st x =F"y;
thus thesis by A10;
end;
consider B being Function of NAT,bool Omega2 such that
A11: for x being Element of NAT
holds Q[x,B.x] from FUNCT_2:sch 3(A9);
reconsider B as SetSequence of bool Omega2;
now let y be object;
assume y in rng B; then
consider x be object such that
A12: x in NAT & B.x = y by FUNCT_2:11;
reconsider x as Element of NAT by A12;
thus y in S2 by A12,A11;
end; then
rng B c= S2; then
reconsider B1 = Intersection B as Element of S2 by PROB_1:15;
F"(B1) = Intersection A1 by Th3,A11;
hence Intersection A1 in S;
end;
hence S is SigmaField of Omega1 by PROB_1:15,A3,A4,A2,XBOOLE_1:1;
end;
Lm2:
for M being Measure of S1,
F be random_variable of S1,S2
ex N be Measure of S2 st for y be Element of S2 holds N.y = M.(F"y)
proof
let M be Measure of S1,
F be random_variable of S1,S2;
deffunc G(set) = M.(F"$1);
A1: for y be set st y in S2 holds G(y) in ExtREAL;
consider N be Function of S2,ExtREAL such that
A2: for y be set st y in S2 holds N.y = G(y) from FUNCT_2:sch 11(A1);
A3: for y be Element of S2 holds N.y = G(y) by A2;
now let A be Element of S2;
F"A in S1 by FINANCE1:def 5; then
0. <= M.(F"A) by MEASURE1:def 2;
hence 0. <= N . A by A2;
end; then
A4: N is nonnegative by MEASURE1:def 2;
now let A,B be Element of S2;
assume A5: A misses B;
A6: F"A /\ F"B = F"(A /\ B) by FUNCT_1:68
.= F"{} by A5
.= {};
A7: F"A in S1 by FINANCE1:def 5;
A8: F"B in S1 by FINANCE1:def 5;
thus N.(A \/ B) = M.(F"(A \/ B)) by A2
.= M.(F"(A) \/ F"(B)) by RELAT_1:140
.= M.(F"(A)) +M.(F"(B)) by A6,A7,A8,MEASURE1:def 8,XBOOLE_0:def 7
.= N.A + M.(F"(B)) by A2
.= N.A + N.B by A2;
end; then
A9: N is additive by MEASURE1:def 8;
N . {} = M.(F"{}) by A2,PROB_1:4
.= 0 by VALUED_0:def 19; then
N is zeroed by VALUED_0:def 19;
hence thesis by A3,A4,A9;
end;
definition
let Omega1,Omega2,S1,S2;
let M be Measure of S1,
F be random_variable of S1,S2;
func image_measure(F,M) -> Measure of S2 means :Def6:
for y be Element of S2 holds it.y = M.(F"y);
existence by Lm2;
uniqueness
proof
let N1,N2 be Measure of S2;
assume A1: for y be Element of S2 holds N1.y = M.(F"y);
assume A2: for y be Element of S2 holds N2.y = M.(F"y);
now let y be Element of S2;
thus N1.y = M.(F"y) by A1
.= N2.y by A2;
end;
hence thesis by FUNCT_2:63;
end;
end;
registration
let Omega1,Omega2,S1,S2;
let M be sigma_Measure of S1,
F be random_variable of S1,S2;
cluster image_measure(F,M) -> sigma-additive;
coherence
proof
set N = image_measure(F,M);
for s2 being Sep_Sequence of S2 holds SUM(N*s2) = N.(union rng s2)
proof
let s2 be Sep_Sequence of S2;
A1:for x, y being object st x <> y holds
(("F)*s2).x misses (("F)*s2) . y
proof
let x, y be object;
assume A2: x <> y;
A3:F"(s2.x) /\ F"(s2.y) = F"(s2.x /\ s2.y) by FUNCT_1:68
.= F"{} by A2,XBOOLE_0:def 7,PROB_2:def 2
.= {};
per cases;
suppose A4: x in dom (("F)*s2) & y in dom (("F)*s2); then
A5: x in dom s2 & s2.x in dom ("F) by FUNCT_1:11;
A6: y in dom s2 & s2.y in dom ("F) by A4,FUNCT_1:11;
A7: (("F)*s2).x =("F).(s2.x) by A4,FUNCT_1:12
.= F"(s2.x) by MEASURE6:def 3,A5;
(("F)*s2).y =("F).(s2.y) by A4,FUNCT_1:12
.= F"(s2.y) by A6,MEASURE6:def 3;
hence (("F)*s2).x misses (("F)*s2) . y by A7,A3;
end;
suppose
not (x in dom (("F)*s2) & y in dom (("F)*s2) );
then (("F)*s2).x = {} or (("F)*s2).y = {} by FUNCT_1:def 2;
hence (("F)*s2).x misses (("F)*s2).y;
end;
end;
s2 in Funcs(NAT,S2) by FUNCT_2:8; then
ex f being Function st s2 = f & dom f = NAT & rng f c= S2
by FUNCT_2:def 2; then
A8: dom s2 = NAT & rng s2 c= S2;
A9: dom ("F) = bool Omega2 by FUNCT_2:def 1; then
A10: dom (("F)*s2) = NAT by A8,RELAT_1:27;
A11: for x be object st x in NAT holds (("F)*s2).x in S1
proof
let x be object;
assume x in NAT; then
reconsider n=x as Element of NAT;
per cases;
suppose A12: n in dom (("F)*s2); then
A13: n in dom s2 & s2.n in dom ("F) by FUNCT_1:11;
(("F)*s2).n =("F).(s2.n) by A12,FUNCT_1:12
.= F"(s2.n) by A13,MEASURE6:def 3;
hence (("F)*s2).x in S1 by FINANCE1:def 5;
end;
suppose not n in dom (("F)*s2); then
(("F)*s2).n = {} by FUNCT_1:def 2;
hence (("F)*s2).x in S1 by PROB_1:4;
end;
end; then
A14:("F)*s2 is Function of NAT, S1 by A10,FUNCT_2:3;
reconsider s1= ("F)*s2 as Sep_Sequence of S1
by A1,PROB_2:def 2,A10,FUNCT_2:3,A11;
A15:SUM(M*s1) = M.(union rng s1) by MEASURE1:def 6;
now let n be Element of NAT;
A16:(M*s1).n =M.(s1.n) by FUNCT_2:15;
A17:(N*s2).n =N.(s2.n) by FUNCT_2:15;
per cases;
suppose A18: n in dom (("F)*s2); then
A19: n in dom s2 & s2.n in dom ("F) by FUNCT_1:11;
A20: s1.n =("F).(s2.n) by A18,FUNCT_1:12
.= F"(s2.n) by A19,MEASURE6:def 3;
thus (M*s1).n =M.(F"(s2.n)) by A20,FUNCT_2:15
.= N.(s2.n) by Def6
.= (N*s2).n by FUNCT_2:15;
end;
suppose A21: not n in dom (("F)*s2);
A22: (M*s1).n =M.({}) by A21,A16,FUNCT_1:def 2
.=0 by VALUED_0:def 19;
A23: not n in dom s2 or not
s2.n in dom ("F) by A21,FUNCT_1:11;
s2.n in S2;
then s2.n = {} by FUNCT_1:def 2,A23,A9;
hence (M*s1).n = (N*s2).n by A22,A17,VALUED_0:def 19;
end;
end; then
A24: M*s1 =N*s2 by FUNCT_2:def 8;
for x be object holds
x in union rng (("F)*s2) iff x in F"((union rng s2))
proof
let x be object;
hereby assume x in union rng (("F)*s2); then
consider Y be set such that
A25: x in Y & Y in rng (("F)*s2) by TARSKI:def 4;
consider n be Element of NAT such that
A26: Y = (("F)*s2).n by A25,A14,FUNCT_2:113;
A27: n in dom s2 & s2.n in dom ("F) by FUNCT_1:11,A10;
A28: (("F)*s2).n =("F).(s2.n) by A10,FUNCT_1:12
.= F"(s2.n) by A27,MEASURE6:def 3;
s2.n c= union rng s2 by ZFMISC_1:74,FUNCT_2:4;
then
F"(s2.n) c= F"(union rng s2) by RELAT_1:143;
hence x in F"(union rng s2) by A25,A26,A28;
end;
assume x in F"((union rng s2)); then
A29: x in dom F & F.x in (union rng s2) by FUNCT_1:def 7;
then consider Z be set such that
A30: F.x in Z & Z in rng s2 by TARSKI:def 4;
consider n be Element of NAT such that
A31: Z = s2.n by A30,FUNCT_2:113;
A32: x in F"Z by A30,FUNCT_1:def 7,A29;
A33:n in dom s2 & s2.n in dom ("F) by FUNCT_1:11,A10;
A34: (("F)*s2).n =("F).(s2.n) by A10,FUNCT_1:12
.= F"(s2.n) by A33,MEASURE6:def 3;
F"Z in rng (("F)*s2) by A31,A10,A34,FUNCT_1:3;
hence x in union rng (("F)*s2) by A32,TARSKI:def 4;
end; then
A35: union rng (("F)*s2) = F"((union rng s2)) by TARSKI:2;
(union rng s2) is Element of S2 by MEASURE1:24;
hence thesis by A15,A24,A35,Def6;
end;
hence thesis by MEASURE1:def 6;
end;
end;
theorem Th12:
for P being Probability of S1,
F being random_variable of S1,S2 holds
(image_measure(F,P2M(P))).Omega2 = 1
proof
let P be Probability of S1,
F be random_variable of S1,S2;
A1: for y be set st y in S2 holds
(image_measure(F,P2M(P))).y = (P2M P).(F"y) by Def6;
thus (image_measure(F,P2M(P))).Omega2
= (P2M(P)).(F"Omega2) by PROB_1:5,A1
.= (P2M(P)).(Omega1) by FUNCT_2:40
.= 1 by PROB_1:def 8;
end;
definition
let Omega1,Omega2,S1,S2;
let P be Probability of S1,
F be random_variable of S1,S2;
func probability(F,P) -> Probability of S2 equals
M2P(image_measure(F,P2M(P)));
coherence;
end;
theorem Th13:
for P being Probability of S1,
F being random_variable of S1,S2 holds
probability(F,P) = image_measure(F,P2M(P))
proof
let P be Probability of S1,
F be random_variable of S1,S2;
(image_measure(F,P2M(P))).Omega2 = 1 by Th12;
hence probability(F,P) = image_measure(F,P2M(P)) by PROB_4:def 2;
end;
theorem Th14:
for P being Probability of S1,
F be random_variable of S1,S2 holds
for y be set st y in S2 holds (probability(F,P)).y = P.(F"y)
proof
let P be Probability of S1, F be random_variable of S1,S2;
let y be set;
assume A1: y in S2;
thus (probability(F,P)).y = (image_measure(F,P2M(P))).y by Th13
.= P.(F"y) by A1,Def6;
end;
theorem Th15:
for F be Function of Omega1, Omega2
holds F is random_variable of
Trivial-SigmaField Omega1, Trivial-SigmaField Omega2
proof
let F be Function of Omega1, Omega2;
set S1 = Trivial-SigmaField Omega1;
set S2 = Trivial-SigmaField Omega2;
for y being set st y in S2 holds F"y in S1;
hence thesis by FINANCE1:def 5;
end;
theorem Th16:
for S be non empty set,
F be non empty FinSequence of S holds
F is random_variable of
Trivial-SigmaField (Seg len F),Trivial-SigmaField (S)
proof
let S be non empty set,
F be non empty FinSequence of S;
reconsider n = len F as non empty Element of NAT;
A1: dom F = Seg n by FINSEQ_1:def 3;
rng F c= S;
hence thesis by Th15,A1,FUNCT_2:2;
end;
theorem Th17:
for V,S be finite non empty set,
G be random_variable of Trivial-SigmaField (V),Trivial-SigmaField (S)
holds
for y be set st y in Trivial-SigmaField (S) holds
(probability(G,Trivial-Probability V)).y = card(G"y)/card(V)
proof
let V,S be finite non empty set,
G be random_variable of Trivial-SigmaField (V),Trivial-SigmaField (S);
now let y be set;
assume A1: y in Trivial-SigmaField (S);
thus (probability(G,Trivial-Probability (V))).y
= (Trivial-Probability (V)).(G"y) by Th14,A1
.= prob(G"y) by RANDOM_1:def 1
.= card(G"y)/card (V);
end;
hence thesis;
end;
theorem
for S be finite non empty set,
s be non empty FinSequence of S
holds
ex G be random_variable of
Trivial-SigmaField (Seg len s),Trivial-SigmaField (S)
st G = s &
for x be set st x in S
holds
(probability(G,Trivial-Probability (Seg len s))).{x}
= FDprobability (x,s)
proof
let S be finite non empty set,
s be non empty FinSequence of S;
reconsider n = len s as non empty Element of NAT;
reconsider G = s as random_variable of
Trivial-SigmaField (Seg len s),Trivial-SigmaField (S) by Th16;
take G;
thus G = s;
let x be set;
assume A1: x in S;
set y = {x};
{x} c= S by A1, ZFMISC_1:31; then
(probability(G,Trivial-Probability (Seg len s))).y
= card(G"y)/card(Seg len s) by Th17
.= card(G"y)/n by FINSEQ_1:57;
hence thesis;
end;
begin :: Product of Probability Spaces
registration
let D be non-empty ManySortedSet of NAT;
let n be Nat;
cluster D.n -> non empty;
correctness
proof
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
D.n1 is non empty set;
hence thesis;
end;
end;
definition
let S, F be ManySortedSet of NAT;
attr F is S -SigmaField_sequence-like means :Def8:
for n be Nat holds F.n is SigmaField of S.n;
end;
registration
let S be ManySortedSet of NAT;
cluster S-SigmaField_sequence-like for ManySortedSet of NAT;
existence
proof
defpred P[set,set] means $2 is SigmaField of S.$1;
set X = union rng S;
A1: for n be Element of NAT ex y be Element of bool bool X st P[n,y]
proof
let n be Element of NAT;
set y = the SigmaField of S.n;
dom S = NAT by PARTFUN1:def 2; then
S.n in rng S by FUNCT_1:3; then
bool (S.n) c= bool X by ZFMISC_1:67,ZFMISC_1:74;
hence thesis;
end;
consider F being Function of NAT,bool bool X such that
A2: for n be Element of NAT holds P[n,F.n] from FUNCT_2:sch 3(A1);
take F;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence F.n is SigmaField of S.n by A2;
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;
redefine func S.n -> SigmaField of D.n; :: redefines . (FUNCT_1, definition)
correctness 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:
for n be Nat holds M.n is Probability of S.n;
end;
registration
let D be non-empty ManySortedSet of NAT;
let S be SigmaField_sequence of D;
cluster S-Probability_sequence-like for ManySortedSet of NAT;
existence
proof
defpred P[set,set] means
ex Dn be non empty set,Sn be SigmaField of Dn
st Dn=D.$1 & Sn=S.$1 & $2 is Probability of Sn;
set X = union rng S;
A1: for n be Element of NAT ex y be Element of PFuncs(X,REAL) st P[n,y]
proof
let n be Element of NAT;
dom S = NAT by PARTFUN1:def 2; then
A2:S.n c= X by ZFMISC_1:74,FUNCT_1:3;
reconsider Sn =S.n as SigmaField of (D.n);
set Mn = the Probability of Sn;
Mn in Funcs((S.n),REAL) by FUNCT_2:8; then
ex f being Function st Mn = f & dom f = S.n & rng f c= REAL
by FUNCT_2:def 2; then
Mn in PFuncs(X,REAL) by PARTFUN1:def 3,A2;
hence thesis;
end;
consider F being Function of NAT,PFuncs(X,REAL) such that
A3: for n be Element of NAT holds P[n,F.n] from FUNCT_2:sch 3(A1);
take F;
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
ex Dn be non empty set,Sn be SigmaField of Dn
st Dn=D.n1 & Sn=S.n1 & F.n1 is Probability of Sn by A3;
hence thesis;
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;
redefine func P.n -> Probability of (S.n); :: redefines . (FUNCT_1, definition)
correctness by Def9;
end;
definition
let D be ManySortedSet of NAT;
func Product_dom(D) -> ManySortedSet of NAT means :Def10:
it.0 = D.0 & for i be Nat holds it.(i+1) = [:it.i, D.(i+1) :];
existence
proof
defpred R[Nat,set,set] means $3 = [: $2, D.($1+1) :];
A1: for n being Nat for x be set ex y being set st R[n,x,y];
consider g be Function such that
A2: dom g = NAT & g.0 = D.0 &
for n being Nat holds R[n,g.n,g.(n+1)] from RECDEF_1:sch 1(A1);
reconsider g as ManySortedSet of NAT by PARTFUN1:def 2,RELAT_1:def 18,A2;
take g;
thus thesis by A2;
end;
uniqueness
proof
let seq1,seq2 be ManySortedSet of NAT;
assume that
A3: seq1.0 = D.0 and
A4: for i be Nat holds seq1.(i+1) = [:seq1.i, D.(i+1) :] and
A5: seq2.0 = D.0 and
A6: for i be Nat holds seq2.(i+1) = [:seq2.i, D.(i+1) :];
A7: dom seq2 = NAT by PARTFUN1:def 2;
defpred P[Nat] means seq1.$1 = seq2.$1;
A8: for k be Nat st P[k] holds P[ k + 1 ]
proof
let k be Nat;
assume
A9: P[k];
thus seq1.(k+1) = [:seq1.k, D.(k+1) :] by A4
.= seq2.(k+1) by A6,A9;
end;
A10: P[0] by A3,A5;
A11: for n be Nat holds P[n] from NAT_1:sch 2(A10,A8);
for n be object st n in dom seq1 holds
seq1.n = seq2.n by A11;
hence seq1 = seq2 by A7,FUNCT_1:2,PARTFUN1:def 2;
end;
end;
theorem Th19:
for D be 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
let D be ManySortedSet of NAT;
thus (Product_dom(D)).0 = D.0 by Def10;
thus
A1:(Product_dom(D)).1
= (Product_dom(D)).( (0 qua Nat ) + 1)
.= [:(Product_dom(D)).0,D.1:] by Def10
.= [:D.0,D.1:] by Def10;
thus
A2:(Product_dom(D)).2 = [:(Product_dom(D)).1,D.(1+1):] by Def10
.= [:D.0,D.1,D.2:] by ZFMISC_1:def 3,A1;
thus (Product_dom(D)).3 = [:(Product_dom(D)).2,D.(2+1):] by Def10
.= [:D.0,D.1,D.2,D.3 :] by ZFMISC_1:def 4,A2;
end;
registration
let D be non-empty ManySortedSet of NAT;
cluster Product_dom(D) -> non-empty;
correctness
proof
set g = Product_dom(D);
defpred P[Nat] means g.$1 is non empty;
D.0 = (Product_dom(D)).0 by Def10; then
A1: P[0];
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
g.(k+1) = [:g.k, D.(k+1) :] by Def10;
hence thesis;
end;
A3: for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
assume not g is non-empty; then
{} in rng g;
then ex x be object st x in dom g & {} = g.x by FUNCT_1:def 3;
hence contradiction by A3;
end;
end;
registration
let D be finite-yielding ManySortedSet of NAT;
cluster Product_dom(D) -> finite-yielding;
correctness
proof
set g = Product_dom(D);
defpred P[Nat] means g.$1 is finite;
D.0 = (Product_dom(D)).0 by Def10; then
A1: P[0];
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
g.(k+1) = [:g.k, D.(k+1) :] by Def10;
hence thesis;
end;
A3: for n be Nat holds P[n] from NAT_1:sch 2(A1,A2);
let x be object;
thus thesis by A3;
end;
end;
definition
let Omega,Sigma;
let P be set;
assume A1: P is Probability of Sigma;
func modetrans(P,Sigma) -> Probability of Sigma equals
:Def11:
P;
correctness by A1;
end;
definition
let D be finite-yielding non-empty ManySortedSet of NAT;
func Trivial-SigmaField_sequence(D) -> SigmaField_sequence of D means
:Def12:
for n be Nat holds it.n = Trivial-SigmaField (D.n);
existence
proof
deffunc F(Nat) = Trivial-SigmaField (D.$1);
consider f be Function such that
A1: dom f = NAT & for x be Element of NAT holds f.x = F(x)
from FUNCT_1:sch 4;
reconsider f as ManySortedSet of NAT
by A1,PARTFUN1:def 2,RELAT_1:def 18;
now let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
f.n1 = Trivial-SigmaField (D.n1) by A1;
hence f.n is SigmaField of D.n;
end;
then reconsider f as SigmaField_sequence of D by Def8;
take f;
now let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
f.n1 = Trivial-SigmaField (D.n1) by A1;
hence f.n = Trivial-SigmaField (D.n);
end;
hence thesis;
end;
uniqueness
proof
let seq1,seq2 be SigmaField_sequence of D;
assume that
A2: for n be Nat holds seq1.n = Trivial-SigmaField D.n and
A3: for n be Nat holds seq2.n = Trivial-SigmaField D.n;
A4: dom seq2 = NAT by PARTFUN1:def 2;
now let n be object;
assume n in dom seq1;
then reconsider i=n as Nat;
thus seq1.n = Trivial-SigmaField (D.i) by A2
.= seq2.n by A3;
end;
hence seq1 = seq2 by A4,FUNCT_1:2,PARTFUN1:def 2;
end;
end;
definition
let D be finite-yielding non-empty ManySortedSet of NAT;
let P be Probability_sequence of Trivial-SigmaField_sequence(D);
let n be Nat;
redefine func P.n -> Probability of Trivial-SigmaField(D.n); :: redefines . (FUNCT_1, definition)
coherence
proof
P.n is Probability of (Trivial-SigmaField_sequence(D)).n;
hence thesis by Def12;
end;
end;
definition
let D be finite-yielding non-empty ManySortedSet of NAT;
let P be Probability_sequence of Trivial-SigmaField_sequence(D);
func Product-Probability(P,D) -> ManySortedSet of NAT means :Def13:
it.0 = P.0 & for i be 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
proof
defpred R[Nat,set,set] means $3=Product-Probability
( (Product_dom(D)).$1,D.($1+1),
modetrans($2,Trivial-SigmaField ((Product_dom(D)).$1)), P.($1+1));
A1: for n being Nat for x be set ex y being set st R[n,x,y];
consider g be Function such that
A2: dom g = NAT & g.0 = P.0 &
for n being Nat holds R[n,g.n,g.(n+1)]
from RECDEF_1:sch 1(A1);
reconsider g as NAT-defined Function by RELAT_1:def 18,A2;
reconsider g as ManySortedSet of NAT by PARTFUN1:def 2,A2;
take g;
thus g.0 = P.0 by A2;
thus thesis by A2;
end;
uniqueness
proof
let seq1,seq2 be ManySortedSet of NAT;
assume that
A3: seq1.0 = P.0 and
A4: for i be Nat holds seq1.(i+1)
= Product-Probability ( (Product_dom(D)).i,D.(i+1),
modetrans(seq1.i,Trivial-SigmaField ((Product_dom(D)).i)), P.(i+1))
and
A5: seq2.0 = P.0 and
A6: for i be Nat holds seq2.(i+1) = Product-Probability
( (Product_dom(D)).i,D.(i+1),
modetrans(seq2.i,Trivial-SigmaField ((Product_dom(D)).i)), P.(i+1));
A7: dom seq2 = NAT by PARTFUN1:def 2;
defpred P[Nat] means seq1.$1 = seq2.$1;
A8: for k be Nat st P[k] holds P[ k + 1 ]
proof
let k be Nat;
assume
A9: P[k];
thus seq1.(k+1) = Product-Probability ( (Product_dom(D)).k,D.(k+1),
modetrans(seq2.k,Trivial-SigmaField ((Product_dom(D)).k)),
P.(k+1)) by A9,A4
.= seq2.(k+1) by A6;
end;
A10: P[0] by A3,A5;
for n be Nat holds P[n] from NAT_1:sch 2(A10,A8); then
for n be object st n in dom seq1 holds seq1.n = seq2.n;
hence seq1 = seq2 by A7,FUNCT_1:2,PARTFUN1:def 2;
end;
end;
theorem Th20:
for D be finite-yielding non-empty ManySortedSet of NAT,
P be Probability_sequence of Trivial-SigmaField_sequence(D),
n be Nat holds
Product-Probability(P,D).n is
Probability of Trivial-SigmaField ((Product_dom(D)).n)
proof
let D be finite-yielding non-empty ManySortedSet of NAT,
P be Probability_sequence of Trivial-SigmaField_sequence(D);
defpred Q[Nat] means Product-Probability(P,D).$1 is
Probability of Trivial-SigmaField ((Product_dom(D)).$1);
A1: Product-Probability(P,D).0 = P.0 by Def13;
D.0 = (Product_dom(D)).0 by Def10; then
A2: Q[0] by A1;
A3: for k be Nat st Q[k] holds Q[ k + 1 ]
proof
let k be Nat;
assume Q[k];
A4: Product-Probability(P,D).(k+1) = Product-Probability
( (Product_dom(D)).k,D.(k+1),
modetrans(Product-Probability(P,D).k,
Trivial-SigmaField ((Product_dom(D)).k)), P.(k+1)) by Def13;
(Product_dom(D)).(k+1) = [:(Product_dom(D)).k,D.(k+1):] by Def10;
hence thesis by A4;
end;
for n be Nat holds Q[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th21:
for D be finite-yielding non-empty ManySortedSet of NAT,
P be Probability_sequence of Trivial-SigmaField_sequence(D),
n be Nat holds
ex Pn be 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
let D be finite-yielding non-empty ManySortedSet of NAT,
P be Probability_sequence of Trivial-SigmaField_sequence(D),
n be Nat;
reconsider Pn = Product-Probability(P,D).n as
Probability of Trivial-SigmaField ((Product_dom(D)).n) by Th20;
take Pn;
thus Pn = Product-Probability(P,D).n;
thus Product-Probability(P,D).(n+1) = Product-Probability
( (Product_dom(D)).n,D.(n+1),
modetrans(Product-Probability(P,D).n,
Trivial-SigmaField ((Product_dom(D)).n)), P.(n+1)) by Def13
.= Product-Probability ( (Product_dom(D)).n,D.(n+1),Pn,P.(n+1))
by Def11;
end;
theorem
for D be finite-yielding non-empty ManySortedSet of NAT,
P be 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 be 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 be 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 be 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
let D be finite-yielding non-empty ManySortedSet of NAT,
P be Probability_sequence of Trivial-SigmaField_sequence(D);
thus Product-Probability(P,D).0 = P.0 by Def13;
A1: (Product_dom(D)).0 = D.0 by Th19;
A2: modetrans(Product-Probability(P,D).0,
Trivial-SigmaField ((Product_dom(D)).0))
= modetrans(P.0,Trivial-SigmaField (D.0)) by A1, Def13
.= P.0 by Def11;
thus Product-Probability(P,D).1
=Product-Probability(P,D).((0 qua Nat)+1)
.= Product-Probability ( (Product_dom(D)).0,D.1,
modetrans(Product-Probability(P,D).0,
Trivial-SigmaField ((Product_dom(D)).0)),P.1) by Def13
.= Product-Probability(D.0,D.1,P.0,P.1) by A2,Th19;
consider P1 be
Probability of Trivial-SigmaField ((Product_dom(D)).1) such that
A3: P1 = Product-Probability(P,D).1
& Product-Probability(P,D).(1+1)
= Product-Probability ( (Product_dom(D)).1,D.(1+1),P1,P.(1+1))
by Th21;
(Product_dom(D)).1 = [:D.0,D.1:] by Th19; then
reconsider P1 as Probability of Trivial-SigmaField ([:D.0,D.1:]);
A4: Product-Probability(P,D).2
= Product-Probability ( [:D.0,D.1:],D.2,P1,P.2) by A3,Th19;
consider P2 be Probability of Trivial-SigmaField ((Product_dom(D)).2)
such that
A5: P2 = Product-Probability(P,D).2
& Product-Probability(P,D).(2+1)
= Product-Probability ( (Product_dom(D)).2,D.(2+1),P2,P.(2+1))
by Th21;
(Product_dom(D)).2 = [:D.0,D.1,D.2:] by Th19;
then reconsider P2 as
Probability of Trivial-SigmaField ([:D.0,D.1,D.2:]);
A6: Product-Probability(P,D).3
= Product-Probability ( [:D.0,D.1,D.2:],D.3,P2,P.3) by A5,Th19;
consider P3 be
Probability of Trivial-SigmaField ((Product_dom(D)).3) such that
A7: P3 = Product-Probability(P,D).3
& Product-Probability(P,D).(3+1)
= Product-Probability ( (Product_dom(D)).3,D.(3+1),P3,P.(3+1))
by Th21;
(Product_dom(D)).3 = [:D.0,D.1,D.2,D.3:] by Th19;
then reconsider P3 as
Probability of Trivial-SigmaField ([:D.0,D.1,D.2,D.3:]);
Product-Probability(P,D).4
= Product-Probability ( [:D.0,D.1,D.2,D.3:],D.4,P3,P.4) by A7,Th19;
hence thesis by A4,A5,A3,A7,A6;
end;