:: by Andrzej N\c{e}dzusiak

::

:: Received June 1, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

theorem Th2: :: PROB_2:2

for r being Real

for seq, seq1 being Real_Sequence st seq is convergent & ( for n being Nat holds seq1 . n = r - (seq . n) ) holds

( seq1 is convergent & lim seq1 = r - (lim seq) )

for seq, seq1 being Real_Sequence st seq is convergent & ( for n being Nat holds seq1 . n = r - (seq . n) ) holds

( seq1 is convergent & lim seq1 = r - (lim seq) )

proof end;

definition

let Omega be set ;

let Sigma be SigmaField of Omega;

let ASeq be SetSequence of Sigma;

let n be Nat;

:: original: .

redefine func ASeq . n -> Event of Sigma;

coherence

ASeq . n is Event of Sigma by PROB_1:25;

end;
let Sigma be SigmaField of Omega;

let ASeq be SetSequence of Sigma;

let n be Nat;

:: original: .

redefine func ASeq . n -> Event of Sigma;

coherence

ASeq . n is Event of Sigma by PROB_1:25;

definition

let Omega be set ;

let Sigma be SigmaField of Omega;

let ASeq be SetSequence of Sigma;

Intersection ASeq is Event of Sigma

end;
let Sigma be SigmaField of Omega;

let ASeq be SetSequence of Sigma;

:: nie mozna zastapic przez redefinicje - przeplot

coherence Intersection ASeq is Event of Sigma

proof end;

:: deftheorem defines @Intersection PROB_2:def 1 :

for Omega being set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma holds @Intersection ASeq = Intersection ASeq;

for Omega being set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma holds @Intersection ASeq = Intersection ASeq;

theorem Th3: :: PROB_2:3

for Omega being set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for B being Event of Sigma ex BSeq being SetSequence of Sigma st

for n being Nat holds BSeq . n = (ASeq . n) /\ B

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for B being Event of Sigma ex BSeq being SetSequence of Sigma st

for n being Nat holds BSeq . n = (ASeq . n) /\ B

proof end;

theorem Th4: :: PROB_2:4

for Omega being set

for Sigma being SigmaField of Omega

for ASeq, BSeq being SetSequence of Sigma

for B being Event of Sigma st ASeq is non-ascending & ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

BSeq is non-ascending

for Sigma being SigmaField of Omega

for ASeq, BSeq being SetSequence of Sigma

for B being Event of Sigma st ASeq is non-ascending & ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

BSeq is non-ascending

proof end;

theorem Th5: :: PROB_2:5

for Omega being set

for Sigma being SigmaField of Omega

for ASeq, BSeq being SetSequence of Sigma

for B being Event of Sigma st ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

(Intersection ASeq) /\ B = Intersection BSeq

for Sigma being SigmaField of Omega

for ASeq, BSeq being SetSequence of Sigma

for B being Event of Sigma st ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

(Intersection ASeq) /\ B = Intersection BSeq

proof end;

registration

let Omega be set ;

let Sigma be SigmaField of Omega;

let ASeq be SetSequence of Sigma;

coherence

Complement ASeq is Sigma -valued

end;
let Sigma be SigmaField of Omega;

let ASeq be SetSequence of Sigma;

coherence

Complement ASeq is Sigma -valued

proof end;

theorem :: PROB_2:6

for X being set

for S being SetSequence of X holds

( S is non-ascending iff for n being Nat holds S . (n + 1) c= S . n )

for S being SetSequence of X holds

( S is non-ascending iff for n being Nat holds S . (n + 1) c= S . n )

proof end;

theorem :: PROB_2:7

for X being set

for S being SetSequence of X holds

( S is non-descending iff for n being Nat holds S . n c= S . (n + 1) )

for S being SetSequence of X holds

( S is non-descending iff for n being Nat holds S . n c= S . (n + 1) )

proof end;

theorem Th8: :: PROB_2:8

for Omega being set

for ASeq being SetSequence of Omega holds

( ASeq is non-ascending iff Complement ASeq is non-descending )

for ASeq being SetSequence of Omega holds

( ASeq is non-ascending iff Complement ASeq is non-descending )

proof end;

Lm1: for Omega being set

for ASeq being SetSequence of Omega holds

( ASeq is non-descending iff Complement ASeq is non-ascending )

proof end;

definition

let F be Function;

end;
attr F is disjoint_valued means :: PROB_2:def 2

for x, y being object st x <> y holds

F . x misses F . y;

for x, y being object st x <> y holds

F . x misses F . y;

:: deftheorem defines disjoint_valued PROB_2:def 2 :

for F being Function holds

( F is disjoint_valued iff for x, y being object st x <> y holds

F . x misses F . y );

for F being Function holds

( F is disjoint_valued iff for x, y being object st x <> y holds

F . x misses F . y );

definition

let Omega be set ;

