The abstract of the Mizar article:

$\sigma$-Fields and Probability

by

Andrzej Nedzusiak

Received October 16, 1989

MML identifier: PROB_1

[ Mizar article, MML identifier index ]

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;


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 :: PROB_1:2
 for r,r2 st 0 <= r holds r2 - r <= r2;

theorem :: PROB_1:3
 for r,seq st (ex n st for m st n <= m holds seq.m = r) holds
     seq is convergent & lim seq = r;

:::::::::::::::::::::::::::::::::::::::::::::::::::::
:: 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
:: PROB_1:def 1
    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;
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 :: PROB_1:4
   for A,B being Subset of X holds
   {A,B} is Subset-Family of X;

canceled;

theorem :: PROB_1:6
  ex A being Subset of X st A in F;

canceled 2;

theorem :: PROB_1:9
for A, B being set st A in F & B in F holds A \/ B in F;

theorem :: PROB_1:10
{} in F;

theorem :: PROB_1:11
  X in F;

theorem :: PROB_1:12
  for A,B being Subset of X holds
  A in F & B in F implies A \ B in F;

theorem :: PROB_1:13
    for A, B being set holds
   (A \ B) misses B &
   (A in F & B in F implies (A \ B) \/ B in F);

theorem :: PROB_1:14
    { {}, X } is Field_Subset of X;

theorem :: PROB_1:15
   bool X is Field_Subset of X;

theorem :: PROB_1:16
    { {} , X } c= F & F c= bool X;

canceled;

theorem :: PROB_1:18
  (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);

theorem :: PROB_1:19
 ex f st dom f = NAT & for n holds f.n = X;

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;

canceled;

theorem :: PROB_1:21
  ex A1 st for n holds A1.n = X;

theorem :: PROB_1:22
  for A, B being Subset of X
   ex A1 st (A1.0 = A & for n st n <> 0 holds A1.n = B);

definition let X,A1,n;
  redefine func A1.n -> Subset of X;
end;

theorem :: PROB_1:23
  union rng A1 is Subset of X;

definition let f be Function;
 canceled;

  func Union f -> set equals
:: PROB_1:def 3
    union rng f;
end;

definition let X be set, A1 be SetSequence of X;
  redefine func Union A1 -> Subset of X;
end;

canceled;

theorem :: PROB_1:25
  x in Union A1 iff ex n st x in A1.n;

theorem :: PROB_1:26
  ex B1 being SetSequence of X st for n holds B1.n = (A1.n)`;

definition let X be set, A1 be SetSequence of X;
  func Complement A1 -> SetSequence of X means
:: PROB_1:def 4
     for n holds it.n = (A1.n)`;
end;

definition let X be set, A1 be SetSequence of X;
  func Intersection A1 -> Subset of X equals
:: PROB_1:def 5
 (Union Complement A1)`;
end;

canceled 2;

theorem :: PROB_1:29
 x in Intersection A1 iff for n holds x in A1.n;

theorem :: PROB_1:30
  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;

theorem :: PROB_1:31
 Complement Complement A1 = A1;

definition let X,A1;
  attr A1 is non-increasing means
:: PROB_1:def 6
    for n,m st n <= m holds A1.m c= A1.n;
  attr A1 is non-decreasing means
:: PROB_1:def 7
      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
:: PROB_1:def 8
  (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);
end;

theorem :: PROB_1:32
  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);

canceled 2;

theorem :: PROB_1:35
  Y is SigmaField of X implies Y is Field_Subset of X;

definition let X be set;
  cluster -> cap-closed compl-closed SigmaField of X;
end;

reserve Sigma for SigmaField of Omega;
reserve Si for SigmaField of X;

canceled 2;

theorem :: PROB_1:38
   ex A being Subset of X st A in Si;

canceled 2;

theorem :: PROB_1:41
   for A,B being Subset of X st A in Si & B in Si holds A \/ B in Si;

theorem :: PROB_1:42
   {} in Si;

theorem :: PROB_1:43
   X in Si;

theorem :: PROB_1:44
  for A,B being Subset of X st A in Si & B in Si holds A \ B in Si;

:: 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
:: PROB_1:def 9
  for n holds it.n in Si;
end;

canceled;

theorem :: PROB_1:46
 for ASeq being SetSequence of Si holds Union ASeq in Si;

definition let X be set,
               F be SigmaField of X;
  mode Event of F -> Subset of X means
:: PROB_1:def 10
   it in F;
end;

canceled;

theorem :: PROB_1:48
   x in Si implies x is Event of Si;

theorem :: PROB_1:49
 for A,B being Event of Si holds A /\ B is Event of Si;

theorem :: PROB_1:50
   for A being Event of Si holds A` is Event of Si;

