:: Random Variables and Product of Probability Spaces :: by Hiroyuki Okazaki and Yasunari Shidama :: :: Received December 1, 2012 :: Copyright (c) 2012 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 FUNCT317A: for B being non empty set, f being Function holds f " (union B) = union {f "Y where Y is Element of B :not contradiction} proof let B be non empty set, f be Function; set Z = {f "Y where Y is Element of B :not contradiction}; thus f " (union B) c= union Z proof let x be element; assume A3: x in f " (union B); then f . x in union B by FUNCT_1:def 7; then consider Y being set such that A4: f . x in Y and A5: Y in B by TARSKI:def 4; reconsider Y as Element of B by A5; x in dom f by A3, FUNCT_1:def 7; then A9: x in f " Y by A4,FUNCT_1:def 7; f " Y in Z; hence x in union Z by A9,TARSKI:def 4; end; let x be element; assume x in union Z; then consider Y being set such that A4: x in Y and A5: Y in Z by TARSKI:def 4; consider D be Element of B such that A6: Y = f " D by A5; f " D c= f "(union B) by RELAT_1:143,ZFMISC_1:74; hence x in f "(union B) by A4,A6; end; theorem FUNCT317B: 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 AS: for n be Element of NAT holds D.n = f "(B.n); set Z = rng D; set Q = {f "Y where Y is Element of (rng B) :not contradiction}; for x be element holds x in Z iff x in Q proof let x be element; hereby assume x in Z; then consider n be Element of NAT such that A0: x = D.n by FUNCT_2:113; A1: x = f "(B.n) by AS,A0; B.n in rng B by FUNCT_2:112; hence x in Q by A1; end; assume x in Q; then consider Y be Element of (rng B) such that A3:x =f "Y; consider n be Element of NAT such that A4: Y=B.n by FUNCT_2:113; x =D.n by AS,A3,A4; hence x in Z by FUNCT_2:112; end; then Z = Q by TARSKI:2; hence thesis by FUNCT317A; end; theorem FUNCT317C: 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 AS:for n be Element of NAT holds D.n = f "(B.n); set Z = {f "(B.n) where n is Element of NAT:not contradiction}; set Q = {f "Y where Y is Element of (rng B) :not contradiction}; set E = Complement D; A1: 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 AS .= 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 FUNCT317B,A1 .=Omega1 \ union rng E; hence thesis; end; theorem LMYY1: 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 X1: X = Omega & F is_measurable_on X by RANDOM_1:def 2; X3:([#]Sigma) /\ (less_dom (F,r)) in Sigma by X1,MESFUNC6:12; for z be element holds z in F"(].-infty,r.[) iff z in ([#]Sigma) /\ (less_dom (F,r)) proof let z be element; hereby assume A1: z in F"(].-infty,r.[); then A2: 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 Def06; 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 :Def01: 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 Def01; 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 :Def02: 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 Def02; end; end; LM2: 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 LM2; 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 LM2; 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 P3: F.y = P by A1; take P2M(P); thus thesis by P3; 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 :Def03: 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 Def03; 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 C2: y <> {}; set D = {z where z is Element of Omega1: F.z is Element of y}; for x be element holds x in D iff x in F"y proof let x be element; 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,C2; 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 element st x in S holds x in S1 proof let z be element; assume z in S; then consider x be Subset of Omega1 such that A0: z= x & ex y be Element of S2 st x =F"y; thus z in S1 by A0,Def05,FINANCE1:def 5; end; hence P00: S c= S1; {} is Element of S2 by PROB_1:22; then P1:F"{} in S; P2: 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 Q0: A= x & ex y be Element of S2 st x =F"y; consider y be Element of S2 such that Q1: x = F"y by Q0; Q4: y` in S2 by PROB_1:def 1; F"(y`) = F"Omega2 \ F"y by FUNCT_1:69 .= A` by Q0,Q1,FUNCT_2:40; hence A` in S by Q4; 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 R1: rng A1 c= S; defpred Q[set,set] means A1.$1 = F"$2 & $2 in S2; R2: 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 R1; then consider x be Subset of Omega1 such that Q0: A1.n= x & ex y be Element of S2 st x =F"y; thus thesis by Q0; end; consider B being Function of NAT,bool Omega2 such that R3: for x being Element of NAT holds Q[x,B.x] from FUNCT_2:sch 3(R2); reconsider B as SetSequence of bool Omega2; now let y be element; assume y in rng B; then consider x be element such that R4: x in NAT & B.x = y by FUNCT_2:11; reconsider x as Element of NAT by R4; thus y in S2 by R4,R3; end; then rng B c= S2; then reconsider B1 = Intersection B as Element of S2 by PROB_1:15; F"(B1) = Intersection A1 by FUNCT317C,R3; hence Intersection A1 in S; end; hence S is SigmaField of Omega1 by PROB_1:15,P1,P2,P00,XBOOLE_1:1; end; LM6: 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); P1: for y be set st y in S2 holds G(y) in ExtREAL; consider N be Function of S2,ExtREAL such that p2: for y be set st y in S2 holds N.y = G(y) from FUNCT_2:sch 12(P1); P2: for y be Element of S2 holds N.y = G(y) by p2; now let A be Element of S2; F"A in S1 by Def05,FINANCE1:def 5; then 0. <= M.(F"A) by MEASURE1:def 2; hence 0. <= N . A by p2; end; then P3: N is nonnegative by MEASURE1:def 2; now let A,B be Element of S2; assume ASP30: A misses B; X0: F"A /\ F"B = F"(A /\ B) by FUNCT_1:68 .= F"{} by ASP30 .= {}; X1: F"A in S1 by Def05,FINANCE1:def 5; X2: F"B in S1 by Def05,FINANCE1:def 5; thus N.(A \/ B) = M.(F"(A \/ B)) by p2 .= M.(F"(A) \/ F"(B)) by RELAT_1:140 .= M.(F"(A)) +M.(F"(B)) by X0,X1,X2,MEASURE1:def 3,XBOOLE_0:def 7 .= N.A + M.(F"(B)) by p2 .= N.A + N.B by p2; end; then P4: N is additive by MEASURE1:def 3; N . {} = M.(F"{}) by p2,PROB_1:4 .= 0 by VALUED_0:def 19; then N is zeroed by VALUED_0:def 19; hence thesis by P2,P3,P4; 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 :defIM2: for y be Element of S2 holds it.y = M.(F"y); existence by LM6; 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; Q1:for x, y being element st x <> y holds (("F)*s2).x misses (("F)*s2) . y proof let x, y be element; assume E3: x <> y; E4:F"(s2.x) /\ F"(s2.y) = F"(s2.x /\ s2.y) by FUNCT_1:68 .= F"{} by E3,XBOOLE_0:def 7,PROB_2:def 2 .= {}; per cases; suppose C1: x in dom (("F)*s2) & y in dom (("F)*s2); then C11: x in dom s2 & s2.x in dom ("F) by FUNCT_1:11; CD12: y in dom s2 & s2.y in dom ("F) by C1,FUNCT_1:11; E6: (("F)*s2).x =("F).(s2.x) by C1,FUNCT_1:12 .= F"(s2.x) by MEASURE6:def 3,C11; (("F)*s2).y =("F).(s2.y) by C1,FUNCT_1:12 .= F"(s2.y) by CD12,MEASURE6:def 3; hence (("F)*s2).x misses (("F)*s2) . y by E6,E4; 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 Q2: dom s2 = NAT & rng s2 c= S2; Q4: dom ("F) = bool Omega2 by FUNCT_2:def 1; then Q5: dom (("F)*s2) = NAT by Q2,RELAT_1:27; U1P: for x be set st x in NAT holds (("F)*s2).x in S1 proof let x be set; assume x in NAT; then reconsider n=x as Element of NAT; per cases; suppose C1: n in dom (("F)*s2); then CD11: n in dom s2 & s2.n in dom ("F) by FUNCT_1:11; (("F)*s2).n =("F).(s2.n) by C1,FUNCT_1:12 .= F"(s2.n) by CD11,MEASURE6:def 3; hence (("F)*s2).x in S1 by Def05,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 U1:("F)*s2 is Function of NAT, S1 by Q5,FUNCT_2:3; reconsider s1= ("F)*s2 as Sep_Sequence of S1 by Q1,PROB_2:def 2,Q5,FUNCT_2:3,U1P; Q8:SUM(M*s1) = M.(union rng s1) by MEASURE1:def 6; now let n be Element of NAT; X1:(M*s1).n =M.(s1.n) by FUNCT_2:15; X2:(N*s2).n =N.(s2.n) by FUNCT_2:15; per cases; suppose C1: n in dom (("F)*s2); then CD11: n in dom s2 & s2.n in dom ("F) by FUNCT_1:11; E6: s1.n =("F).(s2.n) by C1,FUNCT_1:12 .= F"(s2.n) by CD11,MEASURE6:def 3; thus (M*s1).n =M.(F"(s2.n)) by E6,FUNCT_2:15 .= N.(s2.n) by defIM2 .= (N*s2).n by FUNCT_2:15; end; suppose C2: not n in dom (("F)*s2); D1: (M*s1).n =M.({}) by C2,X1,FUNCT_1:def 2 .=0 by VALUED_0:def 19; C4: not n in dom s2 or not s2.n in dom ("F) by C2,FUNCT_1:11; s2.n in S2; then s2.n = {} by FUNCT_1:def 2,C4,Q4; hence (M*s1).n = (N*s2).n by D1,X2,VALUED_0:def 19; end; end; then Q9: M*s1 =N*s2 by FUNCT_2:def 8; for x be element holds x in union rng (("F)*s2) iff x in F"((union rng s2)) proof let x be element; hereby assume x in union rng (("F)*s2); then consider Y be set such that A2: x in Y & Y in rng (("F)*s2) by TARSKI:def 4; consider n be Element of NAT such that A3: Y = (("F)*s2).n by A2,U1,FUNCT_2:113; CD11: n in dom s2 & s2.n in dom ("F) by FUNCT_1:11,Q5; E6: (("F)*s2).n =("F).(s2.n) by Q5,FUNCT_1:12 .= F"(s2.n) by CD11,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 A2,A3,E6; end; assume x in F"((union rng s2)); then A2: x in dom F & F.x in (union rng s2) by FUNCT_1:def 7; then consider Z be set such that A3: F.x in Z & Z in rng s2 by TARSKI:def 4; consider n be Element of NAT such that A4: Z = s2.n by A3,FUNCT_2:113; A5: x in F"Z by A3,FUNCT_1:def 7,A2; CD11:n in dom s2 & s2.n in dom ("F) by FUNCT_1:11,Q5; E6: (("F)*s2).n =("F).(s2.n) by Q5,FUNCT_1:12 .= F"(s2.n) by CD11,MEASURE6:def 3; F"Z in rng (("F)*s2) by A4,Q5,E6,FUNCT_1:3; hence x in union rng (("F)*s2) by A5,TARSKI:def 4; end; then Q10: union rng (("F)*s2) = F"((union rng s2)) by TARSKI:2; (union rng s2) is Element of S2 by MEASURE1:24; hence thesis by Q8,Q9,Q10,defIM2; end; hence thesis by MEASURE1:def 6; end; end; theorem LM8: 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; A: for y be set st y in S2 holds (image_measure(F,P2M(P))).y = (P2M P).(F"y) by defIM2; thus (image_measure(F,P2M(P))).Omega2 = (P2M(P)).(F"Omega2) by PROB_1:5,A .= (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 LM9: 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 LM8; hence probability(F,P) = image_measure(F,P2M(P)) by PROB_4:def 2; end; theorem LM10: 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 LM9 .= P.(F"y) by A1,defIM2; end; theorem LM11: 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 Def05,FINANCE1:def 5; end; theorem LM12: 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; P1: dom F = Seg n by FINSEQ_1:def 3; rng F c= S; hence thesis by LM11,P1,FUNCT_2:2; end; theorem LM13: 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 LM10,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, x be set st x in S ex G be random_variable of Trivial-SigmaField (Seg len s),Trivial-SigmaField (S) st G = s & (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, x be set; assume AS: x in 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 LM12; take G; thus G = s; set y = {x}; {x} c= S by AS, ZFMISC_1:31; then (probability(G,Trivial-Probability (Seg len s))).y = card(G"y)/card(Seg len s) by LM13 .= 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 :SigmaSeq: 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; P1: 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 P2: for n be Element of NAT holds P[n,F.n] from FUNCT_2:sch 3(P1); take F; let n be Nat; n in NAT by ORDINAL1:def 12; hence F.n is SigmaField of S.n by P2; 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 SigmaSeq; 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 :ProbSeq: 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; P1: 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 X3: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,X3; hence thesis; end; consider F being Function of NAT,PFuncs(X,REAL) such that P2: for n be Element of NAT holds P[n,F.n] from FUNCT_2:sch 3(P1); 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 P2; 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 ProbSeq; end; definition let D be ManySortedSet of NAT; func Product_dom(D) -> ManySortedSet of NAT means :proddom: 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 A3A: for i be Nat holds seq1.(i+1) = [:seq1.i, D.(i+1) :] and A4: seq2.0 = D.0 and A4A: for i be Nat holds seq2.(i+1) = [:seq2.i, D.(i+1) :]; D2: dom seq2 = NAT by PARTFUN1:def 2; defpred P[Nat] means seq1.$1 = seq2.$1; A7: for k be Nat st P[k] holds P[ k + 1 ] proof let k be Nat; assume A8: P[k]; thus seq1.(k+1) = [:seq1.k, D.(k+1) :] by A3A .= seq2.(k+1) by A4A,A8; end; A9: P[0] by A3,A4; A10: for n be Nat holds P[n] from NAT_1:sch 2(A9,A7); for n be element st n in dom seq1 holds seq1.n = seq2.n by A10; hence seq1 = seq2 by D2,FUNCT_1:2,PARTFUN1:def 2; end; end; theorem LMproddom1: 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 proddom; thus A2:(Product_dom(D)).1 = (Product_dom(D)).( (0 qua Nat ) + 1) .= [:(Product_dom(D)).0,D.1:] by proddom .= [:D.0,D.1:] by proddom; thus A3:(Product_dom(D)).2 = [:(Product_dom(D)).1,D.(1+1):] by proddom .= [:D.0,D.1,D.2:] by ZFMISC_1:def 3,A2; thus (Product_dom(D)).3 = [:(Product_dom(D)).2,D.(2+1):] by proddom .= [:D.0,D.1,D.2,D.3 :] by ZFMISC_1:def 4,A3; 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 proddom; then A5: P[0]; A6: 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 proddom; hence thesis; end; A7: for n be Nat holds P[n] from NAT_1:sch 2(A5,A6); assume not g is non-empty; then {} in rng g; then ex x be element st x in dom g & {} = g.x by FUNCT_1:def 3; hence contradiction by A7; 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 proddom; then A5: P[0]; A6: 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 proddom; hence thesis; end; A7: for n be Nat holds P[n] from NAT_1:sch 2(A5,A6); let x be element; thus thesis by A7; end; end; definition let Omega,Sigma; let P be set; assume AS: P is Probability of Sigma; func modetrans(P,Sigma) -> Probability of Sigma equals :defmode1: P; correctness by AS; end; definition let D be finite-yielding non-empty ManySortedSet of NAT; func Trivial-SigmaField_sequence(D) -> SigmaField_sequence of D means :TrivialSigmaSeq: 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 P1: 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 P1,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 P1; hence f.n is SigmaField of D.n; end; then reconsider f as SigmaField_sequence of D by SigmaSeq; 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 P1; hence f.n = Trivial-SigmaField (D.n); end; hence thesis; end; uniqueness proof let seq1,seq2 be SigmaField_sequence of D; assume that A3: for n be Nat holds seq1.n = Trivial-SigmaField D.n and A4: for n be Nat holds seq2.n = Trivial-SigmaField D.n; D2: dom seq2 = NAT by PARTFUN1:def 2; now let n be element; assume n in dom seq1; then reconsider i=n as Nat; thus seq1.n = Trivial-SigmaField (D.i) by A3 .= seq2.n by A4; end; hence seq1 = seq2 by D2,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 TrivialSigmaSeq; 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 :prodProb: 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 A3A: 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 A4: seq2.0 = P.0 and A4A: 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)); D2: dom seq2 = NAT by PARTFUN1:def 2; defpred P[Nat] means seq1.$1 = seq2.$1; A7: for k be Nat st P[k] holds P[ k + 1 ] proof let k be Nat; assume A8: 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 A8,A3A .= seq2.(k+1) by A4A; end; A9: P[0] by A3,A4; for n be Nat holds P[n] from NAT_1:sch 2(A9,A7); then for n be element st n in dom seq1 holds seq1.n = seq2.n; hence seq1 = seq2 by D2,FUNCT_1:2,PARTFUN1:def 2; end; end; theorem THprodProb0: 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 prodProb; D.0 = (Product_dom(D)).0 by proddom; then A3: Q[0] by A1; A4: for k be Nat st Q[k] holds Q[ k + 1 ] proof let k be Nat; assume Q[k]; A9: 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 prodProb; (Product_dom(D)).(k+1) = [:(Product_dom(D)).k,D.(k+1):] by proddom; hence thesis by A9; end; for n be Nat holds Q[n] from NAT_1:sch 2(A3,A4); hence thesis; end; theorem THprodProb1: 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 THprodProb0; 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 prodProb .= Product-Probability ( (Product_dom(D)).n,D.(n+1),Pn,P.(n+1)) by defmode1; 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 prodProb; B1: (Product_dom(D)).0 = D.0 by LMproddom1; B2: modetrans(Product-Probability(P,D).0, Trivial-SigmaField ((Product_dom(D)).0)) = modetrans(P.0,Trivial-SigmaField (D.0)) by B1, prodProb .= P.0 by defmode1; 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 prodProb .= Product-Probability(D.0,D.1,P.0,P.1) by B2,LMproddom1; consider P1 be Probability of Trivial-SigmaField ((Product_dom(D)).1) such that B4: 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 THprodProb1; (Product_dom(D)).1 = [:D.0,D.1:] by LMproddom1; then reconsider P1 as Probability of Trivial-SigmaField ([:D.0,D.1:]); T2: Product-Probability(P,D).2 = Product-Probability ( [:D.0,D.1:],D.2,P1,P.2) by B4,LMproddom1; consider P2 be Probability of Trivial-SigmaField ((Product_dom(D)).2) such that B4A: 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 THprodProb1; (Product_dom(D)).2 = [:D.0,D.1,D.2:] by LMproddom1; then reconsider P2 as Probability of Trivial-SigmaField ([:D.0,D.1,D.2:]); T4: Product-Probability(P,D).3 = Product-Probability ( [:D.0,D.1,D.2:],D.3,P2,P.3) by B4A,LMproddom1; consider P3 be Probability of Trivial-SigmaField ((Product_dom(D)).3) such that B4Z: 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 THprodProb1; (Product_dom(D)).3 = [:D.0,D.1,D.2,D.3:] by LMproddom1; 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 B4Z,LMproddom1; hence thesis by T2,B4A,B4,B4Z,T4; end;