:: Posterior Probability on Finite Set
:: by Hiroyuki Okazaki
::
:: Received July 4, 2012
:: Copyright (c) 2012-2026 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;
equalities SUBSET_1, RELAT_1, FINSEQ_1, RPR_1, DIST_1, XBOOLEAN, CARD_3;
expansions DIST_1;
theorems TARSKI, FINSEQ_2, CARD_1, FINSEQ_4, FUNCT_1, FINSEQ_1, XBOOLE_0,
XBOOLE_1, PROB_2, RELAT_1, ZFMISC_1, FUNCT_2, XCMPLX_1, VALUED_1,
FINSEQ_5, RVSUM_1, DIST_1, ORDINAL1, INTEGRA1, BVFUNC_1, MARGREL1,
XBOOLEAN, PROB_1, CARD_2, FUNCT_3, RANDOM_1, XREAL_0, SETFAM_1;
schemes FUNCT_1, FUNCT_2;
begin :: Equivalent Distributed Finite and Distributed Sample Spaces
theorem
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,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)
.=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;
end;
hence thesis by A4,A1,DIST_1:def 3;
end;
theorem
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 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 being 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);
redefine mode Element of D -> FinSequence of S; :: redefines Element (SUBSET_1, definition)
coherence
proof
let x be Element of D;
x is Element of S*;
hence thesis;
end;
end;
theorem 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 being 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 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,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 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 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 being FinSequence of S
such that A2: D = Finseq-EQclass(t) by DIST_1:def 6;
D=Finseq-EQclass(s) by A2,DIST_1:9,7;
hence thesis by A1,DIST_1:12;
end;
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
a..(canFS(S));
correctness;
end;
definition
let S be non empty finite set,
D be EqSampleSpaces of S;
func ProbFinS_of D -> distProbFinS of S equals
(GenProbSEQ S).D;
correctness by Th7;
end;
definition
let judgefunc be BOOLEAN-valued Function;
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 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;
func Prob(judgefunc,s) -> Real equals
card (trueEVENT(judgefunc*s))/(len s);
correctness;
end;
theorem
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 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,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;
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 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 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 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 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 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 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 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 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 being 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;
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 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;
func MembershipDecision(SS) -> Function of S,BOOLEAN equals
chi(SS,S);
coherence by MARGREL1:def 11;
end;
theorem
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
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 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 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 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 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 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 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 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
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 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 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 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 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;
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 being 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 being 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 being 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 being 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 being SetSequence of Trivial-SigmaField (S) st ASeq is
non-ascending holds EP * ASeq is convergent & lim (EP * ASeq)
= EP.( Intersection ASeq)
proof
let ASeq being 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;
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 :: 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 :Def10:
ex s being 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;
func Prob(x) -> Real equals
Prob(MembershipDecision({x}),D);
coherence;
end;
theorem
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;
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;
func Prob(X) -> Real equals
Prob(MembershipDecision(X),D);
coherence;
end;
theorem 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 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 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 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 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;
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 being 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;
func Prob(f,X) -> Real equals
Prob(f, ConditionalSS(X));
coherence;
end;
theorem
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,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;