:: Probability on Finite and Discrete Set and Uniform Distribution
::  by Hiroyuki Okazaki
::
:: Received May 5, 2009
:: Copyright (c) 2009-2012 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, NUMBERS,
      XXREAL_0, BINOP_2, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
      FINSEQ_1, FINSEQ_2, VALUED_1, FUNCT_2, ORDINAL1, SETFAM_1, RPR_1, PROB_2,
      RVSUM_1, UPROOTS, MATRPROB;
 constructors RPR_1, RVSUM_1, SEQ_1, BINOP_2, PARTFUN3, PROB_2, UPROOTS,
      MATRPROB, RELSET_1;
 registrations FUNCT_1, SUBSET_1, NAT_1, XREAL_0, XXREAL_0, ORDINAL1, UPROOTS,
      FINSEQ_1, RELAT_1, XBOOLE_0, FINSET_1, NUMBERS, VALUED_0, VALUED_1,
      CARD_1, MATRPROB, ENTROPY1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, RPR_1, FINSEQ_1, RELAT_1, FUNCT_1, CARD_3, XBOOLE_0;
 theorems 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_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;

theorem Th1:
  for S be set, s be FinSequence of S holds whole_event (s) = s"S
proof
  let S be set, s be FinSequence of S;
  s"S c= s"rng s & s"rng s c= s"S by RELAT_1:135,143;
  then s"rng s = s"S by XBOOLE_0:def 10;
  hence thesis by RELAT_1:134;
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;

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 Th1;
  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;

theorem Th3:
  for S be set, s be FinSequence of S holds card whole_event(s) = len s
proof
  let S be set, s be FinSequence of S;
  thus card whole_event(s)= card Seg len s by FINSEQ_1:def 3
    .= len s by FINSEQ_1:57;
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;

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,set] 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];
    consider g be FinSequence of REAL such that
A2: 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 A2;
  end;
  uniqueness
  proof
    let g,h be FinSequence of REAL;
    assume that
A3: dom g =Seg card S and
A4: for n be Nat st n in dom g holds g.n=FDprobability((canFS(S)).n,s);
    assume that
A5: dom h =Seg card S and
A6: for n be Nat st n in dom h holds h.n=FDprobability((canFS(S)).n,s);
A7: now
      let n be Nat;
      assume
A8:   n in dom g;
      hence g.n = FDprobability((canFS(S)).n,s) by A4
        .= h.n by A3,A5,A6,A8;
    end;
    len g = card S by A3,FINSEQ_1:def 3
      .= len h by A5,FINSEQ_1:def 3;
    hence thesis by A7,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 Th3;

definition
  let S be finite set, s,t be FinSequence of S;
  pred s,t -are_prob_equivalent means
  :Def4:
  for x be set holds FDprobability (x,s)=FDprobability (x,t);
  reflexivity;
  symmetry;
end;

theorem Th6:
  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,Def4
    .=FDprobability (x,u) by A2,Def4;
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 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;
  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 Th7:
  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 Th8:
  for S be finite set, s be FinSequence of S holds s in Finseq-EQclass(s);

theorem Th9:
  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
A2: 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 set;
      assume x in Finseq-EQclass(t);
      then consider u be FinSequence of S such that
A3:   x=u and
A4:   t,u -are_prob_equivalent;
      s,u -are_prob_equivalent by A2,A4,Th6;
      hence x in Finseq-EQclass(s) by A3;
    end;
      let x be set;
      assume x in Finseq-EQclass(s);
      then consider u be FinSequence of S such that
A6:   x=u and
A7:   s,u -are_prob_equivalent;
      t,u -are_prob_equivalent by A2,A7,Th6;
      hence x in Finseq-EQclass(t) by A6;
  end;
  end;
    assume Finseq-EQclass(t) = Finseq-EQclass(s);
    then t in Finseq-EQclass(s);
    hence t,s -are_prob_equivalent by Th7;
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
A2: for A being Subset of S* holds A in F1 iff P[A] and
A3: for A being Subset of S* holds A in F2 iff P[A];
    thus thesis from SUBSET_1:sch 4(A2,A3);
  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 Th10:
  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 set 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 UPROOTS:3;
        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 by Def4;
  end;
  now
    assume
A13: s,t -are_prob_equivalent;
A14: 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 A13,Def4;
    end;
    dom FDprobSEQ t = Seg card S by Def3;
    hence FDprobSEQ s = FDprobSEQ t by A14,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 Th10;
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,Th8;
    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,Th7;
      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,Th7;
      then t,s -are_prob_equivalent by A9,Th6;
      hence g.x = h.x by A11,A8,Th10;
    end;
    hence thesis by FUNCT_2:def 8;
  end;
