Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### $\sigma$-Fields and Probability

by
Andrzej Nedzusiak

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;

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;
`