:: 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{ F₁() -> set , F₂() -> SigmaField of F₁(), F₃( set ) -> Element of F₂() } :

ex f being SetSequence of F₂() st
for n being Element of NAT holds f . n = F₃(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 b₁ being SetSequence of X holds b₁ 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 b₁ being SetSequence of Si holds b₁ 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 b₁ being Subset of Omega ex A being set st
( A in Sigma & b₁ 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 b₄ being Subset of Omega holds
( b₄ is thin of P iff ex A being set st
( A in Sigma & b₄ 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 b₁ being non empty Subset-Family of Omega st
for A being set holds
( A in b₁ iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) )

proof end;

uniqueness
for b₁, b₂ being non empty Subset-Family of Omega st ( for A being set holds
( A in b₁ 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 b₂ iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) holds
b₁ = b₂

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 b₄ being non empty Subset-Family of Omega holds
( b₄ = COM (Sigma,P) iff for A being set holds
( A in b₄ 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 b₁ being non empty Subset-Family of Omega st
for B being set holds
( B in b₁ iff ( B in Sigma & B c= A & A \ B is thin of P ) )

proof end;

uniqueness
for b₁, b₂ being non empty Subset-Family of Omega st ( for B being set holds
( B in b₁ iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) & ( for B being set holds
( B in b₂ iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) holds
b₁ = b₂

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 b₅ being non empty Subset-Family of Omega holds
( b₅ = ProbPart A iff for B being set holds
( B in b₅ 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 b₁ being thin of P holds b₁ 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 b₁ being Probability of COM (Sigma,P) st
for B being set st B in Sigma holds
for C being thin of P holds b₁ . (B \/ C) = P . B

proof end;

uniqueness
for b₁, b₂ being Probability of COM (Sigma,P) st ( for B being set st B in Sigma holds
for C being thin of P holds b₁ . (B \/ C) = P . B ) & ( for B being set st B in Sigma holds
for C being thin of P holds b₂ . (B \/ C) = P . B ) holds
b₁ = b₂

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 b₄ being Probability of COM (Sigma,P) holds
( b₄ = COM P iff for B being set st B in Sigma holds
for C being thin of P holds b₄ . (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;