:: Random Variables and Product of Probability Spaces :: by Hiroyuki Okazaki and Yasunari Shidama :: :: Received December 1, 2012 :: Copyright (c) 2012-2018 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, 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, PROB_2, 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 consider X being Element of Sigma such that A1: X = Omega & F is_measurable_on X by RANDOM_1:def 2; A2:([#]Sigma) /\ (less_dom (F,r)) in Sigma by A1,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

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 proof let X,Y be non empty set; let S be SigmaField of Y; let M be Probability of S; set F = X --> M; for x be set st x in dom F holds ex P being Probability of S st F.x = P by FUNCOP_1:7; hence thesis; end; 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,Def1,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 Def1,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 Def1,FINANCE1:def 5; A8: F"B in S1 by Def1,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 Def1,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 Def1,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; 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); 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); 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;