:: $\sigma$-Fields and Probability
:: by Andrzej N\c{e}dzusiak
::
:: Received October 16, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: PROB_1:1
for r being real number
for seq being Real_Sequence st ex n being Element of NAT st
for m being Element of NAT st n <= m holds
seq . m = r holds
( seq is convergent & lim seq = r )
proof 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: :: PROB_1:def 1
for A being Subset of X st A in IT holds
A ` in IT;
end;

:: deftheorem Def1 defines compl-closed PROB_1:def 1 :
for X being set
for IT being Subset-Family of X holds
( IT is compl-closed iff for A being Subset of X st A in IT holds
A ` in IT );

registration
let X be set ;
cluster bool X -> cap-closed ;
coherence
bool X is cap-closed
proof end;
end;

registration
let X be set ;
cluster bool X -> compl-closed for Subset-Family of X;
coherence
for b1 being Subset-Family of X st b1 = bool X holds
b1 is compl-closed
proof end;
end;

registration
let X be set ;
cluster non empty cap-closed compl-closed for Event of ;
existence
ex b1 being Subset-Family of X st
( not b1 is empty & b1 is compl-closed & b1 is cap-closed )
proof end;
end;

definition
let X be set ;
mode Field_Subset of X is non empty cap-closed compl-closed Subset-Family of X;
end;

theorem Th2: :: PROB_1:2
for X being set
for A, B being Subset of X holds {A,B} is Subset-Family of X
proof end;

theorem Th3: :: PROB_1:3
for X being set
for F being Field_Subset of X
for A, B being set st A in F & B in F holds
A \/ B in F
proof end;

theorem Th4: :: PROB_1:4
for X being set
for F being Field_Subset of X holds {} in F
proof end;

theorem Th5: :: PROB_1:5
for X being set
for F being Field_Subset of X holds X in F
proof end;

theorem Th6: :: PROB_1:6
for X being set
for F being Field_Subset of X
for A, B being Subset of X st A in F & B in F holds
A \ B in F
proof end;

theorem :: PROB_1:7
for X being set
for F being Field_Subset of X
for A, B being set st A in F & B in F holds
(A \ B) \/ B in F
proof end;

registration
let X be set ;
cluster {{},X} -> cap-closed ;
coherence
{{},X} is cap-closed
proof end;
end;

theorem :: PROB_1:8
for X being set holds {{},X} is Field_Subset of X
proof end;

theorem :: PROB_1:9
for X being set holds bool X is Field_Subset of X ;

theorem :: PROB_1:10
for X being set
for F being Field_Subset of X holds
( {{},X} c= F & F c= bool X )
proof end;

definition
let X be set ;
mode SetSequence of X is sequence of (bool X);
end;

theorem Th11: :: PROB_1:11
for X being set
for A1 being SetSequence of X holds union (rng A1) is Subset of X
proof end;

definition
let X be set ;
let A1 be SetSequence of X;
:: original: Union
redefine func Union A1 -> Subset of X;
coherence
Union A1 is Subset of X
by Th11;
end;

theorem Th12: :: PROB_1:12
for X, x being set
for A1 being SetSequence of X holds
( x in Union A1 iff ex n being Element of NAT st x in A1 . n )
proof end;

definition
let X be set ;
let A1 be SetSequence of X;
func Complement A1 -> SetSequence of X means :Def2: :: PROB_1:def 2
for n being Element of NAT holds it . n = (A1 . n) ` ;
existence
ex b1 being SetSequence of X st
for n being Element of NAT holds b1 . n = (A1 . n) `
proof end;
uniqueness
for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) ` ) & ( for n being Element of NAT holds b2 . n = (A1 . n) ` ) holds
b1 = b2
proof end;
involutiveness
for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (b2 . n) ` ) holds
for n being Element of NAT holds b2 . n = (b1 . n) `
proof end;
end;

