:: The Relevance of Measure and Probability and Definition of Completeness
:: of Probability
::  by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received November 23, 2005
:: Copyright (c) 2005-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, SUBSET_1, PROB_1, XBOOLE_0, TARSKI, FUNCT_1, RELAT_1,
      NAT_1, PROB_2, FUNCOP_1, FUNCT_7, CARD_1, XXREAL_0, ARYTM_3, ZFMISC_1,
      CARD_3, EQREL_1, RPR_1, ARYTM_1, SERIES_1, SEQ_2, ORDINAL2, PROB_3,
      SUPINF_2, REAL_1, XXREAL_2, SUPINF_1, MEASURE1, VALUED_0, SETFAM_1,
      MEASURE3, PROB_4, SEQ_4, REWRITE1;
 notations TARSKI, XBOOLE_0, XREAL_0, CARD_3, ORDINAL1, MEASURE3, SUPINF_2,
      XXREAL_0, XXREAL_2, XCMPLX_0, NAT_1, SEQ_2, SETFAM_1, FUNCT_1, RELSET_1,
      SUBSET_1, NUMBERS, SUPINF_1, PARTFUN1, FUNCT_2, FUNCT_7, PROB_1, PROB_3,
      MEASURE1, FUNCOP_1, SEQM_3, SERIES_1, RINFSUP1, ZFMISC_1, MEASURE6,
      PROB_2;
 constructors REAL_1, SERIES_1, MEASURE3, MEASURE6, PARTFUN3, KURATO_0,
      RINFSUP1, PROB_3, SUPINF_1, FUNCT_7, RELSET_1, COMSEQ_2;
 registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, NAT_1,
      MEMBERED, MEASURE1, MEASURE3, VALUED_0, SEQ_2, SEQ_4, FUNCT_7, PROB_1,
      RELSET_1, PROB_3;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve n,m,k for Element of NAT,
  x,X for set,
  A1 for SetSequence of X,
  Si for SigmaField of X,
  XSeq for SetSequence of Si;
reserve Omega for non empty set,
  Sigma for SigmaField of Omega,
  ASeq for SetSequence of Sigma,
  P for Probability of Sigma;

definition
  let X,Si,XSeq,n;
  redefine func XSeq.n -> Element of Si;
end;

theorem :: PROB_4:1
  rng XSeq c= Si;

theorem :: PROB_4:2
  for f being Function holds f is SetSequence of Si iff f is sequence of Si;

scheme :: PROB_4:sch 1
  LambdaSigmaSSeq { X() -> set, Si() -> SigmaField of X(), F(set) -> Element
  of Si() } : ex f being SetSequence of Si() st for n holds f.n = F(n);

registration
  let X;
  cluster disjoint_valued for SetSequence of X;
end;

registration
  let X,Si;
  cluster disjoint_valued for SetSequence of Si;
end;

theorem :: PROB_4:3
  for A, B being Subset of X st A misses B holds (A,B) followed_by
  {} is disjoint_valued;

