:: $\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 &amp; lim seq = r )
proofend;

:: 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;
attrIT 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
proofend;
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
proofend;
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 &amp; b1 is compl-closed &amp; b1 is cap-closed )
proofend;
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
proofend;

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 &amp; B in F holds
A \/ B in F
proofend;

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

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

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 &amp; B in F holds
A \ B in F
proofend;

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

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

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

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 &amp; F c= bool X )
proofend;

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

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 )
proofend;

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) `
proofend;
uniqueness
 for b1, b2 being SetSequence of X st ( for n being Element of NAT holds b1 . n = (A1 . n) ` ) &amp; ( for n being Element of NAT holds b2 . n = (A1 . n) ` ) holds
b1 = b2
proofend;
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) `
proofend;
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 )
proofend;

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

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

definition
let f be Function;
attrf 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;
attrf 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;
attrF 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
proofend;
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 &amp; b1 is sigma-multiplicative &amp; not b1 is empty )
proofend;
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 &amp; ( for A1 being SetSequence of X st rng A1 c= S holds
Intersection A1 in S ) &amp; ( 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
proofend;

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 &amp; 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
proofend;
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
proofend;

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
proofend;
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
proofend;
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 funcA /\ B ->  Event of Si;
coherence
 A /\ B is Event of Si by FINSUB_1:def_2;
:: original:\/
redefine funcA \/ B ->  Event of Si;
coherence
 A \/ B is Event of Si by Th3;
:: original:\
redefine funcA \ 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 )
proofend;

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 &amp; ( for D being Subset of Omega st D in Sigma holds
( ( p in D implies f . D = 1 ) &amp; ( not p in D implies f . D = 0 ) ) ) )
proofend;

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 ) &amp; ( not p in D implies P . D = 0 ) )
proofend;

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

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 funcP * 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 ) &amp; it . Omega = 1 &amp; ( for A, B being Event of Sigma st A misses B holds
it . (A \/ B) = (it . A) + (it . B) ) &amp; ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( it * ASeq is convergent &amp; 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 ) &amp; b1 . Omega = 1 &amp; ( for A, B being Event of Sigma st A misses B holds
b1 . (A \/ B) = (b1 . A) + (b1 . B) ) &amp; ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( b1 * ASeq is convergent &amp; lim (b1 * ASeq) = b1 . (Intersection ASeq) ) ) )
proofend;
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 ) &amp; b3 . Omega = 1 &amp; ( for A, B being Event of Sigma st A misses B holds
b3 . (A \/ B) = (b3 . A) + (b3 . B) ) &amp; ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( b3 * ASeq is convergent &amp; 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
proofend;
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
proofend;

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)
proofend;

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)
proofend;

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

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

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))
proofend;

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)))
proofend;

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))
proofend;

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)
proofend;

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 &amp; ( for Z being set st X c= Z &amp; Z is SigmaField of Omega holds
it c= Z ) );
existence
 ex b1 being SigmaField of Omega st
( X c= b1 &amp; ( for Z being set st X c= Z &amp; Z is SigmaField of Omega holds
b1 c= Z ) )
proofend;
uniqueness
 for b1, b2 being SigmaField of Omega st X c= b1 &amp; ( for Z being set st X c= Z &amp; Z is SigmaField of Omega holds
b1 c= Z ) &amp; X c= b2 &amp; ( for Z being set st X c= Z &amp; Z is SigmaField of Omega holds
b2 c= Z ) holds
b1 = b2
proofend;
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 &amp; ( for Z being set st X c= Z &amp; 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
proofend;
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
proofend;
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 funcF . x ->  Subset-Family of X;
coherence
 F . x is Subset-Family of X
proofend;
end;