:: Probability on Finite and Discrete Set and Uniform Distribution
:: by Hiroyuki Okazaki
::
:: Received May 5, 2009
:: Copyright (c) 2009 Association of Mizar Users
theorem Th1: :: DIST_1:1
:: deftheorem defines frequency DIST_1:def 1 :
theorem :: DIST_1:2
theorem Th3: :: DIST_1:3
:: deftheorem defines FDprobability DIST_1:def 2 :
theorem :: DIST_1:4
:: deftheorem Def3 defines FDprobSEQ DIST_1:def 3 :
theorem :: DIST_1:5
definition
let S be non
empty finite set ;
let s,
t be
FinSequence of
S;
pred s,
t -are_prob_equivalent means :
Def4:
:: DIST_1:def 4
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: :: DIST_1:6
:: deftheorem defines Finseq-EQclass DIST_1:def 5 :
theorem Th7: :: DIST_1:7
theorem Th8: :: DIST_1:8
theorem Th9: :: DIST_1:9
:: deftheorem Def6 defines distribution_family DIST_1:def 6 :
theorem Th10: :: DIST_1:10
theorem :: DIST_1:11
:: deftheorem Def7 defines GenProbSEQ DIST_1:def 7 :
theorem Th12: :: DIST_1:12
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: :: DIST_1:13
theorem Th14: :: DIST_1:14
theorem Th15: :: DIST_1:15
theorem :: DIST_1:16
theorem Th17: :: DIST_1:17
theorem Th18: :: DIST_1:18
theorem Th19: :: DIST_1:19
theorem Th20: :: DIST_1:20
theorem Th21: :: DIST_1:21
:: deftheorem Def10 defines distProbFinS DIST_1:def 10 :
theorem Th22: :: DIST_1:22
:: deftheorem Def11 defines is_uniformly_distributed DIST_1:def 11 :
theorem Th23: :: DIST_1:23
theorem Th24: :: DIST_1:24
theorem Th25: :: DIST_1:25
theorem Th26: :: DIST_1:26
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 :: DIST_1:27