:: Probability on Finite and Discrete Set and Uniform Distribution
:: by Hiroyuki Okazaki
::
:: Received May 5, 2009
:: Copyright (c) 2009 Association of Mizar Users
theorem defwe: :: DIST_1:1
:: deftheorem defines frequency DIST_1:def 1 :
theorem :: DIST_1:2
theorem nazo6: :: DIST_1:3
:: deftheorem defines FDprobability DIST_1:def 2 :
theorem :: DIST_1:4
:: deftheorem defFREQDIST 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 :
defequiv:
:: 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 defequiv defines -are_prob_equivalent DIST_1:def 4 :
theorem EQX01: :: DIST_1:6
:: deftheorem defines Finseq-EQclass DIST_1:def 5 :
theorem EQX02: :: DIST_1:7
theorem EQX03: :: DIST_1:8
theorem EQX04: :: DIST_1:9
:: deftheorem defQuot defines distribution_family DIST_1:def 6 :
theorem EQX05: :: DIST_1:10
theorem :: DIST_1:11
:: deftheorem defFREQDIST2 defines GenProbSEQ DIST_1:def 7 :
theorem EQX07: :: DIST_1:12
EQX08:
for S being non empty finite set holds GenProbSEQ S is one-to-one
:: deftheorem defBUNBPU defines distribution DIST_1:def 8 :
:: deftheorem defDIST defines freqSEQ DIST_1:def 9 :
theorem nazonazo: :: DIST_1:13
theorem nnnazo1: :: DIST_1:14
theorem nnazo2: :: DIST_1:15
theorem :: DIST_1:16
theorem LMCARD1: :: DIST_1:17
theorem LMCARD: :: DIST_1:18
theorem DISTSUM: :: DIST_1:19
theorem FREQDISTSUM: :: DIST_1:20
theorem FREQDISTSUM2: :: DIST_1:21
:: deftheorem defdistProbFinS defines distProbFinS DIST_1:def 10 :
theorem pbf: :: DIST_1:22
:: deftheorem defunidistseq defines is_uniformly_distributed DIST_1:def 11 :
theorem THUDEQ0: :: DIST_1:23
theorem THUDEQ: :: DIST_1:24
theorem THUDEQ2: :: DIST_1:25
theorem THUDS: :: DIST_1:26
THCFS:
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
THCFS2:
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 defunidist defines uniform_distribution DIST_1:def 12 :
:: deftheorem defines Uniform_FDprobSEQ DIST_1:def 13 :
theorem :: DIST_1:27