Grace/Cumulus/Combinatorics/DerangementFormula.g17

Open in Workbench Download source

Imports

Derangements · Int

Declarations

Source

1-- The derangement formula: d(n) = ∑_{k ≤ n} (−1)^k (n choose k) (n − k)!,2-- the inclusion–exclusion count of the permutations with no fixed point,3-- proved in the integers from the one-step recurrence4-- d(n + 1) = (n + 1) d(n) + (−1)^(n + 1).5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Combinatorics.DerangementFormula11import Derangements12import Int1314-- The partial sums ∑_{k < j} (−1)^k (n choose k) (n − k)!: the term of15-- index k counts the permutations of n points fixing k chosen points,16-- with the sign of inclusion–exclusion.17def derangementSum (n j : Nat) → Integer18  | n, zero => integerZero19  | n, succ(k) => derangementSum(n, k) +20      integerPow(-1, k) * integerOfNat(mul(choose(n, k), factorial(sub(n, k))))2122theorem derangementSum.integer (n j : Nat)23  shows Integer(derangementSum(n, j))24proof25  induction j26  | zero =>27    simp [derangementSum]28    exact integerZero.integer29  | succ(k) using ih =>30    simp [derangementSum]31    have minus : Integer(-1) by typecheck32    have power := integerPow.integer at -1, k with minus33    have term := integerOfNat.integer at (n choose k) * (n - k)!34    typecheck3536theorem derangementSum.zero (n : Nat)37  shows derangementSum(n, 0) = 038proof39  simp [derangementSum]4041theorem derangementSum.succ (n k : Nat)42  shows derangementSum(n, k + 1) = derangementSum(n, k) +43    integerPow(-1, k) * integerOfNat((n choose k) * (n - k)!)44proof45  have one : k + 1 = succ(k) := add.right_one with *46  rw one47  simp [derangementSum]4849-- The term of index k grows by the factor n + 1 when n grows by one.50theorem choose.factorial_step (n k : Nat)51  requires le : k ≤ n52  shows ((n + 1) choose k) * (n + 1 - k)! = (n + 1) * ((n choose k) * (n - k)!)53proof54  obtain ⟨d, dNat, shape⟩ := le55  have form : n = k + d56    rw ← shape57    rfl58  have difference : n - k = d59    have commute : k + d = d + k by ring60    rw [form, commute]61    exact sub.add_right at d, k62  have differenceSucc : n + 1 - k = d + 163    have commute : k + d + 1 = (d + 1) + k by ring64    rw [form, commute]65    exact sub.add_right at d + 1, k66  have leSucc : k ≤ n + 1 by arith67  have top := choose.factorial_form at n + 1, k with leSucc68  have bottom := choose.factorial_form at n, k with le69  rw [difference, differenceSucc]70  rw differenceSucc at top71  rw difference at bottom72  have chooseTop := choose.natural at n + 1, k73  have chooseBottom := choose.natural at n, k74  have closedK := factorial.closed at k75  have closedD := factorial.closed at d76  have closedD1 := factorial.closed at d + 177  have closedN := factorial.closed at n78  have left : k! * (((n + 1) choose k) * (d + 1)!) = (n + 1)!79    have reorder : k! * (((n + 1) choose k) * (d + 1)!) =80      ((n + 1) choose k) * (k! * (d + 1)!) by ring81    rw [reorder, top]82    rfl83  have right : k! * ((n + 1) * ((n choose k) * d!)) = (n + 1)!84    have reorder : k! * ((n + 1) * ((n choose k) * d!)) =85      (n + 1) * ((n choose k) * (k! * d!)) by ring86    rw [reorder, bottom, factorial.succ]87    rfl88  have balanced : k! * (((n + 1) choose k) * (d + 1)!) =89      k! * ((n + 1) * ((n choose k) * d!))90    rw [left, right]91    rfl92  exact mul.left_cancel_positive with (factorial.nonzero at k), balanced9394-- Up to the last term, the sums for n + 1 and for n differ by the factor95-- n + 1.96theorem derangementSum.scale (n j : Nat)97  shows j ≤ n + 1 →98    derangementSum(n + 1, j) = integerOfNat(n + 1) * derangementSum(n, j)99proof100  induction j101  | zero =>102    intro le103    rw [derangementSum.zero, derangementSum.zero]104    have top := integerOfNat.integer at n + 1105    ring106  | k + 1 using ih =>107    intro le108    have kLe : k ≤ n by arith109    have kLeSucc : k ≤ n + 1 by arith110    have inner := ih with kLeSucc111    rw [derangementSum.succ, derangementSum.succ, inner]112    have term := choose.factorial_step with kLe113    rw [term, integerOfNat.mul]114    have minus : Integer(-1) by typecheck115    have power := integerPow.integer at -1, k with minus116    have sumInt := derangementSum.integer at n, k117    have topInt := integerOfNat.integer at n + 1118    have termInt := integerOfNat.integer at (n choose k) * (n - k)!119    ring120121-- The one-step recurrence d(n + 1) = (n + 1) d(n) + (−1)^(n + 1), in ℤ.122theorem derangement.succ_integer (n : Nat)123  shows integerOfNat(derangement(n + 1)) =124    integerOfNat(n + 1) * integerOfNat(derangement(n)) + integerPow(-1, n + 1)125proof126  have minus : Integer(-1) by typecheck127  have alternatives := parity.exhaustive at n128  cases alternatives with even | odd129  . have iff := Even.iff_two_mul at n130    obtain ⟨k, kNat, shape⟩ := iff.forward with even131    rw shape132    have step := derangement.odd_succ at k133    have cast : integerOfNat(derangement(2 * k + 1) + 1) =134        integerOfNat((2 * k + 1) * derangement(2 * k))135      rw step136      rfl137    rw [integerOfNat.add, integerOfNat.mul, integerOfNat.one] at cast138    have sign : integerPow(-1, 2 * k + 1) = -1139      have double : 2 * k + 1 = k + k + 1 by ring140      rw [double, integerPow.neg_double_add_one, integerPow.one_left]141      rfl142    rw sign143    have dInt := integerOfNat.integer at derangement(2 * k + 1)144    have unfold : integerOfNat(derangement(2 * k + 1)) =145        (integerOfNat(derangement(2 * k + 1)) + 1) + -1 by ring146    rw [unfold, cast]147    have topInt := integerOfNat.integer at 2 * k + 1148    have previousInt := integerOfNat.integer at derangement(2 * k)149    ring150  . have iff := Odd.iff_two_mul_add_one at n151    obtain ⟨k, kNat, shape⟩ := iff.forward with odd152    rw shape153    have step := derangement.even_succ at k154    have two : 2 * k + 1 + 1 = 2 * k + 2 by ring155    rw two156    have cast : integerOfNat(derangement(2 * k + 2)) =157        integerOfNat((2 * k + 2) * derangement(2 * k + 1) + 1)158      rw step159      rfl160    rw [integerOfNat.add, integerOfNat.mul, integerOfNat.one] at cast161    have sign : integerPow(-1, 2 * k + 2) = 1162      have double : 2 * k + 2 = (k + 1) + (k + 1) by ring163      rw [double, integerPow.neg_double, integerPow.one_left]164      rfl165    rw [sign, cast]166    rfl167168-- The derangement formula.169theorem derangement.closed_form (n : Nat)170  shows integerOfNat(derangement(n)) = derangementSum(n, n + 1)171proof172  induction n173  | zero =>174    have shape := derangementSum.succ at 0, 0175    have term : (0 choose 0) * (0 - 0)! = 1 by compute176    rw [derangement.zero, integerOfNat.one, shape, term]177    rw [derangementSum.zero, integerPow.zero, integerOfNat.one]178    ring179  | k + 1 using ih =>180    have step := derangement.succ_integer at k181    have last : ((k + 1) choose (k + 1)) * (k + 1 - (k + 1))! = 1182      rw [choose.diagonal, sub.self]183      compute184    have scale := derangementSum.scale at k, k + 1185    have scaled := scale with (LessEqual.reflexive at k + 1)186    rw [derangementSum.succ, last, integerOfNat.one, scaled, step, ih]187    have minus : Integer(-1) by typecheck188    have power := integerPow.integer at -1, k + 1 with minus189    have sumInt := derangementSum.integer at k, k + 1190    have topInt := integerOfNat.integer at k + 1191    ring192