:: Posterior Probability on Finite Set
:: by Hiroyuki Okazaki
::
:: Received July 4, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users


theorem :: DIST_2:1
for Y being non empty finite set
for s being FinSequence of Y st Y = {1} & s = <*1*> holds
FDprobSEQ s = <*1*>
proof end;

theorem :: DIST_2:2
for S being non empty finite set
for p being distProbFinS of S
for s being FinSequence of S st FDprobSEQ s = p holds
( distribution (p,S) = Finseq-EQclass s & s in distribution (p,S) )
proof end;

theorem Th3: :: DIST_2:3
for S being non empty finite set
for x being Element of S holds
( x in rng (canFS S) & ex n being Nat st
( n in dom (canFS S) & x = (canFS S) . n & n in Seg (card S) ) )
proof end;

Lm1: for S being non empty finite set
for A being Element of distribution_family S holds not A is empty

proof end;

registration
let S be non empty finite set ;
cluster -> non empty for Element of distribution_family S;
coherence
for b1 being Element of distribution_family S holds not b1 is empty
by Lm1;
end;

definition
let S be non empty finite set ;
let D be Element of distribution_family S;
:: original: Element
redefine mode Element of D -> FinSequence of S;
coherence
for b1 being Element of D holds b1 is FinSequence of S
proof end;
end;

theorem Th4: :: DIST_2:4
for S being non empty finite set
for D being Element of distribution_family S
for s, t being Element of D holds s,t -are_prob_equivalent
proof end;

notation
let S be non empty finite set ;
let D be Element of distribution_family S;
synonym well-distributed D for with_non-empty_elements ;
end;

theorem Th5: :: DIST_2:5
for S being non empty finite set
for s being FinSequence of S holds
( ( for x being set holds FDprobability (x,s) = 0 ) iff s is empty )
proof end;

registration
let S be non empty finite set ;
cluster non empty well-distributed for Element of distribution_family S;
existence
ex b1 being Element of distribution_family S st b1 is well-distributed
proof end;
end;

theorem Th6: :: DIST_2:6
for S being non empty finite set
for D being Element of distribution_family S holds
( not D is well-distributed iff D = {(<*> S)} )
proof end;

definition
let S be non empty finite set ;
mode EqSampleSpaces of S is well-distributed Element of distribution_family S;
end;

registration
let S be non empty finite set ;
cluster uniform_distribution S -> well-distributed ;
coherence
uniform_distribution S is well-distributed
proof end;
end;

theorem Th7: :: DIST_2:7
for S being non empty finite set
for D being EqSampleSpaces of S holds (GenProbSEQ S) . D is distProbFinS of S
proof end;

definition
let S be non empty finite set ;
let a be Element of S;
func index a -> Element of NAT equals :: DIST_2:def 1
a .. (canFS S);
correctness
coherence
a .. (canFS S) is Element of NAT
;
;
end;

:: deftheorem defines index DIST_2:def 1 :
for S being non empty finite set
for a being Element of S holds index a = a .. (canFS S);

definition
let S be non empty finite set ;
let D be EqSampleSpaces of S;
func ProbFinS_of D -> distProbFinS of S equals :: DIST_2:def 2
(GenProbSEQ S) . D;
correctness
coherence
(GenProbSEQ S) . D is distProbFinS of S
;
by Th7;
end;

:: deftheorem defines ProbFinS_of DIST_2:def 2 :
for S being non empty finite set
for D being EqSampleSpaces of S holds ProbFinS_of D = (GenProbSEQ S) . D;

definition
let judgefunc be BOOLEAN -valued Function;
func trueEVENT judgefunc -> Event of (dom judgefunc) equals :: DIST_2:def 3
judgefunc " {TRUE};
coherence
judgefunc " {TRUE} is Event of (dom judgefunc)
proof end;
end;

:: deftheorem defines trueEVENT DIST_2:def 3 :
for judgefunc being BOOLEAN -valued Function holds trueEVENT judgefunc = judgefunc " {TRUE};

theorem Th8: :: DIST_2:8
for S being non empty finite set
for f being b1 -valued Function
for judgefunc being Function of S,BOOLEAN holds trueEVENT (judgefunc * f) is Event of (dom f)
proof end;

