dist_2.miz



    begin

    theorem :: DIST_2:1

    for Y be non empty finite set, s be FinSequence of Y st Y = {1} & s = <*1*> holds ( FDprobSEQ s) = <*1*>

    proof

      let Y be non empty finite set, s be FinSequence of Y;

      assume

       A1: Y = {1} & s = <*1*>;

      

       A2: ( dom s) = {1} & (s . 1) = 1 by A1, FINSEQ_1: 2, FINSEQ_1:def 8;

      

       A3: ( len s) = 1 & ( card Y) = 1 by A1, CARD_1: 30;

      

       A4: ( dom s) = ( Seg ( card Y)) by A2, A1, CARD_1: 30, FINSEQ_1: 2;

      ( rng s) = {1} by A1, FINSEQ_1: 39;

      then

       A5: 1 in ( rng s) by TARSKI:def 1;

      

       A6: ( FDprobability ((( canFS Y) . 1),s)) = ( FDprobability (( <*1*> . 1),s)) by A1, FINSEQ_1: 94

      .= ( FDprobability (1,s)) by FINSEQ_1:def 8

      .= 1 by A1, A5, A3, FINSEQ_4: 73;

      for n be Nat st n in ( dom s) holds (s . n) = ( FDprobability ((( canFS Y) . n),s))

      proof

        let n be Nat;

        assume n in ( dom s);

        then n = 1 by A2, TARSKI:def 1;

        hence thesis by A6, A1, FINSEQ_1:def 8;

      end;

      hence thesis by A4, A1, DIST_1:def 3;

    end;

    theorem :: DIST_2:2

    for S be non empty finite set, p be distProbFinS of S, s be FinSequence of S st ( FDprobSEQ s) = p holds ( distribution (p,S)) = ( Finseq-EQclass s) & s in ( distribution (p,S))

    proof

      let S be non empty finite set, p be distProbFinS of S, s be FinSequence of S;

      assume

       A1: ( FDprobSEQ s) = p;

      set D = ( Finseq-EQclass s);

      reconsider D as Element of ( distribution_family S) by DIST_1:def 6;

      (( GenProbSEQ S) . ( Finseq-EQclass s)) = p by A1, DIST_1: 12;

      then D = ( distribution (p,S)) by A1, DIST_1:def 8;

      hence thesis;

    end;

    theorem :: DIST_2:3

    

     Th3: for S be non empty finite set, x be Element of S holds x in ( rng ( canFS S)) & ex n be Nat st n in ( dom ( canFS S)) & x = (( canFS S) . n) & n in ( Seg ( card S))

    proof

      let S be non empty finite set, x be Element of S;

      

       A1: x in S;

      then x in ( rng ( canFS S)) by FUNCT_2:def 3;

      then

      consider n be object such that

       A2: n in ( dom ( canFS S)) & x = (( canFS S) . n) by FUNCT_1:def 3;

      reconsider n as Nat by A2;

      ( len ( canFS S)) = ( card S) by FINSEQ_1: 93;

      then n in ( Seg ( card S)) by A2, FINSEQ_1:def 3;

      hence thesis by A2, A1, FUNCT_2:def 3;

    end;

    

     Lm1: for S be non empty finite set, A be Element of ( distribution_family S) holds A is non empty

    proof

      let S be non empty finite set, A be Element of ( distribution_family S);

      ex s be FinSequence of S st A = ( Finseq-EQclass s) by DIST_1:def 6;

      hence thesis;

    end;

    registration

      let S be non empty finite set;

      cluster -> non empty for Element of ( distribution_family S);

      coherence by Lm1;

    end

    definition

      let S be non empty finite set, D be Element of ( distribution_family S);

      :: original: Element

      redefine

      mode Element of D -> FinSequence of S ;

      coherence

      proof

        let x be Element of D;

        x is Element of (S * );

        hence thesis;

      end;

    end

    theorem :: DIST_2:4

    

     Th4: for S be non empty finite set, D be Element of ( distribution_family S), s,t be Element of D holds (s,t) -are_prob_equivalent

    proof

      let S be non empty finite set, D be Element of ( distribution_family S), s,t be Element of D;

      consider x be FinSequence of S such that

       A1: D = ( Finseq-EQclass x) by DIST_1:def 6;

      (s,x) -are_prob_equivalent & (x,t) -are_prob_equivalent by A1, DIST_1: 7;

      hence thesis by DIST_1: 6;

    end;

    notation

      let S be non empty finite set, D be Element of ( distribution_family S);

      synonym D is well-distributed for D is with_non-empty_elements;

    end

    theorem :: DIST_2:5

    

     Th5: for S be non empty finite set, s be FinSequence of S holds (for x be set holds ( FDprobability (x,s)) = 0 ) iff s is empty

    proof

      for S be non empty finite set, s be FinSequence of S holds (for x be set holds ( FDprobability (x,s)) = 0 ) implies s is empty

      proof

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

        assume

         A1: for x be set holds ( FDprobability (x,s)) = 0 ;

        assume

         A2: not s is empty;

        1 in ( dom s) by A2, FINSEQ_5: 6;

        then

         A3: (s . 1) in ( rng s) by FUNCT_1: 3;

        then

        reconsider y = (s . 1) as Element of S;

        

         A4: (s " {y}) <> {} by A3, FUNCT_1: 72;

        ( FDprobability (y,s)) = 0 by A1;

        hence contradiction by A4, A2;

      end;

      hence thesis;

    end;

    registration

      let S be non empty finite set;

      cluster well-distributed for Element of ( distribution_family S);

      existence

      proof

        set x = the Element of S;

        reconsider sx = <*x*> as FinSequence of S;

        reconsider sx as Element of (S * ) by FINSEQ_1:def 11;

        reconsider Dx = ( Finseq-EQclass sx) as Element of ( distribution_family S) by DIST_1:def 6;

        reconsider z = {} as Element of (S * ) by FINSEQ_1: 49;

         not {} in Dx

        proof

          assume {} in Dx;

          then

          reconsider z = {} as Element of Dx;

          

           A1: ( len sx) = 1 & ( rng sx) = {x} by FINSEQ_1: 39;

          ( len sx) = ( card ( rng sx)) by A1, CARD_1: 30;

          then

           A2: sx is one-to-one by FINSEQ_4: 62;

          

           A3: x in ( rng sx) by A1, TARSKI:def 1;

          ( FDprobability (x,sx)) = ( FDprobability (x,z)) by DIST_1:def 4, DIST_1: 7;

          hence contradiction by A3, A1, A2, FINSEQ_4: 73;

        end;

        then Dx is well-distributed by SETFAM_1:def 8;

        hence thesis;

      end;

    end

    theorem :: DIST_2:6

    

     Th6: for S be non empty finite set, D be Element of ( distribution_family S) holds not D is well-distributed iff D = {( <*> S)}

    proof

      let S be non empty finite set, D be Element of ( distribution_family S);

      thus not D is well-distributed implies D = {( <*> S)}

      proof

        assume not D is well-distributed;

        then

        reconsider o = {} as Element of D by SETFAM_1:def 8;

        

         A1: for s be Element of D holds s in {( <*> S)} & s = ( <*> S)

        proof

          let s be Element of D;

          for x be set holds ( FDprobability (x,s)) = 0

          proof

            let x be set;

            ( FDprobability (x,s)) = ( FDprobability (x,o)) by Th4, DIST_1:def 4;

            hence thesis;

          end;

          then s is empty by Th5;

          hence thesis by TARSKI:def 1;

        end;

        then

         A2: for z be object st z in D holds z in {( <*> S)};

        for z be object st z in {( <*> S)} holds z in D

        proof

          let z be object;

          assume

           A3: z in {( <*> S)};

          z is Element of D

          proof

            assume

             A4: not z is Element of D;

            set t = the Element of D;

            t = ( <*> S) by A1;

            hence contradiction by A4, A3, TARSKI:def 1;

          end;

          hence thesis;

        end;

        hence thesis by A2, TARSKI: 2;

      end;

      assume

       A5: D = {( <*> S)};

      assume

       A6: D is well-distributed;

      set s = the Element of D;

      s = {} by A5, TARSKI:def 1;

      hence contradiction by A6;

    end;

    definition

      let S be non empty finite set;

      mode EqSampleSpaces of S is well-distributed Element of ( distribution_family S);

    end

    registration

      let S be non empty finite set;

      cluster ( uniform_distribution S) -> well-distributed;

      coherence

      proof

        

         A1: ( canFS S) in ( uniform_distribution S) by DIST_1:def 12;

        ( uniform_distribution S) <> {( <*> S)} by A1, TARSKI:def 1;

        hence thesis by Th6;

      end;

    end

    theorem :: DIST_2:7

    

     Th7: for S be non empty finite set, D be EqSampleSpaces of S holds (( GenProbSEQ S) . D) is distProbFinS of S

    proof

      let S be non empty finite set, D be well-distributed Element of ( distribution_family S);

      set s = the Element of D;

      reconsider p = ( FDprobSEQ s) as ProbFinS FinSequence of REAL ;

      ( dom p) = ( Seg ( card S)) by DIST_1:def 3;

      then ( len p) = ( card S) by FINSEQ_1:def 3;

      then

       A1: p is distProbFinS of S by DIST_1:def 10;

      consider t be FinSequence of S such that

       A2: D = ( Finseq-EQclass t) by DIST_1:def 6;

      D = ( Finseq-EQclass s) by A2, DIST_1: 9, DIST_1: 7;

      hence thesis by A1, DIST_1: 12;

    end;

    begin

    definition

      let S be non empty finite set, a be Element of S;

      :: DIST_2:def1

      func index (a) -> Element of NAT equals (a .. ( canFS S));

      correctness ;

    end

    definition

      let S be non empty finite set, D be EqSampleSpaces of S;

      :: DIST_2:def2

      func ProbFinS_of D -> distProbFinS of S equals (( GenProbSEQ S) . D);

      correctness by Th7;

    end

    definition

      let judgefunc be BOOLEAN -valued Function;

      :: DIST_2:def3

      func trueEVENT (judgefunc) -> Event of ( dom judgefunc) equals (judgefunc " { TRUE });

      coherence

      proof

        for x be object holds x in (judgefunc " { TRUE }) implies x in ( dom judgefunc) by FUNCT_1:def 7;

        hence thesis by TARSKI:def 3;

      end;

    end

    theorem :: DIST_2:8

    

     Th8: for S be non empty finite set, f be S -valued Function, judgefunc be Function of S, BOOLEAN holds ( trueEVENT (judgefunc * f)) is Event of ( dom f)

    proof

      let S be non empty finite set, f be S -valued Function, judgefunc be Function of S, BOOLEAN ;

      for x be object st x in ( dom (judgefunc * f)) holds x in ( dom f) by FUNCT_1: 11;

      then ( dom (judgefunc * f)) c= ( dom f) by TARSKI:def 3;

      hence thesis by XBOOLE_1: 1;

    end;

    definition

      let S be non empty finite set, D be EqSampleSpaces of S, s be Element of D, judgefunc be Function of S, BOOLEAN ;

      :: DIST_2:def4

      func Prob (judgefunc,s) -> Real equals (( card ( trueEVENT (judgefunc * s))) / ( len s));

      correctness ;

    end

    theorem :: DIST_2:9

    for S be non empty finite set, D be EqSampleSpaces of S, s be Element of D, judgefunc be Function of S, BOOLEAN , F be non empty finite set, E be Event of F st F = ( dom s) & E = ( trueEVENT (judgefunc * s)) holds ( Prob (judgefunc,s)) = ( prob E)

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, s be Element of D, judgefunc be Function of S, BOOLEAN , F be non empty finite set, E be Event of F;

      assume

       A1: F = ( dom s) & E = ( trueEVENT (judgefunc * s));

      

      then ( card F) = ( card ( Seg ( len s))) by FINSEQ_1:def 3

      .= ( len s) by FINSEQ_1: 57;

      hence thesis by A1;

    end;

    theorem :: DIST_2:10

    

     Th10: for S be non empty finite set, D be EqSampleSpaces of S, a be Element of S, s be Element of D, judgefunc be Function of S, BOOLEAN st (for x be set holds x = a iff (judgefunc . x) = TRUE ) holds ( Prob (judgefunc,s)) = ( FDprobability (a,s))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, a be Element of S, s be Element of D, judgefunc be Function of S, BOOLEAN ;

      assume

       A1: for x be set holds x = a iff (judgefunc . x) = TRUE ;

      

       A2: for n be set holds n in (s " {a}) iff n in ( dom s) & (s . n) = a

      proof

        let n be set;

        n in (s " {a}) iff n in ( dom s) & (s . n) in {a} by FUNCT_1:def 7;

        hence thesis by TARSKI:def 1;

      end;

      

       A3: for x be object holds x in ((judgefunc * s) " { TRUE }) implies x in (s " {a})

      proof

        let x be object;

        assume x in ((judgefunc * s) " { TRUE });

        then

         A4: x in ( dom (judgefunc * s)) & ((judgefunc * s) . x) in { TRUE } by FUNCT_1:def 7;

        then ((judgefunc * s) . x) = TRUE by TARSKI:def 1;

        then

         A5: x in ( dom s) & (judgefunc . (s . x)) = TRUE by A4, FUNCT_1: 11, FUNCT_1: 12;

        then (s . x) = a by A1;

        then (s . x) in {a} by TARSKI:def 1;

        hence thesis by A5, FUNCT_1:def 7;

      end;

      for x be object holds x in (s " {a}) implies x in ((judgefunc * s) " { TRUE })

      proof

        let x be object;

        assume

         A6: x in (s " {a});

        then

         A7: x in ( dom s) & (s . x) = a by A2;

        (s . x) in S by A7;

        then

         A8: (s . x) in ( dom judgefunc) by FUNCT_2:def 1;

        (judgefunc . (s . x)) = TRUE by A6, A2, A1;

        then ((judgefunc * s) . x) = TRUE by A6, A2, FUNCT_1: 13;

        then

         A9: ((judgefunc * s) . x) in { TRUE } by TARSKI:def 1;

        x in ( dom (judgefunc * s)) by A7, A8, FUNCT_1: 11;

        hence thesis by A9, FUNCT_1:def 7;

      end;

      hence thesis by A3, TARSKI: 2;

    end;

    definition

      let S be set, s be FinSequence of S, A be Subset of ( dom s);

      :: DIST_2:def5

      func extract (s,A) -> FinSequence of S equals (s * ( canFS A));

      coherence

      proof

        

         A1: ( rng (s * ( canFS A))) c= S;

        ( rng ( canFS A)) c= A by FINSEQ_1:def 4;

        then (s * ( canFS A)) is FinSequence by FINSEQ_1: 16, XBOOLE_1: 1;

        hence thesis by A1, FINSEQ_1:def 4;

      end;

    end

    theorem :: DIST_2:11

    

     Th11: for S be set, s be FinSequence of S, A be Subset of ( dom s) holds ( len ( extract (s,A))) = ( card A) & for i be Nat st i in ( dom ( extract (s,A))) holds (( extract (s,A)) . i) = (s . (( canFS A) . i))

    proof

      let S be set, s be FinSequence of S, A be Subset of ( dom s);

      ( rng ( canFS A)) c= A by FINSEQ_1:def 4;

      

      then ( len ( extract (s,A))) = ( len ( canFS A)) by FINSEQ_2: 29, XBOOLE_1: 1

      .= ( card A) by FINSEQ_1: 93;

      hence thesis by FUNCT_1: 12;

    end;

    theorem :: DIST_2:12

    

     Th12: for S be non empty finite set, s be FinSequence of S, A be Subset of ( dom s), f be Function st f = ( canFS A) holds (( extract (s,A)) * (f " )) = (s | A)

    proof

      let S be non empty finite set, s be FinSequence of S, A be Subset of ( dom s), f be Function;

      assume

       A1: f = ( canFS A);

      

       A2: (f * (f " )) = ( id ( rng f)) by A1, FUNCT_1: 39

      .= ( id A) by A1, FUNCT_2:def 3;

      

       A3: ( dom (s | A)) = (( dom s) /\ A) by RELAT_1: 61

      .= ( dom (s * ( id A))) by FUNCT_1: 19;

      now

        let x be object;

        assume

         A4: x in ( dom (s | A));

        then

         A5: x in (( dom s) /\ A) by RELAT_1: 61;

        

        thus ((s | A) . x) = (s . x) by A4, FUNCT_1: 47

        .= ((s * ( id A)) . x) by A5, FUNCT_1: 20;

      end;

      then

       A6: (s * ( id A)) = (s | A) by A3, FUNCT_1: 2;

      thus (( extract (s,A)) * (f " )) = (s | A) by A6, A2, A1, RELAT_1: 36;

    end;

    theorem :: DIST_2:13

    

     Th13: for S be non empty finite set, f be S -valued Function, judgefunc be Function of S, BOOLEAN , n be set st n in ( dom f) holds n in ( trueEVENT (judgefunc * f)) iff (f . n) in ( trueEVENT judgefunc)

    proof

      let S be non empty finite set, f be S -valued Function, judgefunc be Function of S, BOOLEAN , n be set;

      assume

       A1: n in ( dom f);

      

       A2: ( trueEVENT (judgefunc * f)) is Subset of ( dom f) by Th8;

      thus n in ( trueEVENT (judgefunc * f)) implies (f . n) in ( trueEVENT judgefunc)

      proof

        assume

         A3: n in ( trueEVENT (judgefunc * f));

        then ((judgefunc * f) . n) in { TRUE } by FUNCT_1:def 7;

        then

         A4: ((judgefunc * f) . n) = TRUE by TARSKI:def 1;

        (judgefunc . (f . n)) = TRUE by A4, A3, A2, FUNCT_1: 13;

        then

         A5: (judgefunc . (f . n)) in { TRUE } by TARSKI:def 1;

        (f . n) in ( rng f) by A3, A2, FUNCT_1:def 3;

        then (f . n) in S;

        then (f . n) in ( dom judgefunc) by FUNCT_2:def 1;

        hence thesis by A5, FUNCT_1:def 7;

      end;

      assume

       A6: (f . n) in ( trueEVENT judgefunc);

      

       A7: (f . n) in ( dom judgefunc) & (judgefunc . (f . n)) in { TRUE } by A6, FUNCT_1:def 7;

      

       A8: ((judgefunc * f) . n) in { TRUE } by A7, A1, FUNCT_1: 13;

      n in ( dom (judgefunc * f)) by A1, A6, FUNCT_1: 11;

      hence thesis by A8, FUNCT_1:def 7;

    end;

    theorem :: DIST_2:14

    

     Th14: for S be non empty finite set, f be S -valued Function, judgefunc be Function of S, BOOLEAN holds ( trueEVENT (judgefunc * f)) = (f " ( trueEVENT judgefunc))

    proof

      let S be non empty finite set, f be S -valued Function, judgefunc be Function of S, BOOLEAN ;

      

       A1: ( trueEVENT (judgefunc * f)) is Subset of ( dom f) by Th8;

      for x be object holds x in (f " ( trueEVENT judgefunc)) iff x in ( trueEVENT (judgefunc * f))

      proof

        let x be object;

        thus x in (f " ( trueEVENT judgefunc)) implies x in ( trueEVENT (judgefunc * f))

        proof

          assume x in (f " ( trueEVENT judgefunc));

          then x in ( dom f) & (f . x) in ( trueEVENT judgefunc) by FUNCT_1:def 7;

          hence thesis by Th13;

        end;

        assume

         A2: x in ( trueEVENT (judgefunc * f));

        (f . x) in ( trueEVENT judgefunc) by Th13, A2, A1;

        hence thesis by A1, A2, FUNCT_1:def 7;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: DIST_2:15

    

     Th15: for S be non empty finite set, D be EqSampleSpaces of S, s be Element of D, judgefunc be Function of S, BOOLEAN holds ex A be Subset of ( dom ( freqSEQ s)) st A = ( trueEVENT (judgefunc * ( canFS S))) & ( card ( trueEVENT (judgefunc * s))) = ( Sum ( extract (( freqSEQ s),A)))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, s be Element of D, judgefunc be Function of S, BOOLEAN ;

      ( len ( canFS S)) = ( card S) by FINSEQ_1: 93;

      then

       A1: ( dom ( canFS S)) = ( Seg ( card S)) by FINSEQ_1:def 3;

      

       A2: ( trueEVENT (judgefunc * ( canFS S))) is Event of ( dom ( canFS S)) by Th8;

      reconsider A = ( trueEVENT (judgefunc * ( canFS S))) as Subset of ( dom ( freqSEQ s)) by A1, A2, DIST_1:def 9;

      

       A3: ( len ( extract (( freqSEQ s),A))) = ( card A) by Th11;

      set L = ( extract (( freqSEQ s),A));

      

       A4: ( dom L) = ( Seg ( card A)) by A3, FINSEQ_1:def 3;

      defpred P[ object, object] means ex z be Element of S st z = (( canFS S) . (( canFS A) . $1)) & $2 = ( event_pick (z,s));

      ( len ( canFS A)) = ( card A) by FINSEQ_1: 93;

      then

       A5: ( dom ( canFS A)) = ( Seg ( card A)) by FINSEQ_1:def 3;

      

       A6: for x,y1,y2 be object st x in ( dom L) & P[x, y1] & P[x, y2] holds y1 = y2;

      

       A7: for x be object st x in ( dom L) holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in ( dom L);

        then

         A8: x in ( Seg ( card A)) by A3, FINSEQ_1:def 3;

        set z = (( canFS S) . (( canFS A) . x));

        ( rng ( canFS A)) = A by FUNCT_2:def 3;

        then

         A9: (( canFS A) . x) in A by A5, A8, FUNCT_1: 3;

        ( rng ( canFS S)) = S by FUNCT_2:def 3;

        then

        reconsider z as Element of S by A9, A2, FUNCT_1: 3;

        set y = (s " {z});

        

         A10: y = ( event_pick (z,s));

        take y;

        thus thesis by A10;

      end;

      consider G be Function such that

       A11: ( dom G) = ( dom L) & for x be object st x in ( dom L) holds P[x, (G . x)] from FUNCT_1:sch 2( A6, A7);

      

       A12: for a,b be set st a in ( dom G) & b in ( dom G) & a <> b holds (G . a) misses (G . b)

      proof

        let a,b be set;

        assume

         A13: a in ( dom G) & b in ( dom G) & a <> b;

        then

         A14: a in ( dom ( canFS A)) & b in ( dom ( canFS A)) by A3, A5, A11, FINSEQ_1:def 3;

        ( rng ( canFS A)) = A by FUNCT_2:def 3;

        then

         A15: (( canFS A) . a) in A & (( canFS A) . b) in A by A14, FUNCT_1: 3;

        (( canFS A) . a) <> (( canFS A) . b) by A14, A13, FUNCT_1:def 4;

        then

         A16: (( canFS S) . (( canFS A) . a)) <> (( canFS S) . (( canFS A) . b)) by A15, A2, FUNCT_1:def 4;

        consider za be Element of S such that

         A17: za = (( canFS S) . (( canFS A) . a)) & (G . a) = ( event_pick (za,s)) by A11, A13;

        consider zb be Element of S such that

         A18: zb = (( canFS S) . (( canFS A) . b)) & (G . b) = ( event_pick (zb,s)) by A11, A13;

        thus thesis by A17, A18, A16, FUNCT_1: 71, ZFMISC_1: 11;

      end;

      

       A19: for i be Nat st i in ( dom G) holds (G . i) is finite & (L . i) = ( card (G . i))

      proof

        let i be Nat;

        assume

         A20: i in ( dom G);

        then

        consider zi be Element of S such that

         A21: zi = (( canFS S) . (( canFS A) . i)) & (G . i) = ( event_pick (zi,s)) by A11;

        

         A22: i in ( dom ( canFS A)) by A3, A5, A11, A20, FINSEQ_1:def 3;

        ( rng ( canFS A)) = A by FUNCT_2:def 3;

        then

         A23: (( canFS A) . i) in A by A22, FUNCT_1: 3;

        then

         A24: (( canFS A) . i) in ( Seg ( card S)) by A2, A1;

        

         A25: (( canFS A) . i) in ( dom ( FDprobSEQ s)) by A24, DIST_1:def 3;

        (L . i) = (( freqSEQ s) . (( canFS A) . i)) by A20, A11, Th11

        .= (( len s) * (( FDprobSEQ s) . (( canFS A) . i))) by A23, DIST_1:def 9

        .= (( len s) * ( FDprobability ((( canFS S) . (( canFS A) . i)),s))) by A25, DIST_1:def 3

        .= ( card (G . i)) by A21, XCMPLX_1: 87;

        hence thesis;

      end;

      for a,b be object st a <> b holds (G . a) misses (G . b)

      proof

        let a,b be object;

        assume

         A26: a <> b;

        per cases ;

          suppose a in ( dom G) & b in ( dom G);

          hence thesis by A12, A26;

        end;

          suppose not a in ( dom G);

          then (G . a) = {} by FUNCT_1:def 2;

          hence thesis by XBOOLE_1: 65;

        end;

          suppose a in ( dom G) & not b in ( dom G);

          then (G . b) = {} by FUNCT_1:def 2;

          hence thesis by XBOOLE_1: 65;

        end;

      end;

      then

       A27: G is disjoint_valued by PROB_2:def 2;

      for X be set st X in ( rng G) holds X c= ( trueEVENT (judgefunc * s))

      proof

        let X be set;

        assume X in ( rng G);

        then

        consider j be object such that

         A28: j in ( dom G) & X = (G . j) by FUNCT_1:def 3;

        consider zj be Element of S such that

         A29: zj = (( canFS S) . (( canFS A) . j)) & (G . j) = ( event_pick (zj,s)) by A11, A28;

        zj in ( trueEVENT judgefunc)

        proof

          j in ( dom ( canFS A)) by A28, A5, A11, A3, FINSEQ_1:def 3;

          then (( canFS A) . j) in ( rng ( canFS A)) by FUNCT_1: 3;

          then (( canFS A) . j) in A by FUNCT_2:def 3;

          hence thesis by Th13, A29, A2;

        end;

        then for x be object st x in {zj} holds x in ( trueEVENT judgefunc) by TARSKI:def 1;

        then (s " {zj}) c= (s " ( trueEVENT judgefunc)) by RELAT_1: 143, TARSKI:def 3;

        hence thesis by A28, A29, Th14;

      end;

      then

       A30: ( union ( rng G)) c= ( trueEVENT (judgefunc * s)) by ZFMISC_1: 76;

      for x be object st x in ( trueEVENT (judgefunc * s)) holds x in ( union ( rng G))

      proof

        let x be object;

        assume

         A31: x in ( trueEVENT (judgefunc * s));

        

         A32: ( trueEVENT (judgefunc * s)) is Event of ( dom s) by Th8;

        reconsider n = x as Nat by A31;

        

         A33: (s . n) in ( trueEVENT judgefunc) by A32, Th13, A31;

        

         A34: ( trueEVENT judgefunc) c= S

        proof

          ( dom judgefunc) = S by FUNCT_2:def 1;

          hence thesis;

        end;

        ex m be Nat st m in ( Seg ( card S)) & (s . n) = (( canFS S) . m)

        proof

          (s . n) in ( rng ( canFS S)) & ex m be Nat st m in ( dom ( canFS S)) & (s . n) = (( canFS S) . m) & m in ( Seg ( card S)) by Th3, A34, A33;

          hence thesis;

        end;

        then

        consider m be Nat such that

         A35: m in ( Seg ( card S)) & (s . n) = (( canFS S) . m);

        reconsider D0 = ( uniform_distribution S) as EqSampleSpaces of S;

        ( len ( canFS S)) = ( card S) by FINSEQ_1: 93;

        then

         A36: m in ( dom ( canFS S)) by A35, FINSEQ_1:def 3;

        

         A37: m in ( trueEVENT (judgefunc * ( canFS S))) by A36, Th13, A33, A35;

        ex k be Nat st k in ( Seg ( card A)) & m = (( canFS A) . k)

        proof

          reconsider m as Element of A by A36, Th13, A33, A35;

          m in ( rng ( canFS A)) & ex k be Nat st k in ( dom ( canFS A)) & m = (( canFS A) . k) & k in ( Seg ( card A)) by Th3, A37;

          hence thesis;

        end;

        then

        consider k be Nat such that

         A38: k in ( Seg ( card A)) & m = (( canFS A) . k);

        (s . n) in {(( canFS S) . (( canFS A) . k))} by A35, A38, TARSKI:def 1;

        then

         A39: n in (s " {(( canFS S) . (( canFS A) . k))}) by A32, A31, FUNCT_1:def 7;

        consider z be Element of S such that

         A40: z = (( canFS S) . (( canFS A) . k)) & (G . k) = ( event_pick (z,s)) by A38, A11, A4;

        ( dom G) = ( Seg ( card A)) by A11, A3, FINSEQ_1:def 3;

        then (G . k) c= ( union ( rng G)) by A38, FUNCT_1: 3, ZFMISC_1: 74;

        hence x in ( union ( rng G)) by A39, A40;

      end;

      then ( trueEVENT (judgefunc * s)) c= ( union ( rng G)) by TARSKI:def 3;

      then

       A41: ( union ( rng G)) = ( trueEVENT (judgefunc * s)) by A30, XBOOLE_0:def 10;

      ( card ( Union G)) = ( Sum L) by A11, A19, A27, DIST_1: 17;

      hence thesis by A41;

    end;

    theorem :: DIST_2:16

    

     Th16: for S be non empty finite set, D be EqSampleSpaces of S, s be Element of D holds ( freqSEQ s) = (( len s) (#) ( FDprobSEQ s))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, s be Element of D;

      ( dom ( freqSEQ s)) = ( Seg ( card S)) by DIST_1:def 9;

      then

       A1: ( dom ( freqSEQ s)) = ( dom ( FDprobSEQ s)) by DIST_1:def 3;

      for n be object st n in ( dom ( freqSEQ s)) holds (( freqSEQ s) . n) = (( len s) * (( FDprobSEQ s) . n)) by DIST_1:def 9;

      hence thesis by A1, VALUED_1:def 5;

    end;

    theorem :: DIST_2:17

    

     Th17: for S be non empty finite set, D be EqSampleSpaces of S, s,t be Element of D, judgefunc be Function of S, BOOLEAN holds ( Prob (judgefunc,s)) = ( Prob (judgefunc,t))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, s,t be Element of D, judgefunc be Function of S, BOOLEAN ;

      consider A be Subset of ( dom ( freqSEQ s)) such that

       A1: A = ( trueEVENT (judgefunc * ( canFS S))) & ( card ( trueEVENT (judgefunc * s))) = ( Sum ( extract (( freqSEQ s),A))) by Th15;

      consider B be Subset of ( dom ( freqSEQ t)) such that

       A2: B = ( trueEVENT (judgefunc * ( canFS S))) & ( card ( trueEVENT (judgefunc * t))) = ( Sum ( extract (( freqSEQ t),B))) by Th15;

      consider v be FinSequence of S such that

       A3: D = ( Finseq-EQclass v) by DIST_1:def 6;

      A c= ( dom ( freqSEQ s));

      then

       A4: A c= ( Seg ( card S)) by DIST_1:def 9;

      then

       A5: A c= ( dom ( FDprobSEQ s)) by DIST_1:def 3;

      reconsider A0 = A as Subset of ( dom ( FDprobSEQ s)) by A4, DIST_1:def 3;

      reconsider A1 = A as Subset of ( dom (( len s) (#) ( FDprobSEQ s))) by A5, VALUED_1:def 5;

      B c= ( dom ( freqSEQ t));

      then

       A6: B c= ( Seg ( card S)) by DIST_1:def 9;

      then

       A7: B c= ( dom ( FDprobSEQ t)) by DIST_1:def 3;

      reconsider B0 = B as Subset of ( dom ( FDprobSEQ t)) by A6, DIST_1:def 3;

      reconsider B1 = B as Subset of ( dom (( len t) (#) ( FDprobSEQ t))) by A7, VALUED_1:def 5;

      

       A8: (v,s) -are_prob_equivalent by A3, DIST_1: 7;

      (v,t) -are_prob_equivalent by A3, DIST_1: 7;

      then

       A9: ( FDprobSEQ s) = ( FDprobSEQ t) by DIST_1: 10, A8, DIST_1: 6;

      

       A10: ( freqSEQ s) = (( len s) (#) ( FDprobSEQ s)) by Th16;

      

       A11: ( freqSEQ t) = (( len t) (#) ( FDprobSEQ t)) by Th16;

      

       A12: ( extract ((( len s) * ( FDprobSEQ s)),A1)) = (( len s) * ( extract (( FDprobSEQ s),A0)))

      proof

        ( len ( extract ((( len s) * ( FDprobSEQ s)),A1))) = ( card A1) by Th11;

        then

         A13: ( dom ( extract ((( len s) * ( FDprobSEQ s)),A1))) = ( Seg ( card A)) by FINSEQ_1:def 3;

        ( len ( extract (( FDprobSEQ s),A0))) = ( card A0) by Th11;

        then

         A14: ( dom ( extract ((( len s) * ( FDprobSEQ s)),A1))) = ( dom ( extract (( FDprobSEQ s),A0))) by A13, FINSEQ_1:def 3;

        for c be object st c in ( dom ( extract ((( len s) * ( FDprobSEQ s)),A1))) holds (( extract ((( len s) * ( FDprobSEQ s)),A1)) . c) = (( len s) * (( extract (( FDprobSEQ s),A0)) . c))

        proof

          let c be object;

          assume

           A15: c in ( dom ( extract ((( len s) * ( FDprobSEQ s)),A1)));

          

          then

           A16: (( extract ((( len s) * ( FDprobSEQ s)),A1)) . c) = ((( len s) * ( FDprobSEQ s)) . (( canFS A1) . c)) by Th11

          .= (( freqSEQ s) . (( canFS A) . c)) by DIST_1: 14;

          ( len ( canFS A)) = ( card A) by FINSEQ_1: 93;

          then

           A17: ( dom ( canFS A)) = ( Seg ( card A)) by FINSEQ_1:def 3;

          (( canFS A) . c) in ( rng ( canFS A)) by A17, A15, A13, FUNCT_1: 3;

          then

           A18: (( canFS A) . c) in A by FUNCT_2:def 3;

          (( extract (( FDprobSEQ s),A0)) . c) = (( FDprobSEQ s) . (( canFS A) . c)) by Th11, A14, A15;

          hence thesis by A16, A18, DIST_1:def 9;

        end;

        hence thesis by A14, VALUED_1:def 5;

      end;

      

       A19: ( extract ((( len t) * ( FDprobSEQ t)),B1)) = (( len t) * ( extract (( FDprobSEQ t),B0)))

      proof

        ( len ( extract ((( len t) * ( FDprobSEQ t)),B1))) = ( card B1) by Th11;

        then

         A20: ( dom ( extract ((( len t) * ( FDprobSEQ t)),B1))) = ( Seg ( card B)) by FINSEQ_1:def 3;

        ( len ( extract (( FDprobSEQ t),B0))) = ( card B0) by Th11;

        then

         A21: ( dom ( extract ((( len t) * ( FDprobSEQ t)),B1))) = ( dom ( extract (( FDprobSEQ t),B0))) by A20, FINSEQ_1:def 3;

        for c be object st c in ( dom ( extract ((( len t) * ( FDprobSEQ t)),B1))) holds (( extract ((( len t) * ( FDprobSEQ t)),B1)) . c) = (( len t) * (( extract (( FDprobSEQ t),B0)) . c))

        proof

          let c be object;

          assume

           A22: c in ( dom ( extract ((( len t) * ( FDprobSEQ t)),B1)));

          

          then

           A23: (( extract ((( len t) * ( FDprobSEQ t)),B1)) . c) = ((( len t) * ( FDprobSEQ t)) . (( canFS B1) . c)) by Th11

          .= (( freqSEQ t) . (( canFS B) . c)) by DIST_1: 14;

          ( len ( canFS B)) = ( card B) by FINSEQ_1: 93;

          then

           A24: ( dom ( canFS B)) = ( Seg ( card B)) by FINSEQ_1:def 3;

          (( canFS B) . c) in ( rng ( canFS B)) by A24, A22, A20, FUNCT_1: 3;

          then

           A25: (( canFS B) . c) in B by FUNCT_2:def 3;

          (( len t) * (( extract (( FDprobSEQ t),B0)) . c)) = (( len t) * (( FDprobSEQ t) . (( canFS B) . c))) by Th11, A21, A22

          .= (( freqSEQ t) . (( canFS B) . c)) by A25, DIST_1:def 9;

          hence thesis by A23;

        end;

        hence thesis by A21, VALUED_1:def 5;

      end;

      

       A26: ( card ( trueEVENT (judgefunc * s))) = (( len s) * ( Sum ( extract (( FDprobSEQ s),A0)))) by A12, A1, A10, RVSUM_1: 87;

      

       A27: ( card ( trueEVENT (judgefunc * t))) = (( len t) * ( Sum ( extract (( FDprobSEQ t),B0)))) by A19, A11, A2, RVSUM_1: 87;

      

      thus ( Prob (judgefunc,s)) = ( Sum ( extract (( FDprobSEQ s),A0))) by A26, XCMPLX_1: 89

      .= ( Prob (judgefunc,t)) by A27, A9, A1, A2, XCMPLX_1: 89;

    end;

    definition

      let S be non empty finite set, D be EqSampleSpaces of S, judgefunc be Function of S, BOOLEAN ;

      :: DIST_2:def6

      func Prob (judgefunc,D) -> Real means

      : Def6: for s be Element of D holds it = ( Prob (judgefunc,s));

      existence

      proof

        set s = the Element of D;

        take ( Prob (judgefunc,s));

        thus thesis by Th17;

      end;

      uniqueness

      proof

        let a,b be Real;

        defpred P[ Real] means for s be Element of D holds $1 = ( Prob (judgefunc,s));

        assume

         A1: P[a];

        assume

         A2: P[b];

        now

          let s be Element of D;

          (a = ( Prob (judgefunc,s)) & b = ( Prob (judgefunc,s))) by A1, A2;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: DIST_2:18

    

     Th18: for S be non empty finite set, s be Element of (S * ), judgefunc be Function of S, BOOLEAN holds ( Coim ((judgefunc * s), TRUE )) in ( bool ( dom s))

    proof

      let S be non empty finite set, s be Element of (S * ), judgefunc be Function of S, BOOLEAN ;

      reconsider s0 = s as FinSequence of S;

      ( rng s0) c= S;

      then ( rng s0) c= ( dom judgefunc) by FUNCT_2:def 1;

      then

       A1: ( dom (judgefunc * s0)) = ( dom s0) by RELAT_1: 27;

      for x be object st x in ( Coim ((judgefunc * s), TRUE )) holds x in ( dom s) by A1, FUNCT_1:def 7;

      then ( Coim ((judgefunc * s), TRUE )) c= ( dom s) by TARSKI:def 3;

      hence thesis;

    end;

    definition

      let S be set, SS be Subset of S;

      :: DIST_2:def7

      func MembershipDecision (SS) -> Function of S, BOOLEAN equals ( chi (SS,S));

      coherence by MARGREL1:def 11;

    end

    theorem :: DIST_2:19

    for S be non empty finite set, BS be Subset of S holds ex judgefunc be Function of S, BOOLEAN st ( Coim (judgefunc, TRUE )) = BS

    proof

      let S be non empty finite set, BS be Subset of S;

      reconsider f = ( chi (BS,S)) as Function of S, BOOLEAN by MARGREL1:def 11;

      

       A1: ( dom f) = S by FUNCT_2:def 1;

      

       A2: for x be object holds x in BS iff x in ( Coim (f, TRUE ))

      proof

        let x be object;

        

         A3: x in BS implies (f . x) in { TRUE }

        proof

          assume

           A4: x in BS;

          (f . x) = TRUE by A4, FUNCT_3:def 3;

          hence thesis by TARSKI:def 1;

        end;

        (f . x) in { TRUE } implies x in BS

        proof

          assume (f . x) in { TRUE };

          then (f . x) = TRUE by TARSKI:def 1;

          hence thesis by FUNCT_3: 36;

        end;

        hence thesis by A3, A1, FUNCT_1:def 7;

      end;

      take f;

      thus thesis by A2, TARSKI: 2;

    end;

    theorem :: DIST_2:20

    for S be non empty finite set, s be Element of (S * ), f be Function of S, BOOLEAN , F be SigmaField of ( dom s) st F = ( bool ( dom s)) holds ( Coim ((f * s), TRUE )) is Event of F by Th18;

    

     Lm2: for p,q be boolean-valued Function, x be set st x in (( dom p) /\ ( dom q)) holds ((p 'or' q) . x) = TRUE iff (p . x) = TRUE or (q . x) = TRUE

    proof

      let p,q be boolean-valued Function, x be set;

      assume

       A1: x in (( dom p) /\ ( dom q));

      

       A2: x in ( dom (p 'or' q)) by A1, BVFUNC_1:def 2;

      then

       A3: ((p 'or' q) . x) = ((p . x) 'or' (q . x)) by BVFUNC_1:def 2;

      hereby

        assume ((p 'or' q) . x) = TRUE ;

        then ((p . x) 'or' (q . x)) = TRUE by A2, BVFUNC_1:def 2;

        then ( 'not' (p . x)) = FALSE or ( 'not' (q . x)) = FALSE ;

        hence (p . x) = TRUE or (q . x) = TRUE ;

      end;

      assume (p . x) = TRUE or (q . x) = TRUE ;

      hence ((p 'or' q) . x) = TRUE by A3;

    end;

    

     Lm3: for p,q be boolean-valued Function, x be set st x in (( dom p) /\ ( dom q)) holds ((p '&' q) . x) = TRUE iff (p . x) = TRUE & (q . x) = TRUE

    proof

      let p,q be boolean-valued Function, x be set;

      assume

       A1: x in (( dom p) /\ ( dom q));

      x in ( dom (p '&' q)) by A1, MARGREL1:def 18;

      then ((p '&' q) . x) = ((p . x) '&' (q . x)) by MARGREL1:def 18;

      hence thesis by MARGREL1: 12;

    end;

    

     Lm4: for p be boolean-valued Function, x be set st x in ( dom p) holds (( 'not' p) . x) = TRUE iff (p . x) = FALSE

    proof

      let p be boolean-valued Function, x be set;

      assume x in ( dom p);

      then (( 'not' p) . x) = ( 'not' (p . x)) by MARGREL1:def 17;

      hence thesis;

    end;

    theorem :: DIST_2:21

    

     Th21: for S be non empty finite set, s be Element of (S * ), f,g be Function of S, BOOLEAN holds ( Coim (((f 'or' g) * s), TRUE )) = (( Coim ((f * s), TRUE )) \/ ( Coim ((g * s), TRUE )))

    proof

      let S be non empty finite set, s be Element of (S * ), f,g be Function of S, BOOLEAN ;

       A1:

      now

        let x be object;

        

         A2: ( dom f) = S & ( dom g) = S by FUNCT_2:def 1;

        

         A3: x in ( dom (f 'or' g)) iff x in (( dom f) /\ ( dom g)) by BVFUNC_1:def 2;

        

         A4: x in ((f 'or' g) " { TRUE }) iff x in ( dom (f 'or' g)) & ((f 'or' g) . x) in { TRUE } by FUNCT_1:def 7;

        x in ( dom (f 'or' g)) & ((f 'or' g) . x) = TRUE iff x in (( dom f) /\ ( dom g)) & ((f . x) = TRUE or (g . x) = TRUE ) by Lm2, A3;

        then x in ((f 'or' g) " { TRUE }) iff ((x in ( dom f)) & ((f . x) in { TRUE })) or ((x in ( dom g)) & ((g . x) = TRUE )) by A4, A2, TARSKI:def 1;

        then x in ((f 'or' g) " { TRUE }) iff x in (f " { TRUE }) or ((x in ( dom g)) & ((g . x) in { TRUE })) by FUNCT_1:def 7, TARSKI:def 1;

        then x in ((f 'or' g) " { TRUE }) iff x in (f " { TRUE }) or x in (g " { TRUE }) by FUNCT_1:def 7;

        hence x in ((f 'or' g) " { TRUE }) iff x in ((f " { TRUE }) \/ (g " { TRUE })) by XBOOLE_0:def 3;

      end;

      

      thus ( Coim (((f 'or' g) * s), TRUE )) = (s " ((f 'or' g) " { TRUE })) by RELAT_1: 146

      .= (s " ((f " { TRUE }) \/ (g " { TRUE }))) by A1, TARSKI: 2

      .= ((s " (f " { TRUE })) \/ (s " (g " { TRUE }))) by RELAT_1: 140

      .= (((f * s) " { TRUE }) \/ (s " (g " { TRUE }))) by RELAT_1: 146

      .= (( Coim ((f * s), TRUE )) \/ ( Coim ((g * s), TRUE ))) by RELAT_1: 146;

    end;

    theorem :: DIST_2:22

    

     Th22: for S be non empty finite set, s be Element of (S * ), f,g be Function of S, BOOLEAN holds ( Coim (((f '&' g) * s), TRUE )) = (( Coim ((f * s), TRUE )) /\ ( Coim ((g * s), TRUE )))

    proof

      let S be non empty finite set, s be Element of (S * ), f,g be Function of S, BOOLEAN ;

       A1:

      now

        let x be object;

        

         A2: ( dom f) = S & ( dom g) = S by FUNCT_2:def 1;

        

         A3: x in ( dom (f '&' g)) iff x in (( dom f) /\ ( dom g)) by MARGREL1:def 18;

        

         A4: x in ((f '&' g) " { TRUE }) iff x in ( dom (f '&' g)) & ((f '&' g) . x) in { TRUE } by FUNCT_1:def 7;

        x in ( dom (f '&' g)) & ((f '&' g) . x) = TRUE iff x in (( dom f) /\ ( dom g)) & ((f . x) = TRUE & (g . x) = TRUE ) by Lm3, A3;

        then x in ((f '&' g) " { TRUE }) iff ((x in ( dom f)) & ((f . x) in { TRUE })) & ((x in ( dom g)) & ((g . x) = TRUE )) by A4, A2, TARSKI:def 1;

        then x in ((f '&' g) " { TRUE }) iff x in (f " { TRUE }) & ((x in ( dom g)) & ((g . x) in { TRUE })) by FUNCT_1:def 7, TARSKI:def 1;

        then x in ((f '&' g) " { TRUE }) iff x in (f " { TRUE }) & x in (g " { TRUE }) by FUNCT_1:def 7;

        hence x in ((f '&' g) " { TRUE }) iff x in ((f " { TRUE }) /\ (g " { TRUE })) by XBOOLE_0:def 4;

      end;

      

       A5: (s " ((f " { TRUE }) /\ (g " { TRUE }))) c= ((s " (f " { TRUE })) /\ (s " (g " { TRUE }))) by RELAT_1: 141;

      for x be object st x in ((s " (f " { TRUE })) /\ (s " (g " { TRUE }))) holds x in (s " ((f " { TRUE }) /\ (g " { TRUE })))

      proof

        let x be object;

        assume

         A6: x in ((s " (f " { TRUE })) /\ (s " (g " { TRUE })));

        assume

         A7: not x in (s " ((f " { TRUE }) /\ (g " { TRUE })));

        x in (s " (f " { TRUE })) & x in (s " (g " { TRUE })) by A6, XBOOLE_0:def 4;

        then

         A8: x in ( dom s) & (s . x) in (f " { TRUE }) & (s . x) in (g " { TRUE }) by FUNCT_1:def 7;

        then

        reconsider y = (s . x) as Element of S;

         not y in ((f " { TRUE }) /\ (g " { TRUE })) by A7, A8, FUNCT_1:def 7;

        hence contradiction by A8, XBOOLE_0:def 4;

      end;

      then

       A9: ((s " (f " { TRUE })) /\ (s " (g " { TRUE }))) c= (s " ((f " { TRUE }) /\ (g " { TRUE }))) by TARSKI:def 3;

      

      thus ( Coim (((f '&' g) * s), TRUE )) = (s " ((f '&' g) " { TRUE })) by RELAT_1: 146

      .= (s " ((f " { TRUE }) /\ (g " { TRUE }))) by A1, TARSKI: 2

      .= ((s " (f " { TRUE })) /\ (s " (g " { TRUE }))) by A9, A5, XBOOLE_0:def 10

      .= (((f * s) " { TRUE }) /\ (s " (g " { TRUE }))) by RELAT_1: 146

      .= (( Coim ((f * s), TRUE )) /\ ( Coim ((g * s), TRUE ))) by RELAT_1: 146;

    end;

    theorem :: DIST_2:23

    

     Th23: for S be non empty finite set, s be Element of (S * ), f be Function of S, BOOLEAN holds ( Coim ((( 'not' f) * s), TRUE )) = (( dom s) \ ( Coim ((f * s), TRUE )))

    proof

      let S be non empty finite set, s be Element of (S * ), f be Function of S, BOOLEAN ;

       A1:

      now

        let x be object;

        

         A2: (f . x) = FALSE iff not (f . x) = TRUE by XBOOLEAN:def 3;

        

         A3: x in ( dom ( 'not' f)) iff x in ( dom f) by MARGREL1:def 17;

        

         A4: x in (( 'not' f) " { TRUE }) iff x in ( dom ( 'not' f)) & (( 'not' f) . x) in { TRUE } by FUNCT_1:def 7;

        x in ( dom ( 'not' f)) & (( 'not' f) . x) = TRUE iff x in ( dom f) & not ((f . x) = TRUE ) by Lm4, A3, A2;

        then x in (( 'not' f) " { TRUE }) iff x in ( dom f) & not (x in ( dom f) & (f . x) in { TRUE }) by A4, TARSKI:def 1;

        then x in (( 'not' f) " { TRUE }) iff x in ( dom f) & not x in (f " { TRUE }) by FUNCT_1:def 7;

        hence x in (( 'not' f) " { TRUE }) iff x in (( dom f) \ (f " { TRUE })) by XBOOLE_0:def 5;

      end;

      ( dom f) = S by FUNCT_2:def 1;

      then

       A5: (( rng s) /\ ( dom f)) = ( rng s) by XBOOLE_1: 28;

      (s " ( dom f)) = (s " (( rng s) /\ ( dom f))) by RELAT_1: 133;

      then

       A6: (s " ( dom f)) = ( dom s) by A5, RELAT_1: 134;

      

      thus ( Coim ((( 'not' f) * s), TRUE )) = (s " (( 'not' f) " { TRUE })) by RELAT_1: 146

      .= (s " (( dom f) \ (f " { TRUE }))) by A1, TARSKI: 2

      .= ((s " ( dom f)) \ (s " (f " { TRUE }))) by FUNCT_1: 69

      .= (( dom s) \ ( Coim ((f * s), TRUE ))) by A6, RELAT_1: 146;

    end;

    theorem :: DIST_2:24

    

     Th24: for S be non empty finite set, D be EqSampleSpaces of S, s be Element of D, f,g be Function of S, BOOLEAN holds ( Prob ((f 'or' g),s)) = (( card (( trueEVENT (f * s)) \/ ( trueEVENT (g * s)))) / ( len s))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, s be Element of D, f,g be Function of S, BOOLEAN ;

      

       A1: s is Element of (S * ) by FINSEQ_1:def 11;

      ( trueEVENT ((f 'or' g) * s)) = ( Coim (((f 'or' g) * s), TRUE ))

      .= (( Coim ((f * s), TRUE )) \/ ( Coim ((g * s), TRUE ))) by Th21, A1

      .= (( trueEVENT (f * s)) \/ ( trueEVENT (g * s)));

      hence thesis;

    end;

    theorem :: DIST_2:25

    

     Th25: for S be non empty finite set, D be EqSampleSpaces of S, s be Element of D, f,g be Function of S, BOOLEAN holds ( Prob ((f '&' g),s)) = (( card (( trueEVENT (f * s)) /\ ( trueEVENT (g * s)))) / ( len s))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, s be Element of D, f,g be Function of S, BOOLEAN ;

      

       A1: s is Element of (S * ) by FINSEQ_1:def 11;

      ( trueEVENT ((f '&' g) * s)) = ( Coim (((f '&' g) * s), TRUE ))

      .= (( Coim ((f * s), TRUE )) /\ ( Coim ((g * s), TRUE ))) by Th22, A1

      .= (( trueEVENT (f * s)) /\ ( trueEVENT (g * s)));

      hence thesis;

    end;

    theorem :: DIST_2:26

    

     Th26: for S be non empty finite set, D be EqSampleSpaces of S, s be Element of D, f be Function of S, BOOLEAN holds ( Prob (( 'not' f),s)) = (1 - ( Prob (f,s)))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, s be Element of D, f be Function of S, BOOLEAN ;

      

       A1: s is Element of (S * ) by FINSEQ_1:def 11;

      reconsider s0 = ( dom s) as finite set;

      reconsider CfS = ( Coim ((f * s), TRUE )) as finite set;

      ( card ( Seg ( len s))) = ( len s) by FINSEQ_1: 57;

      then

       A2: ( card s0) = ( len s) by FINSEQ_1:def 3;

      

       A3: ( Coim ((f * s), TRUE )) in ( bool ( dom s)) by A1, Th18;

      ( trueEVENT (( 'not' f) * s)) = ( Coim ((( 'not' f) * s), TRUE ))

      .= (( dom s) \ ( Coim ((f * s), TRUE ))) by A1, Th23;

      then

       A4: ( card ( trueEVENT (( 'not' f) * s))) = (( card s0) - ( card CfS)) by A3, CARD_2: 44;

      

      thus ( Prob (( 'not' f),s)) = ((( card s0) / ( len s)) - (( card CfS) / ( len s))) by A4, XCMPLX_1: 120

      .= (1 - ( Prob (f,s))) by A2, XCMPLX_1: 60;

    end;

    theorem :: DIST_2:27

    

     Th27: for S be non empty finite set, D be EqSampleSpaces of S, f,g be Function of S, BOOLEAN holds ( Prob ((f 'or' g),D)) = ((( Prob (f,D)) + ( Prob (g,D))) - ( Prob ((f '&' g),D)))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, f,g be Function of S, BOOLEAN ;

      set s = the Element of D;

      ( card (( trueEVENT (f * s)) \/ ( trueEVENT (g * s)))) = ((( card ( trueEVENT (f * s))) + ( card ( trueEVENT (g * s)))) - ( card (( trueEVENT (f * s)) /\ ( trueEVENT (g * s))))) by CARD_2: 45;

      

      then ( Prob ((f 'or' g),s)) = (((( card ( trueEVENT (f * s))) + ( card ( trueEVENT (g * s)))) - ( card (( trueEVENT (f * s)) /\ ( trueEVENT (g * s))))) / ( len s)) by Th24

      .= (((( card ( trueEVENT (f * s))) / ( len s)) + (( card ( trueEVENT (g * s))) / ( len s))) - (( card (( trueEVENT (f * s)) /\ ( trueEVENT (g * s)))) / ( len s))) by XCMPLX_1: 124

      .= ((( Prob (f,s)) + ( Prob (g,s))) - ( Prob ((f '&' g),s))) by Th25

      .= ((( Prob (f,D)) + ( Prob (g,s))) - ( Prob ((f '&' g),s))) by Def6

      .= ((( Prob (f,D)) + ( Prob (g,D))) - ( Prob ((f '&' g),s))) by Def6

      .= ((( Prob (f,D)) + ( Prob (g,D))) - ( Prob ((f '&' g),D))) by Def6;

      hence thesis by Def6;

    end;

    theorem :: DIST_2:28

    for S be non empty finite set, D be EqSampleSpaces of S, f be Function of S, BOOLEAN holds ( Prob (( 'not' f),D)) = (1 - ( Prob (f,D)))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, f be Function of S, BOOLEAN ;

      set s = the Element of D;

      

      thus ( Prob (( 'not' f),D)) = ( Prob (( 'not' f),s)) by Def6

      .= (1 - ( Prob (f,s))) by Th26

      .= (1 - ( Prob (f,D))) by Def6;

    end;

    theorem :: DIST_2:29

    

     Th29: for S be non empty finite set, D be EqSampleSpaces of S, f be Function of S, BOOLEAN st f = ( chi (S,S)) holds ( Prob (f,D)) = 1

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, f be Function of S, BOOLEAN ;

      assume

       A1: f = ( chi (S,S));

      set s = the Element of D;

      reconsider s0 = ( dom s) as finite set;

      reconsider CfS = ( Coim ((f * s), TRUE )) as finite set;

      ( card ( Seg ( len s))) = ( len s) by FINSEQ_1: 57;

      then

       A2: ( card s0) = ( len s) by FINSEQ_1:def 3;

      

       A3: s is Function of ( dom s), ( rng s) by FUNCT_2: 1;

      

       A4: s is Function of ( dom s), S by A3, FUNCT_2: 2;

      

       A5: f is Function of ( dom f), ( rng f) by FUNCT_2: 1;

      S c= S;

      then

       A6: f is Function of ( dom f), { TRUE } by A5, A1, INTEGRA1: 17;

      

       A7: ( dom f) = S by FUNCT_2:def 1;

      

       A8: ( trueEVENT (f * s)) = (s " ( trueEVENT f)) by Th14

      .= (s " S) by A7, A6, FUNCT_2: 40

      .= ( dom s) by A4, FUNCT_2: 40;

      

      thus ( Prob (f,D)) = ( Prob (f,s)) by Def6

      .= 1 by A2, A8, XCMPLX_1: 60;

    end;

    theorem :: DIST_2:30

    

     Th30: for S be non empty finite set, D be EqSampleSpaces of S, f be Function of S, BOOLEAN holds 0 <= ( Prob (f,D))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, f be Function of S, BOOLEAN ;

      set s = the Element of D;

      ( Prob (f,D)) = ( Prob (f,s)) by Def6

      .= (( card ( trueEVENT (f * s))) / ( len s));

      hence 0 <= ( Prob (f,D));

    end;

    theorem :: DIST_2:31

    

     Th31: for S be non empty finite set, A,B be set, f,g be Function of S, BOOLEAN st A c= S & B c= S & f = ( chi (A,S)) & g = ( chi (B,S)) holds ( chi ((A \/ B),S)) = (f 'or' g)

    proof

      let S be non empty finite set, A,B be set, f,g be Function of S, BOOLEAN ;

      assume

       A1: A c= S & B c= S & f = ( chi (A,S)) & g = ( chi (B,S));

      

       A2: ( dom ( chi ((A \/ B),S))) = S by FUNCT_3:def 3;

      

       A3: ( dom ( chi (A,S))) = S by FUNCT_3:def 3;

      

       A4: ( dom ( chi (B,S))) = S by FUNCT_3:def 3;

      

       A5: ( dom (f 'or' g)) = (( dom f) /\ ( dom g)) by BVFUNC_1:def 2

      .= S by A1, A3, A4;

      now

        let x be object;

        assume

         A6: x in ( dom (f 'or' g));

        

         A7: x in (( dom f) /\ ( dom g)) by A6, BVFUNC_1:def 2;

        per cases ;

          suppose

           A8: ((f 'or' g) . x) = TRUE ;

          then (( chi (A,S)) . x) = 1 or (( chi (B,S)) . x) = 1 by A1, Lm2, A7;

          then x in A or x in B by FUNCT_3: 36;

          then x in (A \/ B) by XBOOLE_0:def 3;

          hence (( chi ((A \/ B),S)) . x) = ((f 'or' g) . x) by A8, A6, FUNCT_3:def 3;

        end;

          suppose

           A9: ((f 'or' g) . x) <> TRUE ;

          

           A10: ((f 'or' g) . x) = FALSE by A9, XBOOLEAN:def 3;

           not ((( chi (A,S)) . x) = 1) & not ((( chi (B,S)) . x) = 1) by A1, A9, Lm2, A7;

          then not (x in A) & not (x in B) by A6, FUNCT_3:def 3;

          then not x in (A \/ B) by XBOOLE_0:def 3;

          hence (( chi ((A \/ B),S)) . x) = ((f 'or' g) . x) by A10, A6, FUNCT_3:def 3;

        end;

      end;

      hence thesis by A2, A5, FUNCT_1: 2;

    end;

    theorem :: DIST_2:32

    

     Th32: for S be non empty finite set, D be EqSampleSpaces of S, A,B be set, f,g be Function of S, BOOLEAN st A c= S & B c= S & A misses B & f = ( chi (A,S)) & g = ( chi (B,S)) holds ( Prob ((f '&' g),D)) = 0

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, A,B be set, f,g be Function of S, BOOLEAN ;

      assume

       A1: A c= S & B c= S & A misses B & f = ( chi (A,S)) & g = ( chi (B,S));

      set s = the Element of D;

      

       A2: ( Prob ((f '&' g),D)) = ( Prob ((f '&' g),s)) by Def6

      .= (( card (( trueEVENT (f * s)) /\ ( trueEVENT (g * s)))) / ( len s)) by Th25;

      (( trueEVENT (f * s)) /\ ( trueEVENT (g * s))) = {}

      proof

        assume (( trueEVENT (f * s)) /\ ( trueEVENT (g * s))) <> {} ;

        then

        consider x be object such that

         A3: x in (( trueEVENT (f * s)) /\ ( trueEVENT (g * s))) by XBOOLE_0:def 1;

        

         A4: ( trueEVENT (f * s)) = (s " ( trueEVENT f)) by Th14

        .= (s " (f " { TRUE }));

        

         A5: ( trueEVENT (g * s)) = (s " ( trueEVENT g)) by Th14

        .= (s " (g " { TRUE }));

        x in (s " (f " { TRUE })) & x in (s " (g " { TRUE })) by A4, A5, A3, XBOOLE_0:def 4;

        then x in ( dom s) & (s . x) in (f " { TRUE }) & (s . x) in (g " { TRUE }) by FUNCT_1:def 7;

        then (f . (s . x)) in {1} & (g . (s . x)) in {1} by FUNCT_1:def 7;

        then (f . (s . x)) = 1 & (g . (s . x)) = 1 by TARSKI:def 1;

        then (s . x) in A & (s . x) in B by A1, FUNCT_3: 36;

        then (s . x) in (A /\ B) by XBOOLE_0:def 4;

        hence contradiction by A1, XBOOLE_0:def 7;

      end;

      hence thesis by A2;

    end;

    definition

      let S be non empty finite set, D be EqSampleSpaces of S;

      :: DIST_2:def8

      mode Probability of D -> Function of ( Funcs (S, BOOLEAN )), REAL means for judgefunc be Element of ( Funcs (S, BOOLEAN )) holds (it . judgefunc) = ( Prob (judgefunc,D));

      existence

      proof

        deffunc F( Element of ( Funcs (S, BOOLEAN ))) = ( In (( Prob ($1,D)), REAL ));

        consider f be Function of ( Funcs (S, BOOLEAN )), REAL such that

         A1: for x be Element of ( Funcs (S, BOOLEAN )) holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        let x be Element of ( Funcs (S, BOOLEAN ));

        (f . x) = ( In (( Prob (x,D)), REAL )) by A1

        .= ( Prob (x,D));

        hence thesis;

      end;

    end

    

     Lm5: for S be non empty finite set, D be EqSampleSpaces of S holds ex EP be Probability of ( Trivial-SigmaField S) st for x be set st x in ( Trivial-SigmaField S) holds ex ch be Function of S, BOOLEAN st ch = ( chi (x,S)) & (EP . x) = ( Prob (ch,D))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S;

      defpred F[ object, object] means ex D1 be set, ch be Function of S, BOOLEAN st D1 = $1 & ch = ( chi (D1,S)) & $2 = ( Prob (ch,D));

       A1:

      now

        let x be object;

        assume x in ( Trivial-SigmaField S);

        reconsider xx = x as set by TARSKI: 1;

        reconsider ch = ( chi (xx,S)) as Function of S, BOOLEAN by MARGREL1:def 11;

        ( Prob (ch,D)) in REAL by XREAL_0:def 1;

        hence ex y be object st y in REAL & F[x, y];

      end;

      consider EP be Function of ( Trivial-SigmaField S), REAL such that

       A2: for x be object st x in ( Trivial-SigmaField S) holds F[x, (EP . x)] from FUNCT_2:sch 1( A1);

      

       A3: for A,B be Event of ( Trivial-SigmaField S) st A misses B holds (EP . (A \/ B)) = ((EP . A) + (EP . B))

      proof

        let A,B be Event of ( Trivial-SigmaField S);

        assume

         A4: A misses B;

         F[A, (EP . A)] by A2;

        then

        consider chA be Function of S, BOOLEAN such that

         A5: chA = ( chi (A,S)) & (EP . A) = ( Prob (chA,D));

         F[B, (EP . B)] by A2;

        then

        consider chB be Function of S, BOOLEAN such that

         A6: chB = ( chi (B,S)) & (EP . B) = ( Prob (chB,D));

         F[(A \/ B), (EP . (A \/ B))] by A2;

        then

        consider chAB be Function of S, BOOLEAN such that

         A7: chAB = ( chi ((A \/ B),S)) & (EP . (A \/ B)) = ( Prob (chAB,D));

        

         A8: chAB = (chA 'or' chB) by A5, A6, A7, Th31;

        

        thus (EP . (A \/ B)) = ((( Prob (chA,D)) + ( Prob (chB,D))) - ( Prob ((chA '&' chB),D))) by Th27, A7, A8

        .= ((( Prob (chA,D)) + ( Prob (chB,D))) - 0 ) by A5, A6, A4, Th32

        .= ((EP . A) + (EP . B)) by A6, A5;

      end;

      

       A9: for A be Event of ( Trivial-SigmaField S) holds 0 <= (EP . A)

      proof

        let A be Event of ( Trivial-SigmaField S);

         F[A, (EP . A)] by A2;

        then

        consider chA be Function of S, BOOLEAN such that

         A10: chA = ( chi (A,S)) & (EP . A) = ( Prob (chA,D));

        thus thesis by A10, Th30;

      end;

      

       A11: for ASeq be SetSequence of ( Trivial-SigmaField S) st ASeq is non-ascending holds (EP * ASeq) is convergent & ( lim (EP * ASeq)) = (EP . ( Intersection ASeq))

      proof

        let ASeq be SetSequence of ( Trivial-SigmaField S);

        assume ASeq is non-ascending;

        then

        consider N be Nat such that

         A12: for m be Nat st N <= m holds ( Intersection ASeq) = (ASeq . m) by RANDOM_1: 15;

        now

          let m be Nat;

          assume

           A13: N <= m;

          m in NAT by ORDINAL1:def 12;

          then m in ( dom ASeq) by FUNCT_2:def 1;

          

          hence ((EP * ASeq) . m) = (EP . (ASeq . m)) by FUNCT_1: 13

          .= (EP . ( Intersection ASeq)) by A12, A13;

        end;

        hence thesis by PROB_1: 1;

      end;

       F[( [#] S), (EP . ( [#] S))] by A2;

      then

      consider chS be Function of S, BOOLEAN such that

       A14: chS = ( chi (S,S)) & (EP . S) = ( Prob (chS,D));

      reconsider EP as Probability of ( Trivial-SigmaField S) by A9, A3, PROB_1:def 8, Th29, A11, A14;

      take EP;

      let x be set;

      assume x in ( Trivial-SigmaField S);

      then F[x, (EP . x)] by A2;

      hence thesis;

    end;

    definition

      let S be non empty finite set, D be EqSampleSpaces of S;

      :: DIST_2:def9

      func Trivial-Probability (D) -> Probability of ( Trivial-SigmaField S) means for x be set st x in ( Trivial-SigmaField S) holds ex ch be Function of S, BOOLEAN st ch = ( chi (x,S)) & (it . x) = ( Prob (ch,D));

      existence by Lm5;

      uniqueness

      proof

        let F,G be Probability of ( Trivial-SigmaField S);

        assume

         A1: for A be set st A in ( Trivial-SigmaField S) holds ex ch be Function of S, BOOLEAN st ch = ( chi (A,S)) & (F . A) = ( Prob (ch,D));

        assume

         A2: for A be set st A in ( Trivial-SigmaField S) holds ex ch be Function of S, BOOLEAN st ch = ( chi (A,S)) & (G . A) = ( Prob (ch,D));

        now

          let x be object;

          assume

           A3: x in ( Trivial-SigmaField S);

          reconsider X = x as set by TARSKI: 1;

          consider ch1 be Function of S, BOOLEAN such that

           A4: ch1 = ( chi (X,S)) & (F . x) = ( Prob (ch1,D)) by A1, A3;

          consider ch2 be Function of S, BOOLEAN such that

           A5: ch2 = ( chi (X,S)) & (G . x) = ( Prob (ch2,D)) by A3, A2;

          thus (F . x) = (G . x) by A4, A5;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    begin

    definition

      let S be non empty finite set, D be EqSampleSpaces of S;

      :: DIST_2:def10

      mode sample of D -> Element of S means

      : Def10: ex s be Element of D st it in ( rng s);

      existence

      proof

        set s = the Element of D;

        1 in ( dom s) by FINSEQ_5: 6;

        then (s . 1) in ( rng s) by FUNCT_1: 3;

        hence thesis;

      end;

    end

    definition

      let S be non empty finite set, D be EqSampleSpaces of S, x be sample of D;

      :: DIST_2:def11

      func Prob (x) -> Real equals ( Prob (( MembershipDecision {x}),D));

      coherence ;

    end

    theorem :: DIST_2:33

    for S be non empty finite set, D be EqSampleSpaces of S, x be sample of D holds ( Prob x) = (( ProbFinS_of D) . ( index x))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, x be sample of D;

      reconsider f = ( chi ( {x},S)) as Element of ( Funcs (S, BOOLEAN )) by FUNCT_2: 8, MARGREL1:def 11;

      set s = the Element of D;

      

       A1: for a be set holds a = x implies (f . a) = TRUE

      proof

        let a be set;

        assume a = x;

        then a in {x} by TARSKI:def 1;

        hence thesis by FUNCT_3:def 3;

      end;

      for a be set holds (f . a) = TRUE implies a = x

      proof

        let a be set;

        assume (f . a) = TRUE ;

        then a in {x} by FUNCT_3: 36;

        hence thesis by TARSKI:def 1;

      end;

      then

       A2: ( Prob (f,s)) = ( FDprobability (x,s)) by Th10, A1;

      

       A3: ( Prob x) = ( FDprobability (x,s)) by A2, Def6;

      consider t be FinSequence of S such that

       A4: t in D & (( GenProbSEQ S) . D) = ( FDprobSEQ t) by DIST_1:def 7;

      

       A5: (( GenProbSEQ S) . D) = ( FDprobSEQ s) by A4, DIST_1: 10, Th4;

      reconsider n = (x .. ( canFS S)) as Nat;

      ( len ( canFS S)) = ( card S) by FINSEQ_1: 93;

      then

       A6: ( dom ( canFS S)) = ( Seg ( card S)) by FINSEQ_1:def 3;

      

       A7: x in ( rng ( canFS S)) by Th3;

      then n in ( dom ( canFS S)) by FINSEQ_4: 20;

      then

       A8: n in ( dom ( FDprobSEQ s)) by A6, DIST_1:def 3;

      (( canFS S) . n) = x by A7, FINSEQ_4: 19;

      hence thesis by A3, A5, A8, DIST_1:def 3;

    end;

    definition

      let S be non empty finite set, D be EqSampleSpaces of S;

      :: DIST_2:def12

      mode samplingRNG of D -> non empty Subset of S means

      : Def12: ex x be sample of D st x in it ;

      existence

      proof

        set x = the sample of D;

        

         A1: x in {x} by TARSKI:def 1;

        reconsider X = {x} as non empty Element of ( bool S);

        take X;

        thus thesis by A1;

      end;

    end

    definition

      let S be non empty finite set, D be EqSampleSpaces of S, X be samplingRNG of D;

      :: DIST_2:def13

      func Prob (X) -> Real equals ( Prob (( MembershipDecision X),D));

      coherence ;

    end

    theorem :: DIST_2:34

    

     Th34: for S be non empty finite set, X be Subset of S, s,t be FinSequence of S, SD be Subset of ( dom s), x be Subset of X st SD = (s " X) & t = ( extract (s,SD)) holds ( card (s " x)) = ( card (t " x))

    proof

      let S be non empty finite set, X be Subset of S, s,t be FinSequence of S, SD be Subset of ( dom s), x be Subset of X;

      assume

       A1: SD = (s " X) & t = ( extract (s,SD));

      reconsider SD as finite set;

      set f = (( canFS SD) " );

      ( len t) = ( card SD) by A1, Th11;

      then

       A2: ( dom t) = ( Seg ( card SD)) by FINSEQ_1:def 3;

      then

      reconsider g = f as Function of SD, ( dom t) by FINSEQ_1: 95;

      

       A3: (( canFS SD) .: (t " x)) = (f " (t " x)) by FUNCT_1: 84

      .= ((t * f) " x) by RELAT_1: 146

      .= ((s | SD) " x) by A1, Th12

      .= (SD /\ (s " x)) by FUNCT_1: 70

      .= (s " x) by A1, RELAT_1: 143, XBOOLE_1: 28;

      then

       A4: ( card (s " x)) c= ( card (t " x)) by CARD_1: 66;

      

       A5: (t " x) c= ( Seg ( card SD)) by A2, RELAT_1: 132;

      ( len ( canFS SD)) = ( card SD) by FINSEQ_1: 93;

      then

       A6: (t " x) is Subset of ( dom ( canFS SD)) by A5, FINSEQ_1:def 3;

      

       A7: (f * ( canFS SD)) = ( id ( dom ( canFS SD))) by FUNCT_1: 39;

      (f .: (s " x)) = ((f * ( canFS SD)) .: (t " x)) by A3, RELAT_1: 126

      .= (t " x) by A6, A7, FUNCT_1: 92;

      then ( card (t " x)) c= ( card (s " x)) by CARD_1: 66;

      hence thesis by A4, XBOOLE_0:def 10;

    end;

    theorem :: DIST_2:35

    

     Th35: for S be non empty finite set, X be Subset of S, s,t be FinSequence of S, SD be Subset of ( dom s), x be set st SD = (s " X) & t = ( extract (s,SD)) & x in X holds ( frequency (x,s)) = ( frequency (x,t))

    proof

      let S be non empty finite set, X be Subset of S, s,t be FinSequence of S, SD be Subset of ( dom s), x be set;

      assume

       A1: SD = (s " X) & t = ( extract (s,SD)) & x in X;

      then for a be object st a in {x} holds a in X by TARSKI:def 1;

      then {x} is Subset of X by TARSKI:def 3;

      hence thesis by Th34, A1;

    end;

    theorem :: DIST_2:36

    

     Th36: for S be non empty finite set, D be Element of ( distribution_family S), s be FinSequence of S st s in D holds D = ( Finseq-EQclass s)

    proof

      let S be non empty finite set, D be Element of ( distribution_family S), s be FinSequence of S;

      assume

       A1: s in D;

      consider t be FinSequence of S such that

       A2: D = ( Finseq-EQclass t) by DIST_1:def 6;

      thus thesis by A2, DIST_1: 9, A1, DIST_1: 7;

    end;

    theorem :: DIST_2:37

    

     Th37: for S be non empty finite set, X be Subset of S, s be FinSequence of S holds (s " X) = ( trueEVENT (( MembershipDecision X) * s))

    proof

      let S be non empty finite set, X be Subset of S, s be FinSequence of S;

      set SX = (s " X);

      reconsider SX as Subset of ( dom s) by RELAT_1: 132;

      ( dom (( MembershipDecision X) * s)) c= ( dom s) by RELAT_1: 25;

      then

      reconsider SY = ( trueEVENT (( MembershipDecision X) * s)) as Subset of ( dom s) by XBOOLE_1: 1;

      consider f be Function of S, BOOLEAN such that

       A1: f = ( chi (X,S)) & ( MembershipDecision X) = f;

      

       A2: ( dom f) = S by A1, FUNCT_3:def 3;

      

       A3: for x be object st x in SY holds x in SX

      proof

        let x be object;

        assume

         A4: x in SY;

        (s . x) in ( trueEVENT f) by A1, Th13, A4;

        then (s . x) in ( dom f) & (f . (s . x)) in { TRUE } by FUNCT_1:def 7;

        then (s . x) in ( dom f) & (f . (s . x)) = TRUE by TARSKI:def 1;

        then (s . x) in X by A1, FUNCT_3: 36;

        hence thesis by A4, FUNCT_1:def 7;

      end;

      for x be object st x in SX holds x in SY

      proof

        let x be object;

        assume

         A5: x in SX;

        

         A6: (s . x) in ( rng s) by A5, FUNCT_1: 3;

        (s . x) in X by A5, FUNCT_1:def 7;

        then (f . (s . x)) = TRUE by A1, FUNCT_3:def 3;

        then (f . (s . x)) in { TRUE } by TARSKI:def 1;

        then (s . x) in ( trueEVENT f) by A6, A2, FUNCT_1:def 7;

        hence thesis by A1, Th13, A5;

      end;

      hence thesis by A3, TARSKI: 2;

    end;

    theorem :: DIST_2:38

    

     Th38: for S be non empty finite set, X be non empty Subset of S, D be EqSampleSpaces of S, s1,s2 be Element of D, t1,t2 be FinSequence of S, SD1 be Subset of ( dom s1), SD2 be Subset of ( dom s2) st SD1 = (s1 " X) & t1 = ( extract (s1,SD1)) & SD2 = (s2 " X) & t2 = ( extract (s2,SD2)) holds (t1,t2) -are_prob_equivalent

    proof

      let S be non empty finite set, X be non empty Subset of S, D be EqSampleSpaces of S, s1,s2 be Element of D, t1,t2 be FinSequence of S, SD1 be Subset of ( dom s1), SD2 be Subset of ( dom s2);

      assume

       A1: SD1 = (s1 " X) & t1 = ( extract (s1,SD1)) & SD2 = (s2 " X) & t2 = ( extract (s2,SD2));

      then SD1 = ( trueEVENT (( MembershipDecision X) * s1)) by Th37;

      then

       A2: ( Prob (( MembershipDecision X),s1)) = (( len t1) / ( len s1)) by Th11, A1;

      SD2 = ( trueEVENT (( MembershipDecision X) * s2)) by A1, Th37;

      then

       A3: ( Prob (( MembershipDecision X),s2)) = (( len t2) / ( len s2)) by Th11, A1;

      

       A4: t1 = {} implies t2 = {} by A3, A2, Th17;

      

       A5: for n,x be set st n in SD1 & not x in X holds not (s1 . n) in {x}

      proof

        let n,x be set;

        assume

         A6: n in SD1 & not x in X;

        assume (s1 . n) in {x};

        then not (s1 . n) in X by A6, TARSKI:def 1;

        hence contradiction by A1, A6, FUNCT_1:def 7;

      end;

      

       A7: for n,x be set st n in SD2 & not x in X holds not (s2 . n) in {x}

      proof

        let n,x be set;

        assume

         A8: n in SD2 & not x in X;

        assume (s2 . n) in {x};

        then not (s2 . n) in X by A8, TARSKI:def 1;

        hence contradiction by A1, A8, FUNCT_1:def 7;

      end;

      set c = (( len t1) / ( len s1));

      

       A9: c = (( len t2) / ( len s2)) by A3, A2, Th17;

      for x be set holds ( FDprobability (x,t1)) = ( FDprobability (x,t2))

      proof

        let x be set;

        per cases ;

          suppose

           A10: t1 <> {} ;

          per cases ;

            suppose

             A11: x in X;

            ( FDprobability (x,s1)) = ( FDprobability (x,s2)) by DIST_1:def 4, Th4

            .= (( frequency (x,s2)) / ( len s2));

            then (( frequency (x,t1)) / ( len s1)) = (( frequency (x,s2)) / ( len s2)) by Th35, A1, A11;

            then (( frequency (x,t1)) / ( len s1)) = (( frequency (x,t2)) / ( len s2)) by Th35, A1, A11;

            then ((( len t1) * ( FDprobability (x,t1))) / ( len s1)) = (( frequency (x,t2)) / ( len s2)) by DIST_1: 4;

            then ((( len t1) * ( FDprobability (x,t1))) / ( len s1)) = ((( len t2) * ( FDprobability (x,t2))) / ( len s2)) by DIST_1: 4;

            then (( FDprobability (x,t1)) * (( len t1) / ( len s1))) = ((( FDprobability (x,t2)) * ( len t2)) / ( len s2)) by XCMPLX_1: 74;

            then (( FDprobability (x,t1)) * c) = (( FDprobability (x,t2)) * c) by A9, XCMPLX_1: 74;

            hence thesis by A10, XCMPLX_1: 5;

          end;

            suppose

             A12: not x in X;

             not ex i be object st i in (t1 " {x})

            proof

              let i be object;

              assume

               A13: i in (t1 " {x});

              then

               A14: i in ( dom t1) & (t1 . i) in {x} by FUNCT_1:def 7;

              ( len t1) = ( card SD1) by A1, Th11;

              then

               A15: ( dom t1) = ( Seg ( card SD1)) by FINSEQ_1:def 3;

              reconsider i as Nat by A13;

              

               A16: ( rng ( canFS SD1)) c= SD1 by FINSEQ_1:def 4;

              set NE = (( canFS SD1) . i);

              ( len ( canFS SD1)) = ( card SD1) by FINSEQ_1: 93;

              then i in ( dom ( canFS SD1)) by A14, A15, FINSEQ_1:def 3;

              then

               A17: NE in ( rng ( canFS SD1)) by FUNCT_1: 3;

              (t1 . i) = (s1 . NE) by A1, A14, Th11;

              hence contradiction by A14, A17, A16, A5, A12;

            end;

            then ( Coim (t1,x)) is empty by XBOOLE_0:def 1;

            then

             A18: ( FDprobability (x,t1)) = 0 ;

             not ex i be object st i in (t2 " {x})

            proof

              let i be object;

              assume

               A19: i in (t2 " {x});

              then

               A20: i in ( dom t2) & (t2 . i) in {x} by FUNCT_1:def 7;

              ( len t2) = ( card SD2) by A1, Th11;

              then

               A21: ( dom t2) = ( Seg ( card SD2)) by FINSEQ_1:def 3;

              reconsider i as Nat by A19;

              

               A22: ( rng ( canFS SD2)) c= SD2 by FINSEQ_1:def 4;

              set NE = (( canFS SD2) . i);

              ( len ( canFS SD2)) = ( card SD2) by FINSEQ_1: 93;

              then i in ( dom ( canFS SD2)) by A20, A21, FINSEQ_1:def 3;

              then

               A23: NE in ( rng ( canFS SD2)) by FUNCT_1: 3;

              (t2 . i) = (s2 . NE) by A1, A20, Th11;

              hence contradiction by A20, A23, A22, A7, A12;

            end;

            then ( Coim (t2,x)) is empty by XBOOLE_0:def 1;

            hence thesis by A18;

          end;

        end;

          suppose t1 = {} ;

          hence thesis by A4;

        end;

      end;

      hence thesis;

    end;

    definition

      let S be non empty finite set, D be EqSampleSpaces of S, X be samplingRNG of D;

      :: DIST_2:def14

      func ConditionalSS (X) -> EqSampleSpaces of S means

      : Def14: ex s be Element of D, t be FinSequence of S, SD be Subset of ( dom s) st SD = (s " X) & t = ( extract (s,SD)) & t in it ;

      existence

      proof

        consider x be sample of D such that

         A1: x in X by Def12;

        consider s be Element of D such that

         A2: x in ( rng s) by Def10;

        consider n be object such that

         A3: n in ( dom s) and

         A4: x = (s . n) by A2, FUNCT_1:def 3;

        reconsider SD = (s " X) as Subset of ( dom s) by RELAT_1: 132;

        reconsider t = ( extract (s,SD)) as FinSequence of S;

        reconsider DX = ( Finseq-EQclass t) as Element of ( distribution_family S) by DIST_1:def 6;

        

         A5: t in DX;

        n in SD by A3, A4, A1, FUNCT_1:def 7;

        then ( card SD) <> 0 ;

        then ( len t) <> 0 by Th11;

        then t <> ( <*> S);

        then not DX = {( <*> S)} by A5, TARSKI:def 1;

        then

        reconsider DX as EqSampleSpaces of S by Th6;

        take DX;

        thus thesis by A5;

      end;

      uniqueness

      proof

        let DX1,DX2 be EqSampleSpaces of S;

        given s1 be Element of D, t1 be FinSequence of S, SD1 be Subset of ( dom s1) such that

         A6: SD1 = (s1 " X) & t1 = ( extract (s1,SD1)) & t1 in DX1;

        given s2 be Element of D, t2 be FinSequence of S, SD2 be Subset of ( dom s2) such that

         A7: SD2 = (s2 " X) & t2 = ( extract (s2,SD2)) & t2 in DX2;

        DX1 = ( Finseq-EQclass t1) & DX2 = ( Finseq-EQclass t2) by Th36, A6, A7;

        hence thesis by DIST_1: 9, A6, A7, Th38;

      end;

    end

    definition

      let S be non empty finite set, D be EqSampleSpaces of S, X be samplingRNG of D, f be Function of S, BOOLEAN ;

      :: DIST_2:def15

      func Prob (f,X) -> Real equals ( Prob (f,( ConditionalSS X)));

      coherence ;

    end

    theorem :: DIST_2:39

    for S be non empty finite set, D be EqSampleSpaces of S, X be samplingRNG of D, f be Function of S, BOOLEAN holds (( Prob (f,X)) * ( Prob X)) = ( Prob ((f '&' ( MembershipDecision X)),D))

    proof

      let S be non empty finite set, D be EqSampleSpaces of S, X be samplingRNG of D, f be Function of S, BOOLEAN ;

      set g = ( MembershipDecision X);

      set Pc = ( Prob (f,X));

      set Pp = ( Prob X);

      consider s be Element of D, t be FinSequence of S, SD be Subset of ( dom s) such that

       A1: SD = (s " X) & t = ( extract (s,SD)) & t in ( ConditionalSS X) by Def14;

      reconsider t as Element of ( ConditionalSS X) by A1;

      

       A2: ( len t) = ( card SD) by Th11, A1;

      

       A3: ( rng t) c= X

      proof

        assume not ( rng t) c= X;

        then

        consider y be object such that

         A4: y in ( rng t) & not y in X by TARSKI:def 3;

        consider x be object such that

         A5: x in ( dom t) & y = (t . x) by A4, FUNCT_1:def 3;

        

         A6: ( dom t) = ( Seg ( card SD)) by A2, FINSEQ_1:def 3;

        reconsider x as Nat by A5;

        set z = (( canFS SD) . x);

        

         A7: ( rng ( canFS SD)) c= SD by FINSEQ_1:def 4;

        ( len ( canFS SD)) = ( card SD) by FINSEQ_1: 93;

        then ( dom ( canFS SD)) = ( dom t) by A6, FINSEQ_1:def 3;

        then z in ( rng ( canFS SD)) by A5, FUNCT_1: 3;

        then z in ( dom s) & (s . z) in X by A1, A7, FUNCT_1:def 7;

        hence contradiction by A4, A5, Th11, A1;

      end;

      

       A8: SD = ( trueEVENT (g * s)) by Th37, A1;

      

       A9: Pp = ( Prob (g,s)) by Def6

      .= (( len t) / ( len s)) by Th11, A1, A8;

      Pc = ( Prob (f,t)) by Def6

      .= (( card ( trueEVENT (f * t))) / ( len t));

      

      then

       A10: (Pc * Pp) = (((( card ( trueEVENT (f * t))) / ( len t)) * ( len t)) / ( len s)) by A9, XCMPLX_1: 74

      .= ((( card ( trueEVENT (f * t))) / (( len t) / ( len t))) / ( len s)) by XCMPLX_1: 82

      .= ((( card ( trueEVENT (f * t))) / 1) / ( len s)) by XCMPLX_1: 60

      .= (( card ( trueEVENT (f * t))) / ( len s));

      

       A11: ( Prob ((f '&' g),s)) = (( card (( trueEVENT (f * s)) /\ ( trueEVENT (g * s)))) / ( len s)) by Th25;

      

       A12: (t " ( rng t)) c= (t " X) by A3, RELAT_1: 143;

      (t " ( trueEVENT f)) c= (t " ( rng t)) by RELAT_1: 135;

      then ((t " ( trueEVENT f)) /\ (t " X)) = (t " ( trueEVENT f)) by A12, XBOOLE_1: 1, XBOOLE_1: 28;

      then

       A13: (t " (( trueEVENT f) /\ X)) = (t " ( trueEVENT f)) by FUNCT_1: 68;

      (( trueEVENT f) /\ X) c= X by XBOOLE_1: 17;

      

      then

       A14: ( card (s " (( trueEVENT f) /\ X))) = ( card (t " (( trueEVENT f) /\ X))) by Th34, A1

      .= ( card ( trueEVENT (f * t))) by Th14, A13;

      ( card ( trueEVENT (f * t))) = ( card ((s " ( trueEVENT f)) /\ (s " X))) by A14, FUNCT_1: 68

      .= ( card (( trueEVENT (f * s)) /\ ( trueEVENT (g * s)))) by A8, A1, Th14;

      hence thesis by Def6, A10, A11;

    end;