let S be non empty finite set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ( 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) ) ; :: thesis: 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}
proof
let n, x be set ; :: thesis: ( n in SD1 & not x in X implies not s1 . n in {x} )
assume A6: ( n in SD1 & not x in X ) ; :: thesis: not s1 . n in {x}
assume s1 . n in {x} ; :: thesis: contradiction
then not s1 . n in X by A6, TARSKI:def 1;
hence contradiction by A1, A6, FUNCT_1:def 7; :: thesis: verum
end;
A7: for n, x being set st n in SD2 & not x in X holds
not s2 . n in {x}
proof
let n, x be set ; :: thesis: ( n in SD2 & not x in X implies not s2 . n in {x} )
assume A8: ( n in SD2 & not x in X ) ; :: thesis: not s2 . n in {x}
assume s2 . n in {x} ; :: thesis: contradiction
then not s2 . n in X by A8, TARSKI:def 1;
hence contradiction by A1, A8, FUNCT_1:def 7; :: thesis: verum
end;
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 ; :: thesis: FDprobability (x,t1) = FDprobability (x,t2)
per cases ( t1 <> {} or t1 = {} ) ;
suppose A10: t1 <> {} ; :: thesis: FDprobability (x,t1) = FDprobability (x,t2)
per cases ( x in X or not x in X ) ;
suppose A11: x in X ; :: thesis: 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; :: thesis: verum
end;
suppose A12: not x in X ; :: thesis: FDprobability (x,t1) = FDprobability (x,t2)
for i being object holds not i in t1 " {x}
proof
let i be object ; :: thesis: not i in t1 " {x}
assume A13: i in t1 " {x} ; :: thesis: contradiction
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 = 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: (canFS SD1) . i in rng (canFS SD1) by FUNCT_1:3;
t1 . i = s1 . ((canFS SD1) . i) by A1, A14, Th11;
hence contradiction by A14, A17, A16, A5, A12; :: thesis: verum
end;
then Coim (t1,x) is empty by XBOOLE_0:def 1;
then A18: FDprobability (x,t1) = 0 ;
for i being object holds not i in t2 " {x}
proof
let i be object ; :: thesis: not i in t2 " {x}
assume A19: i in t2 " {x} ; :: thesis: contradiction
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 = 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: (canFS SD2) . i in rng (canFS SD2) by FUNCT_1:3;
t2 . i = s2 . ((canFS SD2) . i) by A1, A20, Th11;
hence contradiction by A20, A23, A22, A7, A12; :: thesis: verum
end;
then Coim (t2,x) is empty by XBOOLE_0:def 1;
hence FDprobability (x,t1) = FDprobability (x,t2) by A18; :: thesis: verum
end;
end;
end;
end;
end;
hence t1,t2 -are_prob_equivalent ; :: thesis: verum