:: Counting Derangements, Counting Non Bijective Functions and the Birthday Problem
:: by Cezary Kaliszyk
::
:: Received February 23, 2010
:: Copyright (c) 2010-2021 Association of Mizar Users


registration
let c be Real;
cluster exp_R c -> positive ;
coherence
exp_R c is positive
by SIN_COS:55;
end;

theorem Th1: :: CARDFIN2:1
id {} is without_fixpoints
proof end;

theorem Th2: :: CARDFIN2:2
for c being Real st c < 0 holds
exp_R c < 1
proof end;

definition
let n be Real;
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 holds round n = [\(n + (1 / 2))/];

theorem :: CARDFIN2:3
for a being Integer holds round a = a
proof end;

theorem Th4: :: CARDFIN2:4
for a being Integer
for b being Real st |.(a - b).| < 1 / 2 holds
a = round b
proof end;

theorem Th5: :: CARDFIN2:5
for n being Nat
for a, b being Real st a < b holds
ex c being Real 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) !)) )
proof end;

theorem Th6: :: CARDFIN2:6
for n being positive Nat
for c being Real st c < 0 holds
|.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2
proof end;

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
proof end;
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 ) )
}
proof end;

theorem Th8: :: CARDFIN2:8
for s being non empty finite set ex c being Real st
( c in ].(- 1),0.[ & (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) )
proof end;

theorem Th9: :: CARDFIN2:9
for s being non empty finite set holds |.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2
proof end;

theorem Th10: :: CARDFIN2:10
for s being non empty finite set holds card (derangements s) = round (((card s) !) / number_e)
proof end;

theorem Th11: :: CARDFIN2:11
derangements {} = {{}}
proof end;

theorem Th12: :: CARDFIN2:12
for x being object holds derangements {x} = {}
proof end;

reconsider j = 1, z = 0 as Element of INT by INT_1:def 2;

deffunc H1( Nat, Integer, Integer) -> Element of INT = In ((($1 + 1) * ($2 + $3)),INT);

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))) ) )
proof end;
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
proof end;
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 INT ;
cluster c (#) F -> INT -valued Sequence-like finite ;
coherence
( c (#) F is finite & c (#) F is INT -valued & c (#) F is Sequence-like )
;
end;

registration
let c be Complex;
let F be empty Function;
cluster c (#) F -> empty ;
coherence
c (#) F is empty
;
end;

theorem :: CARDFIN2:13
for F being XFinSequence of INT
for c being Integer holds c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))
proof end;

:: 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 INT 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))
proof end;

theorem :: CARDFIN2:15
for s being finite set holds der_seq . (card s) = card (derangements s)
proof end;

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))
proof end;
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[ object ] } :
{ 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() = {} )
proof end;

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)) !))
proof end;

Lm1: 2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) > 365 |^ 23
proof end;

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))
proof end;

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
proof end;