theorem :: PROB_4:4
  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 Union A1 in S) &
  for A being Subset of X st A in S holds A` in S;

theorem :: PROB_4:5
  for A,B being Event of Sigma holds P.(A \ B) = P.(A \/ B) - P.B;

theorem :: PROB_4:6
  for A,B being Event of Sigma st A c= B & P.B = 0 holds P.A = 0;

theorem :: PROB_4:7
  (for n holds P.(ASeq.n) = 0) iff P.(Union ASeq) = 0;

theorem :: PROB_4:8
  (for A being set st A in rng ASeq holds P.A = 0) iff P.(union rng ASeq) = 0;

theorem :: PROB_4:9
  for seq being sequence of REAL, Eseq being sequence of
  ExtREAL st seq = Eseq holds Partial_Sums seq = Ser Eseq;

theorem :: PROB_4:10
  for seq being sequence of REAL, Eseq being sequence of
  ExtREAL st seq = Eseq & seq is bounded_above
  holds upper_bound seq = sup rng Eseq;

theorem :: PROB_4:11
  for seq being sequence of REAL, Eseq being sequence of
  ExtREAL st seq = Eseq & seq is bounded_below
   holds lower_bound seq = inf rng Eseq;

theorem :: PROB_4:12
  for seq being sequence of REAL, Eseq being sequence of
  ExtREAL st seq = Eseq & seq is nonnegative summable holds Sum seq = SUM Eseq;

theorem :: PROB_4:13
  P is sigma_Measure of Sigma;

definition
  let Omega,Sigma,P;
  func P2M(P) -> sigma_Measure of Sigma equals
:: PROB_4:def 1
  P;
end;

theorem :: PROB_4:14
  for X being non empty set, S being SigmaField of X, M being
  sigma_Measure of S st M.X = 1 holds M is Probability of S;

definition
  let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
  assume
 M.X = 1;
  func M2P(M) -> Probability of S equals
:: PROB_4:def 2
  M;
end;

theorem :: PROB_4:15
  A1 is non-descending implies Partial_Union A1 = A1;

theorem :: PROB_4:16
  A1 is non-descending implies (Partial_Diff_Union A1).0 = A1.0 &
  for n being Nat holds (Partial_Diff_Union A1).(n+1) = A1.(n+1) \ A1.n;

theorem :: PROB_4:17
  A1 is non-descending implies for n holds A1.(n+1) = (
  Partial_Diff_Union A1).(n+1) \/ A1.n;

theorem :: PROB_4:18
  A1 is non-descending implies
  for n being Nat holds (Partial_Diff_Union A1).(n+1) misses A1.n;

theorem :: PROB_4:19
  XSeq is non-descending implies Partial_Union XSeq = XSeq;

theorem :: PROB_4:20
  XSeq is non-descending implies (Partial_Diff_Union XSeq).0 = XSeq.0 &
  for n holds (Partial_Diff_Union XSeq).(n+1) = XSeq.(n+1) \ XSeq.n;

theorem :: PROB_4:21
  XSeq is non-descending implies for n holds (Partial_Diff_Union XSeq).
  (n+1) misses XSeq.n;

definition
  let Omega,Sigma,P;
  attr P is complete means
:: PROB_4:def 3
  for A being Subset of Omega
  for B being set st B in Sigma holds (A c= B & P.B=0 implies A in Sigma);
end;

theorem :: PROB_4:22
  P is complete iff P2M(P) is complete;

definition
  let Omega,Sigma,P;
  mode thin of P -> Subset of Omega means
:: PROB_4:def 4
    ex A being set st A in Sigma & it c= A & P.A = 0;
end;

theorem :: PROB_4:23
  for Y being Subset of Omega holds Y is thin of P iff Y is thin of P2M(P);

theorem :: PROB_4:24
  {} is thin of P;

theorem :: PROB_4:25
  for B1,B2 being set st B1 in Sigma & B2 in Sigma holds for C1,C2
  being thin of P holds B1 \/ C1 = B2 \/ C2 implies P.B1 = P.B2;

definition
  let Omega,Sigma,P;
  func COM(Sigma,P) -> non empty Subset-Family of Omega means
:: PROB_4:def 5

  for A
being set holds A in it iff ex B being set st B in Sigma & ex C being thin of P
  st A = B \/ C;
end;

theorem :: PROB_4:26
  for C being thin of P holds C in COM(Sigma,P);

theorem :: PROB_4:27
  COM(Sigma,P) = COM(Sigma,P2M P);

definition
  let Omega,Sigma,P;
  let A be Element of COM(Sigma,P);
  func P_COM2M_COM(A) -> Element of COM(Sigma,P2M(P)) equals
:: PROB_4:def 6
  A;
end;

theorem :: PROB_4:28
  Sigma c= COM(Sigma,P);

definition
  let Omega,Sigma,P;
  let A be Element of COM(Sigma,P);
  func ProbPart(A) -> non empty Subset-Family of Omega means
:: PROB_4:def 7

  for B
  being set holds (B in it iff B in Sigma & B c= A & A \ B is thin of P );
end;

theorem :: PROB_4:29
  for A being Element of COM(Sigma,P) holds ProbPart(A) = MeasPart(
  P_COM2M_COM(A));

theorem :: PROB_4:30
  for A being Element of COM(Sigma,P) holds for A1,A2 being set st A1 in
  ProbPart(A) & A2 in ProbPart(A) holds P.A1 = P.A2;

theorem :: PROB_4:31
  for F being sequence of COM(Sigma,P) holds ex BSeq being
  SetSequence of Sigma st for n holds BSeq.n in ProbPart(F.n);

theorem :: PROB_4:32
  for F being sequence of COM(Sigma,P), BSeq being SetSequence
of Sigma holds ex CSeq being SetSequence of Omega st for n holds CSeq.n = F.n \
  BSeq.n;

theorem :: PROB_4:33
  for BSeq being SetSequence of Omega st (for n holds BSeq.n is
  thin of P) holds ex CSeq being SetSequence of Sigma st for n holds BSeq.n c=
  CSeq.n & P.(CSeq.n) = 0;

theorem :: PROB_4:34
  for D being non empty Subset-Family of Omega holds (for A being
set holds (A in D iff ex B being set st B in Sigma & ex C being thin of P st A
  = B \/ C)) implies D is SigmaField of Omega;

registration
  let Omega,Sigma,P;
  cluster COM(Sigma,P) -> compl-closed sigma-multiplicative;
end;

definition
  let Omega,Sigma,P;
  redefine mode thin of P -> Event of COM(Sigma,P);
end;

theorem :: PROB_4:35
  for A being set holds (A in COM(Sigma,P) iff ex A1,A2 being set
  st A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P.(A2 \ A1) = 0);

theorem :: PROB_4:36
  for C being non empty Subset-Family of Omega holds (for A being set
holds (A in C iff ex A1,A2 being set st A1 in Sigma & A2 in Sigma & A1 c= A & A
  c= A2 & P.(A2 \ A1) = 0)) implies C = COM(Sigma,P);

definition
  let Omega,Sigma,P;
  func COM(P) -> Probability of COM(Sigma,P) means
:: PROB_4:def 8

  for B being set st B in Sigma for C being thin of P holds it.(B \/ C) = P.B;
end;

theorem :: PROB_4:37
  COM(P) = COM(P2M P);

theorem :: PROB_4:38
  COM(P) is complete;

theorem :: PROB_4:39
  for A being Event of Sigma holds P.A = (COM P).A;

theorem :: PROB_4:40
  for C being thin of P holds (COM P).C = 0;

theorem :: PROB_4:41
  for A being Element of COM(Sigma,P), B being set st B in ProbPart(A)
  holds P.B = (COM P).A;