end;

theorem Th12:
  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,Th7;
  hence thesis by A2,Th10;
end;

registration
  let S be finite set;
  cluster GenProbSEQ S -> one-to-one;
  coherence
  proof
  now
    let x1,x2 be set;
    assume that
A1: x1 in distribution_family(S) and
A2: x2 in distribution_family(S) and
A3: (GenProbSEQ (S)).x1 =(GenProbSEQ (S)).x2;
    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 x2 and
A7: (GenProbSEQ (S)).x2 =FDprobSEQ (v) by A2,Def7;
    consider u be FinSequence of S such that
A8: u in x1 and
A9: (GenProbSEQ (S)).x1 =FDprobSEQ (u) by A1,Def7;
A10: u,v -are_prob_equivalent by A3,A9,A7,Th10;
    u1,u -are_prob_equivalent by A8,A4,Th7;
    then
A11: u1,v -are_prob_equivalent by A10,Th6;
    v,u2 -are_prob_equivalent by A6,A5,Th7;
    then u1,u2 -are_prob_equivalent by A11,Th6;
    hence x1=x2 by A4,A5,Th9;
  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,Th12;
  end;
  uniqueness
  proof
    let CS1,CS2 be Element of distribution_family(S);
    assume
A4: (GenProbSEQ S).CS1 = p; then
A5: CS1 in dom (GenProbSEQ (S)) by FUNCT_1:def 2;
    assume
A6: (GenProbSEQ S).CS2 = p;
    then CS2 in dom (GenProbSEQ (S)) by FUNCT_1:def 2;
    hence thesis by A4,A6,A5,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 UPROOTS:3;
      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;
      set y =(len s)*(FDprobSEQ(s)).k;
      take y;
      k in dom FDprobSEQ(s) by A3,Def3;
      then
A6:   y=(len s)*FDprobability(a,s) by A4,Def3;
      y is Element of NAT
      proof
        per cases;
        suppose
          s={};
          hence thesis by A6;
        end;
        suppose
          s<>{};
          hence thesis by A6,XCMPLX_1:87;
        end;
      end;
      hence thesis;
    end;
    consider g be FinSequence of NAT such that
A7: 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 A7;
  end;
  uniqueness
  proof
    let g,h be FinSequence of NAT;
    assume that
A8: dom g =Seg card S and
A9: for n be Nat st n in dom g holds g.n=(len s) * (FDprobSEQ(s)).n;
    assume that
A10: dom h =Seg card S and
A11: for n be Nat st n in dom h holds h.n=(len s) * (FDprobSEQ(s)).n;
A12: now
      let n be Nat;
      assume
A13:  n in dom g;
      hence g.n =(len s) * (FDprobSEQ(s)).n by A9
        .= h.n by A8,A10,A11,A13;
    end;
    len g =card (S) by A8,FINSEQ_1:def 3
      .=len h by A10,FINSEQ_1:def 3;
    hence thesis by A12,FINSEQ_2:9;
  end;
end;

theorem Th13:
  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;
A2: rng canFS S = S by FUNCT_2:def 3;
  assume
A3: n in Seg card S;
  then
A4: n in dom freqSEQ(s) by Def9;
  Seg len canFS S = Seg card S by UPROOTS:3;
  then n in dom canFS S by A3,FINSEQ_1:def 3;
  then (canFS S).n is Element of S by A2,FUNCT_1:3;
  then consider a be Element of S such that
A5: a=(canFS S).n;
  take a;
  n in dom FDprobSEQ(s) by A3,Def3;
  then y=(len s)*FDprobability(a,s) by A5,Def3;
  then y= frequency(a,s) by XCMPLX_1:87;
  hence thesis by A4,A5,Def9;
end;

theorem Th14:
  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,FINSEQ_1:13;
end;

theorem Th15:
  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 Th14;
  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 set 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 UPROOTS:3;
  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,Th13;
  hence thesis by A2;
end;

Lem1:
  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 A3: S is disjoint_valued;
    set SN = S|X;
      now
        let x,y be set;
        assume
A30:    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 A3,A30,PROB_2:def 2;
        end;
        suppose
A31:      not (x in dom SN & y in dom SN);
          now
            per cases by A31;
            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 by XBOOLE_0:def 7;
            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 by XBOOLE_0:def 7;
            end;
          end;
          hence SN.x misses SN.y;
        end;
  end;
  hence thesis by PROB_2:def 2;
  end;