let Sigma be SigmaField of Omega;

let ASeq be SetSequence of Sigma;

( ASeq is disjoint_valued iff for m, n being Nat st m <> n holds

ASeq . m misses ASeq . n )

end;
let Sigma be SigmaField of Omega;

let ASeq be SetSequence of Sigma;

:: original: disjoint_valued

redefine attr ASeq is disjoint_valued means :: PROB_2:def 3

for m, n being Nat st m <> n holds

ASeq . m misses ASeq . n;

compatibility redefine attr ASeq is disjoint_valued means :: PROB_2:def 3

for m, n being Nat st m <> n holds

ASeq . m misses ASeq . n;

( ASeq is disjoint_valued iff for m, n being Nat st m <> n holds

ASeq . m misses ASeq . n )

proof end;

:: deftheorem defines disjoint_valued PROB_2:def 3 :

for Omega being set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma holds

( ASeq is disjoint_valued iff for m, n being Nat st m <> n holds

ASeq . m misses ASeq . n );

for Omega being set

for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma holds

( ASeq is disjoint_valued iff for m, n being Nat st m <> n holds

ASeq . m misses ASeq . n );

Lm2: for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for ASeq being SetSequence of Sigma st ASeq is non-descending holds

( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) )

proof end;

theorem Th9: :: PROB_2:9

for Omega being non empty set

for Sigma being SigmaField of Omega

for P, P1 being Probability of Sigma st ( for A being Event of Sigma holds P . A = P1 . A ) holds

P = P1

for Sigma being SigmaField of Omega

for P, P1 being Probability of Sigma st ( for A being Event of Sigma holds P . A = P1 . A ) holds

P = P1

proof end;

theorem :: PROB_2:10

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Function of Sigma,REAL holds

( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds

P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds

( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) )

for Sigma being SigmaField of Omega

for P being Function of Sigma,REAL holds

( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds

P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds

( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) )

proof end;

theorem :: PROB_2:11

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B, C being Event of Sigma

for P being Probability of Sigma holds P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C))

for Sigma being SigmaField of Omega

for A, B, C being Event of Sigma

for P being Probability of Sigma holds P . ((A \/ B) \/ C) = ((((P . A) + (P . B)) + (P . C)) - (((P . (A /\ B)) + (P . (B /\ C))) + (P . (A /\ C)))) + (P . ((A /\ B) /\ C))

proof end;

theorem :: PROB_2:12

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \ (A /\ B)) = (P . A) - (P . (A /\ B)) by PROB_1:33, XBOOLE_1:17;

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds P . (A \ (A /\ B)) = (P . A) - (P . (A /\ B)) by PROB_1:33, XBOOLE_1:17;

theorem :: PROB_2:13

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds

( P . (A /\ B) <= P . B & P . (A /\ B) <= P . A ) by PROB_1:34, XBOOLE_1:17;

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds

( P . (A /\ B) <= P . B & P . (A /\ B) <= P . A ) by PROB_1:34, XBOOLE_1:17;

theorem Th14: :: PROB_2:14

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B, C being Event of Sigma

for P being Probability of Sigma st C = B ` holds

P . A = (P . (A /\ B)) + (P . (A /\ C))

for Sigma being SigmaField of Omega

for A, B, C being Event of Sigma

for P being Probability of Sigma st C = B ` holds

P . A = (P . (A /\ B)) + (P . (A /\ C))

proof end;

theorem Th15: :: PROB_2:15

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds ((P . A) + (P . B)) - 1 <= P . (A /\ B)

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma holds ((P . A) + (P . B)) - 1 <= P . (A /\ B)

proof end;

theorem Th16: :: PROB_2:16

