:: 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-2017 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;
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;
pred P is_complete Sigma 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 Sigma iff P2M(P) is_complete Sigma;
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 COM(Sigma,P);
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;