:: Counting Derangements, Counting Non Bijective Functions and the Birthday Problem :: by Cezary Kaliszyk :: :: Received February 23, 2010 :: Copyright (c) 2010-2012 Association of Mizar Users begin registration let c be real number ; cluster exp_R c -> positive ; coherence exp_R c is positive by SIN_COS:55; end; registration cluster number_e -> positive ; coherence number_e is positive by TAYLOR_1:11; end; theorem Th1: :: CARDFIN2:1 id {} is without_fixpoints proofend; theorem Th2: :: CARDFIN2:2 for c being real number st c < 0 holds exp_R c < 1 proofend; begin definition let n be real number ; func round n -> Integer equals :: CARDFIN2:def 1 [\(n + (1 / 2))/]; coherence [\(n + (1 / 2))/] is Integer ; end; :: deftheorem defines round CARDFIN2:def_1_:_ for n being real number holds round n = [\(n + (1 / 2))/]; theorem :: CARDFIN2:3 for a being Integer holds round a = a proofend; theorem Th4: :: CARDFIN2:4 for a being Integer for b being real number st |.(a - b).| < 1 / 2 holds a = round b proofend; begin theorem Th5: :: CARDFIN2:5 for n being Nat for a, b being real number st a < b holds ex c being real number st ( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) proofend; theorem Th6: :: CARDFIN2:6 for n being positive Nat for c being real number st c < 0 holds |.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2 proofend; definition let s be set ; func derangements s -> set equals :: CARDFIN2:def 2 { f where f is Permutation of s : f is without_fixpoints } ; coherence { f where f is Permutation of s : f is without_fixpoints } is set ; end; :: deftheorem defines derangements CARDFIN2:def_2_:_ for s being set holds derangements s = { f where f is Permutation of s : f is without_fixpoints } ; registration let s be finite set ; cluster derangements s -> finite ; coherence derangements s is finite proofend; end; theorem Th7: :: CARDFIN2:7 for s being finite set holds derangements s = { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds h . x <> x ) ) } proofend; theorem Th8: :: CARDFIN2:8 for s being non empty finite set ex c being real number st ( c in ].(- 1),0.[ & (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) ) proofend; theorem Th9: :: CARDFIN2:9 for s being non empty finite set holds |.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2 proofend; theorem Th10: :: CARDFIN2:10 for s being non empty finite set holds card (derangements s) = round (((card s) !) / number_e) proofend; theorem Th11: :: CARDFIN2:11 derangements {} = {{}} proofend; theorem Th12: :: CARDFIN2:12 for x being set holds derangements {x} = {} proofend; reconsider j = 1, z = 0 as Element of INT by INT_1:def_2; deffunc H1( Element of NAT , Integer, Integer) -> Element of INT = ($1 + 1) * ($2 + $3); definition func der_seq -> sequence of INT means :Def3: :: CARDFIN2:def 3 ( it . 0 = 1 & it . 1 = 0 & ( for n being Nat holds it . (n + 2) = (n + 1) * ((it . n) + (it . (n + 1))) ) ); existence ex b1 being sequence of INT st ( b1 . 0 = 1 & b1 . 1 = 0 & ( for n being Nat holds b1 . (n + 2) = (n + 1) * ((b1 . n) + (b1 . (n + 1))) ) ) proofend; uniqueness for b1, b2 being sequence of INT st b1 . 0 = 1 & b1 . 1 = 0 & ( for n being Nat holds b1 . (n + 2) = (n + 1) * ((b1 . n) + (b1 . (n + 1))) ) & b2 . 0 = 1 & b2 . 1 = 0 & ( for n being Nat holds b2 . (n + 2) = (n + 1) * ((b2 . n) + (b2 . (n + 1))) ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines der_seq CARDFIN2:def_3_:_ for b1 being sequence of INT holds ( b1 = der_seq iff ( b1 . 0 = 1 & b1 . 1 = 0 & ( for n being Nat holds b1 . (n + 2) = (n + 1) * ((b1 . n) + (b1 . (n + 1))) ) ) ); registration let c be Integer; let F be XFinSequence of ; clusterc (#) F -> T-Sequence-like INT -valued finite ; coherence ( c (#) F is finite & c (#) F is INT -valued & c (#) F is T-Sequence-like ) ; end; registration let c be complex number ; let F be empty Function; clusterc (#) F -> empty ; coherence c (#) F is empty ; end; theorem :: CARDFIN2:13 for F being XFinSequence of for c being Integer holds c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1))) proofend; :: This theorem is symmetric to the previous one. Since we use Integers :: we cannot divide and it has to be proved separately. theorem Th14: :: CARDFIN2:14 for X, N being XFinSequence of st len N = (len X) + 1 holds for c being Integer st N | (len X) = c (#) X holds Sum N = (c * (Sum X)) + (N . (len X)) proofend; theorem :: CARDFIN2:15 for s being finite set holds der_seq . (card s) = card (derangements s) proofend; begin definition let s, t be set ; func not-one-to-one (s,t) -> Subset of (Funcs (s,t)) equals :: CARDFIN2:def 4 { f where f is Function of s,t : not f is one-to-one } ; coherence { f where f is Function of s,t : not f is one-to-one } is Subset of (Funcs (s,t)) proofend; end; :: deftheorem defines not-one-to-one CARDFIN2:def_4_:_ for s, t being set holds not-one-to-one (s,t) = { f where f is Function of s,t : not f is one-to-one } ; registration let s, t be finite set ; cluster not-one-to-one (s,t) -> finite ; coherence not-one-to-one (s,t) is finite ; end; scheme :: CARDFIN2:sch 1 FraenkelDiff{ F1() -> set , F2() -> set , P1[ set ] } : { f where f is Function of F1(),F2() : P1[f] } = (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] } provided A1: ( F2() = {} implies F1() = {} ) proofend; theorem Th16: :: CARDFIN2:16 for s, t being finite set st card s <= card t holds card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !)) proofend; Lm1: 2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) > 365 |^ 23 proofend; theorem Th17: :: CARDFIN2:17 for s being finite set for t being non empty finite set st card s = 23 & card t = 365 holds 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t)) proofend; theorem :: CARDFIN2:18 for s, t being non empty finite set st card s = 23 & card t = 365 holds prob (not-one-to-one (s,t)) > 1 / 2 proofend;