English
The proportion of derangements among all permutations tends to e^{-1} as the size grows to infinity.
Русский
Доля дерangements среди всех перестановок стремится к e^{-1} при бесконечном росте размера.
LaTeX
$$$\lim_{n\to\infty} \frac{\mathrm{numDerangements}(n)}{n!} = e^{-1}$$$
Lean4
theorem numDerangements_tendsto_inv_e :
Tendsto (fun n => (numDerangements n : ℝ) / n.factorial) atTop (𝓝 (Real.exp (-1))) := by
-- we show that d(n)/n! is the partial sum of exp(-1), but offset by 1.
-- this isn't entirely obvious, since we have to ensure that asc_factorial and
-- factorial interact in the right way, e.g., that k ≤ n always
let s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1 : ℝ) ^ k / k.factorial
suffices ∀ n : ℕ, (numDerangements n : ℝ) / n.factorial = s (n + 1)
by
simp_rw [this]
-- shift the function by 1, and then use the fact that the partial sums
-- converge to the infinite sum
rw [tendsto_add_atTop_iff_nat (f := fun n => ∑ k ∈ Finset.range n, (-1 : ℝ) ^ k / k.factorial) 1]
apply HasSum.tendsto_sum_nat
rw [Real.exp_eq_exp_ℝ]
exact expSeries_div_hasSum_exp ℝ (-1 : ℝ)
intro n
rw [← Int.cast_natCast, numDerangements_sum]
push_cast
rw [Finset.sum_div]
-- get down to individual terms
refine Finset.sum_congr (refl _) ?_
intro k hk
have h_le : k ≤ n := Finset.mem_range_succ_iff.mp hk
rw [Nat.ascFactorial_eq_div, add_tsub_cancel_of_le h_le]
push_cast [Nat.factorial_dvd_factorial h_le]
field_simp
