English
Let s be a finite set, f a function to a semiring, and the values commute appropriately. Then (sum_{i∈s} f(i))^n equals the sum over the antidiagonal piAntidiag(s,n) of multinomial(s,k) times the noncommutative product of powers f(i)^{k(i)} with proper commutativity.
Русский
Пусть s—конечное множество, f—функция в полусопоставимую полупродукцию, и элементы удовлетворяют требуемой коммютативности. Тогда (∑_{i∈s} f(i))^n равняется сумме по антиподиагонали piAntidiag(s,n) множителя multinomial(s,k) на произведение без учёта порядков степеней f(i)^{k(i)} с нужной коммутацией.
LaTeX
$$$(\sum_{i\in s} f(i))^n = \sum_{k\in \mathrm{piAntidiag}(s,n)} \mathrm{multinomial}(s,k)\; s.noncommProd (f(i)^{k(i)})$ (с учетом hc и mono' условий)$$
Lean4
/-- The **multinomial theorem**. -/
theorem sum_pow_eq_sum_piAntidiag_of_commute (s : Finset α) (f : α → R) (hc : (s : Set α).Pairwise (Commute on f))
(n : ℕ) :
(∑ i ∈ s, f i) ^ n =
∑ k ∈ piAntidiag s n, multinomial s k * s.noncommProd (fun i ↦ f i ^ k i) (hc.mono' fun _ _ h ↦ h.pow_pow ..) :=
by
classical
induction s using Finset.cons_induction generalizing n with
| empty => cases n <;> simp
| cons a s has ih => ?_
rw [Finset.sum_cons, piAntidiag_cons, sum_disjiUnion]
simp only [sum_map, Pi.add_apply, multinomial_cons, Pi.add_apply, if_true, Nat.cast_mul, noncommProd_cons, if_true,
sum_add_distrib, sum_ite_eq', has, if_false, add_zero, addRightEmbedding_apply]
suffices
∀ p : ℕ × ℕ,
p ∈ antidiagonal n →
∑ g ∈ piAntidiag s p.2,
((g a + p.1 + s.sum g).choose (g a + p.1) : R) * multinomial s (g + fun i ↦ ite (i = a) p.1 0) *
(f a ^ (g a + p.1) *
s.noncommProd (fun i ↦ f i ^ (g i + ite (i = a) p.1 0))
((hc.mono (by simp)).mono' fun i j h ↦ h.pow_pow ..)) =
∑ g ∈ piAntidiag s p.2,
n.choose p.1 * multinomial s g *
(f a ^ p.1 * s.noncommProd (fun i ↦ f i ^ g i) ((hc.mono (by simp)).mono' fun i j h ↦ h.pow_pow ..))
by
rw [sum_congr rfl this]
simp only [Nat.antidiagonal_eq_map, sum_map, Function.Embedding.coeFn_mk]
rw [(Commute.sum_right _ _ _ fun i hi ↦
hc (by simp) (by simp [hi]) (by simpa [eq_comm] using ne_of_mem_of_not_mem hi has)).add_pow]
simp only [ih (hc.mono (by simp)), sum_mul, mul_sum]
refine sum_congr rfl fun i _ ↦ sum_congr rfl fun g _ ↦ ?_
rw [← Nat.cast_comm, (Nat.commute_cast (f a ^ i) _).left_comm, mul_assoc]
refine fun p hp ↦ sum_congr rfl fun f hf ↦ ?_
rw [mem_piAntidiag] at hf
rw [not_imp_comm.1 (hf.2 _) has, zero_add, hf.1]
congr 2
· rw [mem_antidiagonal.1 hp]
· rw [multinomial_congr]
intro t ht
rw [Pi.add_apply, if_neg, add_zero]
exact ne_of_mem_of_not_mem ht has
refine noncommProd_congr rfl (fun t ht ↦ ?_) _
rw [if_neg, add_zero]
exact ne_of_mem_of_not_mem ht has
