DIST_2: Posterior Probability on Finite Set

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

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;

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 ;

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

end;

:: deftheorem defines index DIST_2:def 1 :

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 by Th7;

end;

:: deftheorem defines ProbFinS_of DIST_2:def 2 :

definition

let judgefunc be BOOLEAN -valued Function;

func trueEVENT judgefunc -> Event of (dom judgefunc) equals :: DIST_2:def 3
judgefunc " {TRUE};

proof end;

end;

:: deftheorem defines trueEVENT DIST_2:def 3 :

theorem Th8: :: DIST_2:8

for S being non empty finite set
for f being b₁ -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);

end;

:: deftheorem defines Prob DIST_2:def 4 :

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

proof end;

end;

:: deftheorem defines extract DIST_2:def 5 :

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 b₁ -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 b₁ -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);

proof end;

proof end;

end;

:: deftheorem Def6 defines Prob DIST_2:def 6 :

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 by MARGREL1:def 11;

end;

:: deftheorem defines MembershipDecision DIST_2:def 7 :

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

proof end;

end;

:: deftheorem defines Probability DIST_2:def 8 :

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 by Lm5;
uniqueness

proof end;

end;

:: deftheorem defines Trivial-Probability DIST_2:def 9 :

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;

proof end;

end;

:: deftheorem Def10 defines sample DIST_2:def 10 :

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

end;

:: deftheorem defines Prob DIST_2:def 11 :

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;

proof end;

end;

:: deftheorem Def12 defines samplingRNG DIST_2:def 12 :

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

end;

:: deftheorem defines Prob DIST_2:def 13 :

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

proof end;

proof end;

end;

:: deftheorem Def14 defines ConditionalSS DIST_2:def 14 :

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

end;

:: deftheorem defines Prob DIST_2:def 15 :

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;