for Omega being non empty set

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds P . A = 1 - (P . (([#] Sigma) \ A))

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds P . A = 1 - (P . (([#] Sigma) \ A))

proof end;

theorem Th17: :: PROB_2:17

for Omega being non empty set

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds

( P . A < 1 iff 0 < P . (([#] Sigma) \ A) )

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds

( P . A < 1 iff 0 < P . (([#] Sigma) \ A) )

proof end;

theorem :: PROB_2:18

for Omega being non empty set

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds

( P . (([#] Sigma) \ A) < 1 iff 0 < P . A )

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds

( P . (([#] Sigma) \ A) < 1 iff 0 < P . A )

proof end;

::

:: INDEPENDENCE OF EVENTS

::

:: INDEPENDENCE OF EVENTS

::

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

let A, B be Event of Sigma;

let C be Event of Sigma;

end;
let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

let A, B be Event of Sigma;

let C be Event of Sigma;

:: deftheorem defines are_independent_respect_to PROB_2:def 4 :

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

( A,B are_independent_respect_to P iff P . (A /\ B) = (P . A) * (P . B) );

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

( A,B are_independent_respect_to P iff P . (A /\ B) = (P . A) * (P . B) );

:: deftheorem defines are_independent_respect_to PROB_2:def 5 :

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B, C being Event of Sigma holds

( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & P . (A /\ B) = (P . A) * (P . B) & P . (A /\ C) = (P . A) * (P . C) & P . (B /\ C) = (P . B) * (P . C) ) );

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B, C being Event of Sigma holds

( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & P . (A /\ B) = (P . A) * (P . B) & P . (A /\ C) = (P . A) * (P . C) & P . (B /\ C) = (P . B) * (P . C) ) );

theorem :: PROB_2:19

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st A,B are_independent_respect_to P holds

B,A are_independent_respect_to P ;

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st A,B are_independent_respect_to P holds

B,A are_independent_respect_to P ;

theorem :: PROB_2:20

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B, C being Event of Sigma

for P being Probability of Sigma holds

( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) ) ;

for Sigma being SigmaField of Omega

for A, B, C being Event of Sigma

for P being Probability of Sigma holds

( A,B,C are_independent_respect_to P iff ( P . ((A /\ B) /\ C) = ((P . A) * (P . B)) * (P . C) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) ) ;

theorem :: PROB_2:21

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B, C being Event of Sigma

for P being Probability of Sigma st A,B,C are_independent_respect_to P holds

B,A,C are_independent_respect_to P ;

for Sigma being SigmaField of Omega

for A, B, C being Event of Sigma

for P being Probability of Sigma st A,B,C are_independent_respect_to P holds

B,A,C are_independent_respect_to P ;

theorem :: PROB_2:22

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B, C being Event of Sigma

for P being Probability of Sigma st A,B,C are_independent_respect_to P holds

A,C,B are_independent_respect_to P by XBOOLE_1:16;

for Sigma being SigmaField of Omega

for A, B, C being Event of Sigma

for P being Probability of Sigma st A,B,C are_independent_respect_to P holds

A,C,B are_independent_respect_to P by XBOOLE_1:16;

theorem :: PROB_2:23

for Omega being non empty set

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma

for E being Event of Sigma st E = {} holds

A,E are_independent_respect_to P

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma

for E being Event of Sigma st E = {} holds

A,E are_independent_respect_to P

proof end;

theorem :: PROB_2:24

for Omega being non empty set

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds A, [#] Sigma are_independent_respect_to P

for Sigma being SigmaField of Omega

for A being Event of Sigma

for P being Probability of Sigma holds A, [#] Sigma are_independent_respect_to P

proof end;

theorem Th25: :: PROB_2:25

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st A,B are_independent_respect_to P holds

A,([#] Sigma) \ B are_independent_respect_to P

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st A,B are_independent_respect_to P holds

A,([#] Sigma) \ B are_independent_respect_to P

proof end;

theorem Th26: :: PROB_2:26

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st A,B are_independent_respect_to P holds

([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st A,B are_independent_respect_to P holds

([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P

proof end;

theorem :: PROB_2:27

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B, C being Event of Sigma

for P being Probability of Sigma st A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C holds

A,B \/ C are_independent_respect_to P

for Sigma being SigmaField of Omega

for A, B, C being Event of Sigma

for P being Probability of Sigma st A,B are_independent_respect_to P & A,C are_independent_respect_to P & B misses C holds

A,B \/ C are_independent_respect_to P

proof end;

theorem :: PROB_2:28

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,B are_independent_respect_to P & P . A < 1 & P . B < 1 holds

P . (A \/ B) < 1

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B being Event of Sigma st A,B are_independent_respect_to P & P . A < 1 & P . B < 1 holds

P . (A \/ B) < 1

proof end;

::

:: CONDITIONAL PROBABILITY

::

:: CONDITIONAL PROBABILITY

::

definition

let Omega be non empty set ;

let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

let B be Event of Sigma;

assume A1: 0 < P . B ;

ex b_{1} being Probability of Sigma st

for A being Event of Sigma holds b_{1} . A = (P . (A /\ B)) / (P . B)

for b_{1}, b_{2} being Probability of Sigma st ( for A being Event of Sigma holds b_{1} . A = (P . (A /\ B)) / (P . B) ) & ( for A being Event of Sigma holds b_{2} . A = (P . (A /\ B)) / (P . B) ) holds

b_{1} = b_{2}

end;
let Sigma be SigmaField of Omega;

let P be Probability of Sigma;

let B be Event of Sigma;

assume A1: 0 < P . B ;

func P .|. B -> Probability of Sigma means :Def6: :: PROB_2:def 6

for A being Event of Sigma holds it . A = (P . (A /\ B)) / (P . B);

existence for A being Event of Sigma holds it . A = (P . (A /\ B)) / (P . B);

ex b

for A being Event of Sigma holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines .|. PROB_2:def 6 :

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for B being Event of Sigma st 0 < P . B holds

for b_{5} being Probability of Sigma holds

( b_{5} = P .|. B iff for A being Event of Sigma holds b_{5} . A = (P . (A /\ B)) / (P . B) );

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for B being Event of Sigma st 0 < P . B holds

for b

( b

theorem Th29: :: PROB_2:29

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for B, A being Event of Sigma st 0 < P . B holds

P . (A /\ B) = ((P .|. B) . A) * (P . B)

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for B, A being Event of Sigma st 0 < P . B holds

P . (A /\ B) = ((P .|. B) . A) * (P . B)

proof end;

theorem :: PROB_2:30

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B, C being Event of Sigma st 0 < P . (A /\ B) holds

P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C)

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B, C being Event of Sigma st 0 < P . (A /\ B) holds

P . ((A /\ B) /\ C) = ((P . A) * ((P .|. A) . B)) * ((P .|. (A /\ B)) . C)

proof end;

theorem Th31: :: PROB_2:31

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B, C being Event of Sigma st C = B ` & 0 < P . B & 0 < P . C holds

P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C))

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B, C being Event of Sigma st C = B ` & 0 < P . B & 0 < P . C holds

P . A = (((P .|. B) . A) * (P . B)) + (((P .|. C) . A) * (P . C))

proof end;

theorem Th32: :: PROB_2:32

for Omega being non empty set

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, A1, A2, A3 being Event of Sigma st A1 misses A2 & A3 = (A1 \/ A2) ` & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 holds

P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3))

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, A1, A2, A3 being Event of Sigma st A1 misses A2 & A3 = (A1 \/ A2) ` & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 holds

P . A = ((((P .|. A1) . A) * (P . A1)) + (((P .|. A2) . A) * (P . A2))) + (((P .|. A3) . A) * (P . A3))

proof end;

theorem :: PROB_2:33

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 0 < P . B holds

( (P .|. B) . A = P . A iff A,B are_independent_respect_to P )

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B being Event of Sigma st 0 < P . B holds

( (P .|. B) . A = P . A iff A,B are_independent_respect_to P )

proof end;

theorem :: PROB_2:34

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 0 < P . B & P . B < 1 & (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A holds

A,B are_independent_respect_to P

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B being Event of Sigma st 0 < P . B & P . B < 1 & (P .|. B) . A = (P .|. (([#] Sigma) \ B)) . A holds

A,B are_independent_respect_to P

proof end;

theorem :: PROB_2:35

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 0 < P . B holds

(((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A

for Sigma being SigmaField of Omega

for P being Probability of Sigma

for A, B being Event of Sigma st 0 < P . B holds

(((P . A) + (P . B)) - 1) / (P . B) <= (P .|. B) . A

proof end;

theorem Th36: :: PROB_2:36

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st 0 < P . A & 0 < P . B holds

(P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B)

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st 0 < P . A & 0 < P . B holds

(P .|. B) . A = (((P .|. A) . B) * (P . A)) / (P . B)

proof end;

theorem :: PROB_2:37

for Omega being non empty set

for Sigma being SigmaField of Omega

for B, A1, A2 being Event of Sigma

for P being Probability of Sigma st 0 < P . B & A2 = A1 ` & 0 < P . A1 & 0 < P . A2 holds

( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) )

for Sigma being SigmaField of Omega

for B, A1, A2 being Event of Sigma

for P being Probability of Sigma st 0 < P . B & A2 = A1 ` & 0 < P . A1 & 0 < P . A2 holds

( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / ((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) )

proof end;

theorem :: PROB_2:38

for Omega being non empty set

for Sigma being SigmaField of Omega

for B, A1, A2, A3 being Event of Sigma

for P being Probability of Sigma st 0 < P . B & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 & A1 misses A2 & A3 = (A1 \/ A2) ` holds

( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) )

for Sigma being SigmaField of Omega

for B, A1, A2, A3 being Event of Sigma

for P being Probability of Sigma st 0 < P . B & 0 < P . A1 & 0 < P . A2 & 0 < P . A3 & A1 misses A2 & A3 = (A1 \/ A2) ` holds

( (P .|. B) . A1 = (((P .|. A1) . B) * (P . A1)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A2 = (((P .|. A2) . B) * (P . A2)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) & (P .|. B) . A3 = (((P .|. A3) . B) * (P . A3)) / (((((P .|. A1) . B) * (P . A1)) + (((P .|. A2) . B) * (P . A2))) + (((P .|. A3) . B) * (P . A3))) )

proof end;

theorem :: PROB_2:39

for Omega being non empty set

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st 0 < P . B holds

1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A

for Sigma being SigmaField of Omega

for A, B being Event of Sigma

for P being Probability of Sigma st 0 < P . B holds

1 - ((P . (([#] Sigma) \ A)) / (P . B)) <= (P .|. B) . A

proof end;