Th17:
  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 set;
        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 set 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) by TARSKI:def 3;
A17:  (Union SN) \/ S.(n+1) c= Union S
      proof
        let x be set;
        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 set 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,XBOOLE_0:def 10;
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;
A32:  SN is disjoint_valued by Lem1,A3;
A33:  dom SN = dom S /\ Seg n by RELAT_1:61
        .= dom LN by A4,RELAT_1:61;
      then
A34:  card Union SN = Sum LN by A2,A32,A7,A26;
      reconsider USN= Union SN as finite set by A2,A32,A33,A7,A26;
A35:  1<= (n+1) by NAT_1:11;
A36:  L= (L|n)^ <* L/.len L *> by A5,FINSEQ_5:21
        .=LN^<*L.(n+1)*> by A5,A35,FINSEQ_4:15;
      n+1 in Seg (len L) by A5,FINSEQ_1:4;
      then
A37:  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,XBOOLE_0:def 10;
      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 set such that
A38:    i in dom SN and
A39:    y=SN.i by FUNCT_1:def 3;
A40:    i in dom S /\ Seg n by A38,RELAT_1:61;
        then
A41:    i in Seg n by XBOOLE_0:def 4;
        reconsider i as Element of NAT by A40;
        i <= n by A41,FINSEQ_1:1;
        then
A42:    i <> n+1 by NAT_1:13;
        y=S.i by A38,A39,FUNCT_1:47;
        hence thesis by A3,A42,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,A37,A34,A25
        .= Sum L by A36,RVSUM_1:74;
    end;
    hence P[n+1];
  end;
A43: P[0]
  proof
    let S be Function,L be FinSequence of NAT;
    assume that
    S is disjoint_valued and
A44: dom S = dom L and
A45: 0=len L and
    for i be Nat st i in dom S holds S.i is finite & L.i = card (S.i);
A46: L= {} by A45;
    then S= {} by A44;
    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 A46,RVSUM_1:72;
  end;
  thus for n be Nat holds P[n] from NAT_1:sch 2(A43,A1);
end;

theorem Th18:
  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,Th17;
end;

theorem Th19:
  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:3;
  then
A1: dom canFS S = Seg card S by FINSEQ_1:def 3;
A2: for x be set st x in dom L ex y be set st P[x,y]
  proof
    let x be set;
    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
A5: dom T = dom L & for x be set st x in dom L holds P[x,T.x] from
     CLASSES1:sch 1(A2);
A6: 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
A7: a in dom T & b in dom T and
A8: a<>b;
    a in dom(canFS S) & b in dom(canFS S) by A1,A5,A7,Def9;
    then
A9: (canFS(S)).a<>(canFS(S)).b by A8,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 A5,A7;
    hence thesis by A9,FUNCT_1:71,ZFMISC_1:11;
  end;
  for a,b be set st a<>b holds T.a misses T.b
  proof
    let a,b be set;
    assume
A10: a<>b;
      per cases;
      suppose
        a in dom T & b in dom T;
        hence thesis by A6,A10;
      end;
      suppose
        not a in dom T;
        then T.a={} by FUNCT_1:def 2;
        hence thesis by XBOOLE_1:65;
      end;
      suppose
        a in dom T & not b in dom T;
        then T.b={} by FUNCT_1:def 2;
        hence thesis by XBOOLE_1:65;
      end;
  end; then
A11: T is disjoint_valued by PROB_2:def 2;
A12: Seg len s c= Union T
  proof
    assume not Seg len s c= Union T;
    then consider ne be set such that
A13: ne in Seg len s and
A14: not ne in Union T by TARSKI:def 3;
    set yne=s.ne;
A15: ne in dom s by A13,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 set such that
A16: nne in dom canFS S and
A17: yne=(canFS S).nne by FUNCT_1:def 3;
A18: nne in dom L by A1,A16,Def9;
    then
A19: T.nne in rng T by A5,FUNCT_1:3;
A20: 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 A5,A18;
    then ne in T.nne by A15,A17,A20,FUNCT_1:def 7;
    hence contradiction by A14,A19,TARSKI:def 4;
  end;
A21: 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
A22: i in dom T;
    then
A23: ex zi be Element of S st zi=(canFS(S)).i & T.i=event_pick (zi,s) by A5;
    dom L= Seg card S by Def9;
    then
