:: Probability on Finite and Discrete Set and Uniform Distribution
:: by Hiroyuki Okazaki
::
:: Received May 5, 2009
:: Copyright (c) 2009 Association of Mizar Users
environ
vocabularies DIST_1, FINSEQ_1, RELAT_1, SETFAM_1, FINSEQ_4, FUNCT_1, RPR_1,
CARD_1, SEQ_1, BOOLE, ARYTM, TARSKI, ARYTM_3, RLVECT_1, PROB_1, PROB_2,
FINSET_1, UPROOTS, MATRPROB, SEQM_3;
notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, CARD_1, ORDINAL1, NUMBERS,
DOMAIN_1, XCMPLX_0, XXREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FINSEQ_1, FINSEQ_2, VALUED_1, FUNCT_2, BINOP_2, NAT_1,
SETFAM_1, SEQ_1, RPR_1, PROB_2, RVSUM_1, UPROOTS, MATRPROB;
constructors DOMAIN_1, RPR_1, RVSUM_1, SEQ_1, BINOP_2, SETWOP_2, PARTFUN3,
INTEGRA2, PROB_2, VALUED_1, UPROOTS, MATRPROB, RELSET_1;
registrations FUNCT_1, SUBSET_1, NAT_1, XREAL_0, XXREAL_0, MEMBERED, ORDINAL1,
UPROOTS, ALGSTR_0, FINSEQ_1, FUNCT_2, RELAT_1, XBOOLE_0, FINSET_1,
NUMBERS, VALUED_0, VALUED_1, ASYMPT_0, CARD_1, MATRPROB, ENTROPY1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, RPR_1, FINSEQ_1, RELAT_1, FUNCT_1;
theorems XREAL_0, TARSKI, FINSEQ_2, CARD_2, FINSEQ_4, FUNCT_1, FINSEQ_1,
XBOOLE_0, XBOOLE_1, XXREAL_0, PROB_2, NAT_1, RELAT_1, ZFMISC_1, FUNCT_2,
XCMPLX_1, VALUED_1, UPROOTS, FINSEQ_5, CARD_1, RVSUM_1, MATRPROB;
schemes NAT_1, FINSEQ_1, FUNCT_1, FUNCT_2, SUBSET_1;
begin :: Probability on Finite and Discrete Set
notation
let S be non empty finite set, s be FinSequence of S;
synonym whole_event (s) for dom s;
end;
definition
let S be non empty finite set, s be non empty FinSequence of S;
redefine func whole_event (s) -> non empty finite set;
correctness;
end;
theorem defwe:
for S be non empty finite set, s be FinSequence of S
holds whole_event (s) = s"S
proof
let S be non empty finite set,
s be FinSequence of S;
P1: s"S c= s"rng s by RELAT_1:170;
s"rng s c= s"S by RELAT_1:178;
then
s"rng s = s"S by P1,XBOOLE_0:def 10;
hence thesis by RELAT_1:169;
end;
notation let S be non empty finite set,
s be FinSequence of S,
x be set;
synonym event_pick (x,s) for Coim(s,x);
end;
definition let S be non empty finite set, s be FinSequence of S, x be set;
redefine func event_pick (x,s) -> Event of whole_event(s);
correctness by RELAT_1:167;
end;
definition
let S be non empty finite set, s be FinSequence of S, x be set;
func frequency(x,s) -> Nat equals
card (event_pick(x,s));
correctness;
end;
theorem
for S be non empty finite set,
s be FinSequence of S, e be set st e in whole_event(s)
ex x be Element of S st e in event_pick(x,s)
proof
let S be non empty finite set,
s be FinSequence of S,
e be set;
assume AS: e in whole_event(s);
then e in s"S by defwe;
then s.e in S by FUNCT_1:def 13;
then consider x be Element of S such that L1: x=s.e;
CON: x in {x} by TARSKI:def 1;
take x;
thus thesis by CON,AS,L1,FUNCT_1:def 13;
end;
theorem nazo6:
for S be non empty finite set,
s be FinSequence of S holds card whole_event(s) = len s
proof
let S be non empty finite set,
s be FinSequence of S;
card whole_event(s)= card Seg len s by FINSEQ_1:def 3
.= len s by FINSEQ_1:78;
hence thesis;
end;
definition let S be non empty finite set,
s be FinSequence of S, x be set;
func FDprobability (x,s) -> Real equals
frequency(x,s) / (len s);
correctness by XREAL_0:def 1;
end;
theorem
for S be non empty finite set,
s be FinSequence of S, x be set holds
frequency(x,s)=(len s)* FDprobability (x,s)
proof
let S be non empty finite set, s be FinSequence of S,x be set;
per cases;
suppose s is non empty;
hence thesis by XCMPLX_1:88;
end;
suppose s is empty; then
event_pick(x,s)={} by RELAT_1:172;
then frequency(x,s)=0;
hence thesis;
end;
end;
definition let S be non empty finite set, s be FinSequence of S;
func FDprobSEQ (s) -> FinSequence of REAL means
:defFREQDIST:
dom it= Seg (card (S)) & for n be Nat st n in dom it
holds it.n=FDprobability((canFS(S)).n,s);
existence
proof
defpred P[Nat,set] means
$2=FDprobability((canFS(S)).$1,s);
P0: for k be Nat st k in Seg (card (S))
ex x being Element of REAL st P[k,x];
consider g be FinSequence of REAL such that
P1: dom g =Seg (card (S))
& for n be Nat st n in Seg (card (S)) holds P[n,g.n]
from FINSEQ_1:sch 5(P0);
take g;
thus thesis by P1;
end;
uniqueness
proof
let g,h be FinSequence of REAL;
assume
A1: dom g =Seg (card (S)) & for n be Nat st n in dom g
holds g.n=FDprobability((canFS(S)).n,s);
assume
A2: dom h =Seg (card (S)) & for n be Nat st n in dom h
holds h.n=FDprobability((canFS(S)).n,s);
A6: len g =card (S) by A1,FINSEQ_1:def 3
.=len h by A2,FINSEQ_1:def 3;
now let n be Nat;
assume A6: n in dom g;
thus g.n = FDprobability((canFS(S)).n,s) by A6,A1
.= h.n by A6,A1,A2;
end;
hence thesis by FINSEQ_2:10,A6;
end;
end;
theorem
for S be non empty finite set,
s be non empty FinSequence of S, x be set holds
FDprobability(x,s)=prob(event_pick(x,s)) by nazo6;
definition let S be non empty finite set,
s,t be FinSequence of S;
pred s,t -are_prob_equivalent means :defequiv:
for x be set holds FDprobability (x,s)=FDprobability (x,t);
reflexivity;
symmetry;
end;
theorem EQX01:
for S be non empty finite set, s,t,u be FinSequence of S st
s,t -are_prob_equivalent & t,u -are_prob_equivalent holds
s,u -are_prob_equivalent
proof
let S be non empty finite set;
let s,t,u be FinSequence of S;
assume AS1: s,t -are_prob_equivalent & t,u -are_prob_equivalent;
now let x be set;
thus FDprobability (x,s)=FDprobability (x,t) by AS1,defequiv
.=FDprobability (x,u) by AS1,defequiv;
end;
hence s,u -are_prob_equivalent by defequiv;
end;
definition let S be non empty finite set, s be FinSequence of S;
func Finseq-EQclass(s) -> non empty Subset of S* equals
{t where t is FinSequence of S: s,t -are_prob_equivalent};
correctness
proof
P0P: s in {t where t is FinSequence of S: s,t -are_prob_equivalent};
{t where t is FinSequence of S: s,t -are_prob_equivalent } c= S*
proof
let x be set;
assume x in {t where t is FinSequence of S : s,t -are_prob_equivalent };
then ex t be FinSequence of S
st x=t & s,t -are_prob_equivalent;
hence x in S* by FINSEQ_1:def 11;
end;
hence thesis by P0P;
end;
end;
theorem EQX02:
for S be non empty finite set, s,t be FinSequence of S holds
(s,t -are_prob_equivalent iff t in Finseq-EQclass(s))
proof
let S be non empty finite set, s,t be FinSequence of S;
now assume t in Finseq-EQclass(s); then
ex t0 be FinSequence of S
st t=t0 & s,t0 -are_prob_equivalent;
hence s,t -are_prob_equivalent;
end;
hence s,t -are_prob_equivalent iff t in Finseq-EQclass(s);
end;
theorem EQX03:
for S be non empty finite set,
s be FinSequence of S holds s in Finseq-EQclass(s);
theorem EQX04:
for S be non empty finite set,
s,t be FinSequence of S holds
s,t -are_prob_equivalent iff Finseq-EQclass(s) = Finseq-EQclass(t)
proof
let S be non empty finite set,
s,t be FinSequence of S;
P1: now assume
P10: s,t -are_prob_equivalent;
now let x be set;
assume x in Finseq-EQclass(s); then
consider u be FinSequence of S such that
P11: x=u & s,u -are_prob_equivalent;
t,u -are_prob_equivalent by EQX01,P10,P11;
hence x in Finseq-EQclass(t) by P11;
end; then
P11: Finseq-EQclass(s) c= Finseq-EQclass(t) by TARSKI:def 3;
now let x be set;
assume x in Finseq-EQclass(t);
then consider u be FinSequence of S such that
P11: x=u & t,u -are_prob_equivalent;
s,u -are_prob_equivalent by EQX01,P11,P10;
hence x in Finseq-EQclass(s) by P11;
end;
then Finseq-EQclass(t) c= Finseq-EQclass(s) by TARSKI:def 3;
hence Finseq-EQclass(t) = Finseq-EQclass(s) by XBOOLE_0:def 10,P11;
end;
now assume Finseq-EQclass(s) = Finseq-EQclass(t);
then s in Finseq-EQclass(t);
hence s,t -are_prob_equivalent by EQX02;
end;
hence thesis by P1;
end;
definition
let S be non empty finite set;
defpred P[set] means ex u being FinSequence of S st
$1 = Finseq-EQclass(u);
func distribution_family(S) -> non empty Subset-Family of S* means
:defQuot:
for A being Subset of S* holds
A in it iff ex s being FinSequence of S st A = Finseq-EQclass(s);
existence
proof
consider T be Subset-Family of S* such that
P1: for A being Subset of S* holds A in T
iff P[A] from SUBSET_1:sch 3;
consider s be Element of S*;
Finseq-EQclass(s) in T by P1;
hence thesis by P1;
end;
uniqueness
proof
let F1,F2 be non empty Subset-Family of S*;
assume that
A1: for A being Subset of S* holds A in F1 iff P[A] and
A2: for A being Subset of S* holds A in F2 iff P[A];
thus thesis from SUBSET_1:sch 4(A1,A2);
end;
end;
theorem EQX05:
for S be non empty finite set,
s,t be FinSequence of S holds
s,t -are_prob_equivalent iff FDprobSEQ(s) = FDprobSEQ(t)
proof
let S be non empty finite set,
s,t be FinSequence of S;
P0: now assume AS: s,t -are_prob_equivalent;
P1: dom FDprobSEQ (t) = Seg (card (S)) by defFREQDIST;
now let n be Nat;
assume P21: n in dom FDprobSEQ (t);
thus (FDprobSEQ (t)).n
=FDprobability((canFS(S)).n,t) by P21,defFREQDIST
.=FDprobability((canFS(S)).n,s) by AS,defequiv;
end;
hence FDprobSEQ (s)=FDprobSEQ (t) by P1, defFREQDIST;
end;
now assume AS: FDprobSEQ (s) = FDprobSEQ (t);
for x be set holds FDprobability(x,t) =FDprobability(x,s)
proof let x be set;
per cases;
suppose x in S;
then x in rng canFS(S) by FUNCT_2:def 3;
then consider n be set such that
C11: n in dom (canFS(S)) & x=(canFS(S)).n by FUNCT_1:def 5;
reconsider n as Element of NAT by C11;
len canFS(S) = card (S) by UPROOTS:5; then
C110:n in Seg (card (S)) by C11,FINSEQ_1:def 3; then
C12: n in dom (FDprobSEQ (s)) by defFREQDIST;
C13: n in dom (FDprobSEQ (t)) by C110,defFREQDIST;
thus FDprobability(x,s) = (FDprobSEQ (s)).n by C12,defFREQDIST,C11
.= FDprobability(x,t) by C11,C13,defFREQDIST,AS;
end;
suppose C2: not x in S;
C21P: s"{x} = {}
proof
assume s"{x} <> {}; then
consider y be set such that
AA1: y in s"{x} by XBOOLE_0:def 1;
AA2:y in dom s & s.y in {x} by FUNCT_1:def 13,AA1;
then s.y in rng s by FUNCT_1:12;
then s.y in S & s.y=x by AA2,TARSKI:def 1;
hence contradiction by C2;
end;
C22P: t"{x} = {}
proof
assume t"{x} <> {};
then consider y be set such that
AA1: y in t"{x} by XBOOLE_0:def 1;
AA2:y in dom t & t.y in {x} by FUNCT_1:def 13,AA1;
then t.y in rng t by FUNCT_1:12;
then t.y in S & t.y=x by AA2,TARSKI:def 1;
hence contradiction by C2;
end;
thus FDprobability(x,s)=0 by C21P .=FDprobability(x,t) by C22P;
end;
end;
hence s,t -are_prob_equivalent by defequiv;
end;
hence thesis by P0;
end;
theorem
for S be non empty finite set,
s,t be FinSequence of S st t in Finseq-EQclass(s)
holds FDprobSEQ(s)=FDprobSEQ(t)
proof
let S be non empty finite set,
s,t be FinSequence of S;
assume t in Finseq-EQclass(s);
then ex w be FinSequence of S
st t=w & s,w -are_prob_equivalent;
hence thesis by EQX05;
end;
definition let S be non empty finite set;
func GenProbSEQ (S) -> Function of distribution_family(S),REAL* means
:defFREQDIST2:
for x be Element of distribution_family(S) holds
ex s be FinSequence of S st s in x & it.x=FDprobSEQ (s);
existence
proof
defpred P[set,set] means
ex s be FinSequence of S st s in $1 & $2=FDprobSEQ (s);
P0: for x being Element of distribution_family(S)
ex y be Element of REAL* st P[x,y]
proof
let x be Element of distribution_family(S);
reconsider A =x as Subset of S*;
consider s being FinSequence of S such that
P02: A = Finseq-EQclass(s) by defQuot;
FDprobSEQ (s) in REAL* by FINSEQ_1:def 11;
hence thesis by EQX03,P02;
end;
consider g be Function of distribution_family(S), REAL* such that
P1: for x being Element of distribution_family(S) holds P[x,g.x]
from FUNCT_2:sch 3(P0);
take g;
thus thesis by P1;
end;
uniqueness
proof
let g,h be Function of distribution_family(S), REAL*;
assume
A1: for x be Element of distribution_family(S) holds
ex s be FinSequence of S st s in x & g.x=FDprobSEQ (s);
assume
A2: for x be Element of distribution_family(S) holds
ex s be FinSequence of S st s in x & h.x=FDprobSEQ (s);
now let x be Element of distribution_family(S);
reconsider A =x as Subset of S*;
consider u being FinSequence of S such that
P02: A = Finseq-EQclass(u) by defQuot;
consider s be FinSequence of S such that
A3: s in x & g.x=FDprobSEQ (s) by A1;
consider t be FinSequence of S such that
A4: t in x & h.x=FDprobSEQ (t) by A2;
A5: u,s -are_prob_equivalent by EQX02,P02,A3;
t,u -are_prob_equivalent by EQX02,P02,A4;
then t,s -are_prob_equivalent by A5,EQX01;
hence g.x = h.x by A3,A4,EQX05;
end;
hence thesis by FUNCT_2:def 9;
end;
end;
theorem EQX07:
for S be non empty finite set, s be FinSequence of S holds
(GenProbSEQ (S)).(Finseq-EQclass(s)) = FDprobSEQ (s)
proof
let S be non empty finite set,
s be FinSequence of S;
Finseq-EQclass(s) is Element of distribution_family(S) by defQuot;
then consider u be FinSequence of S such that
P2: u in Finseq-EQclass(s) & (GenProbSEQ (S)).(Finseq-EQclass(s))
=FDprobSEQ (u) by defFREQDIST2;
s,u -are_prob_equivalent by P2,EQX02;
hence thesis by P2,EQX05;
end;
EQX08: for S be non empty finite set holds GenProbSEQ (S) is one-to-one
proof
let S be non empty finite set;
now let x1,x2 be set;
assume AS: x1 in distribution_family(S)
& x2 in distribution_family(S)
& (GenProbSEQ (S)).x1 =(GenProbSEQ (S)).x2;
then consider u be FinSequence of S such that
P2: u in x1 & (GenProbSEQ (S)).x1 =FDprobSEQ (u) by defFREQDIST2;
consider v be FinSequence of S such that
P3: v in x2 & (GenProbSEQ (S)).x2 =FDprobSEQ (v) by defFREQDIST2,AS;
P4: u,v -are_prob_equivalent by EQX05,AS,P2,P3;
reconsider A1 =x1 as Subset of S* by AS;
consider u1 being FinSequence of S such that
P02: A1 = Finseq-EQclass(u1) by defQuot,AS;
reconsider A2 =x2 as Subset of S* by AS;
consider u2 being FinSequence of S such that
P03: A2 = Finseq-EQclass(u2) by defQuot,AS;
P5: u1,u -are_prob_equivalent by EQX02,P2,P02;
P6: v,u2 -are_prob_equivalent by EQX02,P3,P03;
u1,v -are_prob_equivalent by EQX01,P4,P5;
then u1,u2 -are_prob_equivalent by EQX01,P6;
hence x1=x2 by P02,P03,EQX04;
end;
hence thesis by FUNCT_2:25;
end;
registration let S be non empty finite set;
cluster GenProbSEQ S -> one-to-one;
coherence by EQX08;
end;
definition
let S be non empty finite set,
p be ProbFinS FinSequence of REAL;
assume AS: len p=card S &
ex s be FinSequence of S st FDprobSEQ (s)=p;
func distribution( p,S ) -> Element of distribution_family(S) means
:defBUNBPU:
(GenProbSEQ S).it = p;
existence
proof
consider s be FinSequence of S such that L1: FDprobSEQ (s)=p by AS;
consider CS be non empty Subset of S* such that
L3: CS=Finseq-EQclass(s);
reconsider CS as Element of distribution_family(S) by defQuot,L3;
take CS;
thus thesis by L1,EQX07,L3;
end;
uniqueness
proof
let CS1,CS2 be Element of distribution_family(S);
assume U1:(GenProbSEQ (S)).CS1 = p;
assume U2:(GenProbSEQ (S)).CS2 = p;
CS1 in dom (GenProbSEQ (S)) &
CS2 in dom (GenProbSEQ (S)) by FUNCT_1:def 4,U1,U2;
hence thesis by FUNCT_1:def 8,U1,U2;
end;
end;
definition let S be non empty finite set,
s be FinSequence of S;
func freqSEQ (s) -> FinSequence of NAT means :defDIST:
dom it= Seg (card S) & for n be Nat st n in dom it
holds it.n=(len s) * (FDprobSEQ(s)).n;
existence
proof
defpred P[Nat,set ] means $2=(len s) * (FDprobSEQ(s)).$1;
P0: for k be Nat st k in Seg (card (S))
ex x being Element of NAT st P[k,x]
proof
let k be Nat;
assume SAS1: k in Seg(card (S));
then SAS3P:
k in dom FDprobSEQ(s) by defFREQDIST;
consider y be Real such that
SAS4: y =(len s)*(FDprobSEQ(s)).k;
Seg (len canFS(S))=Seg (card S) by UPROOTS:5; then
SAS5:k in dom (canFS(S)) by SAS1,FINSEQ_1:def 3;
rng (canFS(S))= S by FUNCT_2:def 3;
then (canFS(S)).k is Element of S by SAS5,FUNCT_1:12;
then consider a be Element of S such that SAS7: a=(canFS(S)).k;
SAS8:y=(len s)*FDprobability(a,s) by SAS3P,SAS4,SAS7,defFREQDIST;
SAS9: y is Element of NAT
proof
per cases;
suppose s={};
hence thesis by SAS8;
end;
suppose s<>{};
hence thesis by SAS8,XCMPLX_1:88;
end;
end;
take y;
thus thesis by SAS4,SAS9;
end;
consider g be FinSequence of NAT such that
P1: dom g =Seg (card (S))
& for n be Nat st n in Seg (card (S)) holds P[n,g.n]
from FINSEQ_1:sch 5(P0);
take g;
thus thesis by P1;
end;
uniqueness
proof
let g,h be FinSequence of NAT;
assume
A1: dom g =Seg (card (S)) & for n be Nat st n in dom g
holds g.n=(len s) * (FDprobSEQ(s)).n;
assume
A2: dom h =Seg (card (S)) & for n be Nat st n in dom h
holds h.n=(len s) * (FDprobSEQ(s)).n;
A6: len g =card (S) by A1,FINSEQ_1:def 3
.=len h by A2,FINSEQ_1:def 3;
now let n be Nat;
assume A6: n in dom g;
thus g.n =(len s) * (FDprobSEQ(s)).n by A6,A1
.= h.n by A6,A1,A2;
end;
hence thesis by FINSEQ_2:10,A6;
end;
end;
theorem nazonazo:
for S be non empty finite set,
s be non empty FinSequence of S, n be Nat st n in Seg (card S)
ex x be Element of S st (freqSEQ(s)).n=frequency(x,s)& x=(canFS(S)).n
proof
let S be non empty finite set,
s be non empty FinSequence of S, n be Nat;
assume SAS1: n in Seg(card (S));
SAS2: n in dom freqSEQ(s)
& n in dom FDprobSEQ(s) by defDIST,defFREQDIST,SAS1;
consider y be Real such that
SAS4: y =(len s)*(FDprobSEQ(s)).n;
Seg (len canFS(S))=Seg (card S) by UPROOTS:5; then
SAS5:n in dom (canFS(S)) by SAS1,FINSEQ_1:def 3;
rng (canFS(S))= S by FUNCT_2:def 3;
then (canFS(S)).n is Element of S by SAS5,FUNCT_1:12;
then consider a be Element of S such that SAS7: a=(canFS(S)).n;
SAS8: y=(len s)*FDprobability(a,s) by SAS2,defFREQDIST,SAS4,SAS7;
T2: y= frequency(a,s) by SAS8,XCMPLX_1:88;
take a;
thus thesis by SAS2,T2,SAS7,defDIST,SAS4;
end;
theorem nnnazo1:
for S be non empty finite set, s be FinSequence of S holds
freqSEQ (s) =(len s)* ((FDprobSEQ(s)))
proof
let S be non empty finite set,
s be FinSequence of S;
P1: dom ((len s) (#) ( (FDprobSEQ(s))))
=dom (FDprobSEQ(s)) by VALUED_1:def 5
.=Seg (card (S)) by defFREQDIST
.= dom (freqSEQ (s)) by defDIST;
now let m be Nat;
assume A1: m in dom ((len s) (#) ( (FDprobSEQ(s))));
hence ((len s) (#) ( (FDprobSEQ(s)))).m
=(len s)* ( (FDprobSEQ(s))).m by VALUED_1:def 5
.= (freqSEQ (s)).m by A1,P1,defDIST;
end;
hence freqSEQ s = (len s) (#) (FDprobSEQ s) by FINSEQ_1:17,P1;
end;
theorem nnazo2:
for S be non empty finite set,
s be FinSequence of S holds
Sum ( freqSEQ (s))=(len s)* Sum(FDprobSEQ(s))
proof
let S be non empty finite set,
s be FinSequence of S;
freqSEQ (s) =(len s)*FDprobSEQ(s) by nnnazo1;
hence thesis by RVSUM_1:117;
end;
theorem
for S be non empty finite set,
s be non empty FinSequence of S, n be Nat st n in dom s
ex m be Nat st (freqSEQ(s)).m = frequency(s.n,s) & s.n=(canFS(S)).m
proof
let S be non empty finite set,
s be non empty FinSequence of S,
n be Nat;
assume AS: n in dom s;
set x=s.n;
x in rng s by FUNCT_1:12,AS;
then x in S;
then x in rng (canFS S) by FUNCT_2:def 3;
then consider m be set such that
DM: m in dom (canFS(S))& x=(canFS(S)).m by FUNCT_1:def 5;
reconsider m as Nat by DM;
Seg len (canFS(S))= Seg (card (S)) by UPROOTS:5;
then J1P: dom (canFS(S))=Seg(card (S)) by FINSEQ_1:def 3;
consider xx be Element of S such that J2: (freqSEQ(s)).m
=frequency(xx,s)& xx=(canFS(S)).m by nazonazo,J1P,DM;
take m;
thus thesis by DM,J2;
end;
theorem LMCARD1:
for n be Nat, S be Function,L be FinSequence of NAT
st S is disjoint_valued & dom S = dom L & n=len L
& for i be Nat st i in dom S holds
S.i is finite & L.i = card (S.i)
holds union rng S is finite &
card (union rng S) = Sum L
proof
defpred P[Nat] means
for S be Function,L be FinSequence of NAT
st S is disjoint_valued & dom S = dom L & $1=len L
& for i be Nat st i in dom S holds
S.i is finite & L.i = card (S.i) holds
union rng S is finite & card (union rng S ) = Sum L;
P0: P[0]
proof
let S be Function,L be FinSequence of NAT;
assume AS0:
S is disjoint_valued & dom S = dom L & 0=len L
& for i be Nat st i in dom S holds
S.i is finite & L.i = card (S.i);
P0: L= {} by AS0;
then S= {} by AS0;
then for X be set st X in rng S holds X c= {}; then
P3P: union rng S c= {} by ZFMISC_1:94;
thus union rng S is finite &
card (union rng S) = Sum L by P3P,P0,RVSUM_1:102;
end;
PN: now let n be Nat;
assume P1: P[n];
now let S be Function,L be FinSequence of NAT;
assume
ASN: S is disjoint_valued & dom S = dom L & (n+1)=len L
& for i be Nat st i in dom S holds
S.i is finite & L.i = card (S.i);
reconsider SN=S|(Seg n) as Function;
reconsider LN=L|n as FinSequence of NAT;
n+1 in Seg (len L) by ASN,FINSEQ_1:6; then
Q0: n+1 in dom S by ASN,FINSEQ_1:def 3;
Q1:SN is disjoint_valued
proof
now let x,y be set;
assume
A1: x <> y;
per cases;
suppose x in dom SN & y in dom SN;
then SN.x=S.x & SN.y= S.y by FUNCT_1:70;
hence SN.x misses SN.y by A1,ASN,PROB_2:def 3;
end;
suppose A12: not (x in dom SN & y in dom SN );
now per cases by A12;
suppose not x in dom SN;
then SN.x= {} by FUNCT_1:def 4;
then SN.x /\ SN.y = {};
hence SN.x misses SN.y by XBOOLE_0:def 7;
end;
suppose not y in dom SN;
then SN.y= {} by FUNCT_1:def 4;
then SN.x /\ SN.y = {};
hence SN.x misses SN.y by XBOOLE_0:def 7;
end;
end;
hence SN.x misses SN.y;
end;
end;
hence thesis by PROB_2:def 3;
end;
Q2:dom SN = dom S /\ Seg n by RELAT_1:90
.= dom LN by RELAT_1:90,ASN;
Q3:n=len LN by FINSEQ_1:80,ASN,NAT_1:12;
Q4:for i be Nat st i in dom SN holds
SN.i is finite & LN.i = card (SN.i)
proof
let i be Nat;
assume A2P:i in dom SN; then
A2:i in dom S /\ Seg n by RELAT_1:90; then
A3:i in dom S & i in Seg n by XBOOLE_0:def 4;
LN.i = L.i by FUNCT_1:71,ASN,A2
.= card (S.i) by ASN,A3
.= card (SN.i) by A2P,FUNCT_1:70;
hence thesis;
end;
Q5:union rng SN is finite &
card (union rng SN ) = Sum LN by P1,Q1,Q2,Q3,Q4;
Q6: (union rng SN) \/ S.(n+1) = (union rng S)
proof
now let x be set;
assume x in (union rng S);
then consider y be set such that
A9: x in y & y in rng S by TARSKI:def 4;
consider i be set such that
A3: i in dom S & y=S.i by A9,FUNCT_1:def 5;
A4:i in Seg (n+1) by ASN,FINSEQ_1:def 3,A3;
reconsider i as Element of NAT by ASN,A3;
A5: 1<=i & i <= n+1 by FINSEQ_1:3,A4;
now per cases;
suppose i=n+1;
hence x in (union rng SN) \/ S.(n+1) by XBOOLE_0:def 3,A3,A9;
end;
suppose i<> n+1;
then i < n+1 by A5,XXREAL_0:1;
then i <= n by NAT_1:13;
then i in Seg n by A5;
then i in dom S /\ Seg n by A3,XBOOLE_0:def 4;
then
A8: i in dom SN by RELAT_1:90;
then S.i = SN.i by FUNCT_1:70;
then y in rng SN by FUNCT_1:def 5,A3,A8;
then x in (union rng SN) by A9,TARSKI:def 4;
hence x in (union rng SN) \/ S.(n+1) by XBOOLE_0:def 3;
end;
end;
hence x in (union rng SN) \/ S.(n+1);
end;
then
L1: (union rng S) c= (union rng SN) \/ S.(n+1) by TARSKI:def 3;
(union rng SN) \/ S.(n+1) c= (union rng S)
proof
let x be set;
assume A3P: x in (union rng SN) \/ S.(n+1);
now per cases by A3P,XBOOLE_0:def 3;
suppose C1: x in S.(n+1);
n+1 in Seg (n+1) by FINSEQ_1:6;
then n+1 in dom S by ASN,FINSEQ_1:def 3;
then S.(n+1) in rng S by FUNCT_1:def 5;
hence x in union rng S by C1,TARSKI:def 4;
end;
suppose x in (union rng SN);
then consider y be set such that
A9: x in y & y in rng SN by TARSKI:def 4;
consider i be set such that
A3: i in dom SN & y=SN.i by A9,FUNCT_1:def 5;
A4: i in dom S /\ Seg n by RELAT_1:90,A3;
A5: SN.i = S.i by FUNCT_1:70,A3;
i in dom S by A4,XBOOLE_0:def 4;
then y in rng S by A3,A5,FUNCT_1:def 5;
hence x in (union rng S) by A9,TARSKI:def 4;
end;
end;
hence x in (union rng S);
end;
hence thesis by L1,XBOOLE_0:def 10;
end;
AA: 1<= (n+1) & n+1 <= len L by ASN,NAT_1:11;
Q7P:L= (L|n)^ <* L/.len L *> by ASN,FINSEQ_5:24
.=LN^<*L.(n+1)*> by AA,ASN,FINSEQ_4:24;
reconsider USN= union rng SN as finite set by P1,Q1,Q2,Q3,Q4;
reconsider S1= S.(n+1) as finite set by ASN,Q0;
union rng S = USN \/ S1 by Q6;
hence (union rng S) is finite;
for z be set st z in rng SN holds z misses S.(n+1)
proof
let y be set;
assume
A2: y in rng SN;
consider i be set such that
A3: i in dom SN & y=SN.i by A2,FUNCT_1:def 5;
A4P: i in dom S /\ Seg n by A3,RELAT_1:90; then
A4:i in Seg n by XBOOLE_0:def 4;
reconsider i as Element of NAT by A4P;
i <= n by FINSEQ_1:3,A4; then
A0P: i <> n+1 by NAT_1:13;
y=S.i by A3,FUNCT_1:70;
hence thesis by A0P,PROB_2:def 3,ASN;
end;
then
Q9: union rng SN misses S.(n+1) by ZFMISC_1:98;
Q8: card ((union rng SN) \/ S.(n+1) )
=card (USN)+ card (S1) by Q9,CARD_2:53;
thus card (union rng S ) = Sum LN + L.(n+1) by Q5,ASN,Q0,Q8,Q6
.= Sum L by Q7P,RVSUM_1:104;
end;
hence P[n+1];
end;
thus for n be Nat holds P[n] from NAT_1:sch 2(P0,PN);
end;
theorem LMCARD:
for S be Function,L be FinSequence of NAT
st S is disjoint_valued & dom S = dom L
& for i be Nat st i in dom S holds
S.i is finite & L.i = card (S.i)
holds union rng S is finite
& card (union rng S ) = Sum L
proof
let S be Function,L be FinSequence of NAT;
assume AS: S is disjoint_valued & dom S = dom L
& for i be Nat st i in dom S holds
S.i is finite & L.i = card (S.i);
len L is Element of NAT;
hence thesis by LMCARD1,AS;
end;
theorem DISTSUM:
for S be non empty finite set,
s be non empty FinSequence of S holds
Sum freqSEQ (s) = len s
proof
let S be non empty finite set,
s be non empty FinSequence of S;
set L= freqSEQ (s);
defpred P[set,set] means ex z be Element of S
st z=(canFS(S)).$1 & $2 = event_pick(z,s);
len (canFS(S))= card (S) by UPROOTS:5;
then PP0: dom (canFS(S))=Seg(card (S)) by FINSEQ_1:def 3;
PP1: for x,y1,y2 be set
st x in dom L & P[x,y1] & P[x,y2] holds y1 = y2;
PP2: for x be set st x in dom L ex y be set st P[x,y]
proof
let x be set;
assume x in dom L;
then LPP22P:x in Seg (card (S)) by defDIST;
set z= (canFS(S)).x;
rng (canFS(S))=S by FUNCT_2:def 3;
then reconsider z as Element of S by FUNCT_1:12,LPP22P,PP0;
consider y be set such that
LPP25: y=s"{z};
LPP26: y=event_pick(z,s) by LPP25;
take y;
thus thesis by LPP26;
end;
consider T be Function such that
P1:dom T = dom L &
for x be set st x in dom L holds P[x,T.x] from FUNCT_1:sch 2(PP1,PP2);
LMISS1: for a,b be set st
a in dom T & b in dom T & a<>b holds
T.a misses T.b
proof
let a,b be set;
assume ZTA: a in dom T & b in dom T & a<>b;
ZT1: a in dom(canFS(S)) & b in dom(canFS(S)) by P1,ZTA,PP0,defDIST;
ZT2:(canFS(S)).a<>(canFS(S)).b by ZTA,FUNCT_1:def 8,ZT1;
consider za be Element of S such that ZT3: za=(canFS(S)).a &
T.a=event_pick(za,s) by P1,ZTA;
consider zb be Element of S such that ZT4: zb=(canFS(S)).b &
T.b=event_pick(zb,s) by P1,ZTA;
thus thesis by ZT3,ZT4,FUNCT_1:141,ZFMISC_1:17,ZT2;
end;
for a,b be set st a<>b holds T.a misses T.b
proof
let a,b be set;
assume ANB: a<>b;
now per cases;
case a in dom T & b in dom T;
hence thesis by LMISS1,ANB;
end;
case not a in dom T;
then T.a={} by FUNCT_1:def 4;
hence thesis by XBOOLE_1:65;
end;
case a in dom T & not b in dom T;
then T.b={} by FUNCT_1:def 4;
hence thesis by XBOOLE_1:65;
end;
end;
hence thesis;
end; then
Q1: T is disjoint_valued by PROB_2:def 3;
Q3: for i be Nat st i in dom T holds
T.i is finite & L.i = card (T.i)
proof
let i be Nat;
assume ASQ3: i in dom T;
then consider zi be Element of S such that Q3C1: zi=(canFS(S)).i &
T.i=event_pick(zi,s) by P1;
Q3C3:dom L= Seg (card (S)) by defDIST;
Q3C4:i in dom (FDprobSEQ(s)) by P1,ASQ3,Q3C3,defFREQDIST;
L.i =(len s) * (FDprobSEQ(s)).i by defDIST,ASQ3,P1
.=(len s)*FDprobability((canFS(S)).i,s) by Q3C4,defFREQDIST
.= card (T.i) by Q3C1,XCMPLX_1:88;
hence thesis;
end;
reconsider T1=union rng T as finite set by Q1,P1,Q3,LMCARD;
for X be set st X in rng T holds X c= Seg (len s)
proof
let X be set;
assume X in rng T;
then consider j be set such that
RNGT1: j in dom T & X =T.j by FUNCT_1:def 5;
consider zj be Element of S such that
RNGT2: zj=(canFS(S)).j & T.j = event_pick(zj,s) by P1,RNGT1;
X c= whole_event(s) by RNGT1,RNGT2;
hence thesis by FINSEQ_1:def 3;
end; then
L1: union rng T c= Seg (len s) by ZFMISC_1:94;
Seg (len s) c=union rng T
proof
assume CNTRSEGLS: not Seg (len s) c=union rng T;
consider ne be set such that SEGLS1:
ne in Seg (len s) & not ne in union rng T by TARSKI:def 3,CNTRSEGLS;
SEGLS2: ne in dom s by SEGLS1,FINSEQ_1:def 3;
set yne=s.ne;
SEGLS4: yne in rng s by SEGLS2,FUNCT_1:def 5;
reconsider yne as Element of S by SEGLS4;
rng (canFS(S))=S by FUNCT_2:def 3;
then consider nne be set such that
SEGLS6: nne in dom(canFS(S))&
yne=(canFS(S)).nne by FUNCT_1:def 5;
NINDOML:nne in dom L by defDIST,PP0,SEGLS6;
then consider zne be Element of S such that
SEGLS7: zne=(canFS(S)).nne &
T.nne = event_pick(zne,s) by P1;
s.ne in {s.ne} by TARSKI:def 1;
then SEGLS9: ne in T.nne by SEGLS7,SEGLS6,FUNCT_1:def 13,SEGLS2;
T.nne in rng T by FUNCT_1:12,NINDOML,P1;
hence contradiction by SEGLS1,TARSKI:def 4,SEGLS9;
end;
then
Q5: T1 = Seg (len s) by L1,XBOOLE_0:def 10;
thus Sum freqSEQ (s) = card (T1) by Q1,P1,Q3,LMCARD
.= len s by FINSEQ_1:78,Q5;
end;
theorem FREQDISTSUM:
for S be non empty finite set,
s be non empty FinSequence of S holds Sum FDprobSEQ (s) = 1
proof
let S be non empty finite set,
s be non empty FinSequence of S;
Sum freqSEQ(s) = len s by DISTSUM;
then (len s)* Sum( (FDprobSEQ(s))) = (len s)*1 by nnazo2;
hence thesis by XCMPLX_1:5;
end;
theorem FREQDISTSUM2:
for S be non empty finite set,
s be non empty FinSequence of S holds FDprobSEQ (s) is ProbFinS
proof
let S be non empty finite set,
s be non empty FinSequence of S;
L0: Sum FDprobSEQ (s) = 1 by FREQDISTSUM;
for i be Element of NAT st i in dom (FDprobSEQ(s))
holds (FDprobSEQ(s)).i>=0
proof
let i be Element of NAT;
assume CAS: i in dom (FDprobSEQ(s));
(FDprobSEQ(s)).i =FDprobability((canFS(S)).i,s) by CAS,defFREQDIST;
hence thesis;
end;
hence thesis by L0,MATRPROB:def 5;
end;
definition
let S be non empty finite set;
mode distProbFinS of S -> ProbFinS FinSequence of REAL means
:defdistProbFinS:
len it=card S & ex s be FinSequence of S st FDprobSEQ (s)=it;
existence
proof
consider a be Element of S;
set s=<*a*>;
reconsider p=FDprobSEQ (s) as ProbFinS FinSequence of REAL
by FREQDISTSUM2;
dom p= Seg (card (S)) by defFREQDIST;
then len (p) =card S by FINSEQ_1:def 3;
hence thesis;
end;
end;
theorem pbf:
for S be non empty finite set,
p be distProbFinS of S holds
p is ProbFinS FinSequence of REAL
& len p=card S & (ex s be FinSequence of S st FDprobSEQ (s)=p)
& distribution( p,S ) is Element of distribution_family(S)
& (GenProbSEQ (S)).distribution( p,S ) = p
proof
let S be non empty finite set,
p be distProbFinS of S;
thus p is ProbFinS FinSequence of REAL;
thus P1: len p=card S & (ex s be FinSequence of S st FDprobSEQ (s)=p)
by defdistProbFinS;
thus distribution(p,S) is Element of distribution_family(S);
thus (GenProbSEQ S).distribution(p,S) = p by defBUNBPU,P1;
end;
begin :: uniform distribution
definition let S be non empty finite set, s be FinSequence of S;
pred s is_uniformly_distributed means
:defunidistseq:
for n be Nat st n in dom FDprobSEQ (s) holds
(FDprobSEQ (s)).n=1/(card S);
end;
theorem THUDEQ0:
for S be non empty finite set,
s be FinSequence of S st s is_uniformly_distributed
holds FDprobSEQ (s) is constant
proof
let S be non empty finite set,
s be FinSequence of S;
assume AS: s is_uniformly_distributed;
let a,b be set;
assume a: a in dom FDprobSEQ(s) & b in dom FDprobSEQ(s);
then reconsider na=a,nb=b as Nat;
(FDprobSEQ (s)).na = 1/card S by a,AS,defunidistseq
.= (FDprobSEQ (s)).nb by a,AS,defunidistseq;
hence thesis;
end;
theorem THUDEQ:
for S be non empty finite set,
s,t be FinSequence of S
st s is_uniformly_distributed &
s,t -are_prob_equivalent holds
t is_uniformly_distributed
proof
let S be non empty finite set,
s,t be FinSequence of S;
assume AS:s is_uniformly_distributed & s,t -are_prob_equivalent; then
L1: FDprobSEQ (s)=FDprobSEQ (t) by EQX05;
for n be Nat st n in dom FDprobSEQ (t) holds
(FDprobSEQ (t)).n=1/(card S) by L1,AS,defunidistseq;
hence thesis by defunidistseq;
end;
theorem THUDEQ2:
for S be non empty finite set,
s,t be FinSequence of S st s is_uniformly_distributed &
t is_uniformly_distributed holds
s,t -are_prob_equivalent
proof
let S be non empty finite set,
s,t be FinSequence of S;
assume AS:s is_uniformly_distributed &
t is_uniformly_distributed;
L1: dom FDprobSEQ (s)= Seg (card (S)) &
dom FDprobSEQ (t)= Seg (card (S)) by defFREQDIST;
for n be set st n in dom FDprobSEQ (s) holds
(FDprobSEQ (s)).n=(FDprobSEQ (t)).n
proof
let n be set;
assume n in dom FDprobSEQ (s); then
(FDprobSEQ (s)).n= 1/(card S)
&(FDprobSEQ (t)).n= 1/(card S) by defunidistseq,AS,L1;
hence thesis;
end;
then FDprobSEQ (s) = FDprobSEQ (t) by L1,FUNCT_1:9;
hence thesis by EQX05;
end;
theorem THUDS:
for S be non empty finite set holds
canFS(S) is_uniformly_distributed
proof
let S be non empty finite set;
set s = canFS(S);
L0: len s= card S by UPROOTS:5;then
dom s= Seg(card S) by FINSEQ_1:def 3;
then L01: dom s=dom FDprobSEQ (s) by defFREQDIST;
for n be Nat st n in dom s
holds (FDprobSEQ (s)).n=1/(card S)
proof
let n be Nat;
assume ASB: n in dom s; then
(FDprobSEQ (s)).n=FDprobability(s.n,s) by defFREQDIST,L01
.= card ({n}) /(len s) by FINSEQ_5:4,ASB
.= 1/(card S) by L0,CARD_1:50;
hence thesis;
end;
hence thesis by defunidistseq,L01;
end;
THCFS:
for S be non empty finite set,
s be FinSequence of S st s in Finseq-EQclass(canFS(S)) holds
s is_uniformly_distributed
proof
let S be non empty finite set, s be FinSequence of S;
consider CS be non empty Subset of S*
such that L3: CS=Finseq-EQclass(canFS(S));
reconsider CS as Element of distribution_family(S) by defQuot,L3;
assume s in Finseq-EQclass(canFS(S)); then
s,canFS(S) -are_prob_equivalent by EQX02;
hence thesis by THUDEQ,THUDS;
end;
THCFS2:
for S be non empty finite set,
s be FinSequence of S
st s is_uniformly_distributed holds
for t be FinSequence of S st
t is_uniformly_distributed holds
t in Finseq-EQclass(s)
proof
let S be non empty finite set,
s be FinSequence of S;
assume L1: s is_uniformly_distributed;
for t be FinSequence of S st t is_uniformly_distributed holds
t in Finseq-EQclass(s)
proof
let t be FinSequence of S;
assume t is_uniformly_distributed;
then s,t -are_prob_equivalent by L1,THUDEQ2;
hence thesis;
end;
hence thesis;
end;
definition let S be non empty finite set;
func uniform_distribution(S) -> Element of distribution_family(S) means
:defunidist:
for s be FinSequence of S holds s in it iff s is_uniformly_distributed;
existence
proof
consider s be FinSequence of S such that L1: s=canFS(S);
L2: s is_uniformly_distributed by L1,THUDS;
consider CS be non empty Subset of S*
such that L3: CS=Finseq-EQclass(s);
reconsider CS as Element of distribution_family(S) by defQuot,L3;
for t be FinSequence of S
st t in CS holds
s,t -are_prob_equivalent by EQX02,L3; then
L5: for t be FinSequence of S
st t in CS holds t is_uniformly_distributed by L2,THUDEQ;
take CS;
thus thesis by L2,L5,THCFS2,L3;
end;
uniqueness
proof
let A,B be Element of distribution_family(S);
assume U1:
for s be FinSequence of S holds s in A iff s is_uniformly_distributed;
assume U2:
for s be FinSequence of S holds s in B iff s is_uniformly_distributed;
N1: for s be set st s in A holds s in B
proof
let s be set;
assume A1:s in A;
then reconsider s as Element of S*;
s is_uniformly_distributed by U1,A1;
hence thesis by U2;
end;
for s be set st s in B holds s in A
proof
let s be set;
assume A1: s in B;
then reconsider s as Element of S*;
s is_uniformly_distributed by U2,A1;
hence thesis by U1;
end;
hence thesis by N1,TARSKI:2;
end;
end;
registration
let S be non empty finite set;
cluster constant distProbFinS of S;
existence
proof
consider s be FinSequence of S such that L1: s=canFS(S);
reconsider s as Element of S* by FINSEQ_1:def 11;
consider p be FinSequence of REAL
such that L3: p= FDprobSEQ (s);
T1: p is constant by THUDEQ0,L3,L1,THUDS;
T2: p is ProbFinS by L1,FREQDISTSUM2,L3;
T3: dom p= Seg (card (S)) by defFREQDIST,L3;
T4:len p=card S by T3,FINSEQ_1:def 3;
take p;
thus thesis by T1,defdistProbFinS,L3,T2,T4;
end;
end;
definition
let S be non empty finite set;
func Uniform_FDprobSEQ(S) -> constant distProbFinS of S equals
FDprobSEQ (canFS(S));
coherence
proof
set s=canFS(S);
reconsider s as Element of S* by FINSEQ_1:def 11;
consider p be FinSequence of REAL such that L3:p= FDprobSEQ (s);
L4: p is constant by THUDEQ0,L3,THUDS;
T2: p is ProbFinS by FREQDISTSUM2,L3;
T3: dom p= Seg (card (S)) by defFREQDIST,L3;
len p=card (S) by T3,FINSEQ_1:def 3;
hence thesis by defdistProbFinS,L3,T2,L4;
end;
end;
theorem
for S be non empty finite set holds
uniform_distribution(S)=distribution(Uniform_FDprobSEQ(S),S)
proof
let S be non empty finite set;
set p=Uniform_FDprobSEQ(S),s=canFS(S);
ES1:s is_uniformly_distributed by THUDS;
ZZ0: (GenProbSEQ (S)).(Finseq-EQclass(s)) = p by EQX07;
ZZ1:for t be FinSequence of S st
t in Finseq-EQclass(s) holds
t is_uniformly_distributed by THCFS;
nazo:Finseq-EQclass(s) is
Element of distribution_family(S) by defQuot;
for t be FinSequence of S st
t is_uniformly_distributed holds t in Finseq-EQclass(s)
proof
let t be FinSequence of S;
assume t is_uniformly_distributed;
then s,t -are_prob_equivalent by THUDEQ2,ES1;
hence thesis;
end;
then T1: Finseq-EQclass(s)=uniform_distribution(S)
by ZZ1,defunidist,nazo;
ZZ02:(GenProbSEQ (S)).distribution( p,S ) =
(GenProbSEQ (S)).(Finseq-EQclass(s)) by ZZ0,pbf;
dom (GenProbSEQ (S)) = distribution_family(S) by FUNCT_2:def 1;
hence thesis by ZZ02,T1,FUNCT_1:def 8;
end;