definition
let S be non empty finite set ;
let D be EqSampleSpaces of S;
let s be Element of D;
let judgefunc be Function of S,BOOLEAN;
func Prob (judgefunc,s) -> Real equals :: DIST_2:def 4
(card (trueEVENT (judgefunc * s))) / (len s);
correctness
coherence
(card (trueEVENT (judgefunc * s))) / (len s) is Real
;
;
end;

:: deftheorem defines Prob DIST_2:def 4 :
for S being non empty finite set
for D being EqSampleSpaces of S
for s being Element of D
for judgefunc being Function of S,BOOLEAN holds Prob (judgefunc,s) = (card (trueEVENT (judgefunc * s))) / (len s);

theorem :: DIST_2:9
for S being non empty finite set
for D being EqSampleSpaces of S
for s being Element of D
for judgefunc being Function of S,BOOLEAN
for F being non empty finite set
for E being Event of F st F = dom s & E = trueEVENT (judgefunc * s) holds
Prob (judgefunc,s) = prob E
proof end;

theorem Th10: :: DIST_2:10
for S being non empty finite set
for D being EqSampleSpaces of S
for a being Element of S
for s being Element of D
for judgefunc being Function of S,BOOLEAN st ( for x being set holds
( x = a iff judgefunc . x = TRUE ) ) holds
Prob (judgefunc,s) = FDprobability (a,s)
proof end;

definition
let S be set ;
let s be FinSequence of S;
let A be Subset of (dom s);
func extract (s,A) -> FinSequence of S equals :: DIST_2:def 5
s * (canFS A);
coherence
s * (canFS A) is FinSequence of S
proof end;
end;

:: deftheorem defines extract DIST_2:def 5 :
for S being set
for s being FinSequence of S
for A being Subset of (dom s) holds extract (s,A) = s * (canFS A);

theorem Th11: :: DIST_2:11
for S being set
for s being FinSequence of S
for A being Subset of (dom s) holds
( len (extract (s,A)) = card A & ( for i being Nat st i in dom (extract (s,A)) holds
(extract (s,A)) . i = s . ((canFS A) . i) ) )
proof end;

