:: $\sigma$-Fields and Probability
:: by Andrzej N\c{e}dzusiak
::
:: Received October 16, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, FUNCT_1, SEQ_1, XXREAL_0, SEQ_2,
ORDINAL2, CARD_1, ARYTM_3, COMPLEX1, ARYTM_1, SETFAM_1, FINSUB_1,
ZFMISC_1, TARSKI, RELAT_1, CARD_3, EQREL_1, FUNCT_7, FUNCOP_1, NAT_1,
RPR_1, REAL_1, VALUED_0, XXREAL_1, PROB_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSUB_1, RELAT_1, FUNCT_1,
XCMPLX_0, REAL_1, FUNCT_2, FUNCOP_1, FUNCT_7, ORDINAL1, CARD_3, NUMBERS,
VALUED_0, XREAL_0, COMPLEX1, NAT_1, SEQ_1, COMSEQ_2, SEQ_2, SETFAM_1,
XXREAL_0, XXREAL_1;
constructors SETFAM_1, FINSUB_1, XXREAL_1, COMPLEX1, REAL_1, SEQ_2, CARD_3,
MEMBERED, FUNCT_7, RELSET_1, COMSEQ_2, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0,
XREAL_0, XXREAL_1, RELAT_1, VALUED_0, RELSET_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FINSUB_1, TARSKI, MEMBERED, FUNCT_2, VALUED_0;
equalities SUBSET_1, CARD_3;
expansions TARSKI, FUNCT_2;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, ABSVALUE, SEQ_2, SETFAM_1,
SUBSET_1, RELAT_1, RELSET_1, FINSUB_1, FUNCOP_1, XBOOLE_0, XBOOLE_1,
XREAL_1, XXREAL_0, XXREAL_1, FUNCT_7, NAT_1, ORDINAL1, XREAL_0;
schemes FUNCT_2, PARTFUN1;
begin
reserve Omega for set;
reserve X, Y, Z, p,x,y,z for set;
reserve D, E for Subset of Omega;
reserve f for Function;
reserve m,n for Nat;
reserve r,r1 for Real;
reserve seq for Real_Sequence;
theorem Th1:
for r,seq st (ex n st for m st n <= m holds seq.m = r) holds seq
is convergent & lim seq = r
proof
let r,seq such that
A1: ex n st for m st n <= m holds seq.m = r;
A2: for r1 st 0 < r1 ex n st for m st n <= m holds |.seq.m-r.|<r1
proof
consider n such that
A3: for m st n <= m holds seq.m = r by A1;
let r1 such that
A4: 0 < r1;
take n;
let m;
assume n <= m;
then seq.m = r by A3;
hence thesis by A4,ABSVALUE:2;
end;
then seq is convergent by SEQ_2:def 6;
hence thesis by A2,SEQ_2:def 7;
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:
for A being Subset of X st A in IT holds A` in IT;
end;
registration
let X be set;
cluster bool X -> cap-closed;
coherence
proof
let A, B be set;
assume that
A1: A in bool X and
B in bool X;
A /\ B c= X by A1,XBOOLE_1:108;
hence thesis;
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 compl-closed cap-closed for Subset-Family of X;
existence
proof
take bool X;
thus thesis;
end;
end;
definition
let X be set;
mode Field_Subset of X is non empty compl-closed cap-closed
Subset-Family of X;
end;
reserve F for Field_Subset of X;
theorem Th2:
for A,B being Subset of X holds {A,B} is Subset-Family of X
proof
let A,B be Subset of X;
set C = {A,B};
C c= bool X
proof
let x be object;
assume x in C;
then x = A or x = B by TARSKI:def 2;
hence thesis;
end;
hence thesis;
end;
theorem Th3:
for A, B being set st A in F & B in F holds A \/ B in F
proof
let A, B be set;
assume
A1: A in F & B in F;
then reconsider A1 = A, B1 = B as Subset of X;
A1` in F & B1` in F by A1,Def1;
then A1` /\ B1` in F by FINSUB_1:def 2;
then (A1 \/ B1)` in F by XBOOLE_1:53;
then (A1 \/ B1)`` in F by Def1;
hence thesis;
end;
theorem Th4:
{} in F
proof
consider A being Subset of X such that
A1: A in F by SUBSET_1:4;
A misses A` by XBOOLE_1:79;
then
A2: A /\ A` = {} by XBOOLE_0:def 7;
A` in F by A1,Def1;
hence thesis by A1,A2,FINSUB_1:def 2;
end;
theorem Th5:
X in F
proof
consider A being Subset of X such that
A1: A in F by SUBSET_1:4;
A2: A \/ A` = [#] X by SUBSET_1:10
.= X;
A` in F by A1,Def1;
hence thesis by A1,A2,Th3;
end;
theorem Th6:
for A,B being Subset of X holds A in F & B in F implies A \ B in F
proof
let A,B be Subset of X;
assume
A1: A in F;
assume B in F;
then B` in F by Def1;
then A /\ B` in F by A1,FINSUB_1:def 2;
hence thesis by SUBSET_1:13;
end;
theorem
for A, B being set holds (A in F & B in F implies (A \ B) \/ B in F)
proof
let A, B be set;
A \/ B = (A \ B) \/ B by XBOOLE_1:39;
hence thesis by Th3;
end;
registration
let X be set;
cluster { {}, X } -> cap-closed;
coherence
proof
let A,B be set;
A1: (A = {} or B = {}) implies A /\ B = {};
A = X & B = X implies A /\ B = X;
hence thesis by A1,TARSKI:def 2;
end;
end;
theorem
{ {}, X } is Field_Subset of X
proof
{} c= X & X in bool X by ZFMISC_1:def 1;
then reconsider EX = { {}, X } as Subset-Family of X by Th2;
now
let A be Subset of X;
A1: A = {} implies A` = X;
A = X implies A` = {} X by XBOOLE_1:37;
hence A in EX implies A` in EX by A1,TARSKI:def 2;
end;
hence thesis by Def1;
end;
theorem
bool X is Field_Subset of X;
theorem
{ {} , X } c= F & F c= bool X
proof
{} in F & X in F by Th4,Th5;
then for x being object holds x in { {} , X } implies x in F
by TARSKI:def 2;
hence thesis;
end;
definition
let X be set;
mode SetSequence of X is sequence of bool X;
end;
reserve ASeq,BSeq for SetSequence of Omega;
reserve A1 for SetSequence of X;
theorem Th11:
union rng A1 is Subset of X
proof
for Y st Y in rng A1 holds Y c= X
proof
let Y;
assume Y in rng A1;
then consider y being object such that
A1: y in dom A1 and
A2: Y = A1.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A1,FUNCT_2:def 1;
Y = A1.y by A2;
hence thesis;
end;
hence thesis by ZFMISC_1:76;
end;
definition
let X be set, A1 be SetSequence of X;
redefine func Union A1 -> Subset of X; :: redefines Union (CARD_3, definition)
coherence by Th11;
end;
theorem Th12:
x in Union A1 iff ex n st x in A1.n
proof
set DX = union rng A1;
for x holds x in DX iff ex n st x in A1.n
proof
let x;
thus x in DX implies ex n st x in A1.n
proof
assume x in DX;
then consider Y such that
A1: x in Y and
A2: Y in rng A1 by TARSKI:def 4;
consider p being object such that
A3: p in dom A1 and
A4: Y = A1.p by A2,FUNCT_1:def 3;
p in NAT by A3,FUNCT_2:def 1;
hence thesis by A1,A4;
end;
thus (ex n st x in A1.n) implies x in DX
proof
given n such that
A5: x in A1.n;
n in NAT by ORDINAL1:def 12;
then n in dom A1 by FUNCT_2:def 1;
then A1.n in rng A1 by FUNCT_1:def 3;
hence thesis by A5,TARSKI:def 4;
end;
end;
hence thesis;
end;
definition
let X be set, A1 be SetSequence of X;
func Complement A1 -> SetSequence of X means
:Def2:
for n holds it.n = (A1.n )`;
existence
proof
deffunc F(Element of NAT) = (A1.$1)`;
consider f being sequence of bool X such that
A1: for x being Element of NAT holds f.x = F(x) from FUNCT_2:sch 4;
A2: for x being Nat holds f.x = (A1.x)`
proof let x be Nat;
reconsider x as Element of NAT by ORDINAL1:def 12;
f.x= F(x) by A1;
hence thesis;
end;
take f;
thus thesis by A2;
end;
uniqueness
proof
let BSeq,CSeq be SetSequence of X such that
A3: for n holds BSeq.n = (A1.n)` and
A4: for m holds CSeq.m = (A1.m)`;
A5: for x being object st x in NAT holds BSeq.x = CSeq.x
proof
let x be object;
assume x in NAT;
then reconsider x as Element of NAT;
BSeq.x = (A1.x)` by A3
.= CSeq.x by A4;
hence thesis;
end;
thus thesis by A5;
end;
involutiveness
proof
let IT,A1 be SetSequence of X;
assume
A6: for n holds IT.n = (A1.n)`;
let n;
thus A1.n = (A1.n)`` .= (IT.n)` by A6;
end;
end;
definition
let X be set, A1 be SetSequence of X;
func Intersection A1 -> Subset of X equals
(Union Complement A1)`;
correctness;
end;
theorem Th13:
for x being object holds x in Intersection A1 iff for n holds x in A1.n
proof let x be object;
A1: for n holds X \ (Complement A1).n = A1.n
proof
let n;
X \ (Complement A1).n = ((A1.n)`)` by Def2
.= A1.n;
hence thesis;
end;
A2: (for n holds (x in X & not x in (Complement A1).n)) iff for n holds x in
A1.n
proof
thus (for n holds (x in X & not x in (Complement A1).n)) implies for n
holds x in A1.n
proof
assume
A3: for n holds x in X & not x in (Complement A1).n;
let n;
not x in (Complement A1).n by A3;
then x in X \ (Complement A1).n by A3,XBOOLE_0:def 5;
hence thesis by A1;
end;
assume
A4: for n holds x in A1.n;
let n;
x in A1.n by A4;
then x in X \ (Complement A1).n by A1;
hence thesis by XBOOLE_0:def 5;
end;
x in X & not x in Union Complement A1 iff x in X & for n holds not x in
(Complement A1).n by Th12;
hence thesis by A2,XBOOLE_0:def 5;
end;
Lm1: for A, B being Subset of X holds Complement (A followed_by B) = A`
followed_by B`
proof
let A,B be Subset of X;
let n be Element of NAT;
per cases by NAT_1:3;
suppose
A1: n=0;
thus (Complement (A followed_by B)).n = ((A followed_by B).n)` by Def2
.= A` by A1,FUNCT_7:119
.= (A` followed_by B`).n by A1,FUNCT_7:119;
end;
suppose
A2: n>0;
thus (Complement (A followed_by B)).n = ((A followed_by B).n)` by Def2
.= B` by A2,FUNCT_7:120
.= (A` followed_by B`).n by A2,FUNCT_7:120;
end;
end;
theorem Th14:
for A, B being Subset of X holds Intersection(A followed_by B) = A /\ B
proof
let A, B be Subset of X;
set A1 = A followed_by B;
Complement A1= A` followed_by B` by Lm1;
then rng Complement A1 = {A`,B`} by FUNCT_7:126;
then Union Complement A1 = A` \/ B` by ZFMISC_1:75;
then (Union Complement A1)` = A`` /\ B`` by XBOOLE_1:53;
hence thesis;
end;
definition
let f be Function;
attr f is non-ascending means
for n,m st n <= m holds f.m c= f.n;
attr f is non-descending means
for n,m st n <= m holds f.n c= f.m;
end;
definition
let X be set, F be Subset-Family of X;
attr F is sigma-multiplicative means
:Def6:
for A1 being SetSequence of X st rng A1 c= F holds Intersection A1 in F;
end;
registration
let X be set;
cluster bool X -> sigma-multiplicative for Subset-Family of X;
coherence;
end;
registration
let X be set;
cluster compl-closed sigma-multiplicative non empty for Subset-Family of X;
existence
proof
take bool X;
thus thesis;
end;
end;
definition
let X be set;
mode SigmaField of X is compl-closed sigma-multiplicative non empty
Subset-Family of X;
end;
theorem
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:
Y is SigmaField of X implies Y is Field_Subset of X
proof
assume
A1: Y is SigmaField of X;
Y is cap-closed
proof
let A,B be set;
assume
A2: A in Y & B in Y;
then reconsider A9 = A, B9 = B as Subset of X by A1;
set A1 = A9 followed_by B9;
rng A1 = {A9,B9} by FUNCT_7:126;
then
A3: rng A1 c= Y by A2,ZFMISC_1:32;
Intersection A1 = A /\ B by Th14;
hence thesis by A1,A3,Def6;
end;
hence thesis by A1;
end;
registration
let X be set;
cluster -> cap-closed compl-closed for SigmaField of X;
coherence by Th16;
end;
reserve Sigma for SigmaField of Omega;
reserve Si for SigmaField of X;
:: 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, F be non empty Subset-Family of X;
cluster F-valued for SetSequence of X;
existence
proof
set A1 = NAT --> the Element of F;
reconsider A1 as SetSequence of X by FUNCOP_1:45;
take A1;
thus thesis;
end;
end;
definition
let X be set, F be non empty Subset-Family of X;
mode SetSequence of F is F-valued SetSequence of X;
end;
theorem Th17:
for ASeq being SetSequence of Si holds Union ASeq in Si
proof
let ASeq be SetSequence of Si;
A1: rng A1 c= Si implies for n being Nat holds (Complement A1).n in Si
proof
assume
A2: rng A1 c= Si;
let n be Nat;
A1.n in rng A1 by NAT_1:51;
then n in NAT & (A1.n)` in Si by A2,Def1,ORDINAL1:def 12;
hence thesis by Def2;
end;
A3: rng A1 c= Si implies Union Complement Complement A1 in Si
proof
assume rng A1 c= Si;
then for n being Nat holds (Complement A1).n in Si by A1;
then rng Complement A1 c= Si by NAT_1:52;
then Intersection Complement A1 in Si by Def6;
then (Union Complement Complement A1)`` in Si by Def1;
hence thesis;
end;
A4: for A1 st rng A1 c= Si holds Union A1 in Si
proof
let A1;
assume rng A1 c= Si;
then Union Complement Complement A1 in Si by A3;
hence thesis;
end;
rng ASeq c= Si by RELAT_1:def 19;
hence thesis by A4;
end;
notation
let X be set; let F be SigmaField of X;
synonym Event of F for Element of F;
end;
definition
let X be set, F be SigmaField of X;
redefine mode Event of F -> Subset of X; :: redefines Event (PROB_1, synonym) → Element (SUBSET_1, definition)
coherence
proof
let E be Event of F;
E in F;
hence thesis;
end;
end;
theorem
x in Si implies x is Event of Si;
theorem
for A,B being Event of Si holds A /\ B is Event of Si by FINSUB_1:def 2;
theorem
for A being Event of Si holds A` is Event of Si by Def1;
theorem
for A,B being Event of Si holds A \/ B is Event of Si by Th3;
theorem
{} is Event of Si by Th4;
theorem
X is Event of Si by Th5;
theorem
for A,B being Event of Si holds A \ B is Event of Si by Th6;
registration
let X,Si;
cluster empty for Event of Si;
existence
proof
{} is Event of Si by Th4;
hence thesis;
end;
end;
definition
let X,Si;
func [#] Si -> Event of Si equals
X;
coherence by Th5;
end;
definition
let X,Si;
let A,B be Event of Si;
redefine func A /\ B -> Event of Si; :: redefines /\ (XBOOLE_0, definition)
coherence by FINSUB_1:def 2;
redefine func A \/ B -> Event of Si; :: redefines \/ (XBOOLE_0, definition)
coherence by Th3;
redefine func A \ B -> Event of Si; :: redefines \ (XBOOLE_0, definition)
coherence by Th6;
end;
theorem
A1 is SetSequence of Si iff for n holds A1.n is Event of Si
proof
thus A1 is SetSequence of Si implies for n holds A1.n is Event of
Si
proof
assume A1 is SetSequence of Si;
then
A1: rng A1 c= Si by RELAT_1:def 19;
for n holds A1.n is Event of Si
by NAT_1:51,A1;
hence thesis;
end;
assume
A2: for n holds A1.n is Event of Si;
for n be Nat holds A1.n in Si
proof
let n be Nat;
A1.n is Event of Si by A2;
hence thesis;
end;
then rng A1 c= Si by NAT_1:52;
hence thesis by RELAT_1:def 19;
end;
theorem
ASeq is SetSequence of Sigma implies Union ASeq is Event of Sigma by Th17;
:: DEFINITION OF sigma-ADDITIVE PROBABILITY
reserve A, B for Event of Sigma,
ASeq for SetSequence of Sigma;
theorem Th27:
ex f st (dom f = Sigma & for D st D in Sigma holds (p in D
implies f.D = 1) & (not p in D implies f.D = 0))
proof
deffunc G(set) = 0;
deffunc F(set) = 1;
defpred C[set] means p in $1;
ex f being Function st dom f = Sigma & for x being set st x in Sigma
holds (C[x] implies f.x=F(x)) & (not C[x] implies f.x=G(x))
from PARTFUN1:sch 5;
then consider f being Function such that
A1: dom f = Sigma and
A2: for x being set st x in Sigma holds (C[x] implies f.x = 1) & (not C[
x] implies f.x = 0);
take f;
thus dom f = Sigma by A1;
let D;
assume
A3: D in Sigma;
hence p in D implies f.D = 1 by A2;
assume not p in D;
hence thesis by A2,A3;
end;
reserve P for Function of Sigma,REAL;
theorem Th28:
ex P st for D st D in Sigma holds (p in D implies P.D = 1) & (
not p in D implies P.D = 0)
proof
consider f such that
A1: dom f = Sigma and
A2: for D st D in Sigma holds (p in D implies f.D = 1) & (not p in D
implies f.D = 0) by Th27;
A3: 0 in REAL by XREAL_0:def 1;
rng f c= REAL
proof
let y be object;
assume y in rng f;
then consider x being object such that
A4: x in dom f and
A5: y = f.x by FUNCT_1:def 3;
reconsider x as Subset of Omega by A1,A4;
reconsider j = 1 as Real;
A6: 1 in REAL by XREAL_0:def 1;
A7: not p in x implies y = 0 by A1,A2,A4,A5;
p in x implies y = j by A1,A2,A4,A5;
hence thesis by A7,A3,A6;
end;
then reconsider f as Function of Sigma,REAL by A1,FUNCT_2:def 1,RELSET_1:4;
take f;
thus thesis by A2;
end;
theorem Th29:
P * ASeq is Real_Sequence
proof
rng ASeq c= Sigma by RELAT_1:def 19;
then rng ASeq c= dom P by FUNCT_2:def 1;
then
A1: dom (P * ASeq) = dom ASeq by RELAT_1:27
.= NAT by FUNCT_2:def 1;
rng (P * ASeq) c= REAL by RELAT_1:def 19;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
end;
definition
let Omega,Sigma,ASeq,P;
redefine func P * ASeq -> Real_Sequence; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence by Th29;
end;
reserve Omega for non empty set;
reserve Sigma for SigmaField of Omega;
reserve A, B for Event of Sigma,
ASeq for SetSequence of Sigma;
reserve P for Function of Sigma,REAL;
reserve D, E for Subset of Omega;
reserve BSeq for SetSequence of Omega;
definition
let Omega,Sigma;
mode Probability of Sigma -> Function of Sigma,REAL means
:Def8:
(for A holds 0 <= it.A) & it.Omega = 1 &
(for A,B st A misses B holds it.(A \/ B) = it.A + it.B) &
for ASeq st ASeq is non-ascending holds it * ASeq is convergent &
lim (it * ASeq) = it.Intersection ASeq;
existence
proof
set p = the Element of Omega;
consider P such that
A1: for D st D in Sigma holds (p in D implies P.D = 1) & (not p in D
implies P.D = 0) by Th28;
take P;
thus for A holds 0 <= P.A by A1;
[#]Sigma in Sigma;
hence P.Omega = 1 by A1;
thus for A,B st A misses B holds P.(A \/ B) = P.A + P.B
proof
let A,B such that
A2: A misses B;
A3: p in A & not p in B implies p in A \/ B by XBOOLE_0:def 3;
A4: not p in A & p in B implies P.A = 0 & P.B = 1 by A1;
A5: not p in A & p in B implies p in A \/ B by XBOOLE_0:def 3;
A6: not p in A & not p in B implies P.A = 0 & P.B = 0 by A1;
A7: not p in A & not p in B implies not p in (A \/ B) by XBOOLE_0:def 3;
p in A & not p in B implies P.A = 1 & P.B = 0 by A1;
hence thesis by A1,A2,A3,A4,A5,A6,A7,XBOOLE_0:3;
end;
let ASeq;
A8: for n holds (P * ASeq).n = P.(ASeq.n)
proof
let n;
reconsider n as Element of NAT by ORDINAL1:def 12;
dom (P * ASeq) = NAT by FUNCT_2:def 1;
then (P * ASeq).n = P.(ASeq.n) by FUNCT_1:12;
hence thesis;
end;
A9: (for n holds p in ASeq.n) implies for n holds (P * ASeq).n = 1
proof
assume
A10: for n holds p in ASeq.n;
for n holds (P * ASeq).n = 1
proof
let n;
A11: rng ASeq c= Sigma & ASeq.n in rng ASeq by NAT_1:51,RELAT_1:def 19;
p in ASeq.n by A10;
then P.(ASeq.n) = 1 by A1,A11;
hence thesis by A8;
end;
hence thesis;
end;
assume
A12: ASeq is non-ascending;
A13: not (for n holds p in ASeq.n) implies ex m st for n st m <= n holds
(P * ASeq).n = 0
proof
assume not (for n holds p in ASeq.n);
then consider m such that
A14: not p in ASeq.m;
take m;
for n st m <= n holds (P * ASeq).n = 0
proof
let n;
assume m <= n;
then ASeq.n c= ASeq.m by A12;
then
A15: not p in ASeq.n by A14;
rng ASeq c= Sigma & ASeq.n in rng ASeq by NAT_1:51,RELAT_1:def 19;
then P.(ASeq.n) = 0 by A1,A15;
hence thesis by A8;
end;
hence thesis;
end;
A16: (ex m st (for n st m <= n holds (P * ASeq).n = 0)) implies P * ASeq
is convergent & lim (P * ASeq) = 0 by Th1;
rng ASeq c= Sigma by RELAT_1:def 19;
then
A17: Intersection ASeq in Sigma by Def6;
reconsider r = 1 as Real;
A18: (for n holds (P * ASeq).n = 1) implies P * ASeq is convergent & lim
(P * ASeq) = 1
proof
assume
A19: for n holds (P * ASeq).n = 1;
ex m st for n st m <= n holds (P * ASeq).n = r
proof
take 0;
thus thesis by A19;
end;
hence thesis by Th1;
end;
per cases;
suppose
A20: not (for n holds p in ASeq.n);
then not p in Intersection ASeq by Th13;
hence thesis by A1,A13,A16,A20,A17;
end;
suppose
A21: for n holds p in ASeq.n;
then p in Intersection ASeq by Th13;
hence thesis by A1,A9,A18,A21,A17;
end;
end;
end;
reserve P for Probability of Sigma;
registration
let Omega,Sigma;
cluster -> zeroed for Probability of Sigma;
coherence
proof
reconsider E = {} as Event of Sigma by Th4;
let P be Probability of Sigma;
A1: {} misses ([#] Sigma) & {} \/ ([#] Sigma) = [#] Sigma by XBOOLE_1:65;
1 = P.([#] Sigma) by Def8;
then 1 = P.E + 1 by A1,Def8;
hence P.{} = 0;
end;
end;
theorem
P.([#] Sigma) = 1 by Def8;
theorem Th31:
P.(([#] Sigma) \ A) + P.A = 1
proof
A1: (([#] Sigma) \ A) \/ A = A` \/ A .= [#] Omega by SUBSET_1:10
.= Omega;
(([#] Sigma) \ A) misses A by XBOOLE_1:79;
then P.(([#] Sigma) \ A) + P.A = P.Omega by A1,Def8
.= 1 by Def8;
hence thesis;
end;
theorem
P.(([#] Sigma) \ A) = 1 - P.A
proof
P.(([#] Sigma) \ A) + P.A = 1 by Th31;
hence thesis;
end;
theorem Th33:
A c= B implies P.(B \ A) = P.B - P.A
proof
assume
A1: A c= B;
A misses (B \ A) by XBOOLE_1:79;
then P.A + P.(B \ A) = P.(A \/ (B \ A)) by Def8
.= P.B by A1,XBOOLE_1:45;
hence thesis;
end;
theorem Th34:
A c= B implies P.A <= P.B
proof
assume A c= B;
then P.(B \ A) = P.B - P.A by Th33;
then 0 <= P.B - P.A by Def8;
then 0 + P.A <= P.B by XREAL_1:19;
hence thesis;
end;
theorem
P.A <= 1
proof
P.([#] Sigma) = 1 by Def8;
hence thesis by Th34;
end;
theorem Th36:
P.(A \/ B) = P.A + P.(B \ A)
proof
A1: A misses (B \ A) by XBOOLE_1:79;
P.(A \/ B) = P.(A \/ (B \ A)) by XBOOLE_1:39
.= P.A + P.(B \ A) by A1,Def8;
hence thesis;
end;
theorem Th37:
P.(A \/ B) = P.A + P.(B \ (A /\ B))
proof
thus P.(A \/ B) = P.A + P.(B \ A) by Th36
.= P.A + P.(B \ (A /\ B)) by XBOOLE_1:47;
end;
theorem Th38:
P.(A \/ B) = P.A + P.B - P.(A /\ B)
proof
P.(A \/ B) = P.A + P.(B \ (A /\ B)) by Th37
.= P.A + (P.B - P.(A /\ B)) by Th33,XBOOLE_1:17;
hence thesis;
end;
theorem
P.(A \/ B) <= P.A + P.B
proof
0 <= P.(A /\ B) & P.(A \/ B) = P.A + P.B - P.(A /\ B) by Def8,Th38;
hence thesis by XREAL_1:43;
end;
:: definition of sigma-field generated by families
:: of subsets of given set and family of Borel Sets
reserve D for Subset of REAL;
reserve S for Subset-Family of Omega;
theorem
bool X is SigmaField of X;
definition
let Omega;
let X be Subset-Family of Omega;
func sigma(X) -> SigmaField of Omega means
X c= it & for Z st X c= Z & Z is SigmaField of Omega holds it c= Z;
existence
proof
set V = { S : X c= S & S is SigmaField of Omega};
set Y = meet V;
A1: now
let Z;
assume Z in V;
then ex S st Z = S & X c= S & S is SigmaField of Omega;
hence X c= Z;
end;
A2: bool Omega in V;
A3: for E st E in Y holds E` in Y
proof
let E such that
A4: E in Y;
now
let Z;
assume Z in V;
then E in Z & ex S st Z = S & X c= S & S is SigmaField of Omega by A4,
SETFAM_1:def 1;
hence E` in Z by Def1;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
A5: for BSeq st rng BSeq c= Y holds Intersection BSeq in Y
proof
let BSeq such that
A6: rng BSeq c= Y;
now
let Z;
assume
A7: Z in V;
now
let n be Nat;
BSeq.n in rng BSeq by NAT_1:51;
hence BSeq.n in Z by A6,A7,SETFAM_1:def 1;
end;
then
A8: rng BSeq c= Z by NAT_1:52;
ex S st Z = S & X c= S & S is SigmaField of Omega by A7;
hence Intersection BSeq in Z by A8,Def6;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
now
let Z;
assume Z in V;
then ex S st Z = S & X c= S & S is SigmaField of Omega;
hence {} in Z by Th4;
end;
then reconsider Y as SigmaField of Omega by A2,A5,A3,Def1,Def6,SETFAM_1:3
,def 1;
take Y;
for Z st X c= Z & Z is SigmaField of Omega holds Y c= Z
proof
let Z;
assume that
A9: X c= Z and
A10: Z is SigmaField of Omega;
reconsider Z as Subset-Family of Omega by A10;
Z in V by A9,A10;
hence thesis by SETFAM_1:3;
end;
hence thesis by A2,A1,SETFAM_1:5;
end;
uniqueness
proof
let R1,R2 be SigmaField of Omega;
assume X c= R1 & ( for Z st X c= Z & Z is SigmaField of Omega holds R1 c=
Z)& X c= R2 & for Z st X c= Z & Z is SigmaField of Omega holds R2 c= Z;
then R1 c= R2 & R2 c= R1;
hence thesis by XBOOLE_0:def 10;
end;
end;
definition
let r be ExtReal;
func halfline r -> Subset of REAL equals
].-infty,r.[;
coherence
proof
].-infty,r.[ c= REAL
proof
let x be Real;
assume x in ].-infty,r.[;
then -infty < x & x < r by XXREAL_1:4;
hence thesis by XXREAL_0:48;
end;
hence thesis;
end;
end;
definition
func Family_of_halflines -> Subset-Family of REAL equals
the set of all halfline(r) where r is Element of REAL;
coherence
proof
the set of all halfline(r) where r is Element of REAL
c= bool REAL
proof
let p be object;
assume p in the set of all halfline(r) where r is Element of REAL;
then ex r being Element of REAL st p = halfline(r);
hence p in bool REAL;
end;
hence thesis;
end;
end;
definition
func Borel_Sets -> SigmaField of REAL equals
sigma(Family_of_halflines);
correctness;
end;
theorem
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;
redefine func F.x -> Subset-Family of X; :: redefines . (FUNCT_1, definition)
coherence
proof
per cases;
suppose
A1: x in dom F;
A2: rng F c= bool A by RELAT_1:def 19;
A3: bool A c= bool bool X by ZFMISC_1:67;
F.x in rng F by A1,FUNCT_1:def 3;
then F.x in bool A by A2;
hence thesis by A3;
end;
suppose
not x in dom F;
then F.x = {} by FUNCT_1:def 2;
hence thesis by XBOOLE_1:2;
end;
end;
end;