:: $\sigma$-Fields and Probability
::  by Andrzej N\c{e}dzusiak
::
:: Received October 16, 1989
:: Copyright (c) 1990-2021 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;


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 :: PROB_1:1
  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;

registration
  let X be set;
  cluster bool X -> cap-closed;
end;

registration
  let X be set;
  cluster bool X -> compl-closed for Subset-Family of X;
end;

registration
  let X be set;
  cluster non empty compl-closed cap-closed for 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:2
  for A,B being Subset of X holds {A,B} is Subset-Family of X;

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

theorem :: PROB_1:4
  {} in F;

theorem :: PROB_1:5
  X in F;

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

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

registration
  let X be set;
  cluster { {}, X } -> cap-closed;
end;

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

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

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

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 :: PROB_1:11
  union rng A1 is Subset of X;

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

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

definition
  let X be set, A1 be SetSequence of X;

  func Complement A1 -> SetSequence of X means
:: PROB_1:def 2

  for n holds it.n = (A1.n )`;
  involutiveness;
end;

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

theorem :: PROB_1:13
  for x being object holds x in Intersection A1 iff for n holds x in A1.n;

theorem :: PROB_1:14
  for A, B being Subset of X holds Intersection(A followed_by B) = A /\ B;

definition
  let f be Function;
  attr f is non-ascending means
:: PROB_1:def 4

  for n,m st n <= m holds f.m c= f.n;
  attr f is non-descending means
:: PROB_1:def 5
  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
:: PROB_1:def 6

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

registration
  let X be set;
  cluster compl-closed sigma-multiplicative non empty for Subset-Family of X;
end;

definition
  let X be set;
  mode SigmaField of X is compl-closed sigma-multiplicative non empty
    Subset-Family of X;
end;

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

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

registration
  let X be set;
  cluster -> cap-closed compl-closed for SigmaField of X;
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;
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 :: PROB_1:17
  for ASeq being SetSequence of Si holds Union ASeq in Si;

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

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

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

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

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

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

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

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

registration
  let X,Si;
  cluster empty for Event of Si;
end;

definition

  let X,Si;

  func [#] Si -> Event of Si equals
:: PROB_1:def 7
  X;
end;

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

theorem :: PROB_1:25
  A1 is SetSequence of Si iff for n holds A1.n is Event of Si;

theorem :: PROB_1:26
  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:27
  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:28
  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);

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

definition
  let Omega,Sigma,ASeq,P;
  redefine func P * ASeq -> Real_Sequence;
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
:: PROB_1:def 8

  (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;
end;

reserve P for Probability of Sigma;

registration
  let Omega,Sigma;
  cluster -> zeroed for Probability of Sigma;
end;

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

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

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

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

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

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

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

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

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

theorem :: PROB_1:39
  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-Family of Omega;

theorem :: PROB_1:40
  bool X is SigmaField of X;

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

definition
  let r be ExtReal;
  func halfline r -> Subset of REAL equals
:: PROB_1:def 10
  ].-infty,r.[;
end;

definition
  func Family_of_halflines -> Subset-Family of REAL equals
:: PROB_1:def 11
  the set of all  halfline(r) where r is Element of REAL;
end;

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

theorem :: PROB_1:41
  for A, B being Subset of X holds Complement (A followed_by B) = A`
  followed_by B`;

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