PROB_1: $\sigma$-Fields and Probability

:: $\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 :

registration

let X be set ;

cluster bool X -> cap-closed ;

coherence

proof end;

end;

registration

let X be set ;

cluster bool X -> compl-closed for Subset-Family of X;

coherence ;

end;

registration

let X be set ;

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

existence

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

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

proof end;

uniqueness

proof end;

involutiveness

proof end;

end;

:: deftheorem Def2 defines Complement PROB_1:def 2 :

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 ;

end;

:: deftheorem defines Intersection PROB_1:def 3 :

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 :

:: deftheorem defines non-descending PROB_1:def 5 :

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 :

registration

let X be set ;

cluster bool X -> sigma-multiplicative for Subset-Family of X;

coherence ;

end;

registration

let X be set ;

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

existence

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

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

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

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 by Th5;

end;

:: deftheorem defines [#] PROB_1:def 7 :

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 by FINSUB_1:def 2;
:: original: \/
redefine func A \/ B -> Event of Si;
coherence by Th3;
:: original: \
redefine func A \ B -> Event of Si;
coherence 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 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

proof end;

end;

:: deftheorem Def8 defines Probability PROB_1:def 8 :

registration

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

cluster -> zeroed for Probability of Sigma;

coherence

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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines sigma PROB_1:def 9 :

definition

let r be ExtReal;

func halfline r -> Subset of REAL equals :: PROB_1:def 10
].-infty,r.[;

coherence

proof end;

end;

:: deftheorem defines halfline PROB_1:def 10 :

definition

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

coherence

proof end;

end;

:: deftheorem defines Family_of_halflines PROB_1:def 11 :

definition

func Borel_Sets -> SigmaField of REAL equals :: PROB_1:def 12
sigma Family_of_halflines;

correctness ;

end;

:: deftheorem defines Borel_Sets PROB_1:def 12 :

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

proof end;

end;