:: Posterior Probability on Finite Set
:: by Hiroyuki Okazaki
::
:: Received July 4, 2012
:: Copyright (c) 2012 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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,
ORDINAL1, FUNCT_2, ORDINAL2, ARYTM_1, FUNCT_3, RANDOM_1, SEQ_2, XREAL_0;
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, PROB_1, UPROOTS, MATRPROB,
XBOOLEAN, XCMPLX_0, ORDINAL1, SETFAM_1;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
definitions RELAT_1, FINSEQ_1, RPR_1, DIST_1, XBOOLEAN, CARD_3;
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, MEASURE1, 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
AS: Y={1} & s=<*1*>;
L1: dom s ={1} & s.1 = 1 by AS,FINSEQ_1:2,def 8;
L10:len s=1&card Y =1 by AS,CARD_1:30;
T1: dom s=Seg (card Y) by L1,AS,CARD_1:30,FINSEQ_1:2;
rng s= {1} by AS,FINSEQ_1:39;
then L12: 1 in rng s by TARSKI:def 1;
L21: FDprobability((canFS(Y)).1,s)
=FDprobability(<*1*>.1,s) by AS,FINSEQ_1:94
.=FDprobability(1,s) by FINSEQ_1:def 8
.=1 by AS,L12,L10,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 L1,TARSKI:def 1;
hence thesis by L21,AS,FINSEQ_1:def 8;
end;
hence thesis by T1,AS,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 AS: 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 AS,DIST_1:12; then
D=distribution(p,S) by AS,DIST_1:def 8;
hence thesis;
end;
theorem THCANFS:
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;
CCC: x in S; then
x in rng canFS(S) by FUNCT_2:def 3; then
consider n be set such that
C11: n in dom (canFS(S)) & x=(canFS(S)).n by FUNCT_1:def 3;
reconsider n as Nat by C11;
len canFS(S) = card (S) by FINSEQ_1:93; then
n in Seg (card (S)) by C11,FINSEQ_1:def 3;
hence thesis by C11,CCC,FUNCT_2:def 3;
end;
EDFNE:
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 EDFNE;
end;
definition
let S be non empty finite set,
D be Element of distribution_family(S);
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 EDF1:
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 AS0: D = Finseq-EQclass(x) by DIST_1:def 6;
s,x -are_prob_equivalent
& x,t -are_prob_equivalent by AS0,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 emset:
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 AS: for x be set holds FDprobability(x,s)= 0;
assume CNT: not s is empty;
1 in dom s by CNT,FINSEQ_5:6;
then L2: s.1 in rng s by FUNCT_1:3; then
reconsider y = s.1 as Element of S;
L3:s"{y} <>{} by L2,FUNCT_1:72;
FDprobability(y,s)= 0 by AS;
hence contradiction by L3,CNT;
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;
CL30: len sx =1 & rng sx ={x} by FINSEQ_1:39;
len sx = card rng sx by CL30,CARD_1:30;
then CL40:sx is one-to-one by FINSEQ_4:62;
CL50: x in rng sx by CL30,TARSKI:def 1;
FDprobability (x,sx)=FDprobability (x,z) by DIST_1:def 4,7;
hence contradiction by CL50,CL30,CL40,FINSEQ_4:73;
end;
then Dx is well-distributed by SETFAM_1:def 8;
hence thesis;
end;
end;
theorem THnotWD:
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;
LS0: 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 EDF1,DIST_1:def 4;
hence thesis;
end;
then s is empty by emset;
hence thesis by TARSKI:def 1;
end;
then LS01: for z be element st z in D holds z in {<*>S};
for z be element st z in {<*>S} holds z in D
proof
let z be element;
assume LS015: z in {<*>S};
z is Element of D
proof
assume ASLS02:not z is Element of D;
set t = the Element of D;
t=<*>S by LS0;
hence contradiction by ASLS02,LS015,TARSKI:def 1;
end;
hence thesis;
end;
hence thesis by LS01,TARSKI:2;
end;
assume ASC1:D = {<*>S};
assume ASC2:D is well-distributed;
set s = the Element of D;
s={} by ASC1,TARSKI:def 1;
hence contradiction by ASC2;
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
C1N:canFS(S) in uniform_distribution(S) by DIST_1:def 12;
uniform_distribution(S) <>{<*>S} by C1N,TARSKI:def 1;
hence thesis by THnotWD;
end;
end;
theorem THREG1:
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 C1:p is distProbFinS of S by DIST_1:def 10;
consider t being FinSequence of S
such that CT: D = Finseq-EQclass(t) by DIST_1:def 6;
D=Finseq-EQclass(s) by CT,DIST_1:9,7;
hence thesis by C1,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 THREG1;
end;
definition
let judgefunc be BOOLEAN-valued Function;
func trueEVENT(judgefunc) -> Event of dom judgefunc equals
judgefunc"{TRUE};
coherence
proof
for x be element holds
x in judgefunc"{TRUE} implies x in dom judgefunc by FUNCT_1:def 7;
hence thesis by TARSKI:def 3;
end;
end;
theorem THREG3:
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 element 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 number 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 AS: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 AS;
end;
theorem THEXJFEQ:
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 AS:for x be set holds x=a iff judgefunc.x =TRUE;
L2: 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;
C1: for x be element holds
x in (judgefunc*s)"{TRUE} implies x in s"{a}
proof
let x be element;
assume x in (judgefunc*s)"{TRUE};
then LL0: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 LL1:x in dom s &
judgefunc.(s.x)= TRUE by LL0,FUNCT_1:11,12;
then s.x=a by AS;
then s.x in {a} by TARSKI:def 1;
hence thesis by LL1,FUNCT_1:def 7;
end;
for x be element holds
x in s"{a} implies x in (judgefunc*s)"{TRUE}
proof
let x be element;
assume ll:x in s"{a};
then LL2: x in dom s &s.x =a by L2;
s.x in S by LL2;
then LL4:s.x in dom judgefunc by FUNCT_2:def 1;
judgefunc.(s.x)= TRUE by ll,L2,AS;
then (judgefunc*s).x = TRUE by ll,L2,FUNCT_1:13;
then LL5:(judgefunc*s).x in {TRUE} by TARSKI:def 1;
x in dom (judgefunc*s) by LL2,LL4,FUNCT_1:11;
hence thesis by LL5,FUNCT_1:def 7;
end;
hence thesis by C1,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
L1: 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 L1,FINSEQ_1:def 4;
end;
end;
theorem THEXT:
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 SAI:
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 AS: f=canFS(A);
L3:(f)*(f") =id (rng f) by AS,FUNCT_1:39
.= id A by AS,FUNCT_2:def 3;
P1: dom (s|A) = (dom s) /\ A by RELAT_1:61
.= dom(s*(id A)) by FUNCT_1:19;
now let x be set;
assume P12: x in dom (s|A);
then P13: x in (dom s) /\ A by RELAT_1:61;
thus (s|A).x = s.x by P12,FUNCT_1:47
.=(s*(id A)).x by P13,FUNCT_1:20;
end; then
P2: s*(id A) = s|A by P1,FUNCT_1:2;
thus extract(s,A)*f" = s|A by P2,L3,AS,RELAT_1:36;
end;
theorem GTHTEC:
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 LLLC1: n in dom f;
L1: trueEVENT(judgefunc*f) is Subset of dom f by THREG3;
thus n in trueEVENT(judgefunc*f) implies
f.n in trueEVENT(judgefunc)
proof
assume L10AS: n in trueEVENT(judgefunc*f);
then (judgefunc*f).n in {TRUE} by FUNCT_1:def 7;
then L10L1:(judgefunc*f).n = TRUE by TARSKI:def 1;
judgefunc.(f.n)=TRUE by L10L1,L10AS,L1,FUNCT_1:13;
then L10L4:judgefunc.(f.n) in {TRUE} by TARSKI:def 1;
f.n in rng f by L10AS,L1,FUNCT_1:def 3;
then f.n in S;
then f.n in dom judgefunc by FUNCT_2:def 1;
hence thesis by L10L4,FUNCT_1:def 7;
end;
assume L20AS:f.n in trueEVENT(judgefunc);
LLL1:f.n in dom judgefunc &
judgefunc.(f.n) in {TRUE} by L20AS,FUNCT_1:def 7;
LLLC10:(judgefunc*f).n in {TRUE} by LLL1,LLLC1,FUNCT_1:13;
n in dom (judgefunc*f) by LLLC1,L20AS,FUNCT_1:11;
hence thesis by LLLC10,FUNCT_1:def 7;
end;
theorem GTHTEC2:
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;
C1: trueEVENT(judgefunc*f) is Subset of dom f by THREG3;
for x be element holds
x in f"(trueEVENT(judgefunc)) iff x in trueEVENT(judgefunc*f)
proof
let x be element;
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 GTHTEC;
end;
assume AS1: x in trueEVENT(judgefunc*f);
f.x in trueEVENT(judgefunc) by GTHTEC,AS1,C1;
hence thesis by C1,AS1,FUNCT_1:def 7;
end;
hence thesis by TARSKI:2;
end;
theorem LTHP00:
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
P00000:dom canFS(S) = Seg (card S) by FINSEQ_1:def 3;
P0000: trueEVENT(judgefunc*canFS(S)) is Event of dom canFS(S) by THREG3;
reconsider A= trueEVENT(judgefunc*canFS(S))
as Subset of dom freqSEQ(s) by P00000,P0000,DIST_1:def 9;
P020: len extract(freqSEQ(s),A) =card A by THEXT;
set L=extract(freqSEQ(s),A);
P021: dom L = Seg (card A) by P020,FINSEQ_1:def 3;
defpred P[set,set] 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 PP0: dom (canFS(A))=Seg(card (A)) by FINSEQ_1:def 3;
PP1: for x,y1,y2 be set
st x in dom L & P[x,y1] & P[x,y2] holds y1 = y2;
PP2: for x be set st x in dom L ex y be set st P[x,y]
proof
let x be set;
assume x in dom L;
then LPP22P:x in Seg (card (A)) by P020,FINSEQ_1:def 3;
set z= (canFS S).((canFS A).x);
rng (canFS A)=A by FUNCT_2:def 3; then
X1p: (canFS A).x in A by PP0,LPP22P,FUNCT_1:3;
rng (canFS S)=S by FUNCT_2:def 3;
then reconsider z as Element of S by X1p,P0000,FUNCT_1:3;
set y=s"{z};
LPP26: y=event_pick(z,s);
take y;
thus thesis by LPP26;
end;
consider G be Function such that
P1:dom G = dom L & for x be set st x in dom L
holds P[x,G.x] from FUNCT_1:sch 2(PP1,PP2);
LMISS1: 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 ZTA: a in dom G & b in dom G & a<>b; then
ZT0: a in dom(canFS(A)) & b in dom(canFS(A))
by P020,PP0,P1,FINSEQ_1:def 3;
rng (canFS(A))=A by FUNCT_2:def 3; then
ZT1P: (canFS(A)).a in A & (canFS(A)).b in A by ZT0,FUNCT_1:3;
(canFS(A)).a <> (canFS(A)).b by ZT0,ZTA,FUNCT_1:def 4; then
ZT2: (canFS(S)).((canFS(A)).a)
<>(canFS(S)).((canFS(A)).b) by ZT1P,P0000,FUNCT_1:def 4;
consider za be Element of S such that
ZT3: za=(canFS(S)).((canFS(A)).a) &
G.a=event_pick(za,s) by P1,ZTA;
consider zb be Element of S such that
ZT4: zb=(canFS(S)).((canFS(A)).b) &
G.b=event_pick(zb,s) by P1,ZTA;
thus thesis by ZT3,ZT4,ZT2,FUNCT_1:71,ZFMISC_1:11;
end;
P2: 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 ASQ3: i in dom G;
then consider zi be Element of S
such that Q3C1: zi=(canFS(S)).((canFS(A)).i) &
G.i=event_pick(zi,s) by P1;
ZT0: i in dom(canFS(A)) by P020,PP0,P1,ASQ3,FINSEQ_1:def 3;
rng (canFS(A))=A by FUNCT_2:def 3; then
XX0P: (canFS(A)).i in A by ZT0,FUNCT_1:3; then
XX0: (canFS(A)).i in Seg (card (S)) by P0000,P00000;
XX2: (canFS(A)).i in dom ( FDprobSEQ(s)) by XX0,DIST_1:def 3;
L.i =(freqSEQ(s)).((canFS(A)).i) by ASQ3,P1,THEXT
.= (len s) * ((FDprobSEQ(s)).((canFS(A)).i) ) by XX0P,DIST_1:def 9
.= (len s)*FDprobability((canFS(S)).((canFS(A)).i),s)
by XX2,DIST_1:def 3
.= card (G.i) by Q3C1,XCMPLX_1:87;
hence thesis;
end;
for a,b be set st a<>b holds G.a misses G.b
proof
let a,b be set;
assume ANB: a<>b;
per cases;
suppose a in dom G & b in dom G;
hence thesis by LMISS1,ANB;
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
P3: 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 set such that
RNGT1: j in dom G & X =G.j by FUNCT_1:def 3;
consider zj be Element of S such that
RNGT2:zj=(canFS(S)).((canFS(A)).j) & G.j=event_pick(zj,s) by P1,RNGT1;
zj in trueEVENT(judgefunc)
proof
j in dom canFS(A) by RNGT1,PP0,P1,P020,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 GTHTEC,RNGT2,P0000;
end;
then for x be element 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 RNGT1,RNGT2,GTHTEC2;
end; then
L1: union rng G c= trueEVENT(judgefunc*s) by ZFMISC_1:76;
for x be element st x in trueEVENT(judgefunc*s)
holds x in union rng G
proof
let x be element;
assume ASX: x in trueEVENT(judgefunc*s);
XX1P: trueEVENT(judgefunc*s) is Event of dom s by THREG3;
reconsider n=x as Nat by ASX;
XX3: s.n in trueEVENT(judgefunc) by XX1P,GTHTEC,ASX;
XX4FP: 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 THCANFS,XX4FP,XX3;
hence thesis;
end; then
consider m be Nat such that
XX4: 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
TT2: m in dom (canFS S) by XX4,FINSEQ_1:def 3;
XX9: m in trueEVENT(judgefunc*canFS(S)) by TT2,GTHTEC,XX3,XX4;
ex k be Nat st k in Seg (card A) & m=(canFS(A)).k
proof
reconsider m as Element of A by TT2,GTHTEC,XX3,XX4;
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 THCANFS,XX9;
hence thesis;
end; then
consider k be Nat such that
XX5: k in Seg (card A) & m=(canFS(A)).k;
s.n in {((canFS(S)).((canFS(A)).k))} by XX4,XX5,TARSKI:def 1; then
YY1:n in s"{((canFS(S)).((canFS(A)).k))}
by XX1P,ASX,FUNCT_1:def 7;
consider z be Element of S such that
XX7:z=(canFS(S)).((canFS(A)).k) &
G.k=event_pick(z,s) by XX5,P1,P021;
dom G =Seg (card A) by P1,P020,FINSEQ_1:def 3; then
G.k c=union rng G by XX5,FUNCT_1:3,ZFMISC_1:74;
hence x in union rng G by YY1,XX7;
end; then
trueEVENT(judgefunc*s) c=union rng G by TARSKI:def 3; then
P4: union rng G = trueEVENT(judgefunc*s)
by L1,XBOOLE_0:def 10;
card Union G = Sum L by P1,P2,P3,DIST_1:17;
hence thesis by P4;
end;
theorem LP5P6:
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
CDE: dom freqSEQ(s) = dom FDprobSEQ(s) by DIST_1:def 3;
for n be set st n in dom freqSEQ(s)
holds (freqSEQ(s)).n=(len s) * (FDprobSEQ(s)).n by DIST_1:def 9;
hence thesis by CDE,VALUED_1:def 5;
end;
theorem THP01:
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
P1: A= trueEVENT(judgefunc*canFS(S))&
card (trueEVENT(judgefunc*s))=
Sum extract(freqSEQ(s),A) by LTHP00;
consider B be Subset of dom freqSEQ(t) such that
P2: B= trueEVENT(judgefunc*canFS(S))&
card (trueEVENT(judgefunc*t))=
Sum extract(freqSEQ(t),B) by LTHP00;
consider v being FinSequence of S
such that CT: D = Finseq-EQclass(v) by DIST_1:def 6;
A c= dom freqSEQ(s); then
AD1P: A c= Seg (card S) by DIST_1:def 9; then
AD1: A c= dom FDprobSEQ(s) by DIST_1:def 3;
reconsider A0=A as Subset of dom FDprobSEQ(s) by AD1P,DIST_1:def 3;
reconsider A1=A as Subset of dom ((len s)(#)FDprobSEQ(s))
by AD1,VALUED_1:def 5;
B c= dom freqSEQ(t); then
BD1P: B c= Seg (card S) by DIST_1:def 9; then
BD1: B c= dom FDprobSEQ(t) by DIST_1:def 3;
reconsider B0=B as Subset of dom FDprobSEQ(t) by BD1P,DIST_1:def 3;
reconsider B1=B as Subset of dom ((len t)(#)FDprobSEQ(t))
by BD1,VALUED_1:def 5;
P6P: v,s -are_prob_equivalent by CT,DIST_1:7;
v,t -are_prob_equivalent by CT,DIST_1:7; then
P4: FDprobSEQ(s) = FDprobSEQ(t) by DIST_1:10,P6P,DIST_1:6;
P5: freqSEQ(s) =(len s)(#) FDprobSEQ(s) by LP5P6;
P6: freqSEQ(t) =(len t)(#) FDprobSEQ(t) by LP5P6;
P51: extract(((len s)* FDprobSEQ(s)),A1)
= (len s)* (extract(( FDprobSEQ(s)),A0))
proof
len extract((len s)*FDprobSEQ(s),A1) =card A1 by THEXT;
then P51L1:dom extract((len s)*FDprobSEQ(s),A1) =Seg(card A)
by FINSEQ_1:def 3;
len extract(( FDprobSEQ(s)),A0) =card A0 by THEXT;
then P51L3:
dom extract((len s)*FDprobSEQ(s),A1)
=dom extract(FDprobSEQ(s),A0) by P51L1,FINSEQ_1:def 3;
for c be set 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 set;
assume AP51L4:c in dom extract((len s)*FDprobSEQ(s),A1); then
P51L41:
(extract((len s)*FDprobSEQ(s),A1)).c
=((len s)*FDprobSEQ(s)).((canFS(A1)).c) by THEXT
.=(freqSEQ(s)).((canFS(A)).c) by DIST_1:14;
len canFS(A) = card A by FINSEQ_1:93; then
P51LL0: dom canFS(A) = Seg (card A) by FINSEQ_1:def 3;
((canFS(A)).c) in rng (canFS(A)) by P51LL0,AP51L4,P51L1,FUNCT_1:3;
then P51LL:((canFS(A)).c) in A by FUNCT_2:def 3;
(extract(FDprobSEQ(s),A0)).c
=(FDprobSEQ(s)).((canFS(A)).c) by THEXT,P51L3,AP51L4;
hence thesis by P51L41,P51LL,DIST_1:def 9;
end;
hence thesis by P51L3,VALUED_1:def 5;
end;
P61: extract(((len t)* FDprobSEQ(t)),B1)
= (len t)* (extract(( FDprobSEQ(t)),B0))
proof
len extract((len t)*FDprobSEQ(t),B1) =card B1 by THEXT;
then P61L1:dom extract((len t)*FDprobSEQ(t),B1) =Seg(card B)
by FINSEQ_1:def 3;
len extract(( FDprobSEQ(t)),B0) =card B0 by THEXT;
then P61L3:
dom extract((len t)*FDprobSEQ(t),B1)
=dom extract(FDprobSEQ(t),B0) by P61L1,FINSEQ_1:def 3;
for c be set 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 set;
assume AP61L4:c in dom extract((len t)*FDprobSEQ(t),B1); then
P61L41: (extract((len t)*FDprobSEQ(t),B1)).c
=((len t)*FDprobSEQ(t)).((canFS(B1)).c) by THEXT
.=(freqSEQ(t)).((canFS(B)).c) by DIST_1:14;
len canFS(B) = card B by FINSEQ_1:93; then
P61LL0: dom canFS(B) = Seg (card B) by FINSEQ_1:def 3;
((canFS(B)).c) in rng (canFS(B)) by P61LL0,AP61L4,P61L1,FUNCT_1:3;
then P61LLP:
((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 THEXT,P61L3,AP61L4
.=(freqSEQ(t)).((canFS(B)).c) by P61LLP,DIST_1:def 9;
hence thesis by P61L41;
end;
hence thesis by P61L3,VALUED_1:def 5;
end;
P7: card (trueEVENT(judgefunc*s))
= (len s) * Sum extract((FDprobSEQ(s)),A0) by P51,P1,P5,RVSUM_1:87;
P8: card (trueEVENT(judgefunc*t))
= (len t) * Sum extract((FDprobSEQ(t)),B0) by P61,P6,P2,RVSUM_1:87;
thus
Prob(judgefunc,s) = Sum extract((FDprobSEQ(s)),A0) by P7,XCMPLX_1:89
.=Prob(judgefunc,t) by P8,P4,P1,P2,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 number means :DefProbD:
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 THP01;
end;
uniqueness
proof
let a,b be real number;
defpred P[real number] 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 THPA1:
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 P2: dom (judgefunc*s0) = dom s0 by RELAT_1:27;
for x be element st x in Coim(judgefunc*s,TRUE) holds
x in dom s by P2,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;
L2: dom f = S by FUNCT_2:def 1;
L3: for x be element holds x in BS iff x in Coim(f,TRUE)
proof
let x be element;
LNE1: x in BS implies f.x in {TRUE}
proof
assume ASL1:x in BS;
f.x = TRUE by ASL1,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 LNE1,L2,FUNCT_1:def 7;
end;
take f;
thus thesis by L3,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 THPA1;
LMEXTH4:
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 AS:x in dom p /\ dom q;
P1P:x in dom (p 'or' q) by AS,BVFUNC_1:def 2;
then
P1:(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 P1P,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 P1;
end;
LMEXTH5:
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 AS:x in dom p /\ dom q;
x in dom (p '&' q) by AS,MARGREL1:def 18;
then (p '&' q).x = (p.x) '&' (q.x) by MARGREL1:def 18;
hence thesis by MARGREL1:12;
end;
LMEXTH6:
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 EXTH4:
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;
P1M: now let x be element;
A0: dom f = S & dom g = S by FUNCT_2:def 1;
P1:x in dom ((f 'or' g))
iff x in (dom f /\ dom g) by BVFUNC_1:def 2;
E1P: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 LMEXTH4,P1; 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 E1P,A0,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 P1M,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 EXTH5:
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;
P1M: now let x be element;
A0: dom f = S & dom g = S by FUNCT_2:def 1;
P1:x in dom ((f '&' g))
iff x in (dom f /\ dom g) by MARGREL1:def 18;
E1P: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 LMEXTH5,P1; then
x in (f '&' g)"{TRUE} iff ((x in dom f ) & (f.x in {TRUE}))
& ((x in dom g ) & (g.x = TRUE)) by E1P,A0,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;
P3:s"(f"{TRUE} /\ g"{TRUE}) c= s" (f"{TRUE}) /\ s"(g"{TRUE}) by RELAT_1:141;
for x be element st x in s" (f"{TRUE}) /\ s"(g"{TRUE}) holds
x in s"(f"{TRUE} /\ g"{TRUE})
proof
let x be element;
assume ASN1:x in s" (f"{TRUE}) /\ s"(g"{TRUE});
assume CNT: not x in s"(f"{TRUE} /\ g"{TRUE});
x in s"(f"{TRUE}) & x in s"(g"{TRUE}) by ASN1,XBOOLE_0:def 4;then
CL01: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 CNT,CL01,FUNCT_1:def 7;
hence contradiction by CL01,XBOOLE_0:def 4;
end;
then
P2: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 P1M,TARSKI:2
.= s" (f"{TRUE}) /\ s"(g"{TRUE}) by P2,P3,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 EXTH6:
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;
P1M: now let x be element;
LT: f.x =FALSE iff not f.x=TRUE by XBOOLEAN:def 3;
P1:x in dom ( 'not' f)
iff x in dom f by MARGREL1:def 17;
E1P: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 LMEXTH6,P1,LT;
then
x in ('not' f)"{TRUE} iff x in dom f &
not ( x in dom f & f.x in {TRUE}) by E1P,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
LT4: (rng s) /\ (dom f) = rng s by XBOOLE_1:28;
s"(dom f)= s"((rng s) /\ (dom f)) by RELAT_1:133;
then LT5: s"(dom f) = dom s by LT4,RELAT_1:134;
thus Coim(('not' f)*s,TRUE)
= s"(('not' f)"{TRUE}) by RELAT_1:146
.= s"(dom f \ f"{TRUE} ) by P1M,TARSKI:2
.= s" (dom f ) \ s"(f"{TRUE}) by FUNCT_1:69
.= (dom s) \ Coim(f*s,TRUE) by LT5,RELAT_1:146;
end;
theorem EXTH4A:
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;
P0: 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 EXTH4,P0
.= trueEVENT(f*s) \/ trueEVENT(g*s);
hence thesis;
end;
theorem EXTH5A:
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;
P0: 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 EXTH5,P0
.= trueEVENT(f*s) /\ trueEVENT(g*s);
hence thesis;
end;
theorem EXTH6A:
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;
P0: 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
X2: card s0 = len s by FINSEQ_1:def 3;
X1:Coim(f*s,TRUE) in bool (dom s) by P0,THPA1;
trueEVENT(('not' f)*s)=Coim(( 'not' f)*s,TRUE)
.=dom s \ Coim (f*s,TRUE) by P0,EXTH6; then
P4: card(trueEVENT(('not' f)*s))
=card(s0) - card(CfS) by X1,CARD_2:44;
thus Prob(('not' f),s) = card(s0)/(len s)
- card(CfS)/(len s) by P4,XCMPLX_1:120
.=1-Prob(f,s) by X2,XCMPLX_1:60;
end;
theorem EXTH4B:
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 EXTH4A
.=(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 EXTH5A
.= Prob(f,D) + Prob(g,s) - Prob((f '&' g),s) by DefProbD
.= Prob(f,D) + Prob(g,D) - Prob((f '&' g),s) by DefProbD
.= Prob(f,D) + Prob(g,D) - Prob((f '&' g),D) by DefProbD;
hence thesis by DefProbD;
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 DefProbD
.= 1 - Prob(f,s) by EXTH6A
.= 1 - Prob(f,D) by DefProbD;
end;
theorem EXTH6C:
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 AS: 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
X2: card s0 = len s by FINSEQ_1:def 3;
X3: s is Function of dom s,rng s by FUNCT_2:1;
X8: s is Function of dom s,S by X3,FUNCT_2:2;
X5: f is Function of dom f,rng f by FUNCT_2:1;
S c= S;
then
X6: f is Function of dom f,{TRUE} by X5,AS,INTEGRA1:17;
X7: dom f = S by FUNCT_2:def 1;
P4:trueEVENT(f*s) = s"(trueEVENT(f)) by GTHTEC2
.=s"(S) by X7,X6,FUNCT_2:40
.=dom s by X8,FUNCT_2:40;
thus Prob(f,D) = Prob(f,s) by DefProbD
.=1 by X2,P4,XCMPLX_1:60;
end;
theorem EXTH6D:
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 DefProbD
.= card (trueEVENT(f*s))/(len s);
hence 0 <= Prob(f,D);
end;
theorem EXTH6E:
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 AS:
A c= S & B c= S & f = chi(A,S) & g = chi(B,S);
P1: dom chi((A\/ B),S) = S by FUNCT_3:def 3;
P2: dom chi(A,S) = S by FUNCT_3:def 3;
P3: dom chi(B,S) = S by FUNCT_3:def 3;
P4: dom (f 'or' g)= dom f /\ dom g by BVFUNC_1:def 2
.= S by AS,P2,P3;
now let x be set;
assume AS0: x in dom (f 'or' g);
Q2: x in dom f /\ dom g by AS0,BVFUNC_1:def 2;
per cases;
suppose C0: (f 'or' g).x = TRUE;
then chi(A,S).x =1 or chi(B,S).x =1 by AS,LMEXTH4,Q2;
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 C0,AS0,FUNCT_3:def 3;
end;
suppose R1: (f 'or' g).x <> TRUE;
C0: (f 'or' g).x = FALSE by R1,XBOOLEAN:def 3;
not (chi(A,S).x =1) & not (chi(B,S).x =1) by AS,R1,LMEXTH4,Q2;
then not (x in A) & not ( x in B) by AS0,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 C0,AS0,FUNCT_3:def 3;
end;
end;
hence thesis by P1,P4,FUNCT_1:2;
end;
theorem EXTH6F:
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 AS: A c= S & B c= S & A misses B & f = chi(A,S) & g = chi(B,S);
set s = the Element of D;
P1:Prob(f '&' g,D) = Prob(f '&' g,s) by DefProbD
.= card (trueEVENT(f*s) /\ trueEVENT(g*s))/(len s) by EXTH5A;
trueEVENT(f*s) /\ trueEVENT(g*s) = {}
proof
assume trueEVENT(f*s) /\ trueEVENT(g*s) <> {};
then consider x be set such that
P1: x in trueEVENT(f*s) /\ trueEVENT(g*s) by XBOOLE_0:def 1;
Z1:trueEVENT(f*s) = s"(trueEVENT(f)) by GTHTEC2
.=s"(f"{TRUE});
Z2:trueEVENT(g*s) = s"(trueEVENT(g)) by GTHTEC2
.=s"(g"{TRUE});
x in s"(f"{TRUE}) & x in s"(g"{TRUE}) by Z1,Z2,P1,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 AS,FUNCT_3:36;
then s.x in A /\ B by XBOOLE_0:def 4;
hence contradiction by AS,XBOOLE_0:def 7;
end;
hence thesis by P1;
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
P1: 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 P1 .= Prob(x,D);
hence thesis;
end;
end;
LMPROB1:
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[set,set] means ex ch be Function of S,BOOLEAN
st ch = chi($1,S) & $2 =Prob(ch,D);
X0: now let x be set;
assume x in Trivial-SigmaField (S);
reconsider ch = chi(x,S) as Function of S,BOOLEAN by MARGREL1:def 11;
Prob(ch,D) in REAL by XREAL_0:def 1;
hence ex y be set st y in REAL & F[x,y];
end;
consider EP be Function of Trivial-SigmaField (S),REAL such that
A1: for x be set st x in Trivial-SigmaField (S) holds F[x,EP.x]
from FUNCT_2:sch 1(X0);
A2: 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
A3: A misses B;
consider chA be Function of S,BOOLEAN such that
A30: chA = chi(A,S) & EP.A = Prob(chA,D) by A1;
consider chB be Function of S,BOOLEAN such that
A31: chB = chi(B,S) & EP.B = Prob(chB,D) by A1;
consider chAB be Function of S,BOOLEAN such that
A32: chAB = chi((A\/ B),S) & EP.(A \/ B) = Prob(chAB,D) by A1;
A33: chAB = chA 'or' chB by A30,A31,A32,EXTH6E;
thus EP.(A \/ B) =Prob(chA,D) + Prob(chB,D)
- Prob( (chA '&' chB) ,D) by EXTH4B,A32,A33
.= Prob(chA,D) + Prob(chB,D) - 0 by A30,A31,A3,EXTH6F
.= EP.A + EP.B by A31,A30;
end;
A4: for A being Event of Trivial-SigmaField (S) holds 0 <= EP.A
proof
let A be Event of Trivial-SigmaField (S);
consider chA be Function of S,BOOLEAN such that
A30: chA = chi(A,S) & EP.A = Prob(chA,D) by A1;
thus thesis by A30,EXTH6D;
end;
take EP;
A5: 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
A6: for m be Nat st N<=m holds Intersection ASeq = ASeq.m
by RANDOM_1:15;
now
let m be Nat;
assume
A7: 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 A6,A7;
end;
hence thesis by PROB_1:1;
end;
consider chS be Function of S,BOOLEAN such that
A30: chS = chi(S,S) & EP.S = Prob(chS,D) by A1,MEASURE1:7;
thus thesis by A1,A4,A2,A5,A30,PROB_1:def 8,EXTH6C;
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 LMPROB1;
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 set;
assume A0: x in Trivial-SigmaField (S); then
consider ch1 be Function of S,BOOLEAN such that
A11: ch1 = chi(x,S) & F.x =Prob(ch1,D) by A1;
consider ch2 be Function of S,BOOLEAN such that
A21: ch2 = chi(x,S) & G.x =Prob(ch2,D) by A0,A2;
thus F.x = G.x by A11,A21;
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 :defSAMP:
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 number 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;
T1: 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
T2: Prob(f,s) = FDprobability (x,s) by THEXJFEQ,T1;
CTT1: Prob(x) = FDprobability (x,s) by T2,DefProbD;
consider t be FinSequence of S such that
Ct: t in D & (GenProbSEQ(S)).D=FDprobSEQ (t) by DIST_1:def 7;
Ctt:(GenProbSEQ(S)).D=FDprobSEQ (s) by Ct,DIST_1:10,EDF1;
reconsider n= x..(canFS(S)) as Nat;
len canFS(S) = card S by FINSEQ_1:93; then
LP0: dom canFS(S) = Seg (card S) by FINSEQ_1:def 3;
LL2: x in rng canFS(S) by THCANFS;then
n in dom canFS(S) by FINSEQ_4:20;then
LL3: n in dom (FDprobSEQ (s)) by LP0,DIST_1:def 3;
(canFS(S)).n =x by LL2,FINSEQ_4:19;
hence thesis by CTT1,Ctt,LL3,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 :defSAMPRNG:
ex x be sample of D st x in it;
existence
proof
set x = the sample of D;
L1: x in {x} by TARSKI:def 1;
reconsider X ={x} as non empty Element of (bool S);
take X;
thus thesis by L1;
end;
end;
definition
let S be non empty finite set,
D be EqSampleSpaces of S,
X be samplingRNG of D;
func Prob(X) -> real number equals
Prob(MembershipDecision(X),D);
coherence;
end;
theorem LDEFCSS1C00:
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 AS: SD = s"X &t = extract(s,SD);
reconsider SD as finite set;
set f= (canFS SD)";
len t = card SD by AS,THEXT;then
A1: dom t = Seg (card SD) by FINSEQ_1:def 3;
then
reconsider g= f as Function of SD, dom t by FINSEQ_1:95;
P4: (canFS SD).:(t"x) = f"(t"x) by FUNCT_1:84
.= (t*f)"x by RELAT_1:146
.= (s|SD)"x by AS,SAI
.= SD /\ s"x by FUNCT_1:70
.= s"x by AS,RELAT_1:143,XBOOLE_1:28; then
P5: card (s"x) c= card (t"x) by CARD_1:66;
P61: t"x c= Seg (card SD) by A1,RELAT_1:132;
len canFS(SD) = card SD by FINSEQ_1:93;then
P6: t"x is Subset of dom (canFS SD) by P61,FINSEQ_1:def 3;
P7: (f*(canFS SD)) = id dom (canFS SD) by FUNCT_1:39;
f.:(s"x) =(f*(canFS SD)).:(t"x) by P4,RELAT_1:126
.= t"x by P6,P7,FUNCT_1:92; then
card (t"x) c= card (s"x) by CARD_1:66;
hence thesis by P5,XBOOLE_0:def 10;
end;
theorem LDEFCSS1C:
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 AS: SD = s"X &t = extract(s,SD) & x in X;then
for a be element 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 LDEFCSS1C00,AS;
end;
theorem LDEFCSS2C:
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 AS: s in D;
consider t be FinSequence of S such that
L1: D = Finseq-EQclass(t) by DIST_1:def 6;
thus thesis by L1,DIST_1:9,AS,DIST_1:7;
end;
theorem LDEFCSS3C:
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
CF1: f=chi(X,S) & MembershipDecision(X) =f;
CF2:dom f = S by CF1,FUNCT_3:def 3;
CC1:
for x be element st x in SY holds x in SX
proof
let x be element;
assume ASL1:x in SY;
s.x in trueEVENT( f) by CF1,GTHTEC,ASL1;
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 CF1,FUNCT_3:36;
hence thesis by ASL1,FUNCT_1:def 7;
end;
for x be element st x in SX holds x in SY
proof
let x be element;
assume ASL2:x in SX;
LL22:s.x in rng s by ASL2,FUNCT_1:3;
s.x in X by ASL2,FUNCT_1:def 7;then
f.(s.x) = TRUE by CF1,FUNCT_3:def 3;then
f.(s.x) in {TRUE} by TARSKI:def 1;then
s.x in trueEVENT(f) by LL22,CF2,FUNCT_1:def 7;
hence thesis by CF1,GTHTEC,ASL2;
end;
hence thesis by CC1,TARSKI:2;
end;
theorem LDEFCSS:
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 AS:
SD1 = s1"X &t1 = extract(s1,SD1) &
SD2 = s2"X &t2 = extract(s2,SD2);
then SD1=trueEVENT((MembershipDecision(X))*s1) by LDEFCSS3C;
then L1:Prob( MembershipDecision(X),s1)
=(len t1)/(len s1) by THEXT,AS;
SD2=trueEVENT((MembershipDecision(X))*s2) by AS,LDEFCSS3C;
then L2:Prob( MembershipDecision(X),s2)
=(len t2)/(len s2) by THEXT,AS;
CL33: t1={} implies t2={} by L2,L1,THP01;
L5: 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 ASL5: n in SD1 & not x in X;
assume s1.n in {x};
then not s1.n in X by ASL5,TARSKI:def 1;
hence contradiction by AS,ASL5,FUNCT_1:def 7;
end;
L6: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 ASL5: n in SD2 & not x in X;
assume s2.n in {x};then
not s2.n in X by ASL5,TARSKI:def 1;
hence contradiction by AS,ASL5,FUNCT_1:def 7;
end;
set c = (len t1)/(len s1);
L4: c = (len t2)/(len s2) by L2,L1,THP01;
for x be set holds FDprobability (x,t1)=FDprobability (x,t2)
proof
let x be set;
per cases;
suppose L4b: t1 <> {};
per cases;
suppose ASC1:x in X;
FDprobability (x,s1)=FDprobability (x,s2) by DIST_1:def 4,EDF1
.= frequency(x,s2) / (len s2);then
frequency(x,t1) / (len s1)
= frequency(x,s2) / (len s2) by LDEFCSS1C,AS,ASC1;then
frequency(x,t1) / (len s1)
= frequency(x,t2) / (len s2) by LDEFCSS1C,AS,ASC1;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 L4,XCMPLX_1:74;
hence thesis by L4b,XCMPLX_1:5;
end;
suppose CNOTXINX: not x in X;
not ex i be set st i in t1"{x}
proof
let i be set;
assume AST1EP:i in t1"{x};then
AST1E:i in dom t1 & t1.i in {x} by FUNCT_1:def 7;
len t1 = card SD1 by AS,THEXT;then
LDOMT1:dom t1 = Seg (card SD1) by FINSEQ_1:def 3;
reconsider i as Nat by AST1EP;
LDOMT1A: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 AST1E,LDOMT1,FINSEQ_1:def 3;then
LDOMT1B:NE in rng canFS(SD1) by FUNCT_1:3;
t1.i= s1.NE by AS,AST1E,THEXT;
hence contradiction by AST1E,LDOMT1B,LDOMT1A,L5,CNOTXINX;
end;
then Coim(t1,x) is empty by XBOOLE_0:def 1;
then CNC1: FDprobability (x,t1) = 0;
not ex i be set st i in t2"{x}
proof
let i be set;
assume AST1EP:i in t2"{x};then
AST1E:i in dom t2 & t2.i in {x} by FUNCT_1:def 7;
len t2 = card SD2 by AS,THEXT;then
LDOMT1:dom t2 = Seg (card SD2) by FINSEQ_1:def 3;
reconsider i as Nat by AST1EP;
LDOMT1A: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 AST1E,LDOMT1,FINSEQ_1:def 3;then
LDOMT1B:NE in rng canFS(SD2) by FUNCT_1:3;
t2.i= s2.NE by AS,AST1E,THEXT;
hence contradiction by AST1E,LDOMT1B,LDOMT1A,L6,CNOTXINX;
end;
then Coim(t2,x) is empty by XBOOLE_0:def 1;
hence thesis by CNC1;
end;
end;
suppose t1 ={};
hence thesis by CL33;
end;
end;
hence thesis by DIST_1:def 4;
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
:defCONSS:
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 L0:x in X by defSAMPRNG;
consider s be Element of D
such that L1: x in rng s by defSAMP;
consider n being set such that
W1: n in dom s and
W2: x = s.n by L1,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;
L2:t in DX;
n in SD by W1,W2,L0,FUNCT_1:def 7;then
card SD <> 0;then
len t <> 0 by THEXT;then
t <> <*>S; then
not DX={<*>S} by L2,TARSKI:def 1;then
reconsider DX as EqSampleSpaces of S by THnotWD;
take DX;
thus thesis by L2;
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 AS1:
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
AS2:SD2 = s2"X &t2 = extract(s2,SD2) & t2 in DX2;
DX1 = Finseq-EQclass(t1) &
DX2 = Finseq-EQclass(t2) by LDEFCSS2C,AS1,AS2;
hence thesis by DIST_1:9,AS1,AS2,LDEFCSS;
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 number 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 defCONSS;
reconsider t as Element of ConditionalSS(X) by A1;
L2: len t =card SD by THEXT,A1;
L0:rng t c= X
proof
assume not rng t c= X;then
consider y be element such that
CA1: y in rng t & not y in X by TARSKI:def 3;
consider x be set such that
CA2: x in dom t & y = t.x by CA1,FUNCT_1:def 3;
CA3:dom t = Seg(card SD) by L2,FINSEQ_1:def 3;
reconsider x as Nat by CA2;
set z = (canFS(SD)).x;
CA4: 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 CA3,FINSEQ_1:def 3;then
z in rng (canFS(SD)) by CA2,FUNCT_1:3;then
z in dom s & s.z in X by A1,CA4,FUNCT_1:def 7;
hence contradiction by CA1,CA2,THEXT,A1;
end;
L1: SD = trueEVENT(g*s) by LDEFCSS3C,A1;
L3: Pp = Prob(g, s) by DefProbD
.= (len t)/(len s) by THEXT,A1,L1;
Pc= Prob(f, t ) by DefProbD
.= card (trueEVENT(f*t))/(len t);
then L5:Pc*Pp =((card (trueEVENT(f*t))/(len t))*(len t))
/(len s) by L3,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);
L6: Prob((f '&' g),s) =
card (trueEVENT(f*s) /\ trueEVENT(g*s))/(len s) by EXTH5A;
C1: t"(rng t) c= t"X by L0,RELAT_1:143;
t"(trueEVENT(f)) c= t"(rng t) by RELAT_1:135;then
t"(trueEVENT(f)) /\ t"X = t"(trueEVENT(f)) by C1,XBOOLE_1:1,28;then
L9: t"(trueEVENT(f) /\ X) = t"(trueEVENT(f)) by FUNCT_1:68;
((trueEVENT(f)) /\ X ) c= X by XBOOLE_1:17; then
L10:card (s"(trueEVENT(f) /\ X ))
= card(t"(trueEVENT(f) /\ X )) by LDEFCSS1C00,A1
.= card( trueEVENT(f*t)) by GTHTEC2,L9;
card (trueEVENT(f*t))=card (s"(trueEVENT(f)) /\ s"X) by L10,FUNCT_1:68
.=card (trueEVENT(f*s) /\ trueEVENT(g*s)) by L1,A1,GTHTEC2;
hence thesis by DefProbD,L5,L6;
end;