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


begin

theorem :: PROB_1:1
canceled;

theorem :: PROB_1:2
canceled;

theorem Th3: :: PROB_1:3 [edit]
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
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 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 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 Th4: :: PROB_1:4 [edit]
for X being set
for A, B being Subset of X holds {A,B} is Subset-Family of X
proof end;

theorem :: PROB_1:5
canceled;

theorem :: PROB_1:6
canceled;

theorem :: PROB_1:7
canceled;

theorem :: PROB_1:8
canceled;

theorem Th9: :: PROB_1:9 [edit]
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 Th10: :: PROB_1:10 [edit]
for X being set
for F being Field_Subset of X holds {} in F
proof end;

theorem Th11: :: PROB_1:11 [edit]
for X being set
for F being Field_Subset of X holds X in F
proof end;

theorem Th12: :: PROB_1:12 [edit]
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:13 [edit]
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:14 [edit]
for X being set holds {{},X} is Field_Subset of X
proof end;

theorem :: PROB_1:15 [edit]
for X being set holds bool X is Field_Subset of X ;

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

theorem :: PROB_1:17
canceled;

theorem :: PROB_1:18 [edit]
for X, x, y, z being set st [x,y] in [:NAT,{X}:] & [x,z] in [:NAT,{X}:] holds
y = z
proof end;

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

theorem :: PROB_1:19
canceled;

theorem :: PROB_1:20
canceled;

theorem :: PROB_1:21
canceled;

theorem :: PROB_1:22
canceled;

theorem Th23: :: PROB_1:23 [edit]
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 Th23;
end;

theorem :: PROB_1:24
canceled;

theorem Th25: :: PROB_1:25 [edit]
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;

theorem Th26: :: PROB_1:26 [edit]
for X being set
for A1 being SetSequence of X ex B1 being SetSequence of X st
for n being Element of NAT holds B1 . n = (A1 . n) `
proof end;

definition
let X be set ;
let A1 be SetSequence of X;
canceled;
canceled;
func Complement A1 -> SetSequence of X means :Def4: :: PROB_1:def 4
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) `
by Th26;
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 PROB_1:def 2 :
canceled;

:: deftheorem PROB_1:def 3 :
canceled;

:: deftheorem Def4 defines Complement PROB_1:def 4 :
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 5
(Union (Complement A1)) ` ;
correctness
coherence
(Union (Complement A1)) ` is Subset of X
;
;
end;

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

theorem :: PROB_1:27
canceled;

theorem :: PROB_1:28
canceled;

theorem Th29: :: PROB_1:29 [edit]
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;