:: deftheorem Def2 defines Complement PROB_1:def 2 :
for X being set
for A1, b3 being SetSequence of X holds
( b3 = Complement A1 iff for n being Element of NAT holds b3 . n = (A1 . n) ` );

definition
let X be set ;
let A1 be SetSequence of X;
func Intersection A1 -> Subset of X equals :: PROB_1:def 3
(Union (Complement A1)) ` ;
correctness
coherence
(Union (Complement A1)) ` is Subset of X
;
;
end;

:: deftheorem defines Intersection PROB_1:def 3 :
for X being set
for A1 being SetSequence of X holds Intersection A1 = (Union (Complement A1)) ` ;

theorem Th13: :: PROB_1:13
for X, x being set
for A1 being SetSequence of X holds
( x in Intersection A1 iff for n being Element of NAT holds x in A1 . n )
proof end;

Lm1: for X being set
for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `)

proof end;

theorem Th14: :: PROB_1:14
for X being set
for A, B being Subset of X holds Intersection (A followed_by B) = A /\ B
proof end;

definition
let f be Function;
attr f is non-ascending means :Def4: :: PROB_1:def 4
for n, m being Element of NAT st n <= m holds
f . m c= f . n;
attr f is non-descending means :: PROB_1:def 5
for n, m being Element of NAT st n <= m holds
f . n c= f . m;
end;

:: deftheorem Def4 defines non-ascending PROB_1:def 4 :
for f being Function holds
( f is non-ascending iff for n, m being Element of NAT st n <= m holds
f . m c= f . n );

:: deftheorem defines non-descending PROB_1:def 5 :
for f being Function holds
( f is non-descending iff for n, m being Element of NAT st n <= m holds
f . n c= f . m );

definition
let X be set ;
let F be Subset-Family of X;
attr F is sigma-multiplicative means :Def6: :: PROB_1:def 6
for A1 being SetSequence of X st rng A1 c= F holds
Intersection A1 in F;
end;

:: deftheorem Def6 defines sigma-multiplicative PROB_1:def 6 :
for X being set
for F being Subset-Family of X holds
( F is sigma-multiplicative iff for A1 being SetSequence of X st rng A1 c= F holds
Intersection A1 in F );

registration
let X be set ;
cluster bool X -> sigma-multiplicative for Subset-Family of X;
coherence
for b1 being Subset-Family of X st b1 = bool X holds
b1 is sigma-multiplicative
proof end;
end;

registration
let X be set ;
cluster non empty compl-closed sigma-multiplicative for Event of ;
existence
ex b1 being Subset-Family of X st
( b1 is compl-closed & b1 is sigma-multiplicative & not b1 is empty )
proof end;
end;

definition
let X be set ;
mode SigmaField of X is non empty compl-closed sigma-multiplicative Subset-Family of X;
end;

theorem :: PROB_1:15
for X being set
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 ) ) ) by Def1, Def6;

theorem Th16: :: PROB_1:16
for Y, X being set st Y is SigmaField of X holds
Y is Field_Subset of X
proof end;

registration
let X be set ;
cluster non empty compl-closed sigma-multiplicative -> cap-closed for Event of ;
coherence
for b1 being SigmaField of X holds
( b1 is cap-closed & b1 is compl-closed )
by Th16;
end;

:: 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 ;
let F be non empty Subset-Family of X;
cluster Relation-like NAT -defined F -valued bool X -valued Function-like V37( NAT , bool X) for Event of ;
existence
ex b1 being SetSequence of X st b1 is F -valued
proof end;
end;

definition
let X be set ;
let F be non empty Subset-Family of X;
mode SetSequence of F is F -valued SetSequence of X;
end;

theorem Th17: :: PROB_1:17
for X being set
for Si being SigmaField of X
for ASeq being SetSequence of Si holds Union ASeq in Si
proof end;

notation
let X be set ;
let F be SigmaField of X;
synonym Event of F for Element of X;
end;

definition
let X be set ;
let F be SigmaField of X;
:: original: Event
redefine mode Event of F -> Subset of X;
coherence
for b1 being Event of holds b1 is Subset of X
proof end;
end;

theorem :: PROB_1:18
for X, x being set
for Si being SigmaField of X st x in Si holds
x is Event of Si ;

theorem :: PROB_1:19
for X being set
for Si being SigmaField of X
for A, B being Event of Si holds A /\ B is Event of Si by FINSUB_1:def 2;

theorem :: PROB_1:20
for X being set
for Si being SigmaField of X
for A being Event of Si holds A ` is Event of Si by Def1;

theorem :: PROB_1:21
for X being set
for Si being SigmaField of X
for A, B being Event of Si holds A \/ B is Event of Si by Th3;

theorem :: PROB_1:22
for X being set
for Si being SigmaField of X holds {} is Event of Si by Th4;

theorem :: PROB_1:23
for X being set
for Si being SigmaField of X holds X is Event of Si by Th5;

theorem :: PROB_1:24
for X being set
for Si being SigmaField of X
for A, B being Event of Si holds A \ B is Event of Si by Th6;

registration
let X be set ;
let Si be SigmaField of X;
cluster empty for Event of ;
existence
ex b1 being Event of Si st b1 is empty
proof end;
end;

definition
let X be set ;
let Si be SigmaField of X;
func [#] Si -> Event of Si equals :: PROB_1:def 7
X;
coherence
X is Event of Si
by Th5;
end;

:: deftheorem defines [#] PROB_1:def 7 :
for X being set
for Si being SigmaField of X holds [#] Si = X;

definition
let X be set ;
let Si be SigmaField of X;
let A, B be Event of Si;
:: original: /\
redefine func A /\ B -> Event of Si;
coherence
A /\ B is Event of Si
by FINSUB_1:def 2;
:: original: \/
redefine func A \/ B -> Event of Si;
coherence
A \/ B is Event of Si
by Th3;
:: original: \
redefine func A \ B -> Event of Si;
coherence
A \ B is Event of Si
by Th6;
end;

theorem :: PROB_1:25
for X being set
for A1 being SetSequence of X
for Si being SigmaField of X holds
( A1 is SetSequence of Si iff for n being Element of NAT holds A1 . n is Event of Si )
proof end;

theorem :: PROB_1:26
for Omega being set
for ASeq being SetSequence of Omega
for Sigma being SigmaField of Omega st ASeq is SetSequence of Sigma holds
Union ASeq is Event of Sigma by Th17;

theorem Th27: :: PROB_1:27
for Omega, p being set
for Sigma being SigmaField of Omega ex f being Function st
( dom f = Sigma & ( for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) & ( not p in D implies f . D = 0 ) ) ) )
proof end;

theorem Th28: :: PROB_1:28
for Omega, p being set
for Sigma being SigmaField of Omega ex P being Function of Sigma,REAL st
for D being Subset of Omega st D in Sigma holds
( ( p in D implies P . D = 1 ) & ( not p in D implies P . D = 0 ) )
proof end;

theorem Th29: :: PROB_1:29
for Omega being set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Function of Sigma,REAL holds P * ASeq is Real_Sequence
proof end;

definition
let Omega be set ;
let Sigma be SigmaField of Omega;
let ASeq be SetSequence of Sigma;
let P be Function of Sigma,REAL;
:: original: *
redefine func P * ASeq -> Real_Sequence;
coherence
ASeq * P is Real_Sequence
by Th29;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
mode Probability of Sigma -> Function of Sigma,REAL means :Def8: :: PROB_1:def 8
( ( for A being Event of Sigma holds 0 <= it . A ) & it . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
it . (A \/ B) = (it . A) + (it . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( it * ASeq is convergent & lim (it * ASeq) = it . (Intersection ASeq) ) ) );
existence
ex b1 being Function of Sigma,REAL st
( ( for A being Event of Sigma holds 0 <= b1 . A ) & b1 . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
b1 . (A \/ B) = (b1 . A) + (b1 . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( b1 * ASeq is convergent & lim (b1 * ASeq) = b1 . (Intersection ASeq) ) ) )
proof end;
end;

:: deftheorem Def8 defines Probability PROB_1:def 8 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for b3 being Function of Sigma,REAL holds
( b3 is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= b3 . A ) & b3 . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
b3 . (A \/ B) = (b3 . A) + (b3 . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( b3 * ASeq is convergent & lim (b3 * ASeq) = b3 . (Intersection ASeq) ) ) ) );

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
cluster -> zeroed for Probability of Sigma;
coherence
for b1 being Probability of Sigma holds b1 is zeroed
proof end;
end;

