:: by Hiroyuki Okazaki

::

:: Received July 4, 2012

:: Copyright (c) 2012-2016 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*>

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

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

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 ;

coherence

for b_{1} being Element of distribution_family S holds not b_{1} is empty
by Lm1;

end;
coherence

for b

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 b_{1} being Element of D holds b_{1} is FinSequence of S

end;
let D be Element of distribution_family S;

:: original: Element

redefine mode Element of D -> FinSequence of S;

coherence

for b

proof 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

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;
let D be Element of distribution_family S;

synonym well-distributed D for with_non-empty_elements ;

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 )

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 ;

existence

ex b_{1} being Element of distribution_family S st b_{1} is well-distributed

end;
existence

ex b

proof 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)} )

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;
mode EqSampleSpaces of S is well-distributed Element of distribution_family S;

registration
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

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;

correctness

coherence

a .. (canFS S) is Element of NAT ;

;

end;
let a be Element of S;

correctness

coherence

a .. (canFS S) is Element of NAT ;

;

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

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;

correctness

coherence

(GenProbSEQ S) . D is distProbFinS of S;

by Th7;

end;
let D be EqSampleSpaces of S;

correctness

coherence

(GenProbSEQ S) . D is distProbFinS of S;

by Th7;

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

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;

coherence

judgefunc " {TRUE} is Event of (dom judgefunc)

end;
coherence

judgefunc " {TRUE} is Event of (dom judgefunc)

proof end;

:: deftheorem defines trueEVENT DIST_2:def 3 :

for judgefunc being BOOLEAN -valued Function holds trueEVENT judgefunc = judgefunc " {TRUE};

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 b_{1} -valued Function

for judgefunc being Function of S,BOOLEAN holds trueEVENT (judgefunc * f) is Event of (dom f)

for f being b

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;

correctness

coherence

(card (trueEVENT (judgefunc * s))) / (len s) is Real;

;

end;
let D be EqSampleSpaces of S;

let s be Element of D;

let judgefunc be Function of S,BOOLEAN;

correctness

coherence

(card (trueEVENT (judgefunc * s))) / (len s) is Real;

;

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

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

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)

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

coherence

s * (canFS A) is FinSequence of S

end;
let s be FinSequence of S;

let A be Subset of (dom s);

coherence

s * (canFS A) is FinSequence of S

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

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

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

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_{1} -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 )

for f being b

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_{1} -valued Function

for judgefunc being Function of S,BOOLEAN holds trueEVENT (judgefunc * f) = f " (trueEVENT judgefunc)

for f being b

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

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)

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)

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;

ex b_{1} being Real st

for s being Element of D holds b_{1} = Prob (judgefunc,s)

for b_{1}, b_{2} being Real st ( for s being Element of D holds b_{1} = Prob (judgefunc,s) ) & ( for s being Element of D holds b_{2} = Prob (judgefunc,s) ) holds

b_{1} = b_{2}

end;
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 for s being Element of D holds it = Prob (judgefunc,s);

ex b

for s being Element of D holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being Real holds

( b_{4} = Prob (judgefunc,D) iff for s being Element of D holds b_{4} = Prob (judgefunc,s) );

for S being non empty finite set

for D being EqSampleSpaces of S

for judgefunc being Function of S,BOOLEAN

for b

( b

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)

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;

coherence

chi (SS,S) is Function of S,BOOLEAN by MARGREL1:def 11;

end;
let SS be Subset of S;

coherence

chi (SS,S) is Function of S,BOOLEAN by MARGREL1:def 11;

:: deftheorem defines MembershipDecision DIST_2:def 7 :

for S being set

for SS being Subset of S holds MembershipDecision SS = chi (SS,S);

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

for BS being Subset of S ex judgefunc being Function of S,BOOLEAN st Coim (judgefunc,TRUE) = BS

proof end;

theorem :: DIST_2:20

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

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

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

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)

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)

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

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

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

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

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)

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

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

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;

ex b_{1} being Function of (Funcs (S,BOOLEAN)),REAL st

for judgefunc being Element of Funcs (S,BOOLEAN) holds b_{1} . judgefunc = Prob (judgefunc,D)

end;
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 for judgefunc being Element of Funcs (S,BOOLEAN) holds it . judgefunc = Prob (judgefunc,D);

