let S be non empty finite set ; for D being EqSampleSpaces of S
for X being samplingRNG of D
for f being Function of S,BOOLEAN holds (Prob (f,X)) * (Prob X) = Prob ((f '&' (MembershipDecision X)),D)
let D be EqSampleSpaces of S; for X being samplingRNG of D
for f being Function of S,BOOLEAN holds (Prob (f,X)) * (Prob X) = Prob ((f '&' (MembershipDecision X)),D)
let X be samplingRNG of D; for f being Function of S,BOOLEAN holds (Prob (f,X)) * (Prob X) = Prob ((f '&' (MembershipDecision X)),D)
let f be Function of S,BOOLEAN; (Prob (f,X)) * (Prob X) = Prob ((f '&' (MembershipDecision X)),D)
set g = MembershipDecision X;
set Pc = Prob (f,X);
set Pp = Prob X;
consider s being Element of D, t being FinSequence of S, SD being Subset of (dom s) such that
A1:
( SD = s " X & t = extract (s,SD) & t in ConditionalSS X )
by Def14;
reconsider t = t as Element of ConditionalSS X by A1;
A2:
len t = card SD
by Th11, A1;
A3:
rng t c= X
A8:
SD = trueEVENT ((MembershipDecision X) * s)
by Th37, A1;
A9: Prob X =
Prob ((MembershipDecision X),s)
by Def6
.=
(len t) / (len s)
by Th11, A1, A8
;
Prob (f,X) =
Prob (f,t)
by Def6
.=
(card (trueEVENT (f * t))) / (len t)
;
then A10: (Prob (f,X)) * (Prob X) =
(((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 '&' (MembershipDecision X)),s) = (card ((trueEVENT (f * s)) /\ (trueEVENT ((MembershipDecision X) * s)))) / (len s)
by Th25;
A12:
t " (rng t) c= t " X
by A3, RELAT_1:143;
t " (trueEVENT f) c= t " (rng t)
by RELAT_1:135;
then
(t " (trueEVENT f)) /\ (t " X) = t " (trueEVENT f)
by A12, XBOOLE_1:1, XBOOLE_1:28;
then A13:
t " ((trueEVENT f) /\ X) = t " (trueEVENT f)
by FUNCT_1:68;
(trueEVENT f) /\ X c= X
by XBOOLE_1:17;
then A14: card (s " ((trueEVENT f) /\ X)) =
card (t " ((trueEVENT f) /\ X))
by Th34, A1
.=
card (trueEVENT (f * t))
by Th14, A13
;
card (trueEVENT (f * t)) =
card ((s " (trueEVENT f)) /\ (s " X))
by A14, FUNCT_1:68
.=
card ((trueEVENT (f * s)) /\ (trueEVENT ((MembershipDecision X) * s)))
by A8, A1, Th14
;
hence
(Prob (f,X)) * (Prob X) = Prob ((f '&' (MembershipDecision X)),D)
by Def6, A10, A11; verum