let S be non empty finite set ; 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; 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) );
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;
( A misses B implies EP . (A \/ B) = (EP . A) + (EP . B) )
assume A4:
A misses B
;
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
;
verum
end;
A9:
for A being Event of Trivial-SigmaField S holds 0 <= EP . A
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) )
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
; 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 ; ( 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
; 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) )
; verum