English
A comprehensive sum formula: a product of divided powers across a finite index set equals a multinomial coefficient times the divided power of the sum.
Русский
Полная сумма: произведение делённых степеней по конечному множеству индексов равно мультибиномиальному коэффициенту, умноженному на dpow суммы.
LaTeX
$$$$ \\prod_{i \\in s} hI.dpow (n_i) a = \\mathrm{multinomial}(s,n) \\cdot hI.dpow(\\sum_i n_i) a $$$$
Lean4
/-- Lemma towards `dpow_sum` when we only have partial information on a divided power ideal -/
theorem dpow_sum' {M : Type*} [AddCommMonoid M] {I : AddSubmonoid M} (dpow : ℕ → M → A)
(dpow_zero : ∀ {x}, x ∈ I → dpow 0 x = 1)
(dpow_add : ∀ {n x y}, x ∈ I → y ∈ I → dpow n (x + y) = (antidiagonal n).sum fun k ↦ dpow k.1 x * dpow k.2 y)
(dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0) {ι : Type*} [DecidableEq ι] {s : Finset ι} {x : ι → M}
(hx : ∀ i ∈ s, x i ∈ I) {n : ℕ} :
dpow n (s.sum x) = (s.sym n).sum fun k ↦ s.prod fun i ↦ dpow (Multiset.count i k) (x i) :=
by
simp only [sum_antidiagonal_eq_sum_range_succ_mk] at dpow_add
induction s using Finset.induction generalizing n with
| empty =>
simp only [sum_empty, prod_empty, sum_const, nsmul_eq_mul, mul_one]
by_cases hn : n = 0
· rw [hn]
rw [dpow_zero I.zero_mem]
simp only [sym_zero, card_singleton, cast_one]
· rw [dpow_eval_zero hn, eq_comm, ← cast_zero]
apply congr_arg
rw [card_eq_zero, sym_eq_empty]
exact ⟨hn, rfl⟩
| insert a s ha ih =>
-- This should be golfable using `Finset.symInsertEquiv`
have hx' : ∀ i, i ∈ s → x i ∈ I := fun i hi ↦ hx i (mem_insert_of_mem hi)
simp_rw [sum_insert ha, dpow_add (hx a (mem_insert_self a s)) (I.sum_mem fun i ↦ hx' i), sum_range, ih hx', mul_sum,
sum_sigma', eq_comm]
apply
sum_bij' (fun m _ ↦ m.filterNe a) (fun m _ ↦ m.2.fill a m.1) (fun m hm ↦ mem_sigma.2 ⟨mem_univ _, _⟩)
(fun m hm ↦ by
simp only [succ_eq_add_one, mem_sym_iff, mem_insert, Sym.mem_fill_iff]
simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
intro b
apply Or.imp (fun h ↦ h.2) (fun h ↦ hm b h))
(fun m _ ↦ m.fill_filterNe a)
· intro m hm
simp only [mem_sigma, mem_univ, mem_sym_iff, true_and] at hm
exact Sym.filter_ne_fill a m fun a_1 ↦ ha (hm a a_1)
· intro m hm
simp only [mem_sym_iff, mem_insert] at hm
rw [prod_insert ha]
apply congr_arg₂ _ rfl
apply prod_congr rfl
intro i hi
apply congr_arg₂ _ _ rfl
conv_lhs => rw [← m.fill_filterNe a]
exact Sym.count_coe_fill_of_ne (ne_of_mem_of_not_mem hi ha)
· intro m hm
convert sym_filterNe_mem a hm
rw [erase_insert ha]
