let S be non empty finite set ; :: thesis: for D being EqSampleSpaces of S ex EP being Probability of Trivial-SigmaField S st
for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) )
let D be EqSampleSpaces of S; :: thesis: ex EP being Probability of Trivial-SigmaField S st
for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) )
defpred S1[ object , object ] means ex D1 being set ex ch being Function of S,BOOLEAN st
( D1 = $1 & ch = chi (D1,S) & $2 = Prob (ch,D) );
A1: now :: thesis: for x being object st x in Trivial-SigmaField S holds
ex y being object st
( y in REAL & S1[x,y] )
let x be object ; :: thesis: ( x in Trivial-SigmaField S implies ex y being object st
( y in REAL & S1[x,y] ) )
assume x in Trivial-SigmaField S ; :: thesis: ex y being object st
( y in REAL & S1[x,y] )
reconsider xx = x as set by TARSKI:1;
reconsider ch = chi (xx,S) as Function of S,BOOLEAN by MARGREL1:def 11;
Prob (ch,D) in REAL by XREAL_0:def 1;
hence ex y being object st
( y in REAL & S1[x,y] ) ; :: thesis: verum
end;
consider EP being Function of (Trivial-SigmaField S),REAL such that
A2: for x being object st x in Trivial-SigmaField S holds
S1[x,EP . x] from FUNCT_2:sch 1(A1);
 A3: for A, B being Event of Trivial-SigmaField S st A misses B holds
EP . (A \/ B) = (EP . A) + (EP . B)
proof
let A, B be Event of Trivial-SigmaField S; :: thesis: ( A misses B implies EP . (A \/ B) = (EP . A) + (EP . B) )
assume A4: A misses B ; :: thesis: EP . (A \/ B) = (EP . A) + (EP . B)
S1[A,EP . A] by A2;
then consider chA being Function of S,BOOLEAN such that
A5: ( chA = chi (A,S) & EP . A = Prob (chA,D) ) ;
S1[B,EP . B] by A2;
then consider chB being Function of S,BOOLEAN such that
A6: ( chB = chi (B,S) & EP . B = Prob (chB,D) ) ;
S1[A \/ B,EP . (A \/ B)] by A2;
then consider chAB being Function of S,BOOLEAN such that
A7: ( chAB = chi ((A \/ B),S) & EP . (A \/ B) = Prob (chAB,D) ) ;
A8: chAB = chA 'or' chB by A5, A6, A7, Th31;
thus EP . (A \/ B) = ((Prob (chA,D)) + (Prob (chB,D))) - (Prob ((chA '&' chB),D)) by Th27, A7, A8
.= ((Prob (chA,D)) + (Prob (chB,D))) - 0 by A5, A6, A4, Th32
.= (EP . A) + (EP . B) by A6, A5 ; :: thesis: verum
end;
A9: for A being Event of Trivial-SigmaField S holds 0 <= EP . A
proof
let A be Event of Trivial-SigmaField S; :: thesis: 0 <= EP . A
S1[A,EP . A] by A2;
then consider chA being Function of S,BOOLEAN such that
A10: ( chA = chi (A,S) & EP . A = Prob (chA,D) ) ;
thus 0 <= EP . A by A10, Th30; :: thesis: verum
end;
A11: for ASeq being SetSequence of Trivial-SigmaField S st ASeq is non-ascending holds
( EP * ASeq is convergent & lim (EP * ASeq) = EP . (Intersection ASeq) )
proof
let ASeq be SetSequence of Trivial-SigmaField S; :: thesis: ( ASeq is non-ascending implies ( EP * ASeq is convergent & lim (EP * ASeq) = EP . (Intersection ASeq) ) )
assume ASeq is non-ascending ; :: thesis: ( EP * ASeq is convergent & lim (EP * ASeq) = EP . (Intersection ASeq) )
then consider N being Nat such that
A12: for m being Nat st N <= m holds
Intersection ASeq = ASeq . m by RANDOM_1:15;
now :: thesis: for m being Nat st N <= m holds
(EP * ASeq) . m = EP . (Intersection ASeq)
let m be Nat; :: thesis: ( N <= m implies (EP * ASeq) . m = EP . (Intersection ASeq) )
assume A13: N <= m ; :: thesis: (EP * ASeq) . m = EP . (Intersection ASeq)
m in NAT by ORDINAL1:def 12;
then m in dom ASeq by FUNCT_2:def 1;
hence (EP * ASeq) . m = EP . (ASeq . m) by FUNCT_1:13
.= EP . (Intersection ASeq) by A12, A13 ;
:: thesis: verum
end;
hence ( EP * ASeq is convergent & lim (EP * ASeq) = EP . (Intersection ASeq) ) by PROB_1:1; :: thesis: verum
end;
S1[ [#] S,EP . ([#] S)] by A2;
then consider chS being Function of S,BOOLEAN such that
A14: ( chS = chi (S,S) & EP . S = Prob (chS,D) ) ;
reconsider EP = EP as Probability of Trivial-SigmaField S by A9, A3, PROB_1:def 8, Th29, A11, A14;
take EP ; :: thesis: for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) )
let x be set ; :: thesis: ( x in Trivial-SigmaField S implies ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) ) )
assume x in Trivial-SigmaField S ; :: thesis: ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) )
then S1[x,EP . x] by A2;
hence ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & EP . x = Prob (ch,D) ) ; :: thesis: verum