Lm2: for X being set
for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `)
proof end;

theorem Th30: :: PROB_1:30 [edit]
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 :Def6: :: PROB_1:def 6
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 7
for n, m being Element of NAT st n <= m holds
f . n c= f . m;
end;

:: deftheorem Def6 defines non-ascending PROB_1:def 6 :
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 7 :
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 :Def8: :: PROB_1:def 8
for A1 being SetSequence of X st rng A1 c= F holds
Intersection A1 in F;
end;

:: deftheorem Def8 defines sigma-multiplicative PROB_1:def 8 :
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 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 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:31
canceled;

theorem :: PROB_1:32 [edit]
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, Def8;

theorem :: PROB_1:33
canceled;

theorem :: PROB_1:34
canceled;

theorem Th35: :: PROB_1:35 [edit]
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 Event of ;
coherence
for b1 being SigmaField of X holds
( b1 is cap-closed & b1 is compl-closed )
by Th35;
end;

registration
let X be set ;
let Si be SigmaField of X;
cluster Relation-like NAT -defined Si -valued bool X -valued Function-like V34( NAT , bool X) Event of ;
existence
ex b1 being SetSequence of X st b1 is Si -valued
proof end;
end;

definition
let X be set ;
let Si be SigmaField of X;
mode SetSequence of Si is Si -valued SetSequence of X;
end;

theorem :: PROB_1:36
canceled;

theorem :: PROB_1:37
canceled;

theorem :: PROB_1:38
canceled;

theorem :: PROB_1:39
canceled;

theorem :: PROB_1:40
canceled;

theorem :: PROB_1:41
canceled;

theorem :: PROB_1:42
canceled;

theorem :: PROB_1:43
canceled;

theorem :: PROB_1:44
canceled;

theorem :: PROB_1:45
canceled;

theorem Th46: :: PROB_1:46 [edit]
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:47
canceled;

theorem :: PROB_1:48 [edit]
for X, x being set
for Si being SigmaField of X st x in Si holds
x is Event of Si ;

theorem :: PROB_1:49 [edit]
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:50 [edit]
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:51 [edit]
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 Th9;

theorem :: PROB_1:52 [edit]
for X being set
for Si being SigmaField of X holds {} is Event of Si by Th10;

theorem :: PROB_1:53 [edit]
for X being set
for Si being SigmaField of X holds X is Event of Si by Th11;

theorem :: PROB_1:54 [edit]
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 Th12;

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

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

:: deftheorem PROB_1:def 9 :
canceled;

:: deftheorem PROB_1:def 10 :
canceled;

:: deftheorem defines [#] PROB_1:def 11 :
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 Th9;
:: original: \
redefine func A \ B -> Event of Si;
coherence
A \ B is Event of Si
by Th12;
end;

theorem :: PROB_1:55
canceled;

theorem :: PROB_1:56
canceled;

theorem :: PROB_1:57 [edit]
for Omega being non empty set
for ASeq being SetSequence of Omega
for Sigma being SigmaField of Omega holds
( ASeq is SetSequence of Sigma iff for n being Element of NAT holds ASeq . n is Event of Sigma )
proof end;

theorem :: PROB_1:58 [edit]
for Omega being non empty 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 Th46;

theorem Th59: :: PROB_1:59 [edit]
for Omega being non empty set
for 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 Th60: :: PROB_1:60 [edit]
for Omega being non empty set
for 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 :: PROB_1:61
canceled;

theorem Th62: :: PROB_1:62 [edit]
for Omega being non empty 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 non empty 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 Th62;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
canceled;
mode Probability of Sigma -> Function of Sigma,REAL means :Def13: :: PROB_1:def 13
( ( 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 PROB_1:def 12 :
canceled;

:: deftheorem Def13 defines Probability PROB_1:def 13 :
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 Probability of Sigma;
coherence
for b1 being Probability of Sigma holds b1 is zeroed
proof end;
end;

theorem :: PROB_1:63
canceled;

theorem :: PROB_1:64
canceled;

theorem :: PROB_1:65
canceled;

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

theorem Th67: :: PROB_1:67 [edit]
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:68 [edit]
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 Th69: :: PROB_1:69 [edit]
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 Th70: :: PROB_1:70 [edit]
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:71 [edit]
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 Th72: :: PROB_1:72 [edit]
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 Th73: :: PROB_1:73 [edit]
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 Th74: :: PROB_1:74 [edit]
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:75 [edit]
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:76 [edit]
for X being set holds bool X is SigmaField of X ;

Lm3: for Omega being non empty set
for X being Subset-Family of Omega ex Y being SigmaField of Omega st
( X c= Y & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
Y c= Z ) )
proof end;

definition
let Omega be non empty set ;
let X be Subset-Family of Omega;
func sigma X -> SigmaField of Omega means :: PROB_1:def 14
( 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 ) )
by Lm3;
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 14 :
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 15
].-infty,r.[;
coherence
].-infty,r.[ is Subset of REAL
proof end;
end;

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

definition
func Family_of_halflines -> Subset-Family of REAL equals :: PROB_1:def 16
{ (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 16 :
Family_of_halflines = { (halfline r) where r is Element of REAL : verum } ;

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

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

theorem :: PROB_1:77 [edit]
for X being set
for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `) by Lm2;