:: PROB_2 semantic presentation

theorem Th1: :: PROB_2:1
canceled;

theorem Th2: :: PROB_2:2
canceled;

theorem Th3: :: PROB_2:3
canceled;

theorem Th4: :: PROB_2:4
for b1, b2, b3, b4 being Real st b1 <> 0 & b2 <> 0 holds
( b4 / b2 = b3 / b1 iff b4 * b1 = b3 * b2 )
proof end;

theorem Th5: :: PROB_2:5
for b1 being Real
for b2, b3 being Real_Sequence st b2 is convergent & ( for b4 being Nat holds b3 . b4 = b1 - (b2 . b4) ) holds
( b3 is convergent & lim b3 = b1 - (lim b2) )
proof end;

theorem Th6: :: PROB_2:6
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Event of b2 holds
( b3 /\ b1 = b3 & b3 /\ ([#] b2) = b3 ) by XBOOLE_1:28;

definition
let c1 be non empty set ;
let c2 be SigmaField of c1;
let c3 be SetSequence of c2;
let c4 be Nat;
redefine func . as c3 . c4 -> Event of a2;
coherence
c3 . c4 is Event of c2 by PROB_1:57;
end;

definition
let c1 be non empty set ;
let c2 be SigmaField of c1;
let c3 be SetSequence of c2;
func @Intersection c3 -> Event of a2 equals :: PROB_2:def 1
 Intersection a3;
coherence
Intersection c3 is Event of c2
proof end;
end;

:: deftheorem Def1 defines @Intersection PROB_2:def 1 :
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being SetSequence of b2 holds @Intersection b3 = Intersection b3;

theorem Th7: :: PROB_2:7
canceled;

theorem Th8: :: PROB_2:8
canceled;

theorem Th9: :: PROB_2:9
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being SetSequence of b2
for b4 being Event of b2 ex b5 being SetSequence of b2 st
for b6 being Nat holds b5 . b6 = (b3 . b6) /\ b4
proof end;

theorem Th10: :: PROB_2:10
for b1 being non empty set
for b2 being SigmaField of b1
for b3, b4 being SetSequence of b2
for b5 being Event of b2 st b3 is non-increasing & ( for b6 being Nat holds b4 . b6 = (b3 . b6) /\ b5 ) holds
b4 is non-increasing
proof end;

theorem Th11: :: PROB_2:11
for b1 being non empty set
for b2 being Nat
for b3 being SigmaField of b1
for b4 being SetSequence of b3
for b5 being Function of b3, REAL holds (b5 * b4) . b2 = b5 . (b4 . b2)
proof end;

theorem Th12: :: PROB_2:12
for b1 being non empty set
for b2 being SigmaField of b1
for b3, b4 being SetSequence of b2
for b5 being Event of b2 st ( for b6 being Nat holds b3 . b6 = (b4 . b6) /\ b5 ) holds
(Intersection b4) /\ b5 = Intersection b3
proof end;

theorem Th13: :: PROB_2:13
for b1 being non empty set
for b2 being SigmaField of b1
for b3, b4 being Probability of b2 st ( for b5 being Event of b2 holds b3 . b5 = b4 . b5 ) holds
b3 = b4
proof end;

theorem Th14: :: PROB_2:14
for b1 being set
for b2 being SetSequence of b1 holds
( b2 is non-increasing iff for b3 being Nat holds b2 . (b3 + 1) c= b2 . b3 )
proof end;

theorem Th15: :: PROB_2:15
for b1 being set
for b2 being SetSequence of b1 holds
( b2 is non-decreasing iff for b3 being Nat holds b2 . b3 c= b2 . (b3 + 1) )
proof end;

theorem Th16: :: PROB_2:16
for b1 being non empty set
for b2, b3 being SetSequence of b1 st ( for b4 being Nat holds b2 . b4 = b3 . b4 ) holds
b2 = b3
proof end;

theorem Th17: :: PROB_2:17
for b1 being non empty set
for b2 being SetSequence of b1 holds
( b2 is non-increasing iff Complement b2 is non-decreasing )
proof end;

Lemma10: for b1 being non empty set
for b2 being SetSequence of b1 holds
( b2 is non-decreasing iff Complement b2 is non-increasing )
proof end;

definition
let c1 be non empty set ;
let c2 be SigmaField of c1;
let c3 be SetSequence of c2;
func @Complement c3 -> SetSequence of a2 equals :: PROB_2:def 2
 Complement a3;
coherence
Complement c3 is SetSequence of c2
proof end;
end;

:: deftheorem Def2 defines @Complement PROB_2:def 2 :
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being SetSequence of b2 holds @Complement b3 = Complement b3;

definition
let c1 be Function;
attr a1 is disjoint_valued means :Def3: :: PROB_2:def 3
for b1, b2 being set st b1 <> b2 holds
a1 . b1 misses a1 . b2;
end;

:: deftheorem Def3 defines disjoint_valued PROB_2:def 3 :
for b1 being Function holds
( b1 is disjoint_valued iff for b2, b3 being set st b2 <> b3 holds
b1 . b2 misses b1 . b3 );

definition
let c1 be non empty set ;
let c2 be SigmaField of c1;
let c3 be SetSequence of c2;
redefine attr disjoint_valued as a3 is disjoint_valued means :: PROB_2:def 4
for b1, b2 being Nat st b1 <> b2 holds
a3 . b1 misses a3 . b2;
compatibility
( c3 is disjoint_valued iff for b1, b2 being Nat st b1 <> b2 holds
c3 . b1 misses c3 . b2 )
proof end;
end;

:: deftheorem Def4 defines disjoint_valued PROB_2:def 4 :
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being SetSequence of b2 holds
( b3 is disjoint_valued iff for b4, b5 being Nat st b4 <> b5 holds
b3 . b4 misses b3 . b5 );

Lemma12: for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4 being SetSequence of b2 st b4 is non-decreasing holds
( b3 * b4 is convergent & lim (b3 * b4) = b3 . (Union b4) )
proof end;

theorem Th18: :: PROB_2:18
canceled;

theorem Th19: :: PROB_2:19
canceled;

theorem Th20: :: PROB_2:20
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Function of b2, REAL holds
( b3 is Probability of b2 iff ( ( for b4 being Event of b2 holds 0 <= b3 . b4 ) & b3 . b1 = 1 & ( for b4, b5 being Event of b2 st b4 misses b5 holds
b3 . (b4 \/ b5) = (b3 . b4) + (b3 . b5) ) & ( for b4 being SetSequence of b2 st b4 is non-decreasing holds
( b3 * b4 is convergent & lim (b3 * b4) = b3 . (Union b4) ) ) ) )
proof end;

theorem Th21: :: PROB_2:21
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5, b6 being Event of b2 holds b3 . ((b4 \/ b5) \/ b6) = ((((b3 . b4) + (b3 . b5)) + (b3 . b6)) - (((b3 . (b4 /\ b5)) + (b3 . (b5 /\ b6))) + (b3 . (b4 /\ b6)))) + (b3 . ((b4 /\ b5) /\ b6))
proof end;

theorem Th22: :: PROB_2:22
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 holds b3 . (b4 \ (b4 /\ b5)) = (b3 . b4) - (b3 . (b4 /\ b5))
proof end;

theorem Th23: :: PROB_2:23
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 holds
( b3 . (b4 /\ b5) <= b3 . b5 & b3 . (b4 /\ b5) <= b3 . b4 )
proof end;

theorem Th24: :: PROB_2:24
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5, b6 being Event of b2 st b4 = b5 ` holds
b3 . b6 = (b3 . (b6 /\ b5)) + (b3 . (b6 /\ b4))
proof end;

theorem Th25: :: PROB_2:25
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 holds ((b3 . b4) + (b3 . b5)) - 1 <= b3 . (b4 /\ b5)
proof end;

theorem Th26: :: PROB_2:26
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4 being Event of b2 holds b3 . b4 = 1 - (b3 . (([#] b2) \ b4))
proof end;

theorem Th27: :: PROB_2:27
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4 being Event of b2 holds
( b3 . b4 < 1 iff 0 < b3 . (([#] b2) \ b4) )
proof end;

theorem Th28: :: PROB_2:28
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4 being Event of b2 holds
( b3 . (([#] b2) \ b4) < 1 iff 0 < b3 . b4 )
proof end;

definition
let c1 be non empty set ;
let c2 be SigmaField of c1;
let c3 be Probability of c2;
let c4, c5 be Event of c2;
pred c4,c5 are_independent_respect_to c3 means :Def5: :: PROB_2:def 5
a3 . (a4 /\ a5) = (a3 . a4) * (a3 . a5);
let c6 be Event of c2;
pred c4,c5,c6 are_independent_respect_to c3 means :Def6: :: PROB_2:def 6
( a3 . ((a4 /\ a5) /\ a6) = ((a3 . a4) * (a3 . a5)) * (a3 . a6) & a3 . (a4 /\ a5) = (a3 . a4) * (a3 . a5) & a3 . (a4 /\ a6) = (a3 . a4) * (a3 . a6) & a3 . (a5 /\ a6) = (a3 . a5) * (a3 . a6) );
end;

:: deftheorem Def5 defines are_independent_respect_to PROB_2:def 5 :
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 holds
( b4,b5 are_independent_respect_to b3 iff b3 . (b4 /\ b5) = (b3 . b4) * (b3 . b5) );

:: deftheorem Def6 defines are_independent_respect_to PROB_2:def 6 :
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5, b6 being Event of b2 holds
( b4,b5,b6 are_independent_respect_to b3 iff ( b3 . ((b4 /\ b5) /\ b6) = ((b3 . b4) * (b3 . b5)) * (b3 . b6) & b3 . (b4 /\ b5) = (b3 . b4) * (b3 . b5) & b3 . (b4 /\ b6) = (b3 . b4) * (b3 . b6) & b3 . (b5 /\ b6) = (b3 . b5) * (b3 . b6) ) );

Lemma21: for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 st b4,b5 are_independent_respect_to b3 holds
b5,b4 are_independent_respect_to b3
proof end;

theorem Th29: :: PROB_2:29
canceled;

theorem Th30: :: PROB_2:30
canceled;

theorem Th31: :: PROB_2:31
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 holds
( b4,b5 are_independent_respect_to b3 iff b5,b4 are_independent_respect_to b3 ) by Lemma21;

theorem Th32: :: PROB_2:32
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5, b6 being Event of b2 holds
( b4,b5,b6 are_independent_respect_to b3 iff ( b3 . ((b4 /\ b5) /\ b6) = ((b3 . b4) * (b3 . b5)) * (b3 . b6) & b4,b5 are_independent_respect_to b3 & b5,b6 are_independent_respect_to b3 & b4,b6 are_independent_respect_to b3 ) )
proof end;

theorem Th33: :: PROB_2:33
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5, b6 being Event of b2 st b4,b5,b6 are_independent_respect_to b3 holds
b5,b4,b6 are_independent_respect_to b3
proof end;

theorem Th34: :: PROB_2:34
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5, b6 being Event of b2 st b4,b5,b6 are_independent_respect_to b3 holds
b4,b6,b5 are_independent_respect_to b3
proof end;

theorem Th35: :: PROB_2:35
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 st b5 = {} holds
b4,b5 are_independent_respect_to b3
proof end;

theorem Th36: :: PROB_2:36
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4 being Event of b2 holds b4, [#] b2 are_independent_respect_to b3
proof end;

theorem Th37: :: PROB_2:37
for b1 being non empty set
for b2 being SigmaField of b1
for b3, b4 being Event of b2
for b5 being Probability of b2 st b3,b4 are_independent_respect_to b5 holds
b3,([#] b2) \ b4 are_independent_respect_to b5
proof end;

theorem Th38: :: PROB_2:38
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 st b4,b5 are_independent_respect_to b3 holds
([#] b2) \ b4,([#] b2) \ b5 are_independent_respect_to b3
proof end;

theorem Th39: :: PROB_2:39
for b1 being non empty set
for b2 being SigmaField of b1
for b3, b4, b5 being Event of b2
for b6 being Probability of b2 st b3,b4 are_independent_respect_to b6 & b3,b5 are_independent_respect_to b6 & b4 misses b5 holds
b3,b4 \/ b5 are_independent_respect_to b6
proof end;

theorem Th40: :: PROB_2:40
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 st b4,b5 are_independent_respect_to b3 & b3 . b4 < 1 & b3 . b5 < 1 holds
b3 . (b4 \/ b5) < 1
proof end;

definition
let c1 be non empty set ;
let c2 be SigmaField of c1;
let c3 be Probability of c2;
let c4 be Event of c2;
assume E25: 0 < c3 . c4 ;
func c3 .|. c4 -> Probability of a2 means :Def7: :: PROB_2:def 7
for b1 being Event of a2 holds a5 . b1 = (a3 . (b1 /\ a4)) / (a3 . a4);
existence
ex b1 being Probability of c2 st
for b2 being Event of c2 holds b1 . b2 = (c3 . (b2 /\ c4)) / (c3 . c4)
proof end;
uniqueness
for b1, b2 being Probability of c2 st ( for b3 being Event of c2 holds b1 . b3 = (c3 . (b3 /\ c4)) / (c3 . c4) ) & ( for b3 being Event of c2 holds b2 . b3 = (c3 . (b3 /\ c4)) / (c3 . c4) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines .|. PROB_2:def 7 :
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4 being Event of b2 st 0 < b3 . b4 holds
for b5 being Probability of b2 holds
( b5 = b3 .|. b4 iff for b6 being Event of b2 holds b5 . b6 = (b3 . (b6 /\ b4)) / (b3 . b4) );

theorem Th41: :: PROB_2:41
canceled;

theorem Th42: :: PROB_2:42
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 st 0 < b3 . b4 holds
b3 . (b5 /\ b4) = ((b3 .|. b4) . b5) * (b3 . b4)
proof end;

theorem Th43: :: PROB_2:43
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5, b6 being Event of b2 st 0 < b3 . (b4 /\ b5) holds
b3 . ((b4 /\ b5) /\ b6) = ((b3 . b4) * ((b3 .|. b4) . b5)) * ((b3 .|. (b4 /\ b5)) . b6)
proof end;

theorem Th44: :: PROB_2:44
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5, b6 being Event of b2 st b6 = b5 ` & 0 < b3 . b5 & 0 < b3 . b6 holds
b3 . b4 = (((b3 .|. b5) . b4) * (b3 . b5)) + (((b3 .|. b6) . b4) * (b3 . b6))
proof end;

theorem Th45: :: PROB_2:45
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5, b6, b7 being Event of b2 st b5 misses b6 & b7 = (b5 \/ b6) ` & 0 < b3 . b5 & 0 < b3 . b6 & 0 < b3 . b7 holds
b3 . b4 = ((((b3 .|. b5) . b4) * (b3 . b5)) + (((b3 .|. b6) . b4) * (b3 . b6))) + (((b3 .|. b7) . b4) * (b3 . b7))
proof end;

theorem Th46: :: PROB_2:46
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 st 0 < b3 . b5 holds
( (b3 .|. b5) . b4 = b3 . b4 iff b4,b5 are_independent_respect_to b3 )
proof end;

theorem Th47: :: PROB_2:47
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 st 0 < b3 . b5 & b3 . b5 < 1 & (b3 .|. b5) . b4 = (b3 .|. (([#] b2) \ b5)) . b4 holds
b4,b5 are_independent_respect_to b3
proof end;

theorem Th48: :: PROB_2:48
for b1 being non empty set
for b2 being SigmaField of b1
for b3 being Probability of b2
for b4, b5 being Event of b2 st 0 < b3 . b5 holds
(((b3 . b4) + (b3 . b5)) - 1) / (b3 . b5) <= (b3 .|. b5) . b4
proof end;

theorem Th49: :: PROB_2:49
for b1 being non empty set
for b2 being SigmaField of b1
for b3, b4 being Event of b2
for b5 being Probability of b2 st 0 < b5 . b3 & 0 < b5 . b4 holds
(b5 .|. b4) . b3 = (((b5 .|. b3) . b4) * (b5 . b3)) / (b5 . b4)
proof end;

theorem Th50: :: PROB_2:50
for b1 being non empty set
for b2 being SigmaField of b1
for b3, b4, b5 being Event of b2
for b6 being Probability of b2 st 0 < b6 . b3 & b5 = b4 ` & 0 < b6 . b4 & 0 < b6 . b5 holds
( (b6 .|. b3) . b4 = (((b6 .|. b4) . b3) * (b6 . b4)) / ((((b6 .|. b4) . b3) * (b6 . b4)) + (((b6 .|. b5) . b3) * (b6 . b5))) & (b6 .|. b3) . b5 = (((b6 .|. b5) . b3) * (b6 . b5)) / ((((b6 .|. b4) . b3) * (b6 . b4)) + (((b6 .|. b5) . b3) * (b6 . b5))) )
proof end;

theorem Th51: :: PROB_2:51
for b1 being non empty set
for b2 being SigmaField of b1
for b3, b4, b5, b6 being Event of b2
for b7 being Probability of b2 st 0 < b7 . b3 & 0 < b7 . b4 & 0 < b7 . b5 & 0 < b7 . b6 & b4 misses b5 & b6 = (b4 \/ b5) ` holds
( (b7 .|. b3) . b4 = (((b7 .|. b4) . b3) * (b7 . b4)) / (((((b7 .|. b4) . b3) * (b7 . b4)) + (((b7 .|. b5) . b3) * (b7 . b5))) + (((b7 .|. b6) . b3) * (b7 . b6))) & (b7 .|. b3) . b5 = (((b7 .|. b5) . b3) * (b7 . b5)) / (((((b7 .|. b4) . b3) * (b7 . b4)) + (((b7 .|. b5) . b3) * (b7 . b5))) + (((b7 .|. b6) . b3) * (b7 . b6))) & (b7 .|. b3) . b6 = (((b7 .|. b6) . b3) * (b7 . b6)) / (((((b7 .|. b4) . b3) * (b7 . b4)) + (((b7 .|. b5) . b3) * (b7 . b5))) + (((b7 .|. b6) . b3) * (b7 . b6))) )
proof end;

theorem Th52: :: PROB_2:52
for b1 being non empty set
for b2 being SigmaField of b1
for b3, b4 being Event of b2
for b5 being Probability of b2 st 0 < b5 . b4 holds
1 - ((b5 . (([#] b2) \ b3)) / (b5 . b4)) <= (b5 .|. b4) . b3
proof end;