:: 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


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

proof end;

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 func XSeq . n -> Element of Si;
coherence
XSeq . n is Element of Si
proof end;
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
proof end;

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 sequence of Si )
proof end;

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

registration
let X be set ;
cluster V1() V4( NAT ) V5( bool X) non empty Function-like V25( NAT ) V29( NAT , bool X) V126() for Element of bool [:NAT,(bool X):];
existence
not for b1 being SetSequence of X holds b1 is V126()
proof end;
end;

registration
let X be set ;
let Si be SigmaField of X;
cluster V1() V4( NAT ) V5(Si) V5( bool X) non empty Function-like V25( NAT ) V29( NAT , bool X) V126() for Element of bool [:NAT,(bool X):];
existence
not for b1 being SetSequence of Si holds b1 is V126()
proof end;
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
proof end;

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

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

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

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

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

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

theorem Th10: :: PROB_4:10
for seq being sequence of REAL
for Eseq being sequence of ExtREAL st seq = Eseq & seq is V109() holds
upper_bound seq = sup (rng Eseq)
proof end;

theorem Th11: :: PROB_4:11
for seq being sequence of REAL
for Eseq being sequence of ExtREAL st seq = Eseq & seq is V110() holds
lower_bound seq = inf (rng Eseq)
proof end;

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

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

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 = 1 holds
M is Probability of S
proof end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
assume A1: M . X = 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 = 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 Nat holds (Partial_Union A1) . n = A1 . n

proof end;

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 by Lm2;

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 Nat holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) )
proof end;

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

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

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;
attr P is complete means :: 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 defines 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 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 iff P2M P is complete ) by MEASURE3:def 1;

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

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

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

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

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

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

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

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

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 sequence of (COM (Sigma,P)) ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n in ProbPart (F . n)
proof end;

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 sequence of (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)
proof end;

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

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

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

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

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

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

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

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

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