:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura

::

:: Received November 23, 2005

:: Copyright (c) 2005-2017 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

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

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 )

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_{1}() -> set , F_{2}() -> SigmaField of F_{1}(), F_{3}( set ) -> Element of F_{2}() } :

LambdaSigmaSSeq{ F

proof end;

registration

let X be set ;

not for b_{1} being SetSequence of X holds b_{1} is V125()

end;
cluster V1() V4( NAT ) V5( bool X) non empty Function-like V25( NAT ) V29( NAT , bool X) V125() for Element of bool [:NAT,(bool X):];

existence not for b

proof end;

registration

let X be set ;

let Si be SigmaField of X;

not for b_{1} being SetSequence of Si holds b_{1} is V125()

end;
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) V125() for Element of bool [:NAT,(bool X):];

existence not for b

proof 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

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

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)

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

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 )

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 )

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

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 V108() holds

upper_bound seq = sup (rng Eseq)

for Eseq being sequence of ExtREAL st seq = Eseq & seq is V108() 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 V109() holds

lower_bound seq = inf (rng Eseq)

for Eseq being sequence of ExtREAL st seq = Eseq & seq is V109() 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

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

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;

coherence

P is sigma_Measure of Sigma by Th13;

end;
let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

coherence

P is sigma_Measure of Sigma by Th13;

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

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

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 ;

coherence

M is Probability of S by A1, Th14;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

assume A1: M . X = 1 ;

coherence

M is Probability of S by A1, Th14;

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

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;

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

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)

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

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;

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;

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;

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

:: deftheorem 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 );

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 ) by MEASURE3:def 1;

for Sigma being SigmaField of Omega

for P being Probability of Sigma holds

( P is_complete Sigma iff P2M P is_complete Sigma ) by MEASURE3:def 1;

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

ex b_{1} being Subset of Omega ex A being set st

( A in Sigma & b_{1} c= A & P . A = 0 )

end;
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 A being set st

( A in Sigma & it c= A & P . A = 0 );

ex b

( A in Sigma & b

proof 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_{4} being Subset of Omega holds

( b_{4} is thin of P iff ex A being set st

( A in Sigma & b_{4} c= A & P . A = 0 ) );

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for b

( b

( A in Sigma & b

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 )

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

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

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;

ex b_{1} being non empty Subset-Family of Omega st

for A being set holds

( A in b_{1} iff ex B being set st

( B in Sigma & ex C being thin of P st A = B \/ C ) )

for b_{1}, b_{2} being non empty Subset-Family of Omega st ( for A being set holds

( A in b_{1} 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_{2} iff ex B being set st

( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) holds

b_{1} = b_{2}

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

ex b

for A being set holds

( A in b

( B in Sigma & ex C being thin of P st A = B \/ C ) )

proof end;

uniqueness for b

( A in b

( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) & ( for A being set holds

( A in b

( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) holds

b

proof 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_{4} being non empty Subset-Family of Omega holds

( b_{4} = COM (Sigma,P) iff for A being set holds

( A in b_{4} iff ex B being set st

( B in Sigma & ex C being thin of P st A = B \/ C ) ) );

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for b

( b

( A in b

( 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)

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

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

correctness

coherence

A is Element of COM (Sigma,(P2M P));

by Th27;

end;
let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

let A be Element of COM (Sigma,P);

correctness

coherence

A is Element of COM (Sigma,(P2M P));

by Th27;

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

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)

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

ex b_{1} being non empty Subset-Family of Omega st

for B being set holds

( B in b_{1} iff ( B in Sigma & B c= A & A \ B is thin of P ) )

for b_{1}, b_{2} being non empty Subset-Family of Omega st ( for B being set holds

( B in b_{1} iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) & ( for B being set holds

( B in b_{2} iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) holds

b_{1} = b_{2}

end;
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 for B being set holds

( B in it iff ( B in Sigma & B c= A & A \ B is thin of P ) );

ex b

for B being set holds

( B in b

proof end;

uniqueness for b

( B in b

( B in b

b

proof 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_{5} being non empty Subset-Family of Omega holds

( b_{5} = ProbPart A iff for B being set holds

( B in b_{5} iff ( B in Sigma & B c= A & A \ B is thin of P ) ) );

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

( b

( B in b

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)

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

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)

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)

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 )

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

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;

coherence

( COM (Sigma,P) is compl-closed & COM (Sigma,P) is sigma-multiplicative )

end;
let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

coherence

( COM (Sigma,P) is compl-closed & COM (Sigma,P) is sigma-multiplicative )

proof 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_{1} being thin of P holds b_{1} is Event of COM (Sigma,P)
by Th26;

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

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

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)

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;

ex b_{1} being Probability of COM (Sigma,P) st

for B being set st B in Sigma holds

for C being thin of P holds b_{1} . (B \/ C) = P . B

for b_{1}, b_{2} being Probability of COM (Sigma,P) st ( for B being set st B in Sigma holds

for C being thin of P holds b_{1} . (B \/ C) = P . B ) & ( for B being set st B in Sigma holds

for C being thin of P holds b_{2} . (B \/ C) = P . B ) holds

b_{1} = b_{2}

end;
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 for B being set st B in Sigma holds

for C being thin of P holds it . (B \/ C) = P . B;

ex b

for B being set st B in Sigma holds

for C being thin of P holds b

proof end;

uniqueness for b

for C being thin of P holds b

for C being thin of P holds b

b

proof 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_{4} being Probability of COM (Sigma,P) holds

( b_{4} = COM P iff for B being set st B in Sigma holds

for C being thin of P holds b_{4} . (B \/ C) = P . B );

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for b

( b

for C being thin of P holds 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)

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 COM (Sigma,P)

for Sigma being SigmaField of Omega

for P being Probability of Sigma holds COM P is_complete COM (Sigma,P)

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

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

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

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;