theorem :: PROB_1:30
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds P . ([#] Sigma) = 1 by Def8;

theorem Th31: :: PROB_1:31
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds (P . (([#] Sigma) \ A)) + (P . A) = 1
proof end;

theorem :: PROB_1:32
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds P . (([#] Sigma) \ A) = 1 - (P . A)
proof end;

theorem Th33: :: PROB_1:33
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st A c= B holds
P . (B \ A) = (P . B) - (P . A)
proof end;

theorem Th34: :: PROB_1:34
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma st A c= B holds
P . A <= P . B
proof end;

theorem :: PROB_1:35
for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma
for P being Probability of Sigma holds P . A <= 1
proof end;

theorem Th36: :: PROB_1:36
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ A))
proof end;

theorem Th37: :: PROB_1:37
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) = (P . A) + (P . (B \ (A /\ B)))
proof end;

theorem Th38: :: PROB_1:38
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) = ((P . A) + (P . B)) - (P . (A /\ B))
proof end;

theorem :: PROB_1:39
for Omega being non empty set
for Sigma being SigmaField of Omega
for A, B being Event of Sigma
for P being Probability of Sigma holds P . (A \/ B) <= (P . A) + (P . B)
proof end;

theorem :: PROB_1:40
for X being set holds bool X is SigmaField of X ;

definition
let Omega be non empty set ;
let X be Subset-Family of Omega;
func sigma X -> SigmaField of Omega means :: PROB_1:def 9
( X c= it & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
it c= Z ) );
existence
ex b1 being SigmaField of Omega st
( X c= b1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b1 c= Z ) )
proof end;
uniqueness
for b1, b2 being SigmaField of Omega st X c= b1 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b1 c= Z ) & X c= b2 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b2 c= Z ) holds
b1 = b2
proof end;
end;

:: deftheorem defines sigma PROB_1:def 9 :
for Omega being non empty set
for X being Subset-Family of Omega
for b3 being SigmaField of Omega holds
( b3 = sigma X iff ( X c= b3 & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b3 c= Z ) ) );

