begin
theorem Th1:
:: deftheorem defines frequency DIST_1:def 1 :
theorem
theorem Th3:
:: deftheorem defines FDprobability DIST_1:def 2 :
theorem
:: deftheorem Def3 defines FDprobSEQ DIST_1:def 3 :
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 :
theorem Th6:
:: deftheorem defines Finseq-EQclass DIST_1:def 5 :
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem Def6 defines distribution_family DIST_1:def 6 :
theorem Th10:
theorem
:: deftheorem Def7 defines GenProbSEQ DIST_1:def 7 :
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 :
:: deftheorem Def9 defines freqSEQ DIST_1:def 9 :
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 :
theorem Th22:
begin
:: deftheorem Def11 defines is_uniformly_distributed DIST_1:def 11 :
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 :
:: deftheorem defines Uniform_FDprobSEQ DIST_1:def 13 :
theorem