Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### $\sigma$-Fields and Probability

**by****Andrzej Nedzusiak**- Received October 16, 1989
- MML identifier: PROB_1

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, ARYTM, SEQ_1, ARYTM_1, SEQ_2, ORDINAL2, ABSVALUE, SETFAM_1, SUBSET_1, FINSUB_1, BOOLE, RELAT_1, FUNCOP_1, TARSKI, PROB_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSUB_1, RELAT_1, FUNCT_1, REAL_1, FUNCT_2, FUNCOP_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SETFAM_1; constructors ABSVALUE, SEQ_2, SETFAM_1, FINSUB_1, FUNCOP_1, XCMPLX_0, MEMBERED, XBOOLE_0; clusters FUNCT_1, XREAL_0, RELSET_1, SUBSET_1, FUNCOP_1, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve Omega for non empty set; reserve X, Y, Z, p,x,y,z for set; reserve D, E for Subset of Omega; reserve f for Function; reserve m,n for Nat; reserve r,r1,r2 for real number; reserve seq for Real_Sequence; ::::::::::::::::::::::::::::::::::::::: :: corrolaries from other articles :: ::::::::::::::::::::::::::::::::::::::: canceled; theorem :: PROB_1:2 for r,r2 st 0 <= r holds r2 - r <= r2; theorem :: PROB_1:3 for r,seq st (ex n st for m st n <= m holds seq.m = r) holds seq is convergent & lim seq = r; ::::::::::::::::::::::::::::::::::::::::::::::::::::: :: DEFINITION AND BASIC PROPERTIES OF :: :: a field of subsets of given nonempty set Omega. :: ::::::::::::::::::::::::::::::::::::::::::::::::::::: definition let X be set; let IT be Subset-Family of X; attr IT is compl-closed means :: PROB_1:def 1 for A being Subset of X st A in IT holds A` in IT; end; definition let X be set; cluster non empty compl-closed cap-closed Subset-Family of X; end; definition let X be set; mode Field_Subset of X is non empty compl-closed cap-closed Subset-Family of X; end; reserve F for Field_Subset of X; theorem :: PROB_1:4 for A,B being Subset of X holds {A,B} is Subset-Family of X; canceled; theorem :: PROB_1:6 ex A being Subset of X st A in F; canceled 2; theorem :: PROB_1:9 for A, B being set st A in F & B in F holds A \/ B in F; theorem :: PROB_1:10 {} in F; theorem :: PROB_1:11 X in F; theorem :: PROB_1:12 for A,B being Subset of X holds A in F & B in F implies A \ B in F; theorem :: PROB_1:13 for A, B being set holds (A \ B) misses B & (A in F & B in F implies (A \ B) \/ B in F); theorem :: PROB_1:14 { {}, X } is Field_Subset of X; theorem :: PROB_1:15 bool X is Field_Subset of X; theorem :: PROB_1:16 { {} , X } c= F & F c= bool X; canceled; theorem :: PROB_1:18 (for p st p in [:NAT,{X}:] ex x,y st [x,y]=p) & (for x,y,z st [x,y] in [:NAT,{X}:] & [x,z] in [:NAT,{X}:] holds y=z); theorem :: PROB_1:19 ex f st dom f = NAT & for n holds f.n = X; definition let X be set; mode SetSequence of X is Function of NAT, bool X; end; reserve ASeq,BSeq for SetSequence of Omega; reserve A1 for SetSequence of X; canceled; theorem :: PROB_1:21 ex A1 st for n holds A1.n = X; theorem :: PROB_1:22 for A, B being Subset of X ex A1 st (A1.0 = A & for n st n <> 0 holds A1.n = B); definition let X,A1,n; redefine func A1.n -> Subset of X; end; theorem :: PROB_1:23 union rng A1 is Subset of X; definition let f be Function; canceled; func Union f -> set equals :: PROB_1:def 3 union rng f; end; definition let X be set, A1 be SetSequence of X; redefine func Union A1 -> Subset of X; end; canceled; theorem :: PROB_1:25 x in Union A1 iff ex n st x in A1.n; theorem :: PROB_1:26 ex B1 being SetSequence of X st for n holds B1.n = (A1.n)`; definition let X be set, A1 be SetSequence of X; func Complement A1 -> SetSequence of X means :: PROB_1:def 4 for n holds it.n = (A1.n)`; end; definition let X be set, A1 be SetSequence of X; func Intersection A1 -> Subset of X equals :: PROB_1:def 5 (Union Complement A1)`; end; canceled 2; theorem :: PROB_1:29 x in Intersection A1 iff for n holds x in A1.n; theorem :: PROB_1:30 for A, B being Subset of X holds (A1.0 = A & for n st n <> 0 holds A1.n = B) implies Intersection A1 = A /\ B; theorem :: PROB_1:31 Complement Complement A1 = A1; definition let X,A1; attr A1 is non-increasing means :: PROB_1:def 6 for n,m st n <= m holds A1.m c= A1.n; attr A1 is non-decreasing means :: PROB_1:def 7 for n,m st n <= m holds A1.n c= A1.m; end; definition let X be set; mode SigmaField of X -> non empty Subset-Family of X means :: PROB_1:def 8 (for A1 being SetSequence of X st (for n holds A1.n in it) holds Intersection A1 in it) & (for A being Subset of X st A in it holds A` in it); end; theorem :: PROB_1:32 for S being non empty set holds S is SigmaField of X iff (S c= bool X) & (for A1 being SetSequence of X st (for n holds A1.n in S) holds Intersection A1 in S) & (for A being Subset of X st A in S holds A` in S); canceled 2; theorem :: PROB_1:35 Y is SigmaField of X implies Y is Field_Subset of X; definition let X be set; cluster -> cap-closed compl-closed SigmaField of X; end; reserve Sigma for SigmaField of Omega; reserve Si for SigmaField of X; canceled 2; theorem :: PROB_1:38 ex A being Subset of X st A in Si; canceled 2; theorem :: PROB_1:41 for A,B being Subset of X st A in Si & B in Si holds A \/ B in Si; theorem :: PROB_1:42 {} in Si; theorem :: PROB_1:43 X in Si; theorem :: PROB_1:44 for A,B being Subset of X st A in Si & B in Si holds A \ B in Si; :: sequences of elements of given sigma-field (subsets of given nonempty set :: Omega) Sigma are introduced; also notion of Event from this sigma-field is :: introduced; then some previous theorems are reformulated in language of :: these notions. definition let X be set, Si be SigmaField of X; mode SetSequence of Si -> SetSequence of X means :: PROB_1:def 9 for n holds it.n in Si; end; canceled; theorem :: PROB_1:46 for ASeq being SetSequence of Si holds Union ASeq in Si; definition let X be set, F be SigmaField of X; mode Event of F -> Subset of X means :: PROB_1:def 10 it in F; end; canceled; theorem :: PROB_1:48 x in Si implies x is Event of Si; theorem :: PROB_1:49 for A,B being Event of Si holds A /\ B is Event of Si; theorem :: PROB_1:50 for A being Event of Si holds A` is Event of Si; theorem :: PROB_1:51 for A,B being Event of Si holds A \/ B is Event of Si; theorem :: PROB_1:52 {} is Event of Si; theorem :: PROB_1:53 X is Event of Si; theorem :: PROB_1:54 for A,B being Event of Si holds A \ B is Event of Si; definition let X,Si; cluster empty Event of Si; end; definition let X,Si; func [#] Si -> Event of Si equals :: PROB_1:def 11 X; end; definition let X,Si; let A,B be Event of Si; redefine func A /\ B -> Event of Si; func A \/ B -> Event of Si; func A \ B -> Event of Si; end; canceled 2; theorem :: PROB_1:57 ASeq is SetSequence of Sigma iff for n holds ASeq.n is Event of Sigma; theorem :: PROB_1:58 ASeq is SetSequence of Sigma implies Union ASeq is Event of Sigma; :: DEFINITION OF sigma-ADDITIVE PROBABILITY reserve A, B for Event of Sigma, ASeq for SetSequence of Sigma; theorem :: PROB_1:59 ex f st (dom f = Sigma & for D st D in Sigma holds (p in D implies f.D = 1) & (not p in D implies f.D = 0)); reserve P for Function of Sigma,REAL; theorem :: PROB_1:60 ex P st (for D st D in Sigma holds (p in D implies P.D = 1) & (not p in D implies P.D = 0)); canceled; theorem :: PROB_1:62 P * ASeq is Real_Sequence; definition let Omega,Sigma,ASeq,P; redefine func P * ASeq -> Real_Sequence; end; definition let Omega,Sigma,P,A; redefine func P.A -> Real; end; definition let Omega,Sigma; canceled; mode Probability of Sigma -> Function of Sigma,REAL means :: PROB_1:def 13 (for A holds 0 <= it.A) & (it.Omega = 1) & (for A,B st A misses B holds it.(A \/ B) = it.A + it.B) & (for ASeq st ASeq is non-increasing holds (it * ASeq is convergent & lim (it * ASeq) = it.Intersection ASeq)); end; reserve P for Probability of Sigma; canceled; theorem :: PROB_1:64 P.{} = 0; canceled; theorem :: PROB_1:66 P.([#] Sigma) = 1; theorem :: PROB_1:67 P.(([#] Sigma) \ A) + P.A = 1; theorem :: PROB_1:68 P.(([#] Sigma) \ A) = 1 - P.A; theorem :: PROB_1:69 A c= B implies P.(B \ A) = P.B - P.A; theorem :: PROB_1:70 A c= B implies P.A <= P.B; theorem :: PROB_1:71 P.A <= 1; theorem :: PROB_1:72 P.(A \/ B) = P.A + P.(B \ A); theorem :: PROB_1:73 P.(A \/ B) = P.A + P.(B \ (A /\ B)); theorem :: PROB_1:74 P.(A \/ B) = P.A + P.B - P.(A /\ B); theorem :: PROB_1:75 P.(A \/ B) <= P.A + P.B; :: definition of sigma-field generated by families :: of subsets of given set and family of Borel Sets reserve D for Subset of REAL; reserve S for Subset of bool Omega; theorem :: PROB_1:76 bool Omega is SigmaField of Omega; definition let Omega; let X be Subset of bool Omega; func sigma(X) -> SigmaField of Omega means :: PROB_1:def 14 X c= it & for Z st (X c= Z & Z is SigmaField of Omega) holds it c= Z; end; definition let r; func halfline(r) -> Subset of REAL equals :: PROB_1:def 15 {r1 where r1 is Element of REAL: r1 < r}; end; definition func Family_of_halflines -> Subset of bool REAL equals :: PROB_1:def 16 {D: ex r st D = halfline(r)}; end; definition func Borel_Sets -> SigmaField of REAL equals :: PROB_1:def 17 sigma(Family_of_halflines); end;

Back to top