A24: i in dom FDprobSEQ s by A5,A22,Def3;
    L.i =(len s) * (FDprobSEQ s).i by A5,A22,Def9
      .=(len s)*FDprobability((canFS S).i,s) by A24,Def3
      .= card (T.i) by A23,XCMPLX_1:87;
    hence thesis;
  end;
  then reconsider T1=Union T as finite set by A5,A11,Th18;
  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
A25: j in dom T and
A26: 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 A5,A25;
    then X c= whole_event(s) by A26;
    hence thesis by FINSEQ_1:def 3;
  end;
  then Union T c= Seg len s by ZFMISC_1:76;
  then
A27: T1 = Seg len s by A12,XBOOLE_0:def 10;
  thus Sum freqSEQ s = card T1 by A5,A11,A21,Th18
    .= len s by A27,FINSEQ_1:57;
end;

theorem Th20:
  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 Th19;
  then (len s)* Sum(FDprobSEQ s) = (len s)*1 by Th15;
  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 Element of NAT st i in dom (FDprobSEQ s) holds (FDprobSEQ s).
    i>=0
    proof
      let i be Element of 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 Th20;
    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 Th22:
  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
  :Def11:
  for n be Nat st n in dom FDprobSEQ (s) holds (FDprobSEQ (s)).n=1/(card S);
end;

theorem Th23:
  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 set;
  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,Def11
    .= (FDprobSEQ s).nb by A1,A3,Def11;
  hence thesis;
end;

theorem Th24:
  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,Th10;
  then
  for n be Nat st n in dom FDprobSEQ t holds (FDprobSEQ t).n=1/(card S)
  by A1,Def11;
  hence thesis by Def11;
end;

theorem Th25:
  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 set st n in dom FDprobSEQ (s) holds (FDprobSEQ (s)).n=(
  FDprobSEQ (t)).n
  proof
    let n be set;
    assume
A4: n in dom FDprobSEQ (s);
    then (FDprobSEQ (s)).n= 1/(card S) by A1,Def11;
    hence thesis by A2,A3,A4,Def11;
  end;
  then FDprobSEQ (s) = FDprobSEQ (t) by A3,FUNCT_1:2;
  hence thesis by Th10;
end;

registration
  let S be finite set;
  cluster canFS(S) -> uniformly_distributed;
  coherence
  proof
    set s = canFS S;
A1: len s= card S by UPROOTS:3;
    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,Def11;
  end;
end;

Lm2: for S be finite set, s be FinSequence of S st s in
Finseq-EQclass canFS S holds s is uniformly_distributed
proof
  let S be finite set, s be FinSequence of S;
  assume s in Finseq-EQclass canFS S;
  then s,canFS(S) -are_prob_equivalent by Th7;
  hence thesis by Th24;
end;

Lm3: 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,Th25;
    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
A2: CS=Finseq-EQclass(s);
    reconsider CS as Element of distribution_family(S) by A2,Def6;
    take CS;
    for t be FinSequence of S st t in CS holds s,t -are_prob_equivalent by A2
,Th7;
    then
    for t be FinSequence of S st t in CS holds t is uniformly_distributed
    by Th24;
    hence thesis by A2,Lm3;
  end;
  uniqueness
  proof
    let A,B be Element of distribution_family(S);
    assume
A4: for s be FinSequence of S holds s in A iff s is uniformly_distributed;
    assume
A5: for s be FinSequence of S holds s in B iff s is uniformly_distributed;
A6: for s be set st s in B holds s in A
    proof
      let s be set;
      assume
A7:   s in B;
      then reconsider s as Element of S*;
      s is uniformly_distributed by A5,A7;
      hence thesis by A4;
    end;
    for s be set st s in A holds s in B
    proof
      let s be set;
      assume
A8:   s in A;
      then reconsider s as Element of S*;
      s is uniformly_distributed by A4,A8;
      hence thesis by A5;
    end;
    hence thesis by A6,TARSKI:1;
  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,Th23;
  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 Th23;
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);
A2: 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 Th25;
    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,Lm2; then
A3: Finseq-EQclass(s)=uniform_distribution(S) by A2,Def12;
  (GenProbSEQ S).(Finseq-EQclass s) = p by Th12;
  then
A4: (GenProbSEQ S).distribution(p,S) = (GenProbSEQ S).(Finseq-EQclass s)
    by Th22;
  dom GenProbSEQ S = distribution_family(S) by FUNCT_2:def 1;
  hence thesis by A3,A4,FUNCT_1:def 4;
end;