definition
let r be ext-real number ;
func halfline r -> Subset of REAL equals :: PROB_1:def 10
].-infty,r.[;
coherence
].-infty,r.[ is Subset of REAL
proof end;
end;

:: deftheorem defines halfline PROB_1:def 10 :
for r being ext-real number holds halfline r = ].-infty,r.[;

definition
func Family_of_halflines -> Subset-Family of REAL equals :: PROB_1:def 11
{ (halfline r) where r is Element of REAL : verum } ;
coherence
{ (halfline r) where r is Element of REAL : verum } is Subset-Family of REAL
proof end;
end;

:: deftheorem defines Family_of_halflines PROB_1:def 11 :
Family_of_halflines = { (halfline r) where r is Element of REAL : verum } ;

definition
func Borel_Sets -> SigmaField of REAL equals :: PROB_1:def 12
sigma Family_of_halflines;
correctness
coherence
sigma Family_of_halflines is SigmaField of REAL
;
;
end;

:: deftheorem defines Borel_Sets PROB_1:def 12 :
Borel_Sets = sigma Family_of_halflines;

theorem :: PROB_1:41
for X being set
for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `) by Lm1;

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 ;
:: original: .
redefine func F . x -> Subset-Family of X;
coherence
F . x is Subset-Family of X
proof end;
end;