:: by Hiroyuki Okazaki

::

:: Received May 5, 2009

:: Copyright (c) 2009-2021 Association of Mizar Users

notation
end;

definition

let S be set ;

let s be FinSequence of S;

let x be set ;

:: original: event_pick

redefine func event_pick (x,s) -> Event of (whole_event );

correctness

coherence

event_pick (,x) is Event of (whole_event );

by RELAT_1:132;

end;
let s be FinSequence of S;

let x be set ;

:: original: event_pick

redefine func event_pick (x,s) -> Event of (whole_event );

correctness

coherence

event_pick (,x) is Event of (whole_event );

by RELAT_1:132;

definition

let S be finite set ;

let s be FinSequence of S;

let x be set ;

correctness

coherence

card (event_pick (x,s)) is Nat;

;

end;
let s be FinSequence of S;

let x be set ;

correctness

coherence

card (event_pick (x,s)) is Nat;

;

:: deftheorem defines frequency DIST_1:def 1 :

for S being finite set

for s being FinSequence of S

for x being set holds frequency (x,s) = card (event_pick (x,s));

for S being finite set

for s being FinSequence of S

for x being set holds frequency (x,s) = card (event_pick (x,s));

::$CT

theorem :: DIST_1:2

for S being set

for s being FinSequence of S

for e being set st e in whole_event holds

ex x being Element of S st e in event_pick (x,s)

for s being FinSequence of S

for e being set st e in whole_event holds

ex x being Element of S st e in event_pick (x,s)

proof end;

definition

let S be finite set ;

let s be FinSequence of S;

let x be set ;

correctness

coherence

(frequency (x,s)) / (len s) is Real;

;

end;
let s be FinSequence of S;

let x be set ;

correctness

coherence

(frequency (x,s)) / (len s) is Real;

;

:: deftheorem defines FDprobability DIST_1:def 2 :

for S being finite set

for s being FinSequence of S

for x being set holds FDprobability (x,s) = (frequency (x,s)) / (len s);

for S being finite set

for s being FinSequence of S

for x being set holds FDprobability (x,s) = (frequency (x,s)) / (len s);

::$CT

theorem :: DIST_1:4

for S being finite set

for s being FinSequence of S

for x being set holds frequency (x,s) = (len s) * (FDprobability (x,s))

for s being FinSequence of S

for x being set holds frequency (x,s) = (len s) * (FDprobability (x,s))

proof end;

definition

let S be finite set ;

let s be FinSequence of S;

ex b_{1} being FinSequence of REAL st

( dom b_{1} = Seg (card S) & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = FDprobability (((canFS S) . n),s) ) )

for b_{1}, b_{2} being FinSequence of REAL st dom b_{1} = Seg (card S) & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = FDprobability (((canFS S) . n),s) ) & dom b_{2} = Seg (card S) & ( for n being Nat st n in dom b_{2} holds

b_{2} . n = FDprobability (((canFS S) . n),s) ) holds

b_{1} = b_{2}

end;
let s be FinSequence of S;

func FDprobSEQ s -> FinSequence of REAL means :Def3: :: DIST_1:def 3

( dom it = Seg (card S) & ( for n being Nat st n in dom it holds

it . n = FDprobability (((canFS S) . n),s) ) );

existence ( dom it = Seg (card S) & ( for n being Nat st n in dom it holds

it . n = FDprobability (((canFS S) . n),s) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines FDprobSEQ DIST_1:def 3 :

for S being finite set

for s being FinSequence of S

for b_{3} being FinSequence of REAL holds

( b_{3} = FDprobSEQ s iff ( dom b_{3} = Seg (card S) & ( for n being Nat st n in dom b_{3} holds

b_{3} . n = FDprobability (((canFS S) . n),s) ) ) );

for S being finite set

for s being FinSequence of S

for b

( b

b

theorem :: DIST_1:5

for S being finite set

for s being FinSequence of S

for x being set holds FDprobability (x,s) = prob (event_pick (x,s)) by CARD_1:62;

for s being FinSequence of S

for x being set holds FDprobability (x,s) = prob (event_pick (x,s)) by CARD_1:62;

definition

let S be finite set ;

let s, t be FinSequence of S;

for s being FinSequence of S

for x being set holds FDprobability (x,s) = FDprobability (x,s) ;

symmetry

for s, t being FinSequence of S st ( for x being set holds FDprobability (x,s) = FDprobability (x,t) ) holds

for x being set holds FDprobability (x,t) = FDprobability (x,s) ;

end;
let s, t be FinSequence of S;

pred s,t -are_prob_equivalent means :: DIST_1:def 4

for x being set holds FDprobability (x,s) = FDprobability (x,t);

reflexivity for x being set holds FDprobability (x,s) = FDprobability (x,t);

for s being FinSequence of S

for x being set holds FDprobability (x,s) = FDprobability (x,s) ;

symmetry

for s, t being FinSequence of S st ( for x being set holds FDprobability (x,s) = FDprobability (x,t) ) holds

for x being set holds FDprobability (x,t) = FDprobability (x,s) ;

:: deftheorem defines -are_prob_equivalent DIST_1:def 4 :

for S being finite set

for s, t being FinSequence of S holds

( s,t -are_prob_equivalent iff for x being set holds FDprobability (x,s) = FDprobability (x,t) );

for S being finite set

for s, t being FinSequence of S holds

( s,t -are_prob_equivalent iff for x being set holds FDprobability (x,s) = FDprobability (x,t) );

theorem Th4: :: DIST_1:6

for S being finite set

for s, t, u being FinSequence of S st s,t -are_prob_equivalent & t,u -are_prob_equivalent holds

s,u -are_prob_equivalent

for s, t, u being FinSequence of S st s,t -are_prob_equivalent & t,u -are_prob_equivalent holds

s,u -are_prob_equivalent

proof end;

definition

let S be finite set ;

let s be FinSequence of S;

coherence

{ t where t is FinSequence of S : s,t -are_prob_equivalent } is Subset of (S *);

end;
let s be FinSequence of S;

func Finseq-EQclass s -> Subset of (S *) equals :: DIST_1:def 5

{ t where t is FinSequence of S : s,t -are_prob_equivalent } ;

correctness { t where t is FinSequence of S : s,t -are_prob_equivalent } ;

coherence

{ t where t is FinSequence of S : s,t -are_prob_equivalent } is Subset of (S *);

proof end;

:: deftheorem defines Finseq-EQclass DIST_1:def 5 :

for S being finite set

for s being FinSequence of S holds Finseq-EQclass s = { t where t is FinSequence of S : s,t -are_prob_equivalent } ;

for S being finite set

for s being FinSequence of S holds Finseq-EQclass s = { t where t is FinSequence of S : s,t -are_prob_equivalent } ;

registration
end;

theorem Th5: :: DIST_1:7

for S being finite set

for s, t being FinSequence of S holds

( s,t -are_prob_equivalent iff t in Finseq-EQclass s )

for s, t being FinSequence of S holds

( s,t -are_prob_equivalent iff t in Finseq-EQclass s )

proof end;

theorem Th7: :: DIST_1:9

for S being finite set

for s, t being FinSequence of S holds

( s,t -are_prob_equivalent iff Finseq-EQclass s = Finseq-EQclass t )

for s, t being FinSequence of S holds

( s,t -are_prob_equivalent iff Finseq-EQclass s = Finseq-EQclass t )

proof end;

definition

let S be finite set ;

defpred S_{1}[ set ] means ex u being FinSequence of S st $1 = Finseq-EQclass u;

ex b_{1} being Subset-Family of (S *) st

for A being Subset of (S *) holds

( A in b_{1} iff ex s being FinSequence of S st A = Finseq-EQclass s )

for b_{1}, b_{2} being Subset-Family of (S *) st ( for A being Subset of (S *) holds

( A in b_{1} iff ex s being FinSequence of S st A = Finseq-EQclass s ) ) & ( for A being Subset of (S *) holds

( A in b_{2} iff ex s being FinSequence of S st A = Finseq-EQclass s ) ) holds

b_{1} = b_{2}

end;
defpred S

func distribution_family S -> Subset-Family of (S *) means :Def6: :: DIST_1:def 6

for A being Subset of (S *) holds

( A in it iff ex s being FinSequence of S st A = Finseq-EQclass s );

existence for A being Subset of (S *) holds

( A in it iff ex s being FinSequence of S st A = Finseq-EQclass s );

ex b

for A being Subset of (S *) holds

( A in b

proof end;

uniqueness for b

( A in b

( A in b

b

proof end;

:: deftheorem Def6 defines distribution_family DIST_1:def 6 :

for S being finite set

for b_{2} being Subset-Family of (S *) holds

( b_{2} = distribution_family S iff for A being Subset of (S *) holds

( A in b_{2} iff ex s being FinSequence of S st A = Finseq-EQclass s ) );

for S being finite set

for b

( b

( A in b

theorem Th8: :: DIST_1:10

for S being finite set

for s, t being FinSequence of S holds

( s,t -are_prob_equivalent iff FDprobSEQ s = FDprobSEQ t )

for s, t being FinSequence of S holds

( s,t -are_prob_equivalent iff FDprobSEQ s = FDprobSEQ t )

proof end;

theorem :: DIST_1:11

for S being finite set

for s, t being FinSequence of S st t in Finseq-EQclass s holds

FDprobSEQ s = FDprobSEQ t

for s, t being FinSequence of S st t in Finseq-EQclass s holds

FDprobSEQ s = FDprobSEQ t

proof end;

definition

let S be finite set ;

ex b_{1} being Function of (distribution_family S),(REAL *) st

for x being Element of distribution_family S ex s being FinSequence of S st

( s in x & b_{1} . x = FDprobSEQ s )

for b_{1}, b_{2} being Function of (distribution_family S),(REAL *) st ( for x being Element of distribution_family S ex s being FinSequence of S st

( s in x & b_{1} . x = FDprobSEQ s ) ) & ( for x being Element of distribution_family S ex s being FinSequence of S st

( s in x & b_{2} . x = FDprobSEQ s ) ) holds

b_{1} = b_{2}

end;
func GenProbSEQ S -> Function of (distribution_family S),(REAL *) means :Def7: :: DIST_1:def 7

for x being Element of distribution_family S ex s being FinSequence of S st

( s in x & it . x = FDprobSEQ s );

existence for x being Element of distribution_family S ex s being FinSequence of S st

( s in x & it . x = FDprobSEQ s );

ex b

for x being Element of distribution_family S ex s being FinSequence of S st

( s in x & b

proof end;

uniqueness for b

( s in x & b

( s in x & b

b

proof end;

:: deftheorem Def7 defines GenProbSEQ DIST_1:def 7 :

for S being finite set

for b_{2} being Function of (distribution_family S),(REAL *) holds

( b_{2} = GenProbSEQ S iff for x being Element of distribution_family S ex s being FinSequence of S st

( s in x & b_{2} . x = FDprobSEQ s ) );

for S being finite set

for b

( b

( s in x & b

theorem Th10: :: DIST_1:12

for S being finite set

for s being FinSequence of S holds (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ s

for s being FinSequence of S holds (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ s

proof end;

definition

let S be finite set ;

let p be ProbFinS FinSequence of REAL ;

assume A1: ex s being FinSequence of S st FDprobSEQ s = p ;

ex b_{1} being Element of distribution_family S st (GenProbSEQ S) . b_{1} = p

for b_{1}, b_{2} being Element of distribution_family S st (GenProbSEQ S) . b_{1} = p & (GenProbSEQ S) . b_{2} = p holds

b_{1} = b_{2}

end;
let p be ProbFinS FinSequence of REAL ;

assume A1: ex s being FinSequence of S st FDprobSEQ s = p ;

func distribution (p,S) -> Element of distribution_family S means :Def8: :: DIST_1:def 8

(GenProbSEQ S) . it = p;

existence (GenProbSEQ S) . it = p;

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines distribution DIST_1:def 8 :

for S being finite set

for p being ProbFinS FinSequence of REAL st ex s being FinSequence of S st FDprobSEQ s = p holds

for b_{3} being Element of distribution_family S holds

( b_{3} = distribution (p,S) iff (GenProbSEQ S) . b_{3} = p );

for S being finite set

for p being ProbFinS FinSequence of REAL st ex s being FinSequence of S st FDprobSEQ s = p holds

for b

( b

definition

let S be finite set ;

let s be FinSequence of S;

ex b_{1} being FinSequence of NAT st

( dom b_{1} = Seg (card S) & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = (len s) * ((FDprobSEQ s) . n) ) )

for b_{1}, b_{2} being FinSequence of NAT st dom b_{1} = Seg (card S) & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = (len s) * ((FDprobSEQ s) . n) ) & dom b_{2} = Seg (card S) & ( for n being Nat st n in dom b_{2} holds

b_{2} . n = (len s) * ((FDprobSEQ s) . n) ) holds

b_{1} = b_{2}

end;
let s be FinSequence of S;

func freqSEQ s -> FinSequence of NAT means :Def9: :: DIST_1:def 9

( dom it = Seg (card S) & ( for n being Nat st n in dom it holds

it . n = (len s) * ((FDprobSEQ s) . n) ) );

existence ( dom it = Seg (card S) & ( for n being Nat st n in dom it holds

it . n = (len s) * ((FDprobSEQ s) . n) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines freqSEQ DIST_1:def 9 :

for S being finite set

for s being FinSequence of S

for b_{3} being FinSequence of NAT holds

( b_{3} = freqSEQ s iff ( dom b_{3} = Seg (card S) & ( for n being Nat st n in dom b_{3} holds

b_{3} . n = (len s) * ((FDprobSEQ s) . n) ) ) );

for S being finite set

for s being FinSequence of S

for b

( b

b

theorem Th11: :: DIST_1:13

for S being non empty finite set

for s being non empty FinSequence of S

for n being Nat st n in Seg (card S) holds

ex x being Element of S st

( (freqSEQ s) . n = frequency (x,s) & x = (canFS S) . n )

for s being non empty FinSequence of S

for n being Nat st n in Seg (card S) holds

ex x being Element of S st

( (freqSEQ s) . n = frequency (x,s) & x = (canFS S) . n )

proof end;

theorem Th13: :: DIST_1:15

for S being finite set

for s being FinSequence of S holds Sum (freqSEQ s) = (len s) * (Sum (FDprobSEQ s))

for s being FinSequence of S holds Sum (freqSEQ s) = (len s) * (Sum (FDprobSEQ s))

proof end;

theorem :: DIST_1:16

for S being non empty finite set

for s being non empty FinSequence of S

for n being Nat st n in dom s holds

ex m being Nat st

( (freqSEQ s) . m = frequency ((s . n),s) & s . n = (canFS S) . m )

for s being non empty FinSequence of S

for n being Nat st n in dom s holds

ex m being Nat st

( (freqSEQ s) . m = frequency ((s . n),s) & s . n = (canFS S) . m )

proof end;

Lm1: for S being Function

for X being set st S is disjoint_valued holds

S | X is disjoint_valued

proof end;

Lm2: for n being Nat

for S being Function

for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & n = len L & ( for i being Nat st i in dom S holds

( S . i is finite & L . i = card (S . i) ) ) holds

( Union S is finite & card (Union S) = Sum L )

proof end;

theorem Th15: :: DIST_1:17

for S being Function

for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & ( for i being Nat st i in dom S holds

( S . i is finite & L . i = card (S . i) ) ) holds

( Union S is finite & card (Union S) = Sum L )

for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & ( for i being Nat st i in dom S holds

( S . i is finite & L . i = card (S . i) ) ) holds

( Union S is finite & card (Union S) = Sum L )

proof end;

theorem Th16: :: DIST_1:18

for S being non empty finite set

for s being non empty FinSequence of S holds Sum (freqSEQ s) = len s

for s being non empty FinSequence of S holds Sum (freqSEQ s) = len s

proof end;

registration

let S be non empty finite set ;

let s be non empty FinSequence of S;

coherence

FDprobSEQ s is ProbFinS

end;
let s be non empty FinSequence of S;

coherence

FDprobSEQ s is ProbFinS

proof end;

definition

let S be non empty finite set ;

ex b_{1} being ProbFinS FinSequence of REAL st

( len b_{1} = card S & ex s being FinSequence of S st FDprobSEQ s = b_{1} )

end;
mode distProbFinS of S -> ProbFinS FinSequence of REAL means :Def10: :: DIST_1:def 10

( len it = card S & ex s being FinSequence of S st FDprobSEQ s = it );

existence ( len it = card S & ex s being FinSequence of S st FDprobSEQ s = it );

ex b

( len b

proof end;

:: deftheorem Def10 defines distProbFinS DIST_1:def 10 :

for S being non empty finite set

for b_{2} being ProbFinS FinSequence of REAL holds

( b_{2} is distProbFinS of S iff ( len b_{2} = card S & ex s being FinSequence of S st FDprobSEQ s = b_{2} ) );

for S being non empty finite set

for b

( b

theorem Th18: :: DIST_1:20

for S being non empty finite set

for p being distProbFinS of S holds

( distribution (p,S) is Element of distribution_family S & (GenProbSEQ S) . (distribution (p,S)) = p )

for p being distProbFinS of S holds

( distribution (p,S) is Element of distribution_family S & (GenProbSEQ S) . (distribution (p,S)) = p )

proof end;

:: deftheorem defines uniformly_distributed DIST_1:def 11 :

for S being finite set

for s being FinSequence of S holds

( s is uniformly_distributed iff for n being Nat st n in dom (FDprobSEQ s) holds

(FDprobSEQ s) . n = 1 / (card S) );

for S being finite set

for s being FinSequence of S holds

( s is uniformly_distributed iff for n being Nat st n in dom (FDprobSEQ s) holds

(FDprobSEQ s) . n = 1 / (card S) );

theorem Th19: :: DIST_1:21

for S being finite set

for s being FinSequence of S st s is uniformly_distributed holds

FDprobSEQ s is constant

for s being FinSequence of S st s is uniformly_distributed holds

FDprobSEQ s is constant

proof end;

theorem Th20: :: DIST_1:22

for S being finite set

for s, t being FinSequence of S st s is uniformly_distributed & s,t -are_prob_equivalent holds

t is uniformly_distributed

for s, t being FinSequence of S st s is uniformly_distributed & s,t -are_prob_equivalent holds

t is uniformly_distributed

proof end;

theorem Th21: :: DIST_1:23

for S being finite set

for s, t being FinSequence of S st s is uniformly_distributed & t is uniformly_distributed holds

s,t -are_prob_equivalent

for s, t being FinSequence of S st s is uniformly_distributed & t is uniformly_distributed holds

s,t -are_prob_equivalent

proof end;

registration

let S be finite set ;

coherence

for b_{1} being FinSequence of S st b_{1} = canFS S holds

b_{1} is uniformly_distributed

end;
coherence

for b

b

proof end;

Lm3: for S being finite set

for s being FinSequence of S st s in Finseq-EQclass (canFS S) holds

s is uniformly_distributed

by Th5, Th20;

Lm4: for S being finite set

for s being FinSequence of S st s is uniformly_distributed holds

for t being FinSequence of S st t is uniformly_distributed holds

t in Finseq-EQclass s

proof end;

definition

let S be finite set ;

ex b_{1} being Element of distribution_family S st

for s being FinSequence of S holds

( s in b_{1} iff s is uniformly_distributed )

for b_{1}, b_{2} being Element of distribution_family S st ( for s being FinSequence of S holds

( s in b_{1} iff s is uniformly_distributed ) ) & ( for s being FinSequence of S holds

( s in b_{2} iff s is uniformly_distributed ) ) holds

b_{1} = b_{2}

end;
func uniform_distribution S -> Element of distribution_family S means :Def12: :: DIST_1:def 12

for s being FinSequence of S holds

( s in it iff s is uniformly_distributed );

existence for s being FinSequence of S holds

( s in it iff s is uniformly_distributed );

ex b

for s being FinSequence of S holds

( s in b

proof end;

uniqueness for b

( s in b

( s in b

b

proof end;

:: deftheorem Def12 defines uniform_distribution DIST_1:def 12 :

for S being finite set

for b_{2} being Element of distribution_family S holds

( b_{2} = uniform_distribution S iff for s being FinSequence of S holds

( s in b_{2} iff s is uniformly_distributed ) );

for S being finite set

for b

( b

( s in b

registration

let S be non empty finite set ;

ex b_{1} being distProbFinS of S st b_{1} is constant

end;
cluster Relation-like NAT -defined REAL -valued non empty Function-like constant finite V47() V48() V49() FinSequence-like FinSubsequence-like V77() ProbFinS for distProbFinS of S;

existence ex b

proof end;

definition
end;

:: deftheorem defines Uniform_FDprobSEQ DIST_1:def 13 :

for S being non empty finite set holds Uniform_FDprobSEQ S = FDprobSEQ (canFS S);

for S being non empty finite set holds Uniform_FDprobSEQ S = FDprobSEQ (canFS S);

registration
end;

theorem :: DIST_1:24

for S being non empty finite set holds uniform_distribution S = distribution ((Uniform_FDprobSEQ S),S)

proof end;