ex b

for judgefunc being Element of Funcs (S,BOOLEAN) holds b

proof end;

:: deftheorem defines Probability DIST_2:def 8 :

for S being non empty finite set

for D being EqSampleSpaces of S

for b_{3} being Function of (Funcs (S,BOOLEAN)),REAL holds

( b_{3} is Probability of D iff for judgefunc being Element of Funcs (S,BOOLEAN) holds b_{3} . judgefunc = Prob (judgefunc,D) );

for S being non empty finite set

for D being EqSampleSpaces of S

for b

( b

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;

ex b_{1} 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) & b_{1} . x = Prob (ch,D) )
by Lm5;

uniqueness

for b_{1}, b_{2} 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) & b_{1} . 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) & b_{2} . x = Prob (ch,D) ) ) holds

b_{1} = b_{2}

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

ex b

for x being set st x in Trivial-SigmaField S holds

ex ch being Function of S,BOOLEAN st

( ch = chi (x,S) & b

uniqueness

for b

ex ch being Function of S,BOOLEAN st

( ch = chi (x,S) & b

ex ch being Function of S,BOOLEAN st

( ch = chi (x,S) & b

b

proof end;

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

for S being non empty finite set

for D being EqSampleSpaces of S

for b_{3} being Probability of Trivial-SigmaField S holds

( b_{3} = 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) & b_{3} . x = Prob (ch,D) ) );

for S being non empty finite set

for D being EqSampleSpaces of S

for b

( b

ex ch being Function of S,BOOLEAN st

( ch = chi (x,S) & b

definition

let S be non empty finite set ;

let D be EqSampleSpaces of S;

ex b_{1} being Element of S ex s being Element of D st b_{1} in rng s

end;
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 s being Element of D st it in rng s;

ex b

proof end;

:: deftheorem Def10 defines sample DIST_2:def 10 :

for S being non empty finite set

for D being EqSampleSpaces of S

for b_{3} being Element of S holds

( b_{3} is sample of D iff ex s being Element of D st b_{3} in rng s );

for S being non empty finite set

for D being EqSampleSpaces of S

for b

( b

definition

let S be non empty finite set ;

let D be EqSampleSpaces of S;

let x be sample of D;

coherence

Prob ((MembershipDecision {x}),D) is Real ;

end;
let D be EqSampleSpaces of S;

let x be sample of D;

coherence

Prob ((MembershipDecision {x}),D) is Real ;

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

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)

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;

ex b_{1} being non empty Subset of S ex x being sample of D st x in b_{1}

end;
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 x being sample of D st x in it;

ex b

proof end;

:: deftheorem Def12 defines samplingRNG DIST_2:def 12 :

for S being non empty finite set

for D being EqSampleSpaces of S

for b_{3} being non empty Subset of S holds

( b_{3} is samplingRNG of D iff ex x being sample of D st x in b_{3} );

for S being non empty finite set

for D being EqSampleSpaces of S

for b

( b

definition

let S be non empty finite set ;

let D be EqSampleSpaces of S;

let X be samplingRNG of D;

coherence

Prob ((MembershipDecision X),D) is Real ;

end;
let D be EqSampleSpaces of S;

let X be samplingRNG of D;

coherence

Prob ((MembershipDecision X),D) is Real ;

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

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)

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)

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

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)

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

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;

ex b_{1} 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 b_{1} )

for b_{1}, b_{2} 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 b_{1} ) & 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 b_{2} ) holds

b_{1} = b_{2}

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

ex b

( SD = s " X & t = extract (s,SD) & t in b

proof end;

uniqueness for b

( SD = s " X & t = extract (s,SD) & t in b

( SD = s " X & t = extract (s,SD) & t in b

b

proof 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 b_{4} being EqSampleSpaces of S holds

( b_{4} = 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 b_{4} ) );

for S being non empty finite set

for D being EqSampleSpaces of S

for X being samplingRNG of D

for b

( b

( SD = s " X & t = extract (s,SD) & t in b

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;

coherence

Prob (f,(ConditionalSS X)) is Real ;

end;
let D be EqSampleSpaces of S;

let X be samplingRNG of D;

let f be Function of S,BOOLEAN;

coherence

Prob (f,(ConditionalSS X)) is Real ;

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

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)

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;