:: 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-2012 Association of Mizar Users


begin

Lm1:  for A, B, C being set st C c= B holds
A \ C = (A \ B) \/ (A /\ (B \ C))
proofend;

definition
let X be set ;
let Si be SigmaField of X;
let XSeq be SetSequence of Si;
let n be Element of NAT ;
:: original:.
redefine funcXSeq . n ->  Element of Si;
coherence
 XSeq . n is Element of Si
proofend;
end;

theorem Th1: :: PROB_4:1
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds rng XSeq c= Si
proofend;

theorem Th2: :: PROB_4:2
for X being set
for Si being SigmaField of X
for f being Function holds
( f is SetSequence of Si iff f is Function of NAT,Si )
proofend;

scheme :: PROB_4:sch 1
LambdaSigmaSSeq{ F1() ->  set , F2() ->  SigmaField of F1(), F3( set ) ->  Element of F2() } :
 ex f being SetSequence of F2() st
for n being Element of NAT holds f . n = F3(n)
proofend;

registration
let X be set ;
cluster non empty V13() V16( NAT ) V17( bool X) Function-like V23( NAT ) V27( NAT , bool X) V118() for Element of bool [:NAT,(bool X):];
existence
 not for b1 being SetSequence of X holds b1 is V118()
proofend;
end;

registration
let X be set ;
let Si be SigmaField of X;
cluster non empty V13() V16( NAT ) V17(Si) V17( bool X) Function-like V23( NAT ) V27( NAT , bool X) V118() for Element of bool [:NAT,(bool X):];
existence
 not for b1 being SetSequence of Si holds b1 is V118()
proofend;
end;

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

theorem Th4: :: PROB_4:4
for X being set
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 ) ) )
proofend;

theorem Th5: :: PROB_4:5
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma holds P . (A \ B) = (P . (A \/ B)) - (P . B)
proofend;

theorem Th6: :: PROB_4:6
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma st A c= B & P . B = 0 holds
P . A = 0
proofend;

theorem Th7: :: PROB_4:7
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 )
proofend;

theorem Th8: :: PROB_4:8
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for A being set st A in rng ASeq holds
P . A = 0 ) iff P . (union (rng ASeq)) = 0 )
proofend;

theorem Th9: :: PROB_4:9
for seq being Function of NAT,REAL
for Eseq being Function of NAT,ExtREAL st seq = Eseq holds
Partial_Sums seq = Ser Eseq
proofend;

theorem Th10: :: PROB_4:10
for seq being Function of NAT,REAL
for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is V101() holds
upper_bound seq = sup (rng Eseq)
proofend;

theorem Th11: :: PROB_4:11
for seq being Function of NAT,REAL
for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is V102() holds
lower_bound seq = inf (rng Eseq)
proofend;

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

theorem Th13: :: PROB_4:13
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds P is sigma_Measure of Sigma
proofend;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
func P2M P ->  sigma_Measure of Sigma equals :: PROB_4:def 1
P;
coherence
 P is sigma_Measure of Sigma by Th13;
end;

:: deftheorem  defines P2M PROB_4:def_1_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds P2M P = P;

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

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
assume A1: M . X = R_EAL 1 ;
func M2P M ->  Probability of S equals :: PROB_4:def 2
M;
coherence
 M is Probability of S by A1, Th14;
end;

:: deftheorem  defines M2P PROB_4:def_2_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S st M . X = R_EAL 1 holds
M2P M = M;

Lm2:  for X being set
for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds (Partial_Union A1) . n = A1 . n
proofend;

theorem Th15: :: PROB_4:15
for X being set
for A1 being SetSequence of X st A1 is non-descending holds
Partial_Union A1 = A1
proofend;

theorem Th16: :: PROB_4:16
for X being set
for A1 being SetSequence of X st A1 is non-descending holds
( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) )
proofend;

theorem :: PROB_4:17
for X being set
for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n)
proofend;

theorem Th18: :: PROB_4:18
for X being set
for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n
proofend;

theorem :: PROB_4:19
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si st XSeq is non-descending holds
Partial_Union XSeq = XSeq by Th15;

theorem :: PROB_4:20
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si st XSeq is non-descending holds
( (Partial_Diff_Union XSeq) . 0 = XSeq . 0 & ( for n being Element of NAT holds (Partial_Diff_Union XSeq) . (n + 1) = (XSeq . (n + 1)) \ (XSeq . n) ) ) by Th16;

theorem :: PROB_4:21
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si st XSeq is non-descending holds
for n being Element of NAT holds (Partial_Diff_Union XSeq) . (n + 1) misses XSeq . n by Th18;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
predP is_complete Sigma means :Def3: :: PROB_4:def 3
 for A being Subset of Omega
for B being set st B in Sigma & A c= B & P . B = 0 holds
A in Sigma;
end;

:: deftheorem Def3 defines is_complete PROB_4:def_3_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds
( P is_complete Sigma iff for A being Subset of Omega
for B being set st B in Sigma & A c= B & P . B = 0 holds
A in Sigma );

theorem :: PROB_4:22
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds
( P is_complete Sigma iff P2M P is_complete Sigma )
proofend;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
mode thin of P ->  Subset of Omega means :Def4: :: PROB_4:def 4
 ex A being set st
