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

theorem Th1: :: PROB_1:1

for r being Real
for seq being Real_Sequence st ex n being Nat st
for m being 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 b₁ being Subset-Family of X st b₁ = bool X holds
b₁ is compl-closed ;

end;

registration

let X be set ;

cluster non empty cap-closed compl-closed for Event of ;

existence
ex b₁ being Subset-Family of X st
( not b₁ is empty & b₁ is compl-closed & b₁ 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 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 Nat holds it . n = (A1 . n) ` ;

existence
ex b₁ being SetSequence of X st
for n being Nat holds b₁ . n = (A1 . n) `

proof end;

uniqueness
for b₁, b₂ being SetSequence of X st ( for n being Nat holds b₁ . n = (A1 . n) ` ) & ( for n being Nat holds b<sub>2</sub> . n = (A1 . n) ` ) holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being SetSequence of X st ( for n being Nat holds b₁ . n = (b₂ . n) ` ) holds
for n being Nat holds b<sub>2</sub> . n = (b<sub>1</sub> . n) `

proof end;

end;

:: deftheorem Def2 defines Complement PROB_1:def 2 :
for X being set
for A1, b₃ being SetSequence of X holds
( b₃ = Complement A1 iff for n being Nat holds b₃ . 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 being set
for A1 being SetSequence of X
for x being object holds
( x in Intersection A1 iff for n being 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 :: PROB_1:def 4
for n, m being Nat st n <= m holds
f . m c= f . n;

attr f is non-descending means :: PROB_1:def 5
for n, m being Nat st n <= m holds
f . n c= f . m;

end;

:: deftheorem defines non-ascending PROB_1:def 4 :
for f being Function holds
( f is non-ascending iff for n, m being 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 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 b₁ being Subset-Family of X st b₁ = bool X holds
b₁ is sigma-multiplicative ;

end;

registration

let X be set ;

cluster non empty compl-closed sigma-multiplicative for Event of ;

existence
ex b₁ being Subset-Family of X st
( b₁ is compl-closed & b₁ is sigma-multiplicative & not b₁ 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 X, Y 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 b₁ being SigmaField of X holds
( b₁ is cap-closed & b₁ 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 V40( NAT , bool X) for Event of ;

existence
ex b₁ being SetSequence of X st b₁ 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 b₁ being Event of holds b₁ 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 b₁ being Event of Si st b₁ 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 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 b₁ being Function of Sigma,REAL st
( ( for A being Event of Sigma holds 0 <= b₁ . A ) & b₁ . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
b₁ . (A \/ B) = (b₁ . A) + (b₁ . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( b₁ * ASeq is convergent & lim (b₁ * ASeq) = b₁ . (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 b₃ being Function of Sigma,REAL holds
( b₃ is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= b₃ . A ) & b₃ . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
b₃ . (A \/ B) = (b₃ . A) + (b₃ . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( b₃ * ASeq is convergent & lim (b₃ * ASeq) = b₃ . (Intersection ASeq) ) ) ) );

registration

let Omega be non empty set ;
let Sigma be SigmaField of Omega;

cluster -> zeroed for Probability of Sigma;

coherence
for b₁ being Probability of Sigma holds b₁ 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 b₁ being SigmaField of Omega st
( X c= b₁ & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b₁ c= Z ) )

proof end;

uniqueness
for b₁, b₂ being SigmaField of Omega st X c= b₁ & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b₁ c= Z ) & X c= b₂ & ( for Z being set st X c= Z & Z is SigmaField of Omega holds
b₂ c= Z ) holds
b₁ = b₂

proof end;

end;

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

definition

let r be ExtReal;

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