Copyright (c) 1989 Association of Mizar Users
environ
vocabulary FUNCT_1, ARYTM, SEQ_1, ARYTM_1, SEQ_2, ORDINAL2, ABSVALUE,
SETFAM_1, SUBSET_1, FINSUB_1, BOOLE, RELAT_1, FUNCOP_1, TARSKI, PROB_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSUB_1, RELAT_1, FUNCT_1,
REAL_1, FUNCT_2, FUNCOP_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1,
ABSVALUE, SEQ_1, SEQ_2, SETFAM_1;
constructors ABSVALUE, SEQ_2, SETFAM_1, FINSUB_1, FUNCOP_1, XCMPLX_0,
MEMBERED, XBOOLE_0;
clusters FUNCT_1, XREAL_0, RELSET_1, SUBSET_1, FUNCOP_1, MEMBERED, ZFMISC_1,
XBOOLE_0, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FINSUB_1, TARSKI;
theorems TARSKI, ZFMISC_1, FUNCT_1, REAL_1, FUNCT_2, ABSVALUE, SEQ_2,
SETFAM_1, SUBSET_1, RELAT_1, RELSET_1, FINSUB_1, FUNCOP_1, XBOOLE_0,
XBOOLE_1, XCMPLX_1;
schemes FUNCT_2, PARTFUN1;
begin
reserve Omega for non empty 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,r2 for real number;
reserve seq for Real_Sequence;
:::::::::::::::::::::::::::::::::::::::
:: corrolaries from other articles ::
:::::::::::::::::::::::::::::::::::::::
canceled;
theorem
Th2: for r,r2 st 0 <= r holds r2 - r <= r2
proof let r,r2;
0 <= r implies r2 - r <= r2 - 0 by REAL_1:92;
hence thesis;
end;
theorem
Th3: 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 abs(seq.m-r)<r1
proof let r1 such that
A3: 0 < r1;
consider n such that
A4: for m st n <= m holds seq.m = r by A1;
take n;
let m; assume n <= m;
then seq.m = r by A4;
then seq.m - r = 0 by XCMPLX_1:14;
hence thesis by A3,ABSVALUE:7;
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;
definition let X be set;
cluster non empty compl-closed cap-closed Subset-Family of X;
existence
proof
reconsider S = bool X as Subset-Family of X by SETFAM_1:def 7;
take S;
thus S is non empty;
thus S is compl-closed
proof
let A be Subset of X; assume A in S;
thus thesis;
end;
thus S is cap-closed
proof
let A, B be set; assume A in S & B in S;
then A /\ B c= X by XBOOLE_1:108;
hence thesis;
end;
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 Th4:
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 set;
assume x in C;
then x = A or x = B by TARSKI:def 2;
hence thesis;
end;
hence thesis by SETFAM_1:def 7;
end;
canceled;
theorem Th6:
ex A being Subset of X st A in F
proof consider A being Element of F;
A in F & F c= bool X;
hence thesis;
end;
canceled 2;
theorem Th9:
for A, B being set st A in F & B in F holds A \/ B in F
proof
let A, B be set;
assume that
A1: A in F and
A2: B in F;
reconsider A1 = A, B1 = B as Subset of X by A1,A2;
A3: A1` in F by A1,Def1;
B1` in F by A2,Def1;
then A1` /\ B1` in F by A3,FINSUB_1:def 2;
then (A1 \/ B1)` in F by SUBSET_1:29;
then (A1 \/ B1)`` in F by Def1;
hence thesis;
end;
theorem Th10:
{} in F
proof
consider A being Subset of X such that
A1: A in F by Th6;
A2: A` in F by A1,Def1;
A misses A` by SUBSET_1:26;
then A /\ A` = {} by XBOOLE_0:def 7;
hence thesis by A1,A2,FINSUB_1:def 2;
end;
theorem Th11:
X in F
proof
consider A being Subset of X such that
A1: A in F by Th6;
A2: A` in F by A1,Def1;
A \/ A` = [#] X by SUBSET_1:25
.= X by SUBSET_1:def 4;
hence thesis by A1,A2,Th9;
end;
theorem Th12:
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:32;
end;
theorem
for A, B being set holds
(A \ B) misses B &
(A in F & B in F implies (A \ B) \/ B in F)
proof
let A, B be set;
thus A \ B misses B
proof
x in A \ B implies not x in B by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:3;
end;
assume
A1: A in F & B in F;
A \/ B = (A \ B) \/ B by XBOOLE_1:39;
hence thesis by A1,Th9;
end;
theorem
{ {}, X } is Field_Subset of X
proof
A1: {} c= X by XBOOLE_1:2;
X in bool X by ZFMISC_1:def 1;
then reconsider EX = { {}, X } as Subset-Family of X by A1,Th4;
A2: now let A,B be set; assume
A3: A in EX & B in EX;
A4: (A = {} or B = {}) implies A /\ B = {};
(A = X & B = X) implies A /\ B = X;
hence A /\ B in EX by A3,A4,TARSKI:def 2;
end;
now let A be Subset of X; assume
A5: A in EX;
A = {} implies A = {} X;
then A = {} implies A` = [#] X by SUBSET_1:22;
then A6: A = {} implies A` = X by SUBSET_1:def 4;
A = X implies A = [#] X by SUBSET_1:def 4;
then A = X implies A` = {} X by SUBSET_1:21;
hence A` in EX by A5,A6,TARSKI:def 2;
end;
hence thesis by A2,Def1,FINSUB_1:def 2;
end;
theorem
bool X is Field_Subset of X
proof
reconsider K = bool X as Subset-Family of X by SETFAM_1:def 7;
A1: K is compl-closed
proof
let A be Subset of X; assume A in K;
thus thesis;
end;
K is cap-closed
proof
let A,B be set; assume A in K & B in K;
then A /\ B c= X by XBOOLE_1:108;
hence thesis;
end;
hence thesis by A1;
end;
theorem
{ {} , X } c= F & F c= bool X
proof
A1: {} in F by Th10;
X in F by Th11;
then x in { {} , X } implies x in F by A1,TARSKI:def 2;
hence thesis by TARSKI:def 3;
end;
canceled;
theorem
(for p st p in [:NAT,{X}:] ex x,y st [x,y]=p) &
(for x,y,z st [x,y] in [:NAT,{X}:] & [x,z] in [:NAT,{X}:] holds y=z)
proof
for x,y,z st [x,y] in [:NAT,{X}:] & [x,z] in [:NAT,{X}:] holds y=z
proof
let x,y,z;
assume [x,y] in [:NAT,{X}:] & [x,z] in [:NAT,{X}:];
then y in {X} & z in {X} by ZFMISC_1:106;
then y = X & z = X by TARSKI:def 1;
hence thesis;
end;
hence thesis by ZFMISC_1:102;
end;
theorem
Th19: ex f st dom f = NAT & for n holds f.n = X
proof
take f = NAT --> X;
thus dom f = NAT by FUNCOP_1:19;
let n;
thus f.n = X by FUNCOP_1:13;
end;
definition let X be set;
mode SetSequence of X is Function of NAT, bool X;
end;
reserve ASeq,BSeq for SetSequence of Omega;
reserve A1 for SetSequence of X;
Lm1:
dom A1 = NAT & for n holds A1.n in bool X by FUNCT_2:def 1;
canceled;
theorem Th21:
ex A1 st for n holds A1.n = X
proof
consider f such that
A1: dom f = NAT & for n holds f.n = X by Th19;
for x being set st x in NAT holds f.x in bool X
proof
X in bool X by ZFMISC_1:def 1;
hence thesis by A1;
end;
then f is SetSequence of X by A1,FUNCT_2:5;
hence thesis by A1;
end;
theorem Th22:
for A, B being Subset of X
ex A1 st (A1.0 = A & for n st n <> 0 holds A1.n = B)
proof
let A,B be Subset of X;
defpred P[set] means $1 = 0;
deffunc F(set) = A;
deffunc G(set) = B;
ex f being Function st dom f = NAT &
for x st x in NAT holds
(P[x] implies f.x=F(x)) & (not P[x] implies f.x=G(x)) from LambdaC;
then consider f being Function such that
A1: dom f = NAT & for x st x in NAT holds
(x = 0 implies f.x = A) & (not x = 0 implies f.x = B);
A2: A in bool X & B in bool X;
for x st x in NAT holds f.x in bool X
proof
let x; assume A3: x in NAT;
per cases;
suppose x = 0;
hence thesis by A1,A2;
suppose x <> 0;
hence thesis by A1,A2,A3;
end;
then reconsider f as SetSequence of X by A1,FUNCT_2:5;
take f;
thus thesis by A1;
end;
definition let X,A1,n;
redefine func A1.n -> Subset of X;
coherence by Lm1;
end;
theorem Th23:
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 such that
A1: y in dom A1 & Y = A1.y by FUNCT_1:def 5;
reconsider y as Nat by A1,FUNCT_2:def 1;
Y = A1.y by A1;
hence thesis;
end;
hence thesis by ZFMISC_1:94;
end;
definition let f be Function;
canceled;
func Union f -> set equals :Def3:
union rng f;
correctness;
end;
definition let X be set, A1 be SetSequence of X;
redefine func Union A1 -> Subset of X;
coherence
proof
Union A1 is Subset of X
proof
Union A1 = union rng A1 by Def3;
hence thesis by Th23;
end; hence thesis;
end;
end;
canceled;
theorem Th25:
x in Union A1 iff ex n st x in A1.n
proof
set DX = union rng A1;
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
A2: x in Y & Y in rng A1 by TARSKI:def 4;
consider p such that
A3: p in dom A1 & Y = A1.p by A2,FUNCT_1:def 5;
p in NAT by A3,FUNCT_2:def 1;
hence thesis by A2,A3;
end;
thus (ex n st x in A1.n) implies x in DX
proof
given n such that
A4: x in A1.n;
n in NAT;
then n in dom A1 by FUNCT_2:def 1;
then A1.n in rng A1 by FUNCT_1:def 5;
hence thesis by A4,TARSKI:def 4;
end;
end; DX = Union A1 by Def3;
hence thesis by A1;
end;
theorem Th26:
ex B1 being SetSequence of X st for n holds B1.n = (A1.n)`
proof
deffunc F(Nat) = (A1.$1)`;
ex f being Function of NAT,bool X st
for x being Element of NAT holds f.x = F(x) from LambdaD;
then consider f being Function of NAT,bool X such that
A1: for x being Element of NAT holds f.x = (A1.x)`;
take f;
thus thesis by A1;
end;
definition let X be set, A1 be SetSequence of X;
func Complement A1 -> SetSequence of X means
:Def4: for n holds it.n = (A1.n)`;
existence by Th26;
uniqueness
proof let BSeq,CSeq be SetSequence of X such that
A1: for n holds BSeq.n = (A1.n)` and
A2: for m holds CSeq.m = (A1.m)`;
A3: for x st x in NAT holds BSeq.x = CSeq.x
proof let x; assume x in NAT;
then reconsider x as Nat;
BSeq.x = (A1.x)` by A1
.= CSeq.x by A2; hence thesis;
end;
NAT = dom BSeq & NAT = dom CSeq by FUNCT_2:def 1;
hence thesis by A3,FUNCT_1:9;
end;
end;
definition let X be set, A1 be SetSequence of X;
func Intersection A1 -> Subset of X equals
:Def5: (Union Complement A1)`;
correctness;
end;
canceled 2;
theorem
Th29: x in Intersection A1 iff for n holds x in A1.n
proof
A1: for n holds X \ (Complement A1).n = A1.n
proof let n;
X \ (Complement A1).n = ((Complement A1).n)` by SUBSET_1:def 5
.= ((A1.n)`)` by Def4
.= A1.n;
hence thesis;
end;
A2: x in (Union Complement A1)` iff x in X \ Union Complement A1
by SUBSET_1:def 5;
A3: x in X & not x in Union Complement A1 iff
x in X & for n holds not x in (Complement A1).n by Th25;
(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
A4: (for n holds (x in X & not x in (Complement A1).n)); let n;
x in X & not x in (Complement A1).n by A4;
then x in X \ (Complement A1).n by XBOOLE_0:def 4;
hence thesis by A1;
end;
assume A5: for n holds x in A1.n; let n;
x in A1.n by A5;
then x in X \ (Complement A1).n by A1;
hence thesis by XBOOLE_0:def 4;
end;
hence thesis by A2,A3,Def5,XBOOLE_0:def 4;
end;
theorem Th30:
for A, B being Subset of X holds
(A1.0 = A & for n st n <> 0 holds A1.n = B) implies
Intersection A1 = A /\ B
proof
let A, B be Subset of X; assume
A1: A1.0 = A & for n st n <> 0 holds A1.n = B;
for x holds x in Intersection A1 iff (x in A & x in B)
proof let x; thus
x in Intersection A1 implies (x in A & x in B)
proof
assume A2: x in Intersection A1;
then x in A1.1 by Th29;
hence thesis by A1,A2,Th29;
end;
assume x in A & x in B;
then for n holds x in A1.n by A1; hence thesis by Th29;
end; hence thesis by XBOOLE_0:def 3;
end;
theorem
Th31: Complement Complement A1 = A1
proof
for n holds ((Complement A1).n)` = A1.n
proof let n;
A1.n = (A1.n)``;
hence thesis by Def4;
end;
hence thesis by Def4;
end;
definition let X,A1;
attr A1 is non-increasing means
:Def6: for n,m st n <= m holds A1.m c= A1.n;
attr A1 is non-decreasing means
for n,m st n <= m holds A1.n c= A1.m;
end;
definition let X be set;
mode SigmaField of X -> non empty Subset-Family of X means :Def8:
(for A1 being SetSequence of X st
(for n holds A1.n in it) holds Intersection A1 in it) &
(for A being Subset of X st A in it holds A` in it);
existence
proof
reconsider IT = bool X as non empty Subset-Family of X by SETFAM_1:def 7;
take IT;
thus thesis;
end;
end;
theorem Th32:
for S being non empty set holds
S is SigmaField of X iff
(S c= bool X) &
(for A1 being SetSequence of X st
(for n holds A1.n in S) holds Intersection A1 in S) &
(for A being Subset of X st A in S holds A` in S)
proof
let S be non empty set;
thus S is SigmaField of X implies
S c= bool X &
(for A1 being SetSequence of X st
(for n holds A1.n in S) holds Intersection A1 in S) &
(for A being Subset of X st A in S holds A` in S) by Def8;
assume A1: S c= bool X &
(for A1 being SetSequence of X st
(for n holds A1.n in S) holds Intersection A1 in S) &
(for A being Subset of X st A in S holds A` in S);
then S is Subset-Family of X by SETFAM_1:def 7;
hence thesis by A1,Def8;
end;
canceled 2;
theorem Th35:
Y is SigmaField of X implies Y is Field_Subset of X
proof assume
A1: Y is SigmaField of X;
for A,B being Subset of X st A in Y & B in Y holds A /\ B in Y
proof let A,B be Subset of X such that
A2: A in Y & B in Y;
consider A1 such that
A3: (A1.0 = A & for n st n <> 0 holds A1.n = B) by Th22;
A4: Intersection A1 = A /\ B by A3,Th30;
for n holds A1.n in Y by A2,A3;
hence thesis by A1,A4,Def8;
end;
then A5: (for A,B being Subset of X holds
(Y c= bool X &
((A in Y & B in Y) implies A /\ B in Y) &
(A in Y implies A` in Y))) by A1,Def8;
reconsider Y' = Y as non empty Subset-Family of X by A1;
A6: Y' is compl-closed by A5,Def1;
Y is cap-closed
proof let A,B be set; assume
A7: A in Y & B in Y;
then reconsider A' = A, B' = B as Subset of X by A1;
consider A1 such that
A8: (A1.0 = A' & for n st n <> 0 holds A1.n = B') by Th22;
A9: Intersection A1 = A /\ B by A8,Th30;
for n holds A1.n in Y by A7,A8;
hence thesis by A1,A9,Def8;
end;
hence thesis by A6;
end;
definition let X be set;
cluster -> cap-closed compl-closed SigmaField of X;
coherence by Th35;
end;
reserve Sigma for SigmaField of Omega;
reserve Si for SigmaField of X;
canceled 2;
theorem
ex A being Subset of X st A in Si
proof consider A being Element of Si;
A in Si & Si c= bool X;
hence thesis;
end;
canceled 2;
theorem
for A,B being Subset of X st A in Si & B in Si holds A \/ B in Si by Th9;
theorem
{} in Si by Th10;
theorem
X in Si by Th11;
theorem
for A,B being Subset of X st A in Si & B in Si holds A \ B in Si by Th12;
:: 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.
definition let X be set, Si be SigmaField of X;
mode SetSequence of Si -> SetSequence of X means
:Def9: for n holds it.n in Si;
existence
proof
consider A1 being SetSequence of X such that
A1: for n holds A1.n = X by Th21;
take A1;
for n holds A1.n in Si
proof let n; A1.n = X by A1; hence thesis by Th11; end;
hence thesis;
end;
end;
canceled;
theorem Th46:
for ASeq being SetSequence of Si holds Union ASeq in Si
proof
A1: (for n holds A1.n in Si) implies
Union Complement A1 in Si
proof
assume for n holds A1.n in Si;
then Intersection A1 in Si by Def8;
then (Union Complement A1)` in Si by Def5;
then (Union Complement A1)`` in Si by Def8;
hence thesis;
end;
A2: (for n holds A1.n in Si) implies
(for n holds (Complement A1).n in Si)
proof assume
A3: for n holds A1.n in Si;
for n holds (Complement A1).n in Si
proof let n;
A1.n in Si by A3;
then (A1.n)` in Si by Def8;
hence thesis by Def4;
end; hence thesis;
end;
A4: (for n holds A1.n in Si) implies
Union Complement Complement A1 in Si
proof
assume for n holds A1.n in Si;
then for n holds (Complement A1).n in Si by A2;
hence thesis by A1;
end;
A5: for A1 st (for n holds A1.n in Si) holds Union A1 in Si
proof let A1;
assume for n holds A1.n in Si;
then Union Complement Complement A1 in Si by A4;
hence thesis by Th31;
end;
for ASeq being SetSequence of Si holds Union ASeq in Si
proof let ASeq be SetSequence of Si;
for n holds ASeq.n in Si by Def9;
hence thesis by A5;
end; hence thesis;
end;
definition let X be set,
F be SigmaField of X;
mode Event of F -> Subset of X means
:Def10: it in F;
existence
proof
X c= X;
then reconsider O = X as Subset of X;
take O;
thus thesis by Th11;
end;
end;
canceled;
theorem
x in Si implies x is Event of Si by Def10;
theorem
Th49: for A,B being Event of Si holds A /\ B is Event of Si
proof let A,B be Event of Si;
A in Si & B in Si by Def10;
then A /\ B in Si by FINSUB_1:def 2;
hence thesis by Def10;
end;
theorem
for A being Event of Si holds A` is Event of Si
proof let A be Event of Si;
A in Si by Def10;
then A` in Si by Def8;
hence thesis by Def10;
end;
theorem
Th51: for A,B being Event of Si holds A \/ B is Event of Si
proof let A,B be Event of Si;
A in Si & B in Si by Def10;
then A \/ B in Si by Th9;
hence thesis by Def10;
end;
theorem
Th52: {} is Event of Si
proof
{} in Si by Th10;
hence thesis by Def10;
end;
theorem
Th53: X is Event of Si
proof
X in Si by Th11;
hence thesis by Def10;
end;
theorem
Th54: for A,B being Event of Si holds A \ B is Event of Si
proof let A,B be Event of Si;
A in Si & B in Si by Def10;
then A \ B in Si by Th12;
hence thesis by Def10;
end;
definition let X,Si;
cluster empty Event of Si;
existence
proof {} is Event of Si by Th52;
hence thesis;
end;
end;
definition let X,Si;
func [#] Si -> Event of Si equals
:Def11: X;
coherence by Th53;
end;
definition let X,Si; let A,B be Event of Si;
redefine func A /\ B -> Event of Si;
coherence by Th49;
func A \/ B -> Event of Si;
coherence by Th51;
func A \ B -> Event of Si;
coherence by Th54;
end;
canceled 2;
theorem
ASeq is SetSequence of Sigma iff for n holds ASeq.n is Event of Sigma
proof
A1: ASeq is SetSequence of Sigma implies
for n holds ASeq.n is Event of Sigma
proof assume A2: ASeq is SetSequence of Sigma;
for n holds ASeq.n is Event of Sigma
proof let n;
ASeq.n in Sigma by A2,Def9;
hence thesis by Def10;
end; hence thesis;
end;
(for n holds ASeq.n is Event of Sigma) implies
for n holds ASeq.n in Sigma
proof assume
A3: for n holds ASeq.n is Event of Sigma;
for n holds ASeq.n in Sigma
proof let n;
ASeq.n is Event of Sigma by A3;
hence thesis by Def10;
end; hence thesis;
end;
hence thesis by A1,Def9;
end;
theorem
ASeq is SetSequence of Sigma implies Union ASeq is Event of Sigma
proof assume ASeq is SetSequence of Sigma;
then Union ASeq in Sigma by Th46;
hence thesis by Def10;
end;
:: DEFINITION OF sigma-ADDITIVE PROBABILITY
reserve A, B for Event of Sigma,
ASeq for SetSequence of Sigma;
theorem
Th59: 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
defpred C[set] means p in $1;
deffunc F(set) = 1;
deffunc G(set) = 0;
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 LambdaC;
then consider f being Function such that
A1: dom f = Sigma &
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 A2: D in Sigma;
hence p in D implies f.D = 1 by A1;
assume not p in D;
hence thesis by A1,A2;
end;
reserve P for Function of Sigma,REAL;
theorem Th60:
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 & for D st D in Sigma holds
(p in D implies f.D = 1) & (not p in D implies f.D = 0) by Th59;
rng f c= REAL
proof
let y;
assume y in rng f;
then consider x such that
A2: x in dom f & y = f.x by FUNCT_1:def 5;
reconsider x as Subset of Omega by A1,A2;
A3: p in x implies y = 1 by A1,A2;
not p in x implies y = 0 by A1,A2;
hence thesis by A3;
end;
then reconsider f as Function of Sigma,REAL by A1,FUNCT_2:def 1,RELSET_1:11;
take f;
thus thesis by A1;
end;
canceled;
theorem
Th62: P * ASeq is Real_Sequence
proof
for x holds (x in dom (P * ASeq) iff x in NAT)
proof let x;
x in dom (P * ASeq) iff x in dom ASeq & ASeq.x in
dom P by FUNCT_1:21;
then x in dom (P * ASeq) iff x in NAT & ASeq.x in Sigma by FUNCT_2:def 1;
hence thesis by Def9;
end;
then A1: dom (P * ASeq) = NAT by TARSKI:2;
rng (P * ASeq) c= REAL
proof
rng (P * ASeq) c= rng P & rng P c= REAL by RELAT_1:45,RELSET_1:12;
hence thesis by XBOOLE_1:1;
end; hence thesis by A1,FUNCT_2:def 1,RELSET_1:11;
end;
definition let Omega,Sigma,ASeq,P;
redefine func P * ASeq -> Real_Sequence;
coherence by Th62;
end;
definition let Omega,Sigma,P,A;
redefine func P.A -> Real;
coherence
proof
A in Sigma by Def10;
then A in dom P by FUNCT_2:def 1;
then P.A in rng P by FUNCT_1:def 5;
hence thesis;
end;
end;
definition let Omega,Sigma;
canceled;
mode Probability of Sigma -> Function of Sigma,REAL means :Def13:
(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-increasing holds
(it * ASeq is convergent & lim (it * ASeq) = it.Intersection ASeq));
existence
proof
consider p being 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 Th60;
take P;
A2: for A holds
(p in A implies P.A = 1) & (not p in A implies P.A = 0)
proof let A; A in Sigma by Def10;
hence thesis by A1;
end;
A3: for A holds 0 <= P.A
proof let A;
p in A implies P.A = 1 by A2;
hence thesis by A2;
end;
A4: P.Omega = 1
proof
Omega c= Omega;
then reconsider O = Omega as Subset of Omega;
O in Sigma by Th11;
hence thesis by A1;
end;
A5: for A,B st A misses B holds P.(A \/ B) = P.A + P.B
proof let A,B such that
A6: A misses B;
A7: (p in A & not p in B) implies (P.A = 1 & P.B = 0) by A2;
A8: (p in A & not p in B) implies p in A \/ B by XBOOLE_0:def 2;
A9: (not p in A & p in B) implies (P.A = 0 & P.B = 1) by A2;
A10: (not p in A & p in B) implies p in A \/ B by XBOOLE_0:def 2;
A11: (not p in A & not p in B) implies P.A = 0 & P.B = 0 by A2;
(not p in A & not p in B) implies not p in (A \/ B) by XBOOLE_0:def 2
;
hence thesis by A2,A6,A7,A8,A9,A10,A11,XBOOLE_0:3;
end;
for ASeq st ASeq is non-increasing holds
P * ASeq is convergent & lim (P * ASeq) = P.Intersection ASeq
proof let ASeq;
assume A12: ASeq is non-increasing;
A13: for n holds (P * ASeq).n = P.(ASeq.n)
proof let n;
dom (P * ASeq) = NAT by FUNCT_2:def 1;
hence thesis by FUNCT_1:22;
end;
A14: (for n holds p in ASeq.n) implies for n holds (P * ASeq).n = 1
proof assume
A15: for n holds p in ASeq.n;
for n holds (P * ASeq).n = 1
proof let n;
A16: ASeq.n in Sigma by Def9;
p in ASeq.n by A15;
then P.(ASeq.n) = 1 by A1,A16;
hence thesis by A13;
end; hence thesis;
end;
A17: 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
A18: 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,Def6;
then A19: not p in ASeq.n by A18;
ASeq.n in Sigma by Def9;
then P.(ASeq.n) = 0 by A1,A19;
hence thesis by A13;
end; hence thesis;
end;
A20: (for n holds (P * ASeq).n = 1) implies
P * ASeq is convergent & lim (P * ASeq) = 1
proof reconsider r = 1 as Real; assume
A21: 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 A21; end;
hence thesis by Th3;
end;
A22: (ex m st (for n st m <= n holds (P * ASeq).n = 0)) implies
P * ASeq is convergent & lim (P * ASeq) = 0 by Th3;
A23: (for n holds p in ASeq.n) implies
P * ASeq is convergent & lim (P * ASeq) = P.Intersection ASeq
proof assume
A24: for n holds p in ASeq.n;
then A25: p in Intersection ASeq by Th29;
for n holds ASeq.n in Sigma by Def9;
then Intersection ASeq in Sigma by Def8;
hence thesis by A1,A14,A20,A24,A25;
end;
not (for n holds p in ASeq.n) implies
P * ASeq is convergent & lim (P * ASeq) = P.Intersection ASeq
proof assume
A26: not (for n holds p in ASeq.n);
then A27: not p in Intersection ASeq by Th29;
for n holds ASeq.n in Sigma by Def9;
then Intersection ASeq in Sigma by Def8;
hence thesis by A1,A17,A22,A26,A27;
end;
hence thesis by A23;
end;
hence thesis by A3,A4,A5;
end;
end;
reserve P for Probability of Sigma;
canceled;
theorem
P.{} = 0
proof
A1: {} misses ([#] Sigma) by XBOOLE_1:65;
A2: {} \/ ([#] Sigma) = [#] Sigma;
reconsider E = {} as Event of Sigma by Th52;
1 = P.Omega by Def13
.= P.([#] Sigma) by Def11;
then 1 = P.E + 1 by A1,A2,Def13;
then P.({} Sigma) = 1 - 1 by XCMPLX_1:26
.= 0;
hence thesis;
end;
canceled;
theorem
P.([#] Sigma) = 1
proof
P.Omega = 1 by Def13;
hence thesis by Def11;
end;
theorem
Th67: P.(([#] Sigma) \ A) + P.A = 1
proof
A1: (([#] Sigma) \ A) misses A by XBOOLE_1:79;
(([#] Sigma) \ A) \/ A = (Omega \ A) \/ A by Def11
.= A` \/ A by SUBSET_1:def 5
.= [#] Omega by SUBSET_1:25
.= Omega by SUBSET_1:def 4;
then P.(([#] Sigma) \ A) + P.A = P.Omega by A1,Def13
.= 1 by Def13;
hence thesis;
end;
theorem
P.(([#] Sigma) \ A) = 1 - P.A
proof
P.(([#] Sigma) \ A) + P.A = 1 by Th67;
hence thesis by XCMPLX_1:26;
end;
theorem
Th69: 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 Def13
.= P.B by A1,XBOOLE_1:45;
hence thesis by XCMPLX_1:26;
end;
theorem
Th70: A c= B implies P.A <= P.B
proof assume A c= B;
then P.(B \ A) = P.B - P.A by Th69;
then 0 <= P.B - P.A by Def13;
then 0 + P.A <= P.B by REAL_1:84;
hence thesis;
end;
theorem
P.A <= 1
proof
A1: P.([#] Sigma) = P.Omega by Def11
.= 1 by Def13;
A c= Omega;
then A c= ([#] Sigma) by Def11;
hence thesis by A1,Th70;
end;
theorem
Th72: 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,Def13;
hence thesis;
end;
theorem
Th73: P.(A \/ B) = P.A + P.(B \ (A /\ B))
proof
P.(A \/ B) = P.A + P.(B \ A) by Th72
.= P.A + P.(B \ (A /\ B)) by XBOOLE_1:47; hence thesis;
end;
theorem
Th74: P.(A \/ B) = P.A + P.B - P.(A /\ B)
proof
A1: A /\ B c= B by XBOOLE_1:17;
P.(A \/ B) = P.A + P.(B \ (A /\ B)) by Th73
.= P.A + (P.B - P.(A /\ B)) by A1,Th69;
hence thesis by XCMPLX_1:29;
end;
theorem
P.(A \/ B) <= P.A + P.B
proof
A1: 0 <= P.(A /\ B) by Def13;
P.(A \/ B) = P.A + P.B - P.(A /\ B) by Th74;
hence thesis by A1,Th2;
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 of bool Omega;
theorem
Th76: bool Omega is SigmaField of Omega
proof set Y = bool Omega;
(Y c= bool Omega) &
(for BSeq st (for n holds BSeq.n in Y) holds Intersection BSeq in Y) &
(for E st E in Y holds E` in Y);
hence thesis by Th32;
end;
Lm2: for X being Subset of bool Omega ex Y being SigmaField of Omega
st X c= Y & for Z st (X c= Z & Z is SigmaField of Omega) holds Y c= Z
proof let X be Subset of bool Omega;
set V = { S : X c= S & S is SigmaField of Omega};
set Y = meet V;
A1: bool Omega in V
proof
bool Omega c= bool Omega;
then reconsider X1 = bool Omega as Subset of bool Omega;
X1 is SigmaField of Omega by Th76;
hence thesis;
end;
then A2: Y c= bool Omega by SETFAM_1:4;
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 Th10;
end;
then A3: {} in Y by A1,SETFAM_1:def 1;
A4: for BSeq st (for n holds BSeq.n in Y) holds Intersection BSeq in Y
proof let BSeq such that A5: for n holds BSeq.n in Y;
now let Z; assume A6: Z in V;
then A7: ex S st Z = S & X c= S & S is SigmaField of Omega;
now let n; BSeq.n in Y by A5;
hence BSeq.n in Z by A6,SETFAM_1:def 1;
end;
hence Intersection BSeq in Z by A7,Def8;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
for E st E in Y holds E` in Y
proof let E such that A8: E in Y;
now let Z; assume A9: Z in V;
then A10: E in Z by A8,SETFAM_1:def 1;
ex S st Z = S & X c= S & S is SigmaField of Omega by A9;
hence E` in Z by A10,Def8;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
then reconsider Y as SigmaField of Omega by A2,A3,A4,Th32;
take Y;
A11: 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;
for Z st (X c= Z & Z is SigmaField of Omega) holds Y c= Z
proof let Z; assume A12: X c= Z & Z is SigmaField of Omega;
then reconsider Z as Subset of bool Omega;
Z in V by A12;
hence thesis by SETFAM_1:4;
end;
hence thesis by A1,A11,SETFAM_1:6;
end;
definition let Omega; let X be Subset of bool 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 by Lm2;
uniqueness
proof let R1,R2 be SigmaField of Omega such that
A1: X c= R1 & for Z st X c= Z & Z is SigmaField of Omega holds R1 c= Z and
A2: X c= R2 & for Z st X c= Z & Z is SigmaField of Omega holds R2 c= Z;
A3: R1 c= R2 by A1,A2;
R2 c= R1 by A1,A2;
hence thesis by A3,XBOOLE_0:def 10;
end;
end;
definition let r;
func halfline(r) -> Subset of REAL equals
{r1 where r1 is Element of REAL: r1 < r};
coherence
proof {r1 where r1 is Element of REAL: r1 < r} is Subset of REAL
proof now let p;
assume p in {r1 where r1 is Element of REAL: r1 < r};
then ex r1 being Element of REAL st p = r1 & r1 < r;
hence p in REAL;
end;
hence thesis by TARSKI:def 3;
end; hence thesis;
end;
end;
definition
func Family_of_halflines -> Subset of bool REAL equals
{D: ex r st D = halfline(r)};
coherence
proof {D: ex r st D = halfline(r)} is Subset of bool REAL
proof now let p; assume p in {D: ex r st D = halfline(r)};
then ex D st p = D & ex r st D = halfline(r);
hence p in bool REAL;
end;
hence thesis by TARSKI:def 3;
end; hence thesis;
end;
end;
definition
func Borel_Sets -> SigmaField of REAL equals
sigma(Family_of_halflines);
correctness;
end;