( A in Sigma & it c= A & P . A = 0 );
existence
 ex b1 being Subset of Omega ex A being set st
( A in Sigma & b1 c= A & P . A = 0 )
proofend;
end;

:: deftheorem Def4 defines thin PROB_4:def_4_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for b4 being Subset of Omega holds
( b4 is thin of P iff ex A being set st
( A in Sigma & b4 c= A & P . A = 0 ) );

theorem Th23: :: PROB_4:23
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for Y being Subset of Omega holds
( Y is thin of P iff Y is thin of P2M P )
proofend;

theorem Th24: :: PROB_4:24
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds {} is thin of P
proofend;

theorem Th25: :: PROB_4:25
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B1, B2 being set st B1 in Sigma & B2 in Sigma holds
for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2
proofend;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
func COM (Sigma,P) ->  non empty Subset-Family of Omega means :Def5: :: 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 ) );
existence
 ex b1 being non empty Subset-Family of Omega st
for A being set holds
( A in b1 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) )
proofend;
uniqueness
 for b1, b2 being non empty Subset-Family of Omega st ( for A being set holds
( A in b1 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) & ( for A being set holds
( A in b2 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines COM PROB_4:def_5_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for b4 being non empty Subset-Family of Omega holds
( b4 = COM (Sigma,P) iff for A being set holds
( A in b4 iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) );

theorem Th26: :: PROB_4:26
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being thin of P holds C in COM (Sigma,P)
proofend;

theorem Th27: :: PROB_4:27
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM (Sigma,P) = COM (Sigma,(P2M P))
proofend;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
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;
correctness
coherence
A is Element of COM (Sigma,(P2M P));
by Th27;
end;

:: deftheorem  defines P_COM2M_COM PROB_4:def_6_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM (Sigma,P) holds P_COM2M_COM A = A;

theorem Th28: :: PROB_4:28
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds Sigma c= COM (Sigma,P)
proofend;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let A be Element of COM (Sigma,P);
func ProbPart A ->  non empty Subset-Family of Omega means :Def7: :: 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 ) );
existence
 ex b1 being non empty Subset-Family of Omega st
for B being set holds
( B in b1 iff ( B in Sigma & B c= A & A \ B is thin of P ) )
proofend;
uniqueness
 for b1, b2 being non empty Subset-Family of Omega st ( for B being set holds
( B in b1 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) & ( for B being set holds
( B in b2 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines ProbPart PROB_4:def_7_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM (Sigma,P)
for b5 being non empty Subset-Family of Omega holds
( b5 = ProbPart A iff for B being set holds
( B in b5 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) );

theorem :: PROB_4:29
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM (Sigma,P) holds ProbPart A = MeasPart (P_COM2M_COM A)
proofend;

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

theorem Th31: :: PROB_4:31
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being Function of NAT,(COM (Sigma,P)) ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n in ProbPart (F . n)
proofend;

theorem Th32: :: PROB_4:32
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being Function of NAT,(COM (Sigma,P))
for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st
for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n)
proofend;

theorem Th33: :: PROB_4:33
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for BSeq being SetSequence of Omega st ( for n being Element of NAT holds BSeq . n is thin of P ) holds
ex CSeq being SetSequence of Sigma st
for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )
proofend;

theorem Th34: :: PROB_4:34
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for D being non empty Subset-Family of Omega st ( 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 ) ) ) holds
D is SigmaField of Omega
proofend;

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
cluster COM (Sigma,P) ->  non empty compl-closed sigma-multiplicative ;
coherence
 ( COM (Sigma,P) is compl-closed & COM (Sigma,P) is sigma-multiplicative )
proofend;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
:: original:thin
redefine mode thin of P ->  Event of COM (Sigma,P);
coherence
 for b1 being thin of P holds b1 is Event of COM (Sigma,P) by Th26;
end;

theorem Th35: :: PROB_4:35
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
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 ) )
proofend;

theorem :: PROB_4:36
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being non empty Subset-Family of Omega st ( 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 ) ) ) holds
C = COM (Sigma,P)
proofend;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
func COM P ->  Probability of COM (Sigma,P) means :Def8: :: PROB_4:def 8
 for B being set st B in Sigma holds
for C being thin of P holds it . (B \/ C) = P . B;
existence
 ex b1 being Probability of COM (Sigma,P) st
for B being set st B in Sigma holds
for C being thin of P holds b1 . (B \/ C) = P . B
proofend;
uniqueness
 for b1, b2 being Probability of COM (Sigma,P) st ( for B being set st B in Sigma holds
for C being thin of P holds b1 . (B \/ C) = P . B ) & ( for B being set st B in Sigma holds
for C being thin of P holds b2 . (B \/ C) = P . B ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines COM PROB_4:def_8_:_
 for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for b4 being Probability of COM (Sigma,P) holds
( b4 = COM P iff for B being set st B in Sigma holds
for C being thin of P holds b4 . (B \/ C) = P . B );

theorem :: PROB_4:37
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM P = COM (P2M P)
proofend;

theorem :: PROB_4:38
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM P is_complete COM (Sigma,P)
proofend;

theorem Th39: :: PROB_4:39
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Event of Sigma holds P . A = (COM P) . A
proofend;

theorem Th40: :: PROB_4:40
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being thin of P holds (COM P) . C = 0
proofend;

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