theorem :: PROB_1:51
 for A,B being Event of Si holds A \/ B is Event of Si;

theorem :: PROB_1:52
 {} is Event of Si;

theorem :: PROB_1:53
 X is Event of Si;

theorem :: PROB_1:54
 for A,B being Event of Si holds A \ B is Event of Si;

definition let X,Si;
  cluster empty Event of Si;
end;

definition let X,Si;
  func [#] Si -> Event of Si equals
:: PROB_1:def 11
        X;
end;

definition let X,Si; let A,B be Event of Si;
  redefine func A /\ B -> Event of Si;
  func A \/ B -> Event of Si;
  func A \ B -> Event of Si;
end;

canceled 2;

theorem :: PROB_1:57
   ASeq is SetSequence of Sigma iff for n holds ASeq.n is Event of Sigma;

theorem :: PROB_1:58
    ASeq is SetSequence of Sigma implies Union ASeq is Event of Sigma;

:: DEFINITION OF sigma-ADDITIVE PROBABILITY

 reserve A, B for Event of Sigma,
         ASeq for SetSequence of Sigma;

theorem :: PROB_1:59
 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));

reserve P for Function of Sigma,REAL;

theorem :: PROB_1:60
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));

canceled;

theorem :: PROB_1:62
 P * ASeq is Real_Sequence;

definition let Omega,Sigma,ASeq,P;
  redefine func P * ASeq -> Real_Sequence;
end;

definition let Omega,Sigma,P,A;
  redefine func P.A -> Real;
end;

definition let Omega,Sigma;
 canceled;

  mode Probability of Sigma -> Function of Sigma,REAL means
:: PROB_1:def 13
  (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));
end;

reserve P for Probability of Sigma;

canceled;

theorem :: PROB_1:64
   P.{} = 0;

canceled;

theorem :: PROB_1:66
   P.([#] Sigma) = 1;

theorem :: PROB_1:67
 P.(([#] Sigma) \ A) + P.A = 1;

theorem :: PROB_1:68
   P.(([#] Sigma) \ A) = 1 - P.A;

theorem :: PROB_1:69
 A c= B implies P.(B \ A) = P.B - P.A;

theorem :: PROB_1:70
 A c= B implies P.A <= P.B;

theorem :: PROB_1:71
   P.A <= 1;

theorem :: PROB_1:72
 P.(A \/ B) = P.A + P.(B \ A);

theorem :: PROB_1:73
 P.(A \/ B) = P.A + P.(B \ (A /\ B));

theorem :: PROB_1:74
 P.(A \/ B) = P.A + P.B - P.(A /\ B);

theorem :: PROB_1:75
   P.(A \/ B) <= P.A + P.B;

::  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 :: PROB_1:76
 bool Omega is SigmaField of Omega;

definition let Omega; let X be Subset of bool Omega;
  func sigma(X) -> SigmaField of Omega means
:: PROB_1:def 14
    X c= it &
  for Z st (X c= Z & Z is SigmaField of Omega) holds it c= Z;
end;

definition let r;
 func halfline(r) -> Subset of REAL equals
:: PROB_1:def 15
     {r1 where r1 is Element of REAL: r1 < r};
end;

definition
  func Family_of_halflines -> Subset of bool REAL equals
:: PROB_1:def 16
    {D: ex r st D = halfline(r)};
end;

definition
 func Borel_Sets -> SigmaField of REAL equals
:: PROB_1:def 17
     sigma(Family_of_halflines);
end;