dist_1.miz



    begin

    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;

      :: original: event_pick

      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;

      :: DIST_1:def1

      func frequency (x,s) -> Nat equals ( card ( event_pick (x,s)));

      correctness ;

    end

    ::$Canceled

    theorem :: DIST_1:2

    for S be set, s be FinSequence of S, e be set st e in ( whole_event s) holds 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;

      :: DIST_1:def2

      func FDprobability (x,s) -> Real equals (( frequency (x,s)) / ( len s));

      correctness ;

    end

    ::$Canceled

    theorem :: DIST_1:4

    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;

      :: DIST_1:def3

      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)) holds ex x be Element of REAL st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( card S));

          consider x be 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 :: DIST_1:5

    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;

      :: DIST_1:def4

      pred s,t -are_prob_equivalent means for x be set holds ( FDprobability (x,s)) = ( FDprobability (x,t));

      reflexivity ;

      symmetry ;

    end

    theorem :: DIST_1:6

    

     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;

      :: DIST_1:def5

      func Finseq-EQclass (s) -> Subset of (S * ) equals { t where t be FinSequence of S : (s,t) -are_prob_equivalent };

      correctness

      proof

        { t where t be FinSequence of S : (s,t) -are_prob_equivalent } c= (S * )

        proof

          let x be object;

          assume x in { t where t be 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 :: DIST_1:7

    

     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 :: DIST_1:8

    

     Th6: for S be finite set, s be FinSequence of S holds s in ( Finseq-EQclass s);

    theorem :: DIST_1:9

    

     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 be FinSequence of S st $1 = ( Finseq-EQclass u);

      :: DIST_1:def6

      func distribution_family (S) -> Subset-Family of (S * ) means

      : Def6: for A be Subset of (S * ) holds A in it iff ex s be FinSequence of S st A = ( Finseq-EQclass s);

      existence

      proof

        ex T be Subset-Family of (S * ) st for A be 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 be Subset of (S * ) holds A in F1 iff P[A] and

         A2: for A be 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 :: DIST_1:10

    

     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 :: DIST_1:11

    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;

      :: DIST_1:def7

      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 be Element of ( distribution_family S) holds ex y be Element of ( REAL * ) st P[x, y]

        proof

          let x be Element of ( distribution_family S);

          consider s be 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 be 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 be 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 :: DIST_1:12

    

     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 be FinSequence of S such that

           A4: x1 = ( Finseq-EQclass u1) by A1, Def6;

          consider u2 be 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;

      :: DIST_1:def8

      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;

      :: DIST_1:def9

      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)) holds ex x be 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 :: DIST_1:13

    

     Th11: for S be non empty finite set, s be non empty FinSequence of S, n be Nat st n in ( Seg ( card S)) holds 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 :: DIST_1:14

    

     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 :: DIST_1:15

    

     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 :: DIST_1:16

    for S be non empty finite set, s be non empty FinSequence of S, n be Nat st n in ( dom s) holds 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 be Function, X be 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 :: DIST_1:17

    

     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 :: DIST_1:18

    

     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) holds 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 :: DIST_1:19

    

     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;

      :: DIST_1:def10

      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 :: DIST_1:20

    

     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

    definition

      let S be finite set, s be FinSequence of S;

      :: DIST_1:def11

      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 :: DIST_1:21

    

     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 :: DIST_1:22

    

     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 :: DIST_1:23

    

     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;

      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;

      :: DIST_1:def12

      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;

      :: DIST_1:def13

      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 :: DIST_1:24

    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;