:: Probability on Finite and Discrete Set and Uniform Distribution :: by Hiroyuki Okazaki :: :: Received May 5, 2009 :: Copyright (c) 2009-2018 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, XXREAL_0, ORDINAL1, FINSEQ_1, RELAT_1, FINSET_1, NUMBERS, VALUED_0, VALUED_1, 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); 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;