English
For any a and f, the multinomial of f equals the product of a binomial factor choosing f(a) and the multinomial of f with a set to zero.
Русский
Для любого элемента a и функции f выполняется связь мультиномиала: multinomial(f) = C(f(a)) · multinomial(f, a ↦ 0).
LaTeX
$$$f.multinomial = \binom{\sum} {f(a)} \cdot (f.update\ a\ 0).multinomial$$$
Lean4
theorem multinomial_update (a : α) (f : α →₀ ℕ) :
f.multinomial = (f.sum fun _ => id).choose (f a) * (f.update a 0).multinomial :=
by
simp only [multinomial_eq]
classical
by_cases h : a ∈ f.support
· rw [← Finset.insert_erase h, Nat.multinomial_insert (Finset.notMem_erase a _), Finset.add_sum_erase _ f h,
support_update_zero]
congr 1
exact Nat.multinomial_congr fun _ h ↦ (Function.update_of_ne (mem_erase.1 h).1 0 f).symm
rw [notMem_support_iff] at h
rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
