let S be non empty finite set ; for X being non empty Subset of S
for D being EqSampleSpaces of S
for s1, s2 being Element of D
for t1, t2 being FinSequence of S
for SD1 being Subset of (dom s1)
for SD2 being 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
let X be non empty Subset of S; for D being EqSampleSpaces of S
for s1, s2 being Element of D
for t1, t2 being FinSequence of S
for SD1 being Subset of (dom s1)
for SD2 being 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
let D be EqSampleSpaces of S; for s1, s2 being Element of D
for t1, t2 being FinSequence of S
for SD1 being Subset of (dom s1)
for SD2 being 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
let s1, s2 be Element of D; for t1, t2 being FinSequence of S
for SD1 being Subset of (dom s1)
for SD2 being 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
let t1, t2 be FinSequence of S; for SD1 being Subset of (dom s1)
for SD2 being 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
let SD1 be Subset of (dom s1); for SD2 being 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
let SD2 be Subset of (dom s2); ( SD1 = s1 " X & t1 = extract (s1,SD1) & SD2 = s2 " X & t2 = extract (s2,SD2) implies t1,t2 -are_prob_equivalent )
assume A1:
( SD1 = s1 " X & t1 = extract (s1,SD1) & SD2 = s2 " X & t2 = extract (s2,SD2) )
; t1,t2 -are_prob_equivalent
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 being set st n in SD1 & not x in X holds
not s1 . n in {x}
A7:
for n, x being set st n in SD2 & not x in X holds
not s2 . n in {x}
set c = (len t1) / (len s1);
A9:
(len t1) / (len s1) = (len t2) / (len s2)
by A3, A2, Th17;
for x being set holds FDprobability (x,t1) = FDprobability (x,t2)
proof
let x be
set ;
FDprobability (x,t1) = FDprobability (x,t2)
per cases
( t1 <> {} or t1 = {} )
;
suppose A10:
t1 <> {}
;
FDprobability (x,t1) = FDprobability (x,t2)per cases
( x in X or not x in X )
;
suppose A11:
x in X
;
FDprobability (x,t1) = FDprobability (x,t2) 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)) * ((len t1) / (len s1)) = (FDprobability (x,t2)) * ((len t1) / (len s1))
by A9, XCMPLX_1:74;
hence
FDprobability (
x,
t1)
= FDprobability (
x,
t2)
by A10, XCMPLX_1:5;
verum end; end; end; end;
end;
hence
t1,t2 -are_prob_equivalent
; verum