:: Probability on Finite and Discrete Set and Uniform Distribution
:: by Hiroyuki Okazaki
::
:: Received May 5, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, FINSET_1, FINSEQ_1, RELAT_1, TARSKI, RPR_1,
NAT_1, CARD_1, SUBSET_1, FUNCT_1, REAL_1, ARYTM_3, UPROOTS, SETFAM_1,
MATRPROB, VALUED_1, CARD_3, PROB_2, XXREAL_0, ORDINAL4, PARTFUN1, DIST_1;
notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, CARD_1, CARD_3, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FINSEQ_1, FINSEQ_2, VALUED_1, FUNCT_2, SETFAM_1, RPR_1, PROB_2,
RVSUM_1, UPROOTS, MATRPROB;
constructors RPR_1, RVSUM_1, BINOP_2, PARTFUN3, PROB_2, UPROOTS, MATRPROB,
RELSET_1;
registrations FUNCT_1, SUBSET_1, NAT_1, XREAL_0, ORDINAL1, FINSEQ_1, RELAT_1,
FINSET_1, NUMBERS, VALUED_0, CARD_1, MATRPROB, ENTROPY1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCT_1, XBOOLE_0;
equalities RPR_1, FINSEQ_1, RELAT_1, CARD_3, XBOOLE_0;
expansions TARSKI, FUNCT_1, XBOOLE_0;
theorems TARSKI, FINSEQ_2, CARD_2, FINSEQ_4, FUNCT_1, FINSEQ_1, XBOOLE_0,
XXREAL_0, PROB_2, NAT_1, RELAT_1, ZFMISC_1, FUNCT_2, XCMPLX_1, VALUED_1,
FINSEQ_5, CARD_1, RVSUM_1, MATRPROB, XREAL_0, RELSET_1;
schemes NAT_1, FINSEQ_1, FUNCT_2, SUBSET_1, CLASSES1;
begin :: Probability on Finite and Discrete Set
notation
let S be set, s be FinSequence of S;
synonym whole_event↑ (s) for dom s;
end;
notation
let S be set, s be FinSequence of S, x be set;
synonym event_pick (x,s) for Coim(s,x);
end;
definition
let S be set, s be FinSequence of S, x be set;
redefine func event_pick (x,s) -> Event of whole_event(s); :: redefines event_pick (DIST_1, synonym) → Coim (RELAT_1, definition)
correctness by RELAT_1:132;
end;
definition
let S be finite set, s be FinSequence of S, x be set;
func frequency(x,s) -> Nat equals
card (event_pick(x,s));
correctness;
end;
::$CT
theorem
for S be 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 set, s be FinSequence of S, e be set;
assume
A1: e in whole_event(s);
then e in s"S by RELSET_1:22;
then s.e in S by FUNCT_1:def 7;
then consider x be Element of S such that
A2: x=s.e;
take x;
x in {x} by TARSKI:def 1;
hence thesis by A1,A2,FUNCT_1:def 7;
end;
definition
let S be finite set, s be FinSequence of S, x be set;
func FDprobability (x,s) -> Real equals
frequency(x,s) / (len s);
correctness;
end;
::$CT
theorem
for S be finite set, s be FinSequence of S, x be set holds
frequency(x,s)=(len s)* FDprobability (x,s)
proof
let S be finite set, s be FinSequence of S,x be set;
per cases;
suppose s is non empty;
hence thesis by XCMPLX_1:87;
end;
suppose s is empty;
then frequency(x,s)=0;
hence thesis;
end;
end;
definition
let S be finite set, s be FinSequence of S;
func FDprobSEQ (s) -> FinSequence of REAL means
:Def3:
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,object] means $2=FDprobability((canFS(S)).$1,s);
A1: for k be Nat st k in Seg (card (S))
ex x being Element of REAL st P[k, x]
proof let k be Nat;
assume k in Seg (card (S));
consider x being Real such that
A2: P[k, x];
reconsider x as Element of REAL by XREAL_0:def 1;
take x;
thus thesis by A2;
end;
consider g be FinSequence of REAL such that
A3: 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(A1);
take g;
thus thesis by A3;
end;
uniqueness
proof
let g,h be FinSequence of REAL;
assume that
A4: dom g =Seg card S and
A5: for n be Nat st n in dom g holds g.n=FDprobability((canFS(S)).n,s);
assume that
A6: dom h =Seg card S and
A7: for n be Nat st n in dom h holds h.n=FDprobability((canFS(S)).n,s);
A8: now
let n be Nat;
assume
A9: n in dom g;
hence g.n = FDprobability((canFS(S)).n,s) by A5
.= h.n by A4,A6,A7,A9;
end;
len g = card S by A4,FINSEQ_1:def 3
.= len h by A6,FINSEQ_1:def 3;
hence thesis by A8,FINSEQ_2:9;
end;
end;
theorem
for S be finite set, s be FinSequence of S, x be set
holds FDprobability(x,s)=prob(event_pick(x,s)) by CARD_1:62;
definition
let S be finite set, s,t be FinSequence of S;
pred s,t -are_prob_equivalent means
for x be set holds FDprobability (x,s)=FDprobability (x,t);
reflexivity;
symmetry;
end;
theorem Th4:
for S be 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 finite set;
let s,t,u be FinSequence of S;
assume that
A1: s,t -are_prob_equivalent and
A2: t,u -are_prob_equivalent;
let x be set;
thus FDprobability (x,s)=FDprobability (x,t) by A1
.=FDprobability (x,u) by A2;
end;
definition
let S be finite set, s be FinSequence of S;
func Finseq-EQclass(s) -> Subset of S* equals
{t where t is FinSequence of S: s,t -are_prob_equivalent};
correctness
proof
{t where t is FinSequence of S: s,t -are_prob_equivalent } c= S*
proof
let x be object;
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;
end;
end;
registration
let S be finite set, s be FinSequence of S;
cluster Finseq-EQclass(s) -> non empty;
coherence
proof
s in Finseq-EQclass(s);
hence thesis;
end;
end;
theorem Th5:
for S be finite set, s,t be FinSequence of S holds
s,t -are_prob_equivalent iff t in Finseq-EQclass(s)
proof
let S be 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 thesis;
end;
theorem Th6:
for S be finite set, s be FinSequence of S holds s in Finseq-EQclass(s);
theorem Th7:
for S be 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 finite set, t,s be FinSequence of S;
hereby assume
A1: t,s -are_prob_equivalent;
thus Finseq-EQclass(t) = Finseq-EQclass(s)
proof
thus Finseq-EQclass(t) c= Finseq-EQclass(s)
proof
let x be object;
assume x in Finseq-EQclass(t);
then consider u be FinSequence of S such that
A2: x=u and
A3: t,u -are_prob_equivalent;
s,u -are_prob_equivalent by A1,A3,Th4;
hence x in Finseq-EQclass(s) by A2;
end;
let x be object;
assume x in Finseq-EQclass(s);
then consider u be FinSequence of S such that
A4: x=u and
A5: s,u -are_prob_equivalent;
t,u -are_prob_equivalent by A1,A5,Th4;
hence x in Finseq-EQclass(t) by A4;
end;
end;
assume Finseq-EQclass(t) = Finseq-EQclass(s);
then t in Finseq-EQclass(s);
hence t,s -are_prob_equivalent by Th5;
end;
definition
let S be finite set;
defpred P[set] means ex u being FinSequence of S st $1 = Finseq-EQclass(u);
func distribution_family(S) -> Subset-Family of S* means
:Def6:
for A being Subset of S* holds A in it iff ex s being FinSequence of S st
A = Finseq-EQclass(s);
existence
proof
ex T be Subset-Family of S* st
for A being Subset of S* holds A in T iff P[A] from SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
let F1,F2 be 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;
registration
let S be finite set;
cluster distribution_family(S) -> non empty;
coherence
proof
Finseq-EQclass(the Element of S*) in distribution_family(S) by Def6;
hence thesis;
end;
end;
theorem Th8:
for S be finite set, s,t be FinSequence of S holds
s,t -are_prob_equivalent iff FDprobSEQ(s) = FDprobSEQ(t)
proof
let S be finite set, s,t be FinSequence of S;
A1: now
assume
A2: 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 object such that
A3: n in dom canFS S and
A4: x=(canFS(S)).n by FUNCT_1:def 3;
reconsider n as Element of NAT by A3;
len canFS(S) = card (S) by FINSEQ_1:93;
then
A5: n in Seg card S by A3,FINSEQ_1:def 3;
then
A6: n in dom FDprobSEQ t by Def3;
n in dom FDprobSEQ s by A5,Def3;
hence FDprobability(x,s) = (FDprobSEQ s).n by A4,Def3
.= FDprobability(x,t) by A2,A4,A6,Def3;
end;
suppose
A7: not x in S;
not x in rng t by A7; then
rng t misses {x} by ZFMISC_1:50; then
A8: t"{x} = {} by RELAT_1:138;
not x in rng s by A7; then
rng s misses {x} by ZFMISC_1:50; then
s"{x} = {} by RELAT_1:138;
hence FDprobability(x,s)=0 .=FDprobability(x,t) by A8;
end;
end;
hence s,t -are_prob_equivalent;
end;
now
assume
A9: s,t -are_prob_equivalent;
A10: now
let n be Nat;
assume n in dom FDprobSEQ t;
hence (FDprobSEQ t).n =FDprobability((canFS(S)).n,t) by Def3
.=FDprobability((canFS S).n,s) by A9;
end;
dom FDprobSEQ t = Seg card S by Def3;
hence FDprobSEQ s = FDprobSEQ t by A10,Def3;
end;
hence thesis by A1;
end;
theorem
for S be finite set, s,t be FinSequence of S st
t in Finseq-EQclass(s) holds FDprobSEQ(s)=FDprobSEQ(t)
proof
let S be 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 Th8;
end;
definition
let S be finite set;
func GenProbSEQ (S) -> Function of distribution_family(S),REAL* means
:Def7:
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);
A1: 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);
consider s being FinSequence of S such that
A2: x = Finseq-EQclass(s) by Def6;
FDprobSEQ (s) in REAL* by FINSEQ_1:def 11;
hence thesis by A2,Th6;
end;
consider g be Function of distribution_family(S), REAL* such that
A3: for x being Element of distribution_family(S) holds P[x,g.x] from
FUNCT_2:sch 3(A1);
take g;
thus thesis by A3;
end;
uniqueness
proof
let g,h be Function of distribution_family(S), REAL*;
assume
A4: for x be Element of distribution_family(S) holds ex s be
FinSequence of S st s in x & g.x=FDprobSEQ (s);
assume
A5: 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);
consider u being FinSequence of S such that
A6: x = Finseq-EQclass(u) by Def6;
consider t be FinSequence of S such that
A7: t in x and
A8: h.x=FDprobSEQ (t) by A5;
A9: t,u -are_prob_equivalent by A6,A7,Th5;
consider s be FinSequence of S such that
A10: s in x and
A11: g.x=FDprobSEQ (s) by A4;
u,s -are_prob_equivalent by A6,A10,Th5;
then t,s -are_prob_equivalent by A9,Th4;
hence g.x = h.x by A11,A8,Th8;
end;
hence thesis by FUNCT_2:def 8;
end;
end;
theorem Th10:
for S be finite set, s be FinSequence of S holds
(GenProbSEQ (S)).(Finseq-EQclass(s)) = FDprobSEQ (s)
proof
let S be finite set, s be FinSequence of S;
Finseq-EQclass(s) is Element of distribution_family(S) by Def6;
then consider u be FinSequence of S such that
A1: u in Finseq-EQclass(s) and
A2: (GenProbSEQ (S)).(Finseq-EQclass(s)) =FDprobSEQ (u) by Def7;
s,u -are_prob_equivalent by A1,Th5;
hence thesis by A2,Th8;
end;
registration
let S be finite set;
cluster GenProbSEQ S -> one-to-one;
coherence
proof
now
let x1,x2 be object;
assume that
A1: x1 in distribution_family(S) and
A2: x2 in distribution_family(S) and
A3: (GenProbSEQ (S)).x1 =(GenProbSEQ (S)).x2;
reconsider xx1=x1, xx2=x2 as set by TARSKI:1;
consider u1 being FinSequence of S such that
A4: x1 = Finseq-EQclass(u1) by A1,Def6;
consider u2 being FinSequence of S such that
A5: x2 = Finseq-EQclass(u2) by A2,Def6;
consider v be FinSequence of S such that
A6: v in xx2 and
A7: (GenProbSEQ (S)).x2 =FDprobSEQ (v) by A2,Def7;
consider u be FinSequence of S such that
A8: u in xx1 and
A9: (GenProbSEQ (S)).x1 =FDprobSEQ (u) by A1,Def7;
A10: u,v -are_prob_equivalent by A3,A9,A7,Th8;
u1,u -are_prob_equivalent by A8,A4,Th5;
then
A11: u1,v -are_prob_equivalent by A10,Th4;
v,u2 -are_prob_equivalent by A6,A5,Th5;
then u1,u2 -are_prob_equivalent by A11,Th4;
hence x1=x2 by A4,A5,Th7;
end;
hence thesis by FUNCT_2:19;
end;
end;
definition
let S be finite set, p be ProbFinS FinSequence of REAL;
assume
A1: ex s be FinSequence of S st FDprobSEQ (s)=p;
func distribution (p,S) -> Element of distribution_family(S) means
:Def8:
(GenProbSEQ S).it = p;
existence
proof
consider s be FinSequence of S such that
A2: FDprobSEQ (s)=p by A1;
reconsider CS =Finseq-EQclass(s) as Element of distribution_family(S)
by Def6;
take CS;
thus thesis by A2,Th10;
end;
uniqueness
proof
let CS1,CS2 be Element of distribution_family(S);
assume
A3: (GenProbSEQ S).CS1 = p; then
A4: CS1 in dom (GenProbSEQ (S)) by FUNCT_1:def 2;
assume
A5: (GenProbSEQ S).CS2 = p;
then CS2 in dom (GenProbSEQ (S)) by FUNCT_1:def 2;
hence thesis by A3,A5,A4,FUNCT_1:def 4;
end;
end;
definition
let S be finite set, s be FinSequence of S;
func freqSEQ (s) -> FinSequence of NAT means
:Def9:
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;
A1: for k be Nat st k in Seg (card (S)) ex x being Element of NAT st P[k,x ]
proof
A2: rng (canFS(S))= S by FUNCT_2:def 3;
let k be Nat;
assume
A3: k in Seg(card (S));
Seg (len canFS(S))=Seg (card S) by FINSEQ_1:93;
then k in dom (canFS(S)) by A3,FINSEQ_1:def 3;
then (canFS(S)).k is Element of S by A2,FUNCT_1:3;
then consider a be Element of S such that
A4: a=(canFS(S)).k;
reconsider y =(len s)*(FDprobSEQ(s)).k as Real;
take y;
k in dom FDprobSEQ(s) by A3,Def3;
then
A5: y=(len s)*FDprobability(a,s) by A4,Def3;
y is Element of NAT
proof
per cases;
suppose
s={};
hence thesis;
end;
suppose
s<>{};
hence thesis by A5,XCMPLX_1:87;
end;
end;
hence thesis;
end;
consider g be FinSequence of NAT such that
A6: 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(A1);
take g;
thus thesis by A6;
end;
uniqueness
proof
let g,h be FinSequence of NAT;
assume that
A7: dom g =Seg card S and
A8: for n be Nat st n in dom g holds g.n=(len s) * (FDprobSEQ(s)).n;
assume that
A9: dom h =Seg card S and
A10: for n be Nat st n in dom h holds h.n=(len s) * (FDprobSEQ(s)).n;
A11: now
let n be Nat;
assume
A12: n in dom g;
hence g.n =(len s) * (FDprobSEQ(s)).n by A8
.= h.n by A7,A9,A10,A12;
end;
len g =card (S) by A7,FINSEQ_1:def 3
.=len h by A9,FINSEQ_1:def 3;
hence thesis by A11,FINSEQ_2:9;
end;
end;
theorem Th11:
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;
set y =(len s)*(FDprobSEQ(s)).n;
A1: rng canFS S = S by FUNCT_2:def 3;
assume
A2: n in Seg card S;
then
A3: n in dom freqSEQ(s) by Def9;
Seg len canFS S = Seg card S by FINSEQ_1:93;
then n in dom canFS S by A2,FINSEQ_1:def 3;
then (canFS S).n is Element of S by A1,FUNCT_1:3;
then consider a be Element of S such that
A4: a=(canFS S).n;
take a;
n in dom FDprobSEQ(s) by A2,Def3;
then y=(len s)*FDprobability(a,s) by A4,Def3;
then y= frequency(a,s) by XCMPLX_1:87;
hence thesis by A3,A4,Def9;
end;
theorem Th12:
for S be finite set, s be FinSequence of S holds
freqSEQ (s) =(len s)* ((FDprobSEQ(s)))
proof
let S be finite set, s be FinSequence of S;
A1: dom ((len s) (#) ( (FDprobSEQ(s)))) =dom (FDprobSEQ(s)) by VALUED_1:def 5
.=Seg (card (S)) by Def3
.= dom (freqSEQ (s)) by Def9;
now
let m be Nat;
assume
A2: 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,A2,Def9;
end;
hence freqSEQ s = (len s) (#) (FDprobSEQ s) by A1;
end;
theorem Th13:
for S be finite set, s be FinSequence of S holds
Sum (freqSEQ (s))=(len s)* Sum(FDprobSEQ(s))
proof
let S be finite set, s be FinSequence of S;
freqSEQ (s) =(len s)*FDprobSEQ(s) by Th12;
hence thesis by RVSUM_1:87;
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;
set x=s.n;
assume n in dom s;
then x in rng s by FUNCT_1:3;
then x in S;
then x in rng (canFS S) by FUNCT_2:def 3;
then consider m be object such that
A1: m in dom (canFS(S)) and
A2: x=(canFS(S)).m by FUNCT_1:def 3;
reconsider m as Nat by A1;
take m;
Seg len canFS S = Seg card S by FINSEQ_1:93;
then dom canFS S = Seg card S by FINSEQ_1:def 3;
then
ex xx be Element of S st (freqSEQ s).m =frequency(xx,s) & xx=(canFS S).
m by A1,Th11;
hence thesis by A2;
end;
Lm1:
for S being Function, X being set st S is disjoint_valued holds
S|X is disjoint_valued
proof
let S be Function, X be set;
assume A1: S is disjoint_valued;
set SN = S|X;
now
let x,y be object;
assume
A2: 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:47;
hence SN.x misses SN.y by A1,A2,PROB_2:def 2;
end;
suppose
A3: not (x in dom SN & y in dom SN);
now
per cases by A3;
suppose
not x in dom SN;
then SN.x= {} by FUNCT_1:def 2;
then SN.x /\ SN.y = {};
hence SN.x misses SN.y;
end;
suppose
not y in dom SN;
then SN.y= {} by FUNCT_1:def 2;
then SN.x /\ SN.y = {};
hence SN.x misses SN.y;
end;
end;
hence SN.x misses SN.y;
end;
end;
hence thesis by PROB_2:def 2;
end;
Lm2:
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 S is finite & card Union 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 S is finite & card Union S
= Sum L;
A1: now
let n be Nat;
assume
A2: P[n];
now
let S be Function,L be FinSequence of NAT;
assume that
A3: S is disjoint_valued and
A4: dom S = dom L and
A5: n+1 = len L and
A6: for i be Nat st i in dom S holds S.i is finite & L.i = card (S. i);
set SN=S|(Seg n);
reconsider LN=L|n as FinSequence of NAT;
A7: n=len LN by A5,FINSEQ_1:59,NAT_1:12;
now
let x be object;
assume x in Union S;
then consider y be set such that
A8: x in y and
A9: y in rng S by TARSKI:def 4;
consider i be object such that
A10: i in dom S and
A11: y=S.i by A9,FUNCT_1:def 3;
A12: i in Seg (n+1) by A4,A5,A10,FINSEQ_1:def 3;
reconsider i as Element of NAT by A4,A10;
A13: i <= n+1 by A12,FINSEQ_1:1;
A14: 1<=i by A12,FINSEQ_1:1;
now
per cases;
suppose
i=n+1;
hence x in (Union SN) \/ S.(n+1) by A8,A11,XBOOLE_0:def 3;
end;
suppose
i<> n+1;
then i < n+1 by A13,XXREAL_0:1;
then i <= n by NAT_1:13;
then i in Seg n by A14;
then i in dom S /\ Seg n by A10,XBOOLE_0:def 4;
then
A15: i in dom SN by RELAT_1:61;
then S.i = SN.i by FUNCT_1:47;
then y in rng SN by A11,A15,FUNCT_1:def 3;
then x in (Union SN) by A8,TARSKI:def 4;
hence x in (Union SN) \/ S.(n+1) by XBOOLE_0:def 3;
end;
end;
hence x in (Union SN) \/ S.(n+1);
end; then
A16: Union S c= (Union SN) \/ S.(n+1);
A17: (Union SN) \/ S.(n+1) c= Union S
proof
let x be object;
assume
A18: x in (Union SN) \/ S.(n+1);
now
per cases by A18,XBOOLE_0:def 3;
suppose
A19: x in S.(n+1);
n+1 in Seg (n+1) by FINSEQ_1:4;
then n+1 in dom S by A4,A5,FINSEQ_1:def 3;
then S.(n+1) in rng S by FUNCT_1:def 3;
hence x in Union S by A19,TARSKI:def 4;
end;
suppose
x in Union SN;
then consider y be set such that
A20: x in y and
A21: y in rng SN by TARSKI:def 4;
consider i be object such that
A22: i in dom SN and
A23: y=SN.i by A21,FUNCT_1:def 3;
i in dom S /\ Seg n by A22,RELAT_1:61;
then
A24: i in dom S by XBOOLE_0:def 4;
SN.i = S.i by A22,FUNCT_1:47;
then y in rng S by A23,A24,FUNCT_1:def 3;
hence x in (Union S) by A20,TARSKI:def 4;
end;
end;
hence x in Union S;
end;
then
A25: (Union SN) \/ S.(n+1) = Union S by A16;
A26: 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
A27: i in dom SN; then
A28: i in dom S /\ Seg n by RELAT_1:61; then
A29: i in dom S by XBOOLE_0:def 4;
LN.i = L.i by A4,A28,FUNCT_1:48
.= card (S.i) by A6,A29
.= card (SN.i) by A27,FUNCT_1:47;
hence thesis;
end;
A30: SN is disjoint_valued by Lm1,A3;
A31: dom SN = dom S /\ Seg n by RELAT_1:61
.= dom LN by A4,RELAT_1:61;
then
A32: card Union SN = Sum LN by A2,A30,A7,A26;
reconsider USN= Union SN as finite set by A2,A30,A31,A7,A26;
A33: 1<= (n+1) by NAT_1:11;
A34: L= (L|n)^ <* L/.len L *> by A5,FINSEQ_5:21
.=LN^<*L.(n+1)*> by A5,A33,FINSEQ_4:15;
n+1 in Seg (len L) by A5,FINSEQ_1:4;
then
A35: n+1 in dom S by A4,FINSEQ_1:def 3;
then reconsider S1= S.(n+1) as finite set by A6;
Union S = USN \/ S1 by A16,A17;
hence Union S is finite;
for z be set st z in rng SN holds z misses S.(n+1)
proof
let y be set;
assume y in rng SN;
then consider i be object such that
A36: i in dom SN and
A37: y=SN.i by FUNCT_1:def 3;
A38: i in dom S /\ Seg n by A36,RELAT_1:61;
then
A39: i in Seg n by XBOOLE_0:def 4;
reconsider i as Element of NAT by A38;
i <= n by A39,FINSEQ_1:1;
then
A40: i <> n+1 by NAT_1:13;
y=S.i by A36,A37,FUNCT_1:47;
hence thesis by A3,A40,PROB_2:def 2;
end;
then Union SN misses S.(n+1) by ZFMISC_1:80;
then card ((Union SN) \/ S.(n+1) ) =card (USN)+ card (S1) by CARD_2:40;
hence card (Union S ) = Sum LN + L.(n+1) by A6,A35,A32,A25
.= Sum L by A34,RVSUM_1:74;
end;
hence P[n+1];
end;
A41: P[0]
proof
let S be Function,L be FinSequence of NAT;
assume that
S is disjoint_valued and
A42: dom S = dom L and
A43: 0=len L and
for i be Nat st i in dom S holds S.i is finite & L.i = card (S.i);
A44: L= {} by A43;
then S= {} by A42;
then for X be set st X in rng S holds X c= {};
then Union S c= {} by ZFMISC_1:76;
hence Union S is finite & card (Union S) = Sum L by A44,RVSUM_1:72;
end;
thus for n be Nat holds P[n] from NAT_1:sch 2(A41,A1);
end;
theorem Th15:
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 S is finite & card Union S = Sum L
proof
let S be Function,L be FinSequence of NAT;
A1: len L is Element of NAT;
assume 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);
hence thesis by A1,Lm2;
end;
theorem Th16:
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[object,object] means
ex z be Element of S st z=(canFS(S)).$1 & $2 =
event_pick(z,s);
len canFS S = card S by FINSEQ_1:93;
then
A1: dom canFS S = Seg card S by FINSEQ_1:def 3;
A2: for x be object st x in dom L ex y be object st P[x,y]
proof
let x be object;
set z= (canFS S).x;
assume x in dom L; then
A3: x in Seg card S by Def9;
rng canFS S = S by FUNCT_2:def 3;
then reconsider z as Element of S by A1,A3,FUNCT_1:3;
set y=s"{z};
take y;
y=event_pick(z,s);
hence thesis;
end;
consider T be Function such that
A4: dom T = dom L & for x be object st x in dom L holds P[x,T.x] from
CLASSES1:sch 1(A2);
A5: 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 that
A6: a in dom T & b in dom T and
A7: a<>b;
a in dom(canFS S) & b in dom(canFS S) by A1,A4,A6,Def9;
then
A8: (canFS(S)).a<>(canFS(S)).b by A7,FUNCT_1:def 4;
(ex za be Element of S st za=(canFS S).a & T.a=event_pick (za,s) )&
ex zb be Element of S st zb=(canFS S).b & T.b=event_pick (zb,s) by A4,A6;
hence thesis by A8,FUNCT_1:71,ZFMISC_1:11;
end;
for a,b be object st a<>b holds T.a misses T.b
proof
let a,b be object;
assume
A9: a<>b;
per cases;
suppose
a in dom T & b in dom T;
hence thesis by A5,A9;
end;
suppose
not a in dom T;
then T.a={} by FUNCT_1:def 2;
hence thesis;
end;
suppose
a in dom T & not b in dom T;
then T.b={} by FUNCT_1:def 2;
hence thesis;
end;
end; then
A10: T is disjoint_valued by PROB_2:def 2;
A11: Seg len s c= Union T
proof
assume not Seg len s c= Union T;
then consider ne be object such that
A12: ne in Seg len s and
A13: not ne in Union T;
set yne=s.ne;
A14: ne in dom s by A12,FINSEQ_1:def 3;
then yne in rng s by FUNCT_1:def 3;
then reconsider yne as Element of S;
rng canFS S = S by FUNCT_2:def 3;
then consider nne be object such that
A15: nne in dom canFS S and
A16: yne=(canFS S).nne by FUNCT_1:def 3;
A17: nne in dom L by A1,A15,Def9;
then
A18: T.nne in rng T by A4,FUNCT_1:3;
A19: s.ne in {s.ne} by TARSKI:def 1;
ex zne be Element of S st zne=(canFS(S)).nne & T.nne = event_pick(zne,
s) by A4,A17;
then ne in T.nne by A14,A16,A19,FUNCT_1:def 7;
hence contradiction by A13,A18,TARSKI:def 4;
end;
A20: 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
A21: i in dom T;
then
A22: ex zi be Element of S st zi=(canFS(S)).i & T.i=event_pick (zi,s) by A4;
dom L= Seg card S by Def9;
then
A23: i in dom FDprobSEQ s by A4,A21,Def3;
L.i =(len s) * (FDprobSEQ s).i by A4,A21,Def9
.=(len s)*FDprobability((canFS S).i,s) by A23,Def3
.= card (T.i) by A22,XCMPLX_1:87;
hence thesis;
end;
then reconsider T1=Union T as finite set by A4,A10,Th15;
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 object such that
A24: j in dom T and
A25: X =T.j by FUNCT_1:def 3;
ex zj be Element of S st zj=(canFS(S)).j & T.j = event_pick(zj,s)
by A4,A24;
then X c= whole_event(s) by A25;
hence thesis by FINSEQ_1:def 3;
end;
then Union T c= Seg len s by ZFMISC_1:76;
then
A26: T1 = Seg len s by A11;
thus Sum freqSEQ s = card T1 by A4,A10,A20,Th15
.= len s by A26,FINSEQ_1:57;
end;
theorem Th17:
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 Th16;
then (len s)* Sum(FDprobSEQ s) = (len s)*1 by Th13;
hence thesis by XCMPLX_1:5;
end;
registration
let S be non empty finite set, s be non empty FinSequence of S;
cluster FDprobSEQ s -> ProbFinS;
coherence
proof
A1: for i be Nat st i in dom (FDprobSEQ s) holds (FDprobSEQ s).
i>=0
proof
let i be Nat;
assume i in dom FDprobSEQ s;
then (FDprobSEQ s).i =FDprobability((canFS S).i,s) by Def3;
hence thesis;
end;
Sum FDprobSEQ (s) = 1 by Th17;
hence thesis by A1,MATRPROB:def 5;
end;
end;
definition
let S be non empty finite set;
mode distProbFinS of S -> ProbFinS FinSequence of REAL means
:Def10:
len it = card S & ex s be FinSequence of S st FDprobSEQ (s) = it;
existence
proof
set a = the Element of S;
set s=<*a*>;
set p = FDprobSEQ s;
dom p = Seg card S by Def3;
then len p = card S by FINSEQ_1:def 3;
hence thesis;
end;
end;
theorem Th18:
for S be non empty finite set, p be distProbFinS of S holds
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 distribution(p,S) is Element of distribution_family(S);
ex s be FinSequence of S st FDprobSEQ (s)=p by Def10;
hence (GenProbSEQ S).distribution(p,S) = p by Def8;
end;
begin :: Uniform distribution
definition
let S be finite set, s be FinSequence of S;
attr s is uniformly_distributed means
for n be Nat st n in dom FDprobSEQ (s) holds (FDprobSEQ (s)).n=1/(card S);
end;
theorem Th19:
for S be finite set, s be FinSequence of S st
s is uniformly_distributed holds FDprobSEQ (s) is constant
proof
let S be finite set, s be FinSequence of S;
assume
A1: s is uniformly_distributed;
let a,b be object;
assume that
A2: a in dom FDprobSEQ(s) and
A3: b in dom FDprobSEQ(s);
reconsider na=a,nb=b as Nat by A2,A3;
(FDprobSEQ s).na = 1/card S by A1,A2
.= (FDprobSEQ s).nb by A1,A3;
hence thesis;
end;
theorem Th20:
for S be 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 finite set, s,t be FinSequence of S;
assume that
A1: s is uniformly_distributed and
A2: s,t -are_prob_equivalent;
FDprobSEQ s = FDprobSEQ t by A2,Th8;
then
for n be Nat st n in dom FDprobSEQ t holds (FDprobSEQ t).n=1/(card S)
by A1;
hence thesis;
end;
theorem Th21:
for S be 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 finite set, s,t be FinSequence of S;
assume that
A1: s is uniformly_distributed and
A2: t is uniformly_distributed;
A3: dom FDprobSEQ (s)= Seg (card (S)) & dom FDprobSEQ (t)= Seg (card (S)) by
Def3;
for n be object st n in dom FDprobSEQ (s) holds (FDprobSEQ (s)).n=(
FDprobSEQ (t)).n
proof
let n be object;
assume
A4: n in dom FDprobSEQ (s);
then (FDprobSEQ (s)).n= 1/(card S) by A1;
hence thesis by A2,A3,A4;
end;
then FDprobSEQ (s) = FDprobSEQ (t) by A3;
hence thesis by Th8;
end;
registration
let S be finite set;
cluster canFS(S) -> uniformly_distributed for FinSequence of S;
coherence
proof
set s = canFS S;
A1: len s= card S by FINSEQ_1:93;
then dom s= Seg card S by FINSEQ_1:def 3;
then
A2: dom s=dom FDprobSEQ (s) by Def3;
for n be Nat st n in dom s holds (FDprobSEQ (s)).n=1/(card S)
proof
let n be Nat;
assume
A3: n in dom s;
then (FDprobSEQ s).n=FDprobability(s.n,s) by A2,Def3
.= card ({n}) /(len s) by A3,FINSEQ_5:4
.= 1/(card S) by A1,CARD_1:30;
hence thesis;
end;
hence thesis by A2;
end;
end;
Lm3: for S be finite set, s be FinSequence of S st s in
Finseq-EQclass canFS S holds s is uniformly_distributed
by Th5,Th20;
Lm4: for S be 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 finite set, s be FinSequence of S;
assume
A1: s is uniformly_distributed;
let t be FinSequence of S;
assume t is uniformly_distributed;
then s,t -are_prob_equivalent by A1,Th21;
hence thesis;
end;
definition
let S be finite set;
func uniform_distribution(S) -> Element of distribution_family(S) means
:Def12:
for s be FinSequence of S holds s in it iff s is uniformly_distributed;
existence
proof
set s=canFS S;
consider CS be non empty Subset of S* such that
A1: CS=Finseq-EQclass(s);
reconsider CS as Element of distribution_family(S) by A1,Def6;
take CS;
for t be FinSequence of S st t in CS holds s,t -are_prob_equivalent by A1
,Th5;
then
for t be FinSequence of S st t in CS holds t is uniformly_distributed
by Th20;
hence thesis by A1,Lm4;
end;
uniqueness
proof
let A,B be Element of distribution_family(S);
assume
A2: for s be FinSequence of S holds s in A iff s is uniformly_distributed;
assume
A3: for s be FinSequence of S holds s in B iff s is uniformly_distributed;
A4: for s be object st s in B holds s in A
proof
let s be object;
assume
A5: s in B;
then reconsider s as Element of S*;
s is uniformly_distributed by A3,A5;
hence thesis by A2;
end;
for s be object st s in A holds s in B
proof
let s be object;
assume
A6: s in A;
then reconsider s as Element of S*;
s is uniformly_distributed by A2,A6;
hence thesis by A3;
end;
hence thesis by A4,TARSKI:2;
end;
end;
registration
let S be non empty finite set;
cluster constant for distProbFinS of S;
existence
proof
reconsider s=canFS S as Element of S* by FINSEQ_1:def 11;
take p= FDprobSEQ s;
dom p= Seg card S by Def3;
then len p=card S by FINSEQ_1:def 3;
hence thesis by Def10,Th19;
end;
end;
definition
let S be non empty finite set;
func Uniform_FDprobSEQ(S) -> distProbFinS of S equals
FDprobSEQ canFS S;
coherence
proof
reconsider s=canFS S as Element of S* by FINSEQ_1:def 11;
set p = FDprobSEQ s;
dom p = Seg card S by Def3;
then len p=card S by FINSEQ_1:def 3;
hence thesis by Def10;
end;
end;
registration
let S be non empty finite set;
cluster Uniform_FDprobSEQ(S) -> constant;
coherence by Th19;
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);
A1: 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 Th21;
hence thesis;
end;
(for t be FinSequence of S st t in Finseq-EQclass(s) holds t
is uniformly_distributed)&
Finseq-EQclass(s) is Element of distribution_family S by Def6,Lm3; then
A2: Finseq-EQclass(s)=uniform_distribution(S) by A1,Def12;
(GenProbSEQ S).(Finseq-EQclass s) = p by Th10;
then
A3: (GenProbSEQ S).distribution(p,S) = (GenProbSEQ S).(Finseq-EQclass s)
by Th18;
dom GenProbSEQ S = distribution_family(S) by FUNCT_2:def 1;
hence thesis by A2,A3,FUNCT_1:def 4;
end;