:: 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; 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 :: RANDOM_3:1 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; theorem :: RANDOM_3:2 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; theorem :: RANDOM_3:3 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; theorem :: RANDOM_3:4 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; theorem :: RANDOM_3:5 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; theorem :: RANDOM_3:6 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; theorem :: RANDOM_3:7 for f being Function of Omega,REAL holds f is_random_variable_on Sigma, Borel_Sets iff f is Real-Valued-Random-Variable of Sigma; theorem :: RANDOM_3:8 for f being Function of Omega,REAL holds set_of_random_variables_on (Sigma,Borel_Sets) = Real-Valued-Random-Variables-Set Sigma; definition let Omega1, Omega2, S1, S2; let F be Function of Omega1,Omega2; attr F is (S1,S2)-random_variable-like means :: RANDOM_3:def 1 F is_random_variable_on S1,S2; end; registration let Omega1, Omega2, S1, S2; cluster (S1,S2)-random_variable-like for Function of Omega1, Omega2; 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 :: RANDOM_3:9 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; definition let F be Function; attr F is random_variable_family-like means :: RANDOM_3:def 2 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; 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 :: RANDOM_3:def 3 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; 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 :: RANDOM_3:def 4 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; end; registration let X,Y be non empty set; let S be SigmaField of Y; cluster X-defined for S-Probability_valued Function; end; registration let X, Y be non empty set; let S be SigmaField of Y; cluster total for X-defined S-Probability_valued Function; end; registration let Y be non empty set, S be SigmaField of Y; cluster S-Probability_valued -> S-Measure_valued for Function; 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 :: RANDOM_3:def 5 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; end; theorem :: RANDOM_3:10 for y being Element of S2 st y <> {} holds {z where z is Element of Omega1: F.z is Element of y} = F"y; theorem :: RANDOM_3:11 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; 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 :: RANDOM_3:def 6 for y be Element of S2 holds it.y = M.(F"y); 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; end; theorem :: RANDOM_3:12 for P being Probability of S1, F being random_variable of S1,S2 holds (image_measure(F,P2M(P))).Omega2 = 1; 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 :: RANDOM_3:def 7 M2P(image_measure(F,P2M(P))); end; theorem :: RANDOM_3:13 for P being Probability of S1, F being random_variable of S1,S2 holds probability(F,P) = image_measure(F,P2M(P)); theorem :: RANDOM_3:14 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); theorem :: RANDOM_3:15 for F be Function of Omega1, Omega2 holds F is random_variable of Trivial-SigmaField Omega1, Trivial-SigmaField Omega2; theorem :: RANDOM_3:16 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); theorem :: RANDOM_3:17 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); theorem :: RANDOM_3:18 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); begin :: Product of Probability Spaces registration let D be non-empty ManySortedSet of NAT; let n be Nat; cluster D.n -> non empty; end; definition let S, F be ManySortedSet of NAT; attr F is S -SigmaField_sequence-like means :: RANDOM_3:def 8 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; 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; 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 :: RANDOM_3:def 9 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; 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); end; definition let D be ManySortedSet of NAT; func Product_dom(D) -> ManySortedSet of NAT means :: RANDOM_3:def 10 it.0 = D.0 & for i be Nat holds it.(i+1) = [:it.i, D.(i+1) :]; end; theorem :: RANDOM_3:19 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:]; registration let D be non-empty ManySortedSet of NAT; cluster Product_dom(D) -> non-empty; end; registration let D be finite-yielding ManySortedSet of NAT; cluster Product_dom(D) -> finite-yielding; end; definition let Omega,Sigma; let P be set; assume P is Probability of Sigma; func modetrans(P,Sigma) -> Probability of Sigma equals :: RANDOM_3:def 11 P; end; definition let D be finite-yielding non-empty ManySortedSet of NAT; func Trivial-SigmaField_sequence(D) -> SigmaField_sequence of D means :: RANDOM_3:def 12 for n be Nat holds it.n = Trivial-SigmaField (D.n); 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); 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 :: RANDOM_3:def 13 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)); end; theorem :: RANDOM_3:20 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); theorem :: RANDOM_3:21 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)); theorem :: RANDOM_3:22 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));