:: PROB_2 semantic presentation

theorem :: PROB_2:1

canceled;

theorem :: PROB_2:2

canceled;

theorem :: PROB_2:3

canceled;

theorem Th4: :: PROB_2:4

for r, r1, r2, r3 being Real st r <> 0 & r1 <> 0 holds
( r3 / r1 = r2 / r iff r3 * r = r2 * r1 )

proof end;

theorem Th5: :: PROB_2:5

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

proof end;

theorem Th6: :: PROB_2:6

for Omega being non empty set
for Sigma being SigmaField of Omega
for A being Event of Sigma holds
( A /\ Omega = A & A /\ ([#] Sigma) = A ) by XBOOLE_1:28;

definition

let Omega be non empty 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 by PROB_1:57;

end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let ASeq be SetSequence of Sigma;
func @Intersection ASeq -> Event of Sigma equals :: PROB_2:def 1
Intersection ASeq;
coherence

proof end;

end;

:: deftheorem defines @Intersection PROB_2:def 1 :

theorem :: PROB_2:7

canceled;

theorem :: PROB_2:8

canceled;

theorem Th9: :: PROB_2:9

for Omega being non empty 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

proof end;

theorem Th10: :: PROB_2:10

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq, BSeq being SetSequence of Sigma
for B being Event of Sigma st ASeq is non-increasing & ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds
BSeq is non-increasing

proof end;

theorem Th11: :: PROB_2:11

for Omega being non empty set
for n being Nat
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for f being Function of Sigma, REAL holds (f * ASeq) . n = f . (ASeq . n)

proof end;

theorem Th12: :: PROB_2:12

for Omega being non empty set
for Sigma being SigmaField of Omega
for BSeq, ASeq 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;

theorem Th13: :: PROB_2:13

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

proof end;

theorem :: PROB_2:14

for X being set
for S being SetSequence of X holds
( S is non-increasing iff for n being Nat holds S . (n + 1) c= S . n )

proof end;

theorem :: PROB_2:15

for X being set
for S being SetSequence of X holds
( S is non-decreasing iff for n being Nat holds S . n c= S . (n + 1) )

proof end;

theorem :: PROB_2:16

for Omega being non empty set
for ASeq, BSeq being SetSequence of Omega st ( for n being Nat holds ASeq . n = BSeq . n ) holds
ASeq = BSeq

proof end;

theorem Th17: :: PROB_2:17

for Omega being non empty set
for ASeq being SetSequence of Omega holds
( ASeq is non-increasing iff Complement ASeq is non-decreasing )

proof end;

Lm1: for Omega being non empty set
for ASeq being SetSequence of Omega holds
( ASeq is non-decreasing iff Complement ASeq is non-increasing )

proof end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let ASeq be SetSequence of Sigma;
func @Complement ASeq -> SetSequence of Sigma equals :: PROB_2:def 2
Complement ASeq;
coherence

proof end;

end;

:: deftheorem defines @Complement PROB_2:def 2 :

definition

let F be Function;
attr F is disjoint_valued means :Def3: :: PROB_2:def 3
for x, y being set st x <> y holds
F . x misses F . y;

end;

:: deftheorem Def3 defines disjoint_valued PROB_2:def 3 :

definition

let Omega be non empty set ;
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 4
for m, n being Nat st m <> n holds
ASeq . m misses ASeq . n;
compatibility

proof end;

end;

:: deftheorem defines disjoint_valued PROB_2:def 4 :

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-decreasing holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) )

proof end;

theorem :: PROB_2:18

canceled;

theorem :: PROB_2:19

canceled;

theorem :: PROB_2:20

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-decreasing holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) )

proof end;

theorem :: PROB_2:21

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 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 Th22: :: PROB_2:22

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 \ (A /\ B)) = (P . A) - (P . (A /\ B))

proof end;

theorem Th23: :: PROB_2:23

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 . B & P . (A /\ B) <= P . A )

proof end;

theorem Th24: :: PROB_2:24

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C, B, A being Event of Sigma st C = B ` holds
P . A = (P . (A /\ B)) + (P . (A /\ C))

proof end;

theorem Th25: :: PROB_2:25

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) + (P . B)) - 1 <= P . (A /\ B)

proof end;

theorem Th26: :: PROB_2:26

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

proof end;

theorem Th27: :: PROB_2:27

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

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 being Event of Sigma holds
( P . (([#] Sigma) \ A) < 1 iff 0 < P . A )

proof end;

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;
pred A,B are_independent_respect_to P means :Def5: :: PROB_2:def 5
P . (A /\ B) = (P . A) * (P . B);
let C be Event of Sigma;
pred A,B,C are_independent_respect_to P means :Def6: :: PROB_2:def 6
( 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) );

end;

:: deftheorem Def5 defines are_independent_respect_to PROB_2:def 5 :

:: deftheorem Def6 defines are_independent_respect_to PROB_2:def 6 :

Lm3: 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 holds
B,A are_independent_respect_to P

proof end;

theorem :: PROB_2:29

canceled;

theorem :: PROB_2:30

canceled;

theorem :: PROB_2:31

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 B,A are_independent_respect_to P ) by Lm3;

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, 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) & A,B are_independent_respect_to P & B,C are_independent_respect_to P & A,C are_independent_respect_to P ) )

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, C being Event of Sigma st A,B,C are_independent_respect_to P holds
B,A,C 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, C being Event of Sigma st A,B,C are_independent_respect_to P holds
A,C,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, E being Event of Sigma st E = {} holds
A,E are_independent_respect_to P

proof end;

theorem :: PROB_2:36

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 A, [#] Sigma are_independent_respect_to P

proof end;

theorem Th37: :: PROB_2:37

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

proof end;

theorem Th38: :: PROB_2:38

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 holds
([#] Sigma) \ A,([#] Sigma) \ B are_independent_respect_to P

proof end;

theorem :: PROB_2:39

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

proof end;

theorem :: PROB_2:40

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

proof end;

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 ;
func P .|. B -> Probability of Sigma means :Def7: :: PROB_2:def 7
for A being Event of Sigma holds it . A = (P . (A /\ B)) / (P . B);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines .|. PROB_2:def 7 :

theorem :: PROB_2:41

canceled;

theorem Th42: :: PROB_2:42

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)

proof end;

theorem :: PROB_2:43

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)

proof end;

theorem Th44: :: PROB_2:44

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

proof end;

theorem Th45: :: PROB_2:45

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

proof end;

theorem :: PROB_2:46

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 )

proof end;

theorem :: PROB_2:47

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

proof end;

theorem :: PROB_2:48

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

proof end;

theorem Th49: :: PROB_2:49

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)

proof end;

theorem :: PROB_2:50

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

proof end;

theorem :: PROB_2:51

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

proof end;

theorem :: PROB_2:52

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

proof end;