### The Mizar article:

### $\sigma$-Fields and Probability

**by****Andrzej Nedzusiak**

- Received October 16, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: PROB_1
- [ 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; definitions FINSUB_1, TARSKI; theorems TARSKI, ZFMISC_1, FUNCT_1, REAL_1, FUNCT_2, ABSVALUE, SEQ_2, SETFAM_1, SUBSET_1, RELAT_1, RELSET_1, FINSUB_1, FUNCOP_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes FUNCT_2, PARTFUN1; 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 Th2: for r,r2 st 0 <= r holds r2 - r <= r2 proof let r,r2; 0 <= r implies r2 - r <= r2 - 0 by REAL_1:92; hence thesis; end; theorem Th3: for r,seq st (ex n st for m st n <= m holds seq.m = r) holds seq is convergent & lim seq = r proof let r,seq such that A1: ex n st for m st n <= m holds seq.m = r; A2: for r1 st 0 < r1 ex n st for m st n <= m holds abs(seq.m-r)<r1 proof let r1 such that A3: 0 < r1; consider n such that A4: for m st n <= m holds seq.m = r by A1; take n; let m; assume n <= m; then seq.m = r by A4; then seq.m - r = 0 by XCMPLX_1:14; hence thesis by A3,ABSVALUE:7; end; then seq is convergent by SEQ_2:def 6; hence thesis by A2,SEQ_2:def 7; end; ::::::::::::::::::::::::::::::::::::::::::::::::::::: :: 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 :Def1: 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; existence proof reconsider S = bool X as Subset-Family of X by SETFAM_1:def 7; take S; thus S is non empty; thus S is compl-closed proof let A be Subset of X; assume A in S; thus thesis; end; thus S is cap-closed proof let A, B be set; assume A in S & B in S; then A /\ B c= X by XBOOLE_1:108; hence thesis; end; end; 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 Th4: for A,B being Subset of X holds {A,B} is Subset-Family of X proof let A,B be Subset of X; set C = {A,B}; C c= bool X proof let x be set; assume x in C; then x = A or x = B by TARSKI:def 2; hence thesis; end; hence thesis by SETFAM_1:def 7; end; canceled; theorem Th6: ex A being Subset of X st A in F proof consider A being Element of F; A in F & F c= bool X; hence thesis; end; canceled 2; theorem Th9: for A, B being set st A in F & B in F holds A \/ B in F proof let A, B be set; assume that A1: A in F and A2: B in F; reconsider A1 = A, B1 = B as Subset of X by A1,A2; A3: A1` in F by A1,Def1; B1` in F by A2,Def1; then A1` /\ B1` in F by A3,FINSUB_1:def 2; then (A1 \/ B1)` in F by SUBSET_1:29; then (A1 \/ B1)`` in F by Def1; hence thesis; end; theorem Th10: {} in F proof consider A being Subset of X such that A1: A in F by Th6; A2: A` in F by A1,Def1; A misses A` by SUBSET_1:26; then A /\ A` = {} by XBOOLE_0:def 7; hence thesis by A1,A2,FINSUB_1:def 2; end; theorem Th11: X in F proof consider A being Subset of X such that A1: A in F by Th6; A2: A` in F by A1,Def1; A \/ A` = [#] X by SUBSET_1:25 .= X by SUBSET_1:def 4; hence thesis by A1,A2,Th9; end; theorem Th12: for A,B being Subset of X holds A in F & B in F implies A \ B in F proof let A,B be Subset of X; assume A1: A in F; assume B in F; then B` in F by Def1; then A /\ B` in F by A1,FINSUB_1:def 2; hence thesis by SUBSET_1:32; end; theorem for A, B being set holds (A \ B) misses B & (A in F & B in F implies (A \ B) \/ B in F) proof let A, B be set; thus A \ B misses B proof x in A \ B implies not x in B by XBOOLE_0:def 4; hence thesis by XBOOLE_0:3; end; assume A1: A in F & B in F; A \/ B = (A \ B) \/ B by XBOOLE_1:39; hence thesis by A1,Th9; end; theorem { {}, X } is Field_Subset of X proof A1: {} c= X by XBOOLE_1:2; X in bool X by ZFMISC_1:def 1; then reconsider EX = { {}, X } as Subset-Family of X by A1,Th4; A2: now let A,B be set; assume A3: A in EX & B in EX; A4: (A = {} or B = {}) implies A /\ B = {}; (A = X & B = X) implies A /\ B = X; hence A /\ B in EX by A3,A4,TARSKI:def 2; end; now let A be Subset of X; assume A5: A in EX; A = {} implies A = {} X; then A = {} implies A` = [#] X by SUBSET_1:22; then A6: A = {} implies A` = X by SUBSET_1:def 4; A = X implies A = [#] X by SUBSET_1:def 4; then A = X implies A` = {} X by SUBSET_1:21; hence A` in EX by A5,A6,TARSKI:def 2; end; hence thesis by A2,Def1,FINSUB_1:def 2; end; theorem bool X is Field_Subset of X proof reconsider K = bool X as Subset-Family of X by SETFAM_1:def 7; A1: K is compl-closed proof let A be Subset of X; assume A in K; thus thesis; end; K is cap-closed proof let A,B be set; assume A in K & B in K; then A /\ B c= X by XBOOLE_1:108; hence thesis; end; hence thesis by A1; end; theorem { {} , X } c= F & F c= bool X proof A1: {} in F by Th10; X in F by Th11; then x in { {} , X } implies x in F by A1,TARSKI:def 2; hence thesis by TARSKI:def 3; end; canceled; theorem (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) proof for x,y,z st [x,y] in [:NAT,{X}:] & [x,z] in [:NAT,{X}:] holds y=z proof let x,y,z; assume [x,y] in [:NAT,{X}:] & [x,z] in [:NAT,{X}:]; then y in {X} & z in {X} by ZFMISC_1:106; then y = X & z = X by TARSKI:def 1; hence thesis; end; hence thesis by ZFMISC_1:102; end; theorem Th19: ex f st dom f = NAT & for n holds f.n = X proof take f = NAT --> X; thus dom f = NAT by FUNCOP_1:19; let n; thus f.n = X by FUNCOP_1:13; end; 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; Lm1: dom A1 = NAT & for n holds A1.n in bool X by FUNCT_2:def 1; canceled; theorem Th21: ex A1 st for n holds A1.n = X proof consider f such that A1: dom f = NAT & for n holds f.n = X by Th19; for x being set st x in NAT holds f.x in bool X proof X in bool X by ZFMISC_1:def 1; hence thesis by A1; end; then f is SetSequence of X by A1,FUNCT_2:5; hence thesis by A1; end; theorem Th22: for A, B being Subset of X ex A1 st (A1.0 = A & for n st n <> 0 holds A1.n = B) proof let A,B be Subset of X; defpred P[set] means $1 = 0; deffunc F(set) = A; deffunc G(set) = B; ex f being Function st dom f = NAT & for x st x in NAT holds (P[x] implies f.x=F(x)) & (not P[x] implies f.x=G(x)) from LambdaC; then consider f being Function such that A1: dom f = NAT & for x st x in NAT holds (x = 0 implies f.x = A) & (not x = 0 implies f.x = B); A2: A in bool X & B in bool X; for x st x in NAT holds f.x in bool X proof let x; assume A3: x in NAT; per cases; suppose x = 0; hence thesis by A1,A2; suppose x <> 0; hence thesis by A1,A2,A3; end; then reconsider f as SetSequence of X by A1,FUNCT_2:5; take f; thus thesis by A1; end; definition let X,A1,n; redefine func A1.n -> Subset of X; coherence by Lm1; end; theorem Th23: union rng A1 is Subset of X proof for Y st Y in rng A1 holds Y c= X proof let Y; assume Y in rng A1; then consider y such that A1: y in dom A1 & Y = A1.y by FUNCT_1:def 5; reconsider y as Nat by A1,FUNCT_2:def 1; Y = A1.y by A1; hence thesis; end; hence thesis by ZFMISC_1:94; end; definition let f be Function; canceled; func Union f -> set equals :Def3: union rng f; correctness; end; definition let X be set, A1 be SetSequence of X; redefine func Union A1 -> Subset of X; coherence proof Union A1 is Subset of X proof Union A1 = union rng A1 by Def3; hence thesis by Th23; end; hence thesis; end; end; canceled; theorem Th25: x in Union A1 iff ex n st x in A1.n proof set DX = union rng A1; A1: for x holds x in DX iff ex n st x in A1.n proof let x; thus x in DX implies ex n st x in A1.n proof assume x in DX; then consider Y such that A2: x in Y & Y in rng A1 by TARSKI:def 4; consider p such that A3: p in dom A1 & Y = A1.p by A2,FUNCT_1:def 5; p in NAT by A3,FUNCT_2:def 1; hence thesis by A2,A3; end; thus (ex n st x in A1.n) implies x in DX proof given n such that A4: x in A1.n; n in NAT; then n in dom A1 by FUNCT_2:def 1; then A1.n in rng A1 by FUNCT_1:def 5; hence thesis by A4,TARSKI:def 4; end; end; DX = Union A1 by Def3; hence thesis by A1; end; theorem Th26: ex B1 being SetSequence of X st for n holds B1.n = (A1.n)` proof deffunc F(Nat) = (A1.$1)`; ex f being Function of NAT,bool X st for x being Element of NAT holds f.x = F(x) from LambdaD; then consider f being Function of NAT,bool X such that A1: for x being Element of NAT holds f.x = (A1.x)`; take f; thus thesis by A1; end; definition let X be set, A1 be SetSequence of X; func Complement A1 -> SetSequence of X means :Def4: for n holds it.n = (A1.n)`; existence by Th26; uniqueness proof let BSeq,CSeq be SetSequence of X such that A1: for n holds BSeq.n = (A1.n)` and A2: for m holds CSeq.m = (A1.m)`; A3: for x st x in NAT holds BSeq.x = CSeq.x proof let x; assume x in NAT; then reconsider x as Nat; BSeq.x = (A1.x)` by A1 .= CSeq.x by A2; hence thesis; end; NAT = dom BSeq & NAT = dom CSeq by FUNCT_2:def 1; hence thesis by A3,FUNCT_1:9; end; end; definition let X be set, A1 be SetSequence of X; func Intersection A1 -> Subset of X equals :Def5: (Union Complement A1)`; correctness; end; canceled 2; theorem Th29: x in Intersection A1 iff for n holds x in A1.n proof A1: for n holds X \ (Complement A1).n = A1.n proof let n; X \ (Complement A1).n = ((Complement A1).n)` by SUBSET_1:def 5 .= ((A1.n)`)` by Def4 .= A1.n; hence thesis; end; A2: x in (Union Complement A1)` iff x in X \ Union Complement A1 by SUBSET_1:def 5; A3: x in X & not x in Union Complement A1 iff x in X & for n holds not x in (Complement A1).n by Th25; (for n holds (x in X & not x in (Complement A1).n)) iff for n holds x in A1.n proof thus (for n holds (x in X & not x in (Complement A1).n)) implies for n holds x in A1.n proof assume A4: (for n holds (x in X & not x in (Complement A1).n)); let n; x in X & not x in (Complement A1).n by A4; then x in X \ (Complement A1).n by XBOOLE_0:def 4; hence thesis by A1; end; assume A5: for n holds x in A1.n; let n; x in A1.n by A5; then x in X \ (Complement A1).n by A1; hence thesis by XBOOLE_0:def 4; end; hence thesis by A2,A3,Def5,XBOOLE_0:def 4; end; theorem Th30: 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 proof let A, B be Subset of X; assume A1: A1.0 = A & for n st n <> 0 holds A1.n = B; for x holds x in Intersection A1 iff (x in A & x in B) proof let x; thus x in Intersection A1 implies (x in A & x in B) proof assume A2: x in Intersection A1; then x in A1.1 by Th29; hence thesis by A1,A2,Th29; end; assume x in A & x in B; then for n holds x in A1.n by A1; hence thesis by Th29; end; hence thesis by XBOOLE_0:def 3; end; theorem Th31: Complement Complement A1 = A1 proof for n holds ((Complement A1).n)` = A1.n proof let n; A1.n = (A1.n)``; hence thesis by Def4; end; hence thesis by Def4; end; definition let X,A1; attr A1 is non-increasing means :Def6: for n,m st n <= m holds A1.m c= A1.n; attr A1 is non-decreasing means 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 :Def8: (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); existence proof reconsider IT = bool X as non empty Subset-Family of X by SETFAM_1:def 7; take IT; thus thesis; end; end; theorem Th32: 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) proof let S be non empty set; thus S is SigmaField of X implies 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) by Def8; assume A1: 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); then S is Subset-Family of X by SETFAM_1:def 7; hence thesis by A1,Def8; end; canceled 2; theorem Th35: Y is SigmaField of X implies Y is Field_Subset of X proof assume A1: Y is SigmaField of X; for A,B being Subset of X st A in Y & B in Y holds A /\ B in Y proof let A,B be Subset of X such that A2: A in Y & B in Y; consider A1 such that A3: (A1.0 = A & for n st n <> 0 holds A1.n = B) by Th22; A4: Intersection A1 = A /\ B by A3,Th30; for n holds A1.n in Y by A2,A3; hence thesis by A1,A4,Def8; end; then A5: (for A,B being Subset of X holds (Y c= bool X & ((A in Y & B in Y) implies A /\ B in Y) & (A in Y implies A` in Y))) by A1,Def8; reconsider Y' = Y as non empty Subset-Family of X by A1; A6: Y' is compl-closed by A5,Def1; Y is cap-closed proof let A,B be set; assume A7: A in Y & B in Y; then reconsider A' = A, B' = B as Subset of X by A1; consider A1 such that A8: (A1.0 = A' & for n st n <> 0 holds A1.n = B') by Th22; A9: Intersection A1 = A /\ B by A8,Th30; for n holds A1.n in Y by A7,A8; hence thesis by A1,A9,Def8; end; hence thesis by A6; end; definition let X be set; cluster -> cap-closed compl-closed SigmaField of X; coherence by Th35; end; reserve Sigma for SigmaField of Omega; reserve Si for SigmaField of X; canceled 2; theorem ex A being Subset of X st A in Si proof consider A being Element of Si; A in Si & Si c= bool X; hence thesis; end; canceled 2; theorem for A,B being Subset of X st A in Si & B in Si holds A \/ B in Si by Th9; theorem {} in Si by Th10; theorem X in Si by Th11; theorem for A,B being Subset of X st A in Si & B in Si holds A \ B in Si by Th12; :: 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 :Def9: for n holds it.n in Si; existence proof consider A1 being SetSequence of X such that A1: for n holds A1.n = X by Th21; take A1; for n holds A1.n in Si proof let n; A1.n = X by A1; hence thesis by Th11; end; hence thesis; end; end; canceled; theorem Th46: for ASeq being SetSequence of Si holds Union ASeq in Si proof A1: (for n holds A1.n in Si) implies Union Complement A1 in Si proof assume for n holds A1.n in Si; then Intersection A1 in Si by Def8; then (Union Complement A1)` in Si by Def5; then (Union Complement A1)`` in Si by Def8; hence thesis; end; A2: (for n holds A1.n in Si) implies (for n holds (Complement A1).n in Si) proof assume A3: for n holds A1.n in Si; for n holds (Complement A1).n in Si proof let n; A1.n in Si by A3; then (A1.n)` in Si by Def8; hence thesis by Def4; end; hence thesis; end; A4: (for n holds A1.n in Si) implies Union Complement Complement A1 in Si proof assume for n holds A1.n in Si; then for n holds (Complement A1).n in Si by A2; hence thesis by A1; end; A5: for A1 st (for n holds A1.n in Si) holds Union A1 in Si proof let A1; assume for n holds A1.n in Si; then Union Complement Complement A1 in Si by A4; hence thesis by Th31; end; for ASeq being SetSequence of Si holds Union ASeq in Si proof let ASeq be SetSequence of Si; for n holds ASeq.n in Si by Def9; hence thesis by A5; end; hence thesis; end; definition let X be set, F be SigmaField of X; mode Event of F -> Subset of X means :Def10: it in F; existence proof X c= X; then reconsider O = X as Subset of X; take O; thus thesis by Th11; end; end; canceled; theorem x in Si implies x is Event of Si by Def10; theorem Th49: for A,B being Event of Si holds A /\ B is Event of Si proof let A,B be Event of Si; A in Si & B in Si by Def10; then A /\ B in Si by FINSUB_1:def 2; hence thesis by Def10; end; theorem for A being Event of Si holds A` is Event of Si proof let A be Event of Si; A in Si by Def10; then A` in Si by Def8; hence thesis by Def10; end; theorem Th51: for A,B being Event of Si holds A \/ B is Event of Si proof let A,B be Event of Si; A in Si & B in Si by Def10; then A \/ B in Si by Th9; hence thesis by Def10; end; theorem Th52: {} is Event of Si proof {} in Si by Th10; hence thesis by Def10; end; theorem Th53: X is Event of Si proof X in Si by Th11; hence thesis by Def10; end; theorem Th54: for A,B being Event of Si holds A \ B is Event of Si proof let A,B be Event of Si; A in Si & B in Si by Def10; then A \ B in Si by Th12; hence thesis by Def10; end; definition let X,Si; cluster empty Event of Si; existence proof {} is Event of Si by Th52; hence thesis; end; end; definition let X,Si; func [#] Si -> Event of Si equals :Def11: X; coherence by Th53; end; definition let X,Si; let A,B be Event of Si; redefine func A /\ B -> Event of Si; coherence by Th49; func A \/ B -> Event of Si; coherence by Th51; func A \ B -> Event of Si; coherence by Th54; end; canceled 2; theorem ASeq is SetSequence of Sigma iff for n holds ASeq.n is Event of Sigma proof A1: ASeq is SetSequence of Sigma implies for n holds ASeq.n is Event of Sigma proof assume A2: ASeq is SetSequence of Sigma; for n holds ASeq.n is Event of Sigma proof let n; ASeq.n in Sigma by A2,Def9; hence thesis by Def10; end; hence thesis; end; (for n holds ASeq.n is Event of Sigma) implies for n holds ASeq.n in Sigma proof assume A3: for n holds ASeq.n is Event of Sigma; for n holds ASeq.n in Sigma proof let n; ASeq.n is Event of Sigma by A3; hence thesis by Def10; end; hence thesis; end; hence thesis by A1,Def9; end; theorem ASeq is SetSequence of Sigma implies Union ASeq is Event of Sigma proof assume ASeq is SetSequence of Sigma; then Union ASeq in Sigma by Th46; hence thesis by Def10; end; :: DEFINITION OF sigma-ADDITIVE PROBABILITY reserve A, B for Event of Sigma, ASeq for SetSequence of Sigma; theorem Th59: 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)) proof defpred C[set] means p in $1; deffunc F(set) = 1; deffunc G(set) = 0; ex f being Function st dom f = Sigma & for x being set st x in Sigma holds (C[x] implies f.x=F(x)) & (not C[x] implies f.x=G(x)) from LambdaC; then consider f being Function such that A1: dom f = Sigma & for x being set st x in Sigma holds (C[x] implies f.x = 1) & (not C[x] implies f.x = 0); take f; thus dom f = Sigma by A1; let D; assume A2: D in Sigma; hence p in D implies f.D = 1 by A1; assume not p in D; hence thesis by A1,A2; end; reserve P for Function of Sigma,REAL; theorem Th60: 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)) proof consider f such that A1: 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) by Th59; rng f c= REAL proof let y; assume y in rng f; then consider x such that A2: x in dom f & y = f.x by FUNCT_1:def 5; reconsider x as Subset of Omega by A1,A2; A3: p in x implies y = 1 by A1,A2; not p in x implies y = 0 by A1,A2; hence thesis by A3; end; then reconsider f as Function of Sigma,REAL by A1,FUNCT_2:def 1,RELSET_1:11; take f; thus thesis by A1; end; canceled; theorem Th62: P * ASeq is Real_Sequence proof for x holds (x in dom (P * ASeq) iff x in NAT) proof let x; x in dom (P * ASeq) iff x in dom ASeq & ASeq.x in dom P by FUNCT_1:21; then x in dom (P * ASeq) iff x in NAT & ASeq.x in Sigma by FUNCT_2:def 1; hence thesis by Def9; end; then A1: dom (P * ASeq) = NAT by TARSKI:2; rng (P * ASeq) c= REAL proof rng (P * ASeq) c= rng P & rng P c= REAL by RELAT_1:45,RELSET_1:12; hence thesis by XBOOLE_1:1; end; hence thesis by A1,FUNCT_2:def 1,RELSET_1:11; end; definition let Omega,Sigma,ASeq,P; redefine func P * ASeq -> Real_Sequence; coherence by Th62; end; definition let Omega,Sigma,P,A; redefine func P.A -> Real; coherence proof A in Sigma by Def10; then A in dom P by FUNCT_2:def 1; then P.A in rng P by FUNCT_1:def 5; hence thesis; end; end; definition let Omega,Sigma; canceled; mode Probability of Sigma -> Function of Sigma,REAL means :Def13: (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)); existence proof consider p being Element of Omega; consider P such that A1: for D st D in Sigma holds (p in D implies P.D = 1) & (not p in D implies P.D = 0) by Th60; take P; A2: for A holds (p in A implies P.A = 1) & (not p in A implies P.A = 0) proof let A; A in Sigma by Def10; hence thesis by A1; end; A3: for A holds 0 <= P.A proof let A; p in A implies P.A = 1 by A2; hence thesis by A2; end; A4: P.Omega = 1 proof Omega c= Omega; then reconsider O = Omega as Subset of Omega; O in Sigma by Th11; hence thesis by A1; end; A5: for A,B st A misses B holds P.(A \/ B) = P.A + P.B proof let A,B such that A6: A misses B; A7: (p in A & not p in B) implies (P.A = 1 & P.B = 0) by A2; A8: (p in A & not p in B) implies p in A \/ B by XBOOLE_0:def 2; A9: (not p in A & p in B) implies (P.A = 0 & P.B = 1) by A2; A10: (not p in A & p in B) implies p in A \/ B by XBOOLE_0:def 2; A11: (not p in A & not p in B) implies P.A = 0 & P.B = 0 by A2; (not p in A & not p in B) implies not p in (A \/ B) by XBOOLE_0:def 2 ; hence thesis by A2,A6,A7,A8,A9,A10,A11,XBOOLE_0:3; end; for ASeq st ASeq is non-increasing holds P * ASeq is convergent & lim (P * ASeq) = P.Intersection ASeq proof let ASeq; assume A12: ASeq is non-increasing; A13: for n holds (P * ASeq).n = P.(ASeq.n) proof let n; dom (P * ASeq) = NAT by FUNCT_2:def 1; hence thesis by FUNCT_1:22; end; A14: (for n holds p in ASeq.n) implies for n holds (P * ASeq).n = 1 proof assume A15: for n holds p in ASeq.n; for n holds (P * ASeq).n = 1 proof let n; A16: ASeq.n in Sigma by Def9; p in ASeq.n by A15; then P.(ASeq.n) = 1 by A1,A16; hence thesis by A13; end; hence thesis; end; A17: not (for n holds p in ASeq.n) implies ex m st (for n st m <= n holds (P * ASeq).n = 0) proof assume not (for n holds p in ASeq.n); then consider m such that A18: not p in ASeq.m; take m; for n st m <= n holds (P * ASeq).n = 0 proof let n; assume m <= n; then ASeq.n c= ASeq.m by A12,Def6; then A19: not p in ASeq.n by A18; ASeq.n in Sigma by Def9; then P.(ASeq.n) = 0 by A1,A19; hence thesis by A13; end; hence thesis; end; A20: (for n holds (P * ASeq).n = 1) implies P * ASeq is convergent & lim (P * ASeq) = 1 proof reconsider r = 1 as Real; assume A21: for n holds (P * ASeq).n = 1; ex m st for n st m <= n holds (P * ASeq).n = r proof take 0; thus thesis by A21; end; hence thesis by Th3; end; A22: (ex m st (for n st m <= n holds (P * ASeq).n = 0)) implies P * ASeq is convergent & lim (P * ASeq) = 0 by Th3; A23: (for n holds p in ASeq.n) implies P * ASeq is convergent & lim (P * ASeq) = P.Intersection ASeq proof assume A24: for n holds p in ASeq.n; then A25: p in Intersection ASeq by Th29; for n holds ASeq.n in Sigma by Def9; then Intersection ASeq in Sigma by Def8; hence thesis by A1,A14,A20,A24,A25; end; not (for n holds p in ASeq.n) implies P * ASeq is convergent & lim (P * ASeq) = P.Intersection ASeq proof assume A26: not (for n holds p in ASeq.n); then A27: not p in Intersection ASeq by Th29; for n holds ASeq.n in Sigma by Def9; then Intersection ASeq in Sigma by Def8; hence thesis by A1,A17,A22,A26,A27; end; hence thesis by A23; end; hence thesis by A3,A4,A5; end; end; reserve P for Probability of Sigma; canceled; theorem P.{} = 0 proof A1: {} misses ([#] Sigma) by XBOOLE_1:65; A2: {} \/ ([#] Sigma) = [#] Sigma; reconsider E = {} as Event of Sigma by Th52; 1 = P.Omega by Def13 .= P.([#] Sigma) by Def11; then 1 = P.E + 1 by A1,A2,Def13; then P.({} Sigma) = 1 - 1 by XCMPLX_1:26 .= 0; hence thesis; end; canceled; theorem P.([#] Sigma) = 1 proof P.Omega = 1 by Def13; hence thesis by Def11; end; theorem Th67: P.(([#] Sigma) \ A) + P.A = 1 proof A1: (([#] Sigma) \ A) misses A by XBOOLE_1:79; (([#] Sigma) \ A) \/ A = (Omega \ A) \/ A by Def11 .= A` \/ A by SUBSET_1:def 5 .= [#] Omega by SUBSET_1:25 .= Omega by SUBSET_1:def 4; then P.(([#] Sigma) \ A) + P.A = P.Omega by A1,Def13 .= 1 by Def13; hence thesis; end; theorem P.(([#] Sigma) \ A) = 1 - P.A proof P.(([#] Sigma) \ A) + P.A = 1 by Th67; hence thesis by XCMPLX_1:26; end; theorem Th69: A c= B implies P.(B \ A) = P.B - P.A proof assume A1: A c= B; A misses (B \ A) by XBOOLE_1:79; then P.A + P.(B \ A) = P.(A \/ (B \ A)) by Def13 .= P.B by A1,XBOOLE_1:45; hence thesis by XCMPLX_1:26; end; theorem Th70: A c= B implies P.A <= P.B proof assume A c= B; then P.(B \ A) = P.B - P.A by Th69; then 0 <= P.B - P.A by Def13; then 0 + P.A <= P.B by REAL_1:84; hence thesis; end; theorem P.A <= 1 proof A1: P.([#] Sigma) = P.Omega by Def11 .= 1 by Def13; A c= Omega; then A c= ([#] Sigma) by Def11; hence thesis by A1,Th70; end; theorem Th72: P.(A \/ B) = P.A + P.(B \ A) proof A1: A misses (B \ A) by XBOOLE_1:79; P.(A \/ B) = P.(A \/ (B \ A)) by XBOOLE_1:39 .= P.A + P.(B \ A) by A1,Def13; hence thesis; end; theorem Th73: P.(A \/ B) = P.A + P.(B \ (A /\ B)) proof P.(A \/ B) = P.A + P.(B \ A) by Th72 .= P.A + P.(B \ (A /\ B)) by XBOOLE_1:47; hence thesis; end; theorem Th74: P.(A \/ B) = P.A + P.B - P.(A /\ B) proof A1: A /\ B c= B by XBOOLE_1:17; P.(A \/ B) = P.A + P.(B \ (A /\ B)) by Th73 .= P.A + (P.B - P.(A /\ B)) by A1,Th69; hence thesis by XCMPLX_1:29; end; theorem P.(A \/ B) <= P.A + P.B proof A1: 0 <= P.(A /\ B) by Def13; P.(A \/ B) = P.A + P.B - P.(A /\ B) by Th74; hence thesis by A1,Th2; end; :: 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 Th76: bool Omega is SigmaField of Omega proof set Y = bool Omega; (Y c= bool Omega) & (for BSeq st (for n holds BSeq.n in Y) holds Intersection BSeq in Y) & (for E st E in Y holds E` in Y); hence thesis by Th32; end; Lm2: for X being Subset of bool Omega ex Y being SigmaField of Omega st X c= Y & for Z st (X c= Z & Z is SigmaField of Omega) holds Y c= Z proof let X be Subset of bool Omega; set V = { S : X c= S & S is SigmaField of Omega}; set Y = meet V; A1: bool Omega in V proof bool Omega c= bool Omega; then reconsider X1 = bool Omega as Subset of bool Omega; X1 is SigmaField of Omega by Th76; hence thesis; end; then A2: Y c= bool Omega by SETFAM_1:4; now let Z; assume Z in V; then ex S st Z = S & X c= S & S is SigmaField of Omega; hence {} in Z by Th10; end; then A3: {} in Y by A1,SETFAM_1:def 1; A4: for BSeq st (for n holds BSeq.n in Y) holds Intersection BSeq in Y proof let BSeq such that A5: for n holds BSeq.n in Y; now let Z; assume A6: Z in V; then A7: ex S st Z = S & X c= S & S is SigmaField of Omega; now let n; BSeq.n in Y by A5; hence BSeq.n in Z by A6,SETFAM_1:def 1; end; hence Intersection BSeq in Z by A7,Def8; end; hence thesis by A1,SETFAM_1:def 1; end; for E st E in Y holds E` in Y proof let E such that A8: E in Y; now let Z; assume A9: Z in V; then A10: E in Z by A8,SETFAM_1:def 1; ex S st Z = S & X c= S & S is SigmaField of Omega by A9; hence E` in Z by A10,Def8; end; hence thesis by A1,SETFAM_1:def 1; end; then reconsider Y as SigmaField of Omega by A2,A3,A4,Th32; take Y; A11: now let Z; assume Z in V; then ex S st Z = S & X c= S & S is SigmaField of Omega; hence X c= Z; end; for Z st (X c= Z & Z is SigmaField of Omega) holds Y c= Z proof let Z; assume A12: X c= Z & Z is SigmaField of Omega; then reconsider Z as Subset of bool Omega; Z in V by A12; hence thesis by SETFAM_1:4; end; hence thesis by A1,A11,SETFAM_1:6; end; definition let Omega; let X be Subset of bool Omega; func sigma(X) -> SigmaField of Omega means X c= it & for Z st (X c= Z & Z is SigmaField of Omega) holds it c= Z; existence by Lm2; uniqueness proof let R1,R2 be SigmaField of Omega such that A1: X c= R1 & for Z st X c= Z & Z is SigmaField of Omega holds R1 c= Z and A2: X c= R2 & for Z st X c= Z & Z is SigmaField of Omega holds R2 c= Z; A3: R1 c= R2 by A1,A2; R2 c= R1 by A1,A2; hence thesis by A3,XBOOLE_0:def 10; end; end; definition let r; func halfline(r) -> Subset of REAL equals {r1 where r1 is Element of REAL: r1 < r}; coherence proof {r1 where r1 is Element of REAL: r1 < r} is Subset of REAL proof now let p; assume p in {r1 where r1 is Element of REAL: r1 < r}; then ex r1 being Element of REAL st p = r1 & r1 < r; hence p in REAL; end; hence thesis by TARSKI:def 3; end; hence thesis; end; end; definition func Family_of_halflines -> Subset of bool REAL equals {D: ex r st D = halfline(r)}; coherence proof {D: ex r st D = halfline(r)} is Subset of bool REAL proof now let p; assume p in {D: ex r st D = halfline(r)}; then ex D st p = D & ex r st D = halfline(r); hence p in bool REAL; end; hence thesis by TARSKI:def 3; end; hence thesis; end; end; definition func Borel_Sets -> SigmaField of REAL equals sigma(Family_of_halflines); correctness; end;

Back to top