:: $\sigma$-Fields and Probability
:: by Andrzej N\c{e}dzusiak
::
:: Received October 16, 1989
:: Copyright (c) 1990-2021 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, SUBSET_1, FUNCT_1, SEQ_1, XXREAL_0, SEQ_2,
ORDINAL2, CARD_1, ARYTM_3, COMPLEX1, ARYTM_1, SETFAM_1, FINSUB_1,
ZFMISC_1, TARSKI, RELAT_1, CARD_3, EQREL_1, FUNCT_7, FUNCOP_1, NAT_1,
RPR_1, REAL_1, VALUED_0, XXREAL_1, PROB_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSUB_1, RELAT_1, FUNCT_1,
XCMPLX_0, REAL_1, FUNCT_2, FUNCOP_1, FUNCT_7, ORDINAL1, CARD_3, NUMBERS,
VALUED_0, XREAL_0, COMPLEX1, NAT_1, SEQ_1, COMSEQ_2, SEQ_2, SETFAM_1,
XXREAL_0, XXREAL_1;
constructors SETFAM_1, FINSUB_1, XXREAL_1, COMPLEX1, REAL_1, SEQ_2, CARD_3,
MEMBERED, FUNCT_7, RELSET_1, COMSEQ_2, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0,
XREAL_0, XXREAL_1, RELAT_1, VALUED_0, RELSET_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve Omega for 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 for Real;
reserve seq for Real_Sequence;
theorem :: PROB_1:1
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;
registration
let X be set;
cluster bool X -> cap-closed;
end;
registration
let X be set;
cluster bool X -> compl-closed for Subset-Family of X;
end;
registration
let X be set;
cluster non empty compl-closed cap-closed for 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:2
for A,B being Subset of X holds {A,B} is Subset-Family of X;
theorem :: PROB_1:3
for A, B being set st A in F & B in F holds A \/ B in F;
theorem :: PROB_1:4
{} in F;
theorem :: PROB_1:5
X in F;
theorem :: PROB_1:6
for A,B being Subset of X holds A in F & B in F implies A \ B in F;
theorem :: PROB_1:7
for A, B being set holds (A in F & B in F implies (A \ B) \/ B in F);
registration
let X be set;
cluster { {}, X } -> cap-closed;
end;
theorem :: PROB_1:8
{ {}, X } is Field_Subset of X;
theorem :: PROB_1:9
bool X is Field_Subset of X;
theorem :: PROB_1:10
{ {} , X } c= F & F c= bool X;
definition
let X be set;
mode SetSequence of X is sequence of bool X;
end;
reserve ASeq,BSeq for SetSequence of Omega;
reserve A1 for SetSequence of X;
theorem :: PROB_1:11
union rng A1 is Subset of X;
definition
let X be set, A1 be SetSequence of X;
redefine func Union A1 -> Subset of X;
end;
theorem :: PROB_1:12
x in Union A1 iff ex n st x in A1.n;
definition
let X be set, A1 be SetSequence of X;
func Complement A1 -> SetSequence of X means
:: PROB_1:def 2
for n holds it.n = (A1.n )`;
involutiveness;
end;
definition
let X be set, A1 be SetSequence of X;
func Intersection A1 -> Subset of X equals
:: PROB_1:def 3
(Union Complement A1)`;
end;
theorem :: PROB_1:13
for x being object holds x in Intersection A1 iff for n holds x in A1.n;
theorem :: PROB_1:14
for A, B being Subset of X holds Intersection(A followed_by B) = A /\ B;
definition
let f be Function;
attr f is non-ascending means
:: PROB_1:def 4
for n,m st n <= m holds f.m c= f.n;
attr f is non-descending means
:: PROB_1:def 5
for n,m st n <= m holds f.n c= f.m;
end;
definition
let X be set, F be Subset-Family of X;
attr F is sigma-multiplicative means
:: PROB_1:def 6
for A1 being SetSequence of X st rng A1 c= F holds Intersection A1 in F;
end;
registration
let X be set;
cluster bool X -> sigma-multiplicative for Subset-Family of X;
end;
registration
let X be set;
cluster compl-closed sigma-multiplicative non empty for Subset-Family of X;
end;
definition
let X be set;
mode SigmaField of X is compl-closed sigma-multiplicative non empty
Subset-Family of X;
end;
theorem :: PROB_1:15
for S being non empty set holds S is SigmaField of X iff S c= bool X &
(for A1 being SetSequence of X st rng A1 c= S holds Intersection A1 in S) &
for A being Subset of X st A in S holds A` in S;
theorem :: PROB_1:16
Y is SigmaField of X implies Y is Field_Subset of X;
registration
let X be set;
cluster -> cap-closed compl-closed for SigmaField of X;
end;
reserve Sigma for SigmaField of Omega;
reserve Si for SigmaField of X;
:: 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.
registration
let X be set, F be non empty Subset-Family of X;
cluster F-valued for SetSequence of X;
end;
definition
let X be set, F be non empty Subset-Family of X;
mode SetSequence of F is F-valued SetSequence of X;
end;
theorem :: PROB_1:17
for ASeq being SetSequence of Si holds Union ASeq in Si;
notation
let X be set; let F be SigmaField of X;
synonym Event of F for Element of F;
end;
definition
let X be set, F be SigmaField of X;
redefine mode Event of F -> Subset of X;
end;
theorem :: PROB_1:18
x in Si implies x is Event of Si;
theorem :: PROB_1:19
for A,B being Event of Si holds A /\ B is Event of Si;
theorem :: PROB_1:20
for A being Event of Si holds A` is Event of Si;
theorem :: PROB_1:21
for A,B being Event of Si holds A \/ B is Event of Si;
theorem :: PROB_1:22
{} is Event of Si;
theorem :: PROB_1:23
X is Event of Si;
theorem :: PROB_1:24
for A,B being Event of Si holds A \ B is Event of Si;
registration
let X,Si;
cluster empty for Event of Si;
end;
definition
let X,Si;
func [#] Si -> Event of Si equals
:: PROB_1:def 7
X;
end;
definition
let X,Si;
let A,B be Event of Si;
redefine func A /\ B -> Event of Si;
redefine func A \/ B -> Event of Si;
redefine func A \ B -> Event of Si;
end;
theorem :: PROB_1:25
A1 is SetSequence of Si iff for n holds A1.n is Event of Si;
theorem :: PROB_1:26
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:27
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:28
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);
theorem :: PROB_1:29
P * ASeq is Real_Sequence;
definition
let Omega,Sigma,ASeq,P;
redefine func P * ASeq -> Real_Sequence;
end;
reserve Omega for non empty set;
reserve Sigma for SigmaField of Omega;
reserve A, B for Event of Sigma,
ASeq for SetSequence of Sigma;
reserve P for Function of Sigma,REAL;
reserve D, E for Subset of Omega;
reserve BSeq for SetSequence of Omega;
definition
let Omega,Sigma;
mode Probability of Sigma -> Function of Sigma,REAL means
:: PROB_1:def 8
(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-ascending holds it * ASeq is convergent &
lim (it * ASeq) = it.Intersection ASeq;
end;
reserve P for Probability of Sigma;
registration
let Omega,Sigma;
cluster -> zeroed for Probability of Sigma;
end;
theorem :: PROB_1:30
P.([#] Sigma) = 1;
theorem :: PROB_1:31
P.(([#] Sigma) \ A) + P.A = 1;
theorem :: PROB_1:32
P.(([#] Sigma) \ A) = 1 - P.A;
theorem :: PROB_1:33
A c= B implies P.(B \ A) = P.B - P.A;
theorem :: PROB_1:34
A c= B implies P.A <= P.B;
theorem :: PROB_1:35
P.A <= 1;
theorem :: PROB_1:36
P.(A \/ B) = P.A + P.(B \ A);
theorem :: PROB_1:37
P.(A \/ B) = P.A + P.(B \ (A /\ B));
theorem :: PROB_1:38
P.(A \/ B) = P.A + P.B - P.(A /\ B);
theorem :: PROB_1:39
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-Family of Omega;
theorem :: PROB_1:40
bool X is SigmaField of X;
definition
let Omega;
let X be Subset-Family of Omega;
func sigma(X) -> SigmaField of Omega means
:: PROB_1:def 9
X c= it & for Z st X c= Z & Z is SigmaField of Omega holds it c= Z;
end;
definition
let r be ExtReal;
func halfline r -> Subset of REAL equals
:: PROB_1:def 10
].-infty,r.[;
end;
definition
func Family_of_halflines -> Subset-Family of REAL equals
:: PROB_1:def 11
the set of all halfline(r) where r is Element of REAL;
end;
definition
func Borel_Sets -> SigmaField of REAL equals
:: PROB_1:def 12
sigma(Family_of_halflines);
end;
theorem :: PROB_1:41
for A, B being Subset of X holds Complement (A followed_by B) = A`
followed_by B`;
definition
let X, Y be set;
let A be Subset-Family of X;
let F be Function of Y, bool A;
let x be set;
redefine func F.x -> Subset-Family of X;
end;