theorem Th12: :: DIST_2:12
for S being non empty finite set
for s being FinSequence of S
for A being Subset of (dom s)
for f being Function st f = canFS A holds
(extract (s,A)) * (f ") = s | A
proof end;

theorem Th13: :: DIST_2:13
for S being non empty finite set
for f being b1 -valued Function
for judgefunc being Function of S,BOOLEAN
for n being set st n in dom f holds
( n in trueEVENT (judgefunc * f) iff f . n in trueEVENT judgefunc )
proof end;

theorem Th14: :: DIST_2:14
for S being non empty finite set
for f being b1 -valued Function
for judgefunc being Function of S,BOOLEAN holds trueEVENT (judgefunc * f) = f " (trueEVENT judgefunc)
proof end;

theorem Th15: :: DIST_2:15
for S being non empty finite set
for D being EqSampleSpaces of S
for s being Element of D
for judgefunc being Function of S,BOOLEAN ex A being Subset of (dom (freqSEQ s)) st
( A = trueEVENT (judgefunc * (canFS S)) & card (trueEVENT (judgefunc * s)) = Sum (extract ((freqSEQ s),A)) )
proof end;

theorem Th16: :: DIST_2:16
for S being non empty finite set
for D being EqSampleSpaces of S
for s being Element of D holds freqSEQ s = (len s) (#) (FDprobSEQ s)
proof end;

theorem Th17: :: DIST_2:17
for S being non empty finite set
for D being EqSampleSpaces of S
for s, t being Element of D
for judgefunc being Function of S,BOOLEAN holds Prob (judgefunc,s) = Prob (judgefunc,t)
proof end;

definition
let S be non empty finite set ;
let D be EqSampleSpaces of S;
let judgefunc be Function of S,BOOLEAN;
func Prob (judgefunc,D) -> Real means :Def6: :: DIST_2:def 6
for s being Element of D holds it = Prob (judgefunc,s);
existence
ex b1 being Real st
for s being Element of D holds b1 = Prob (judgefunc,s)
proof end;
uniqueness
for b1, b2 being Real st ( for s being Element of D holds b1 = Prob (judgefunc,s) ) & ( for s being Element of D holds b2 = Prob (judgefunc,s) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Prob DIST_2:def 6 :
for S being non empty finite set
for D being EqSampleSpaces of S
for judgefunc being Function of S,BOOLEAN
for b4 being Real holds
( b4 = Prob (judgefunc,D) iff for s being Element of D holds b4 = Prob (judgefunc,s) );

theorem Th18: :: DIST_2:18
for S being non empty finite set
for s being Element of S *
for judgefunc being Function of S,BOOLEAN holds Coim ((judgefunc * s),TRUE) in bool (dom s)
proof end;

definition
let S be set ;
let SS be Subset of S;
func MembershipDecision SS -> Function of S,BOOLEAN equals :: DIST_2:def 7
chi (SS,S);
coherence
chi (SS,S) is Function of S,BOOLEAN
by MARGREL1:def 11;
end;

:: deftheorem defines MembershipDecision DIST_2:def 7 :
for S being set
for SS being Subset of S holds MembershipDecision SS = chi (SS,S);

theorem :: DIST_2:19
for S being non empty finite set
for BS being Subset of S ex judgefunc being Function of S,BOOLEAN st Coim (judgefunc,TRUE) = BS
proof end;

theorem :: DIST_2:20
for S being non empty finite set
for s being Element of S *
for f being Function of S,BOOLEAN
for F being SigmaField of (dom s) st F = bool (dom s) holds
Coim ((f * s),TRUE) is Event of F by Th18;

Lm2: for p, q being boolean-valued Function
for x being set st x in (dom p) /\ (dom q) holds
( (p 'or' q) . x = TRUE iff ( p . x = TRUE or q . x = TRUE ) )

proof end;

Lm3: for p, q being boolean-valued Function
for x being set st x in (dom p) /\ (dom q) holds
( (p '&' q) . x = TRUE iff ( p . x = TRUE & q . x = TRUE ) )

proof end;

Lm4: for p being boolean-valued Function
for x being set st x in dom p holds
( ('not' p) . x = TRUE iff p . x = FALSE )

proof end;

theorem Th21: :: DIST_2:21
for S being non empty finite set
for s being Element of S *
for f, g being Function of S,BOOLEAN holds Coim (((f 'or' g) * s),TRUE) = (Coim ((f * s),TRUE)) \/ (Coim ((g * s),TRUE))
proof end;

theorem Th22: :: DIST_2:22
for S being non empty finite set
for s being Element of S *
for f, g being Function of S,BOOLEAN holds Coim (((f '&' g) * s),TRUE) = (Coim ((f * s),TRUE)) /\ (Coim ((g * s),TRUE))
proof end;

theorem Th23: :: DIST_2:23
for S being non empty finite set
for s being Element of S *
for f being Function of S,BOOLEAN holds Coim ((('not' f) * s),TRUE) = (dom s) \ (Coim ((f * s),TRUE))
proof end;

theorem Th24: :: DIST_2:24
for S being non empty finite set
for D being EqSampleSpaces of S
for s being Element of D
for f, g being Function of S,BOOLEAN holds Prob ((f 'or' g),s) = (card ((trueEVENT (f * s)) \/ (trueEVENT (g * s)))) / (len s)
proof end;

theorem Th25: :: DIST_2:25
for S being non empty finite set
for D being EqSampleSpaces of S
for s being Element of D
for f, g being Function of S,BOOLEAN holds Prob ((f '&' g),s) = (card ((trueEVENT (f * s)) /\ (trueEVENT (g * s)))) / (len s)
proof end;

theorem Th26: :: DIST_2:26
for S being non empty finite set
for D being EqSampleSpaces of S
for s being Element of D
for f being Function of S,BOOLEAN holds Prob (('not' f),s) = 1 - (Prob (f,s))
proof end;

theorem Th27: :: DIST_2:27
for S being non empty finite set
for D being EqSampleSpaces of S
for f, g being Function of S,BOOLEAN holds Prob ((f 'or' g),D) = ((Prob (f,D)) + (Prob (g,D))) - (Prob ((f '&' g),D))
proof end;

theorem :: DIST_2:28
for S being non empty finite set
for D being EqSampleSpaces of S
for f being Function of S,BOOLEAN holds Prob (('not' f),D) = 1 - (Prob (f,D))
proof end;

theorem Th29: :: DIST_2:29
for S being non empty finite set
for D being EqSampleSpaces of S
for f being Function of S,BOOLEAN st f = chi (S,S) holds
Prob (f,D) = 1
proof end;

theorem Th30: :: DIST_2:30
for S being non empty finite set
for D being EqSampleSpaces of S
for f being Function of S,BOOLEAN holds 0 <= Prob (f,D)
proof end;

theorem Th31: :: DIST_2:31
for S being non empty finite set
for A, B being set
for f, g being Function of S,BOOLEAN st A c= S & B c= S & f = chi (A,S) & g = chi (B,S) holds
chi ((A \/ B),S) = f 'or' g
proof end;

theorem Th32: :: DIST_2:32
for S being non empty finite set
for D being EqSampleSpaces of S
for A, B being set
for f, g being Function of S,BOOLEAN st A c= S & B c= S & A misses B & f = chi (A,S) & g = chi (B,S) holds
Prob ((f '&' g),D) = 0
proof end;

definition
let S be non empty finite set ;
let D be EqSampleSpaces of S;
mode Probability of D -> Function of (Funcs (S,BOOLEAN)),REAL means :: DIST_2:def 8
for judgefunc being Element of Funcs (S,BOOLEAN) holds it . judgefunc = Prob (judgefunc,D);
existence
ex b1 being Function of (Funcs (S,BOOLEAN)),REAL st
for judgefunc being Element of Funcs (S,BOOLEAN) holds b1 . judgefunc = Prob (judgefunc,D)
proof end;
end;

:: deftheorem defines Probability DIST_2:def 8 :
for S being non empty finite set
for D being EqSampleSpaces of S
for b3 being Function of (Funcs (S,BOOLEAN)),REAL holds
( b3 is Probability of D iff for judgefunc being Element of Funcs (S,BOOLEAN) holds b3 . judgefunc = Prob (judgefunc,D) );

Lm5: for S being 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) )

proof end;

definition
let S be non empty finite set ;
let D be EqSampleSpaces of S;
func Trivial-Probability D -> Probability of Trivial-SigmaField S means :: DIST_2:def 9
for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & it . x = Prob (ch,D) );
existence
ex b1 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) & b1 . x = Prob (ch,D) )
by Lm5;
uniqueness
for b1, b2 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) & b1 . x = Prob (ch,D) ) ) & ( for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & b2 . x = Prob (ch,D) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines Trivial-Probability DIST_2:def 9 :
for S being non empty finite set
for D being EqSampleSpaces of S
for b3 being Probability of Trivial-SigmaField S holds
( b3 = Trivial-Probability D iff for x being set st x in Trivial-SigmaField S holds
ex ch being Function of S,BOOLEAN st
( ch = chi (x,S) & b3 . x = Prob (ch,D) ) );

definition
let S be non empty finite set ;
let D be EqSampleSpaces of S;
mode sample of D -> Element of S means :Def10: :: DIST_2:def 10
ex s being Element of D st it in rng s;
existence
ex b1 being Element of S ex s being Element of D st b1 in rng s
proof end;
end;

:: deftheorem Def10 defines sample DIST_2:def 10 :
for S being non empty finite set
for D being EqSampleSpaces of S
for b3 being Element of S holds
( b3 is sample of D iff ex s being Element of D st b3 in rng s );

definition
let S be non empty finite set ;
let D be EqSampleSpaces of S;
let x be sample of D;
func Prob x -> Real equals :: DIST_2:def 11
Prob ((MembershipDecision {x}),D);
coherence
Prob ((MembershipDecision {x}),D) is Real
;
end;

:: deftheorem defines Prob DIST_2:def 11 :
for S being non empty finite set
for D being EqSampleSpaces of S
for x being sample of D holds Prob x = Prob ((MembershipDecision {x}),D);

theorem :: DIST_2:33
for S being non empty finite set
for D being EqSampleSpaces of S
for x being sample of D holds Prob x = (ProbFinS_of D) . (index x)
proof end;

definition
let S be non empty finite set ;
let D be EqSampleSpaces of S;
mode samplingRNG of D -> non empty Subset of S means :Def12: :: DIST_2:def 12
ex x being sample of D st x in it;
existence
ex b1 being non empty Subset of S ex x being sample of D st x in b1
proof end;
end;

:: deftheorem Def12 defines samplingRNG DIST_2:def 12 :
for S being non empty finite set
for D being EqSampleSpaces of S
for b3 being non empty Subset of S holds
( b3 is samplingRNG of D iff ex x being sample of D st x in b3 );

definition
let S be non empty finite set ;
let D be EqSampleSpaces of S;
let X be samplingRNG of D;
func Prob X -> Real equals :: DIST_2:def 13
Prob ((MembershipDecision X),D);
coherence
Prob ((MembershipDecision X),D) is Real
;
end;

:: deftheorem defines Prob DIST_2:def 13 :
for S being non empty finite set
for D being EqSampleSpaces of S
for X being samplingRNG of D holds Prob X = Prob ((MembershipDecision X),D);

theorem Th34: :: DIST_2:34
for S being non empty finite set
for X being Subset of S
for s, t being FinSequence of S
for SD being Subset of (dom s)
for x being Subset of X st SD = s " X & t = extract (s,SD) holds
card (s " x) = card (t " x)
proof end;

theorem Th35: :: DIST_2:35
for S being non empty finite set
for X being Subset of S
for s, t being FinSequence of S
for SD being Subset of (dom s)
for x being set st SD = s " X & t = extract (s,SD) & x in X holds
frequency (x,s) = frequency (x,t)
proof end;

theorem Th36: :: DIST_2:36
for S being non empty finite set
for D being Element of distribution_family S
for s being FinSequence of S st s in D holds
D = Finseq-EQclass s
proof end;

theorem Th37: :: DIST_2:37
for S being non empty finite set
for X being Subset of S
for s being FinSequence of S holds s " X = trueEVENT ((MembershipDecision X) * s)
proof end;

theorem Th38: :: DIST_2:38
for S being non empty finite set
for X being non empty Subset of S
for D being EqSampleSpaces of S
for s1, s2 being Element of D
for t1, t2 being FinSequence of S
for SD1 being Subset of (dom s1)
for SD2 being Subset of (dom s2) st SD1 = s1 " X & t1 = extract (s1,SD1) & SD2 = s2 " X & t2 = extract (s2,SD2) holds
t1,t2 -are_prob_equivalent
proof end;

definition
let S be non empty finite set ;
let D be EqSampleSpaces of S;
let X be samplingRNG of D;
func ConditionalSS X -> EqSampleSpaces of S means :Def14: :: DIST_2:def 14
ex s being Element of D ex t being FinSequence of S ex SD being Subset of (dom s) st
( SD = s " X & t = extract (s,SD) & t in it );
existence
ex b1 being EqSampleSpaces of S ex s being Element of D ex t being FinSequence of S ex SD being Subset of (dom s) st
( SD = s " X & t = extract (s,SD) & t in b1 )
proof end;
uniqueness
for b1, b2 being EqSampleSpaces of S st ex s being Element of D ex t being FinSequence of S ex SD being Subset of (dom s) st
( SD = s " X & t = extract (s,SD) & t in b1 ) & ex s being Element of D ex t being FinSequence of S ex SD being Subset of (dom s) st
( SD = s " X & t = extract (s,SD) & t in b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines ConditionalSS DIST_2:def 14 :
for S being non empty finite set
for D being EqSampleSpaces of S
for X being samplingRNG of D
for b4 being EqSampleSpaces of S holds
( b4 = ConditionalSS X iff ex s being Element of D ex t being FinSequence of S ex SD being Subset of (dom s) st
( SD = s " X & t = extract (s,SD) & t in b4 ) );

definition
let S be non empty finite set ;
let D be EqSampleSpaces of S;
let X be samplingRNG of D;
let f be Function of S,BOOLEAN;
func Prob (f,X) -> Real equals :: DIST_2:def 15
Prob (f,(ConditionalSS X));
coherence
Prob (f,(ConditionalSS X)) is Real
;
end;

:: deftheorem defines Prob DIST_2:def 15 :
for S being non empty finite set
for D being EqSampleSpaces of S
for X being samplingRNG of D
for f being Function of S,BOOLEAN holds Prob (f,X) = Prob (f,(ConditionalSS X));

theorem :: DIST_2:39
for S being non empty finite set
for D being EqSampleSpaces of S
for X being samplingRNG of D
for f being Function of S,BOOLEAN holds (Prob (f,X)) * (Prob X) = Prob ((f '&' (MembershipDecision X)),D)
proof end;