begin
theorem Th1:
:: deftheorem defines frequency DIST_1:def 1 :
for S being non empty finite set
for s being FinSequence of S
for x being set holds frequency (x,s) = card (event_pick (x,s));
theorem
theorem Th3:
:: deftheorem defines FDprobability DIST_1:def 2 :
for S being non empty finite set
for s being FinSequence of S
for x being set holds FDprobability (x,s) = (frequency (x,s)) / (len s);
theorem
:: deftheorem Def3 defines FDprobSEQ DIST_1:def 3 :
for S being non empty finite set
for s being FinSequence of S
for b3 being FinSequence of REAL holds
( b3 = FDprobSEQ s iff ( dom b3 = Seg (card S) & ( for n being Nat st n in dom b3 holds
b3 . n = FDprobability (((canFS S) . n),s) ) ) );
theorem
definition
let S be non
empty finite set ;
let s,
t be
FinSequence of
S;
pred s,
t -are_prob_equivalent means :
Def4:
for
x being
set holds
FDprobability (
x,
s)
= FDprobability (
x,
t);
reflexivity
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;
:: deftheorem Def4 defines -are_prob_equivalent DIST_1:def 4 :
for S being non empty 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 Th6:
:: deftheorem defines Finseq-EQclass DIST_1:def 5 :
for S being non empty finite set
for s being FinSequence of S holds Finseq-EQclass s = { t where t is FinSequence of S : s,t -are_prob_equivalent } ;
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem Def6 defines distribution_family DIST_1:def 6 :
for S being non empty finite set
for b2 being non empty Subset-Family of (S *) holds
( b2 = distribution_family S iff for A being Subset of (S *) holds
( A in b2 iff ex s being FinSequence of S st A = Finseq-EQclass s ) );
theorem Th10:
theorem
:: deftheorem Def7 defines GenProbSEQ DIST_1:def 7 :
for S being non empty finite set
for b2 being Function of (distribution_family S),(REAL *) holds
( b2 = GenProbSEQ S iff for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & b2 . x = FDprobSEQ s ) );
theorem Th12:
Lm1:
for S being non empty finite set holds GenProbSEQ S is one-to-one
:: deftheorem Def8 defines distribution DIST_1:def 8 :
for S being non empty finite set
for p being ProbFinS FinSequence of REAL st ex s being FinSequence of S st FDprobSEQ s = p holds
for b3 being Element of distribution_family S holds
( b3 = distribution (p,S) iff (GenProbSEQ S) . b3 = p );
:: deftheorem Def9 defines freqSEQ DIST_1:def 9 :
for S being non empty finite set
for s being FinSequence of S
for b3 being FinSequence of NAT holds
( b3 = freqSEQ s iff ( dom b3 = Seg (card S) & ( for n being Nat st n in dom b3 holds
b3 . n = (len s) * ((FDprobSEQ s) . n) ) ) );
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
:: deftheorem Def10 defines distProbFinS DIST_1:def 10 :
for S being non empty finite set
for b2 being ProbFinS FinSequence of REAL holds
( b2 is distProbFinS of S iff ( len b2 = card S & ex s being FinSequence of S st FDprobSEQ s = b2 ) );
theorem Th22:
begin
:: deftheorem Def11 defines is_uniformly_distributed DIST_1:def 11 :
for S being non empty 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 Th23:
theorem Th24:
theorem Th25:
theorem Th26:
Lm2:
for S being non empty finite set
for s being FinSequence of S st s in Finseq-EQclass (canFS S) holds
s is_uniformly_distributed
Lm3:
for S being non empty 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
:: deftheorem Def12 defines uniform_distribution DIST_1:def 12 :
for S being non empty finite set
for b2 being Element of distribution_family S holds
( b2 = uniform_distribution S iff for s being FinSequence of S holds
( s in b2 iff s is_uniformly_distributed ) );
:: deftheorem defines Uniform_FDprobSEQ DIST_1:def 13 :
for S being non empty finite set holds Uniform_FDprobSEQ S = FDprobSEQ (canFS S);
theorem