:: Posterior Probability on Finite Set
::  by Hiroyuki Okazaki
::
:: Received July 4, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies DIST_2, DIST_1, FINSEQ_1, RELAT_1, FINSEQ_4, NAT_1, XXREAL_0,
      FUNCT_7, FUNCT_1, RPR_1, CARD_1, XBOOLE_0, CQC_SIM1, ARYTM_3, TARSKI,
      ZFMISC_1, SUBSET_1, NUMBERS, PROB_2, FINSET_1, UPROOTS, MATRPROB,
      MARGREL1, CARD_3, XBOOLEAN, VALUED_1, EQREL_1, PROB_1, SETFAM_1, FUNCT_2,
      ORDINAL2, ARYTM_1, FUNCT_3, RANDOM_1, SEQ_2, REAL_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, ORDINAL1, FUNCT_2, DOMAIN_1, FUNCT_3, FINSET_1, CARD_1,
      NUMBERS, XCMPLX_0, CARD_3, KURATO_0, FRECHET, COMSEQ_2, XXREAL_0,
      XREAL_0, REAL_1, NAT_1, FINSEQ_1, VALUED_1, FINSEQ_2, XBOOLEAN, SEQ_2,
      MARGREL1, FINSEQ_4, RVSUM_1, RPR_1, PROB_1, PROB_2, BVFUNC_1, UPROOTS,
      MATRPROB, RANDOM_1, DIST_1;
 constructors KURATO_0, FRECHET, COMSEQ_2, CARD_3, RELSET_1, DOMAIN_1, REAL_1,
      BINOP_2, FINSEQ_4, RVSUM_1, RPR_1, PROB_4, BVFUNC_1, UPROOTS, PROB_3,
      DIST_1, RANDOM_1, SEQ_2, MESFUNC5, SEQ_4, WELLORD2, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2,
      FINSET_1, CARD_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, VALUED_0,
      FINSEQ_1, DIST_1, VALUED_1, MARGREL1, MATRPROB, XBOOLEAN, XCMPLX_0,
      ORDINAL1;
 requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;


begin :: Equivalent Distributed Finite and Distributed Sample Spaces

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

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

theorem :: DIST_2:3
  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);

registration let S be non empty finite set;
  cluster -> non empty for Element of distribution_family S;
end;

definition
  let S be non empty finite set,
  D be Element of distribution_family(S);
  redefine mode Element of D -> FinSequence of S;
end;

theorem :: DIST_2:4
  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;

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

registration
  let S be non empty finite set;
  cluster well-distributed for Element of distribution_family(S);
end;

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

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

theorem :: DIST_2:7
  for S be non empty finite set,
  D be EqSampleSpaces of S holds
  (GenProbSEQ(S)).D is distProbFinS of S;

begin :: Probability Measure of Equivalent Distributed Finite and Distributed Sample Spaces

definition
  let S be non empty finite set, a be Element of S;
  func index(a) -> Element of NAT equals
:: DIST_2:def 1
  a..(canFS(S));
end;

definition
  let S be non empty finite set,
  D be EqSampleSpaces of S;
  func ProbFinS_of D -> distProbFinS of S equals
:: DIST_2:def 2
  (GenProbSEQ S).D;
end;

definition
  let judgefunc be BOOLEAN-valued Function;
  func trueEVENT(judgefunc) -> Event of dom judgefunc equals
:: DIST_2:def 3
  judgefunc"{TRUE};
end;

theorem :: DIST_2:8
  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;

definition
  let S be non empty finite set,
  D be EqSampleSpaces of S,
  s be Element of D,
  judgefunc be Function of S,BOOLEAN;
  func Prob(judgefunc,s) -> Real equals
:: DIST_2:def 4
  card (trueEVENT(judgefunc*s))/(len s);
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);

theorem :: DIST_2:10
  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);

definition
  let S be set,
  s be FinSequence of S,
  A be Subset of dom s;
  func extract(s,A) -> FinSequence of S equals
:: DIST_2:def 5
  s*(canFS(A));
end;

theorem :: DIST_2:11
  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);

theorem :: DIST_2:12
  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;

theorem :: DIST_2:13
  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);

theorem :: DIST_2:14
  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));

theorem :: DIST_2:15
  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);

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

theorem :: DIST_2:17
  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);

definition
  let S be non empty finite set,
  D be EqSampleSpaces of S,
  judgefunc be Function of S,BOOLEAN;
  func Prob(judgefunc,D) -> Real means
:: DIST_2:def 6
  for s be Element of D holds it = Prob(judgefunc,s);
end;

theorem :: DIST_2:18
  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);

definition
  let S be set,
  SS be Subset of S;
  func MembershipDecision(SS) -> Function of S,BOOLEAN equals
:: DIST_2:def 7
  chi(SS,S);
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;

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;

theorem :: DIST_2:21
  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);

theorem :: DIST_2:22
  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);

theorem :: DIST_2:23
  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);

theorem :: DIST_2:24
  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);

theorem :: DIST_2:25
  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);

theorem :: DIST_2:26
  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);

theorem :: DIST_2:27
  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);

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

theorem :: DIST_2:29

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;

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

theorem :: DIST_2:31
  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;

theorem :: DIST_2:32
  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;

definition
  let S be non empty finite set,
  D be EqSampleSpaces of S;
  mode Probability of D -> Function of Funcs(S,BOOLEAN), REAL means
:: DIST_2:def 8
  for judgefunc be Element of Funcs(S,BOOLEAN) holds
  it.judgefunc = Prob(judgefunc,D);
end;

definition
  let S be non empty finite set,
  D be EqSampleSpaces of S;
  func Trivial-Probability (D) -> Probability of Trivial-SigmaField (S) means
:: DIST_2:def 9
  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);
end;

begin :: Sampling and Posterior Probability

definition
  let S be non empty finite set,
  D be EqSampleSpaces of S;
  mode sample of D -> Element of S means
:: DIST_2:def 10
   ex s being Element of D st it in rng s;
end;

definition
  let S be non empty finite set,
  D be EqSampleSpaces of S,
  x be sample of D;
  func Prob(x) -> Real equals
:: DIST_2:def 11
  Prob(MembershipDecision({x}),D);
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));

definition
  let S be non empty finite set,
  D be EqSampleSpaces of S;
  mode samplingRNG of D -> non empty Subset of S means
:: DIST_2:def 12
  ex x be sample of D st x in it;
end;

definition
  let S be non empty finite set,
  D be EqSampleSpaces of S,
  X be samplingRNG of D;
  func Prob(X) -> Real equals
:: DIST_2:def 13
  Prob(MembershipDecision(X),D);
end;

theorem :: DIST_2:34
  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);

theorem :: DIST_2:35
  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);

theorem :: DIST_2:36
  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);

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

theorem :: DIST_2:38
  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;

definition
  let S be non empty finite set,
  D be EqSampleSpaces of S,
  X be samplingRNG of D;
  func ConditionalSS(X) -> EqSampleSpaces of S means
:: DIST_2:def 14

  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;
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;
  func Prob(f,X) -> Real equals
:: DIST_2:def 15
  Prob(f, ConditionalSS(X));
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);