:: 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 H₁( 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 b₁ being sequence of INT st
( b₁ . 0 = 1 & b₁ . 1 = 0 & ( for n being Nat holds b₁ . (n + 2) = (n + 1) * ((b₁ . n) + (b₁ . (n + 1))) ) )

proof end;

uniqueness
for b₁, b₂ being sequence of INT st b₁ . 0 = 1 & b₁ . 1 = 0 & ( for n being Nat holds b₁ . (n + 2) = (n + 1) * ((b₁ . n) + (b₁ . (n + 1))) ) & b₂ . 0 = 1 & b₂ . 1 = 0 & ( for n being Nat holds b₂ . (n + 2) = (n + 1) * ((b₂ . n) + (b₂ . (n + 1))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines der_seq CARDFIN2:def 3 :
for b₁ being sequence of INT holds
( b₁ = der_seq iff ( b₁ . 0 = 1 & b₁ . 1 = 0 & ( for n being Nat holds b₁ . (n + 2) = (n + 1) * ((b₁ . n) + (b₁ . (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{ F₁() -> set , F₂() -> set , P₁[ object ] } :

{ f where f is Function of F₁(),F₂() : P₁[f] } = (Funcs (F₁(),F₂())) \ { f where f is Function of F₁(),F₂() : P₁[f] }

provided

A1: ( F₂() = {} implies F₁() = {} )

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;