English
Let s be a finite set of indices and a an index not contained in s. Then the set of all finitely supported functions from insert a s to μ whose total sum is n is exactly the bi-union, over all pairs (p, q) with p ∙ q = n, of the functions obtained by taking a function from finsuppAntidiag s and updating its value at a to p, while using q as the remaining sum. In essence, inserting a new index a into s distributes the new antidiagonal across all possible splits of n into two parts with a fixed update at a.
Русский
Пусть s — конечное множество индексов, a — индекс, не принадлежащий s. Тогда множество функций с конечной опорой из insert a s в μ, сумма которых равна n, равняется объединению по всем парам (p, q) с p · q = n: берём функцию из finsuppAntidiag s и обновляем её значение в a на p, сохраняя остаток суммы q. По сути, вставка a в s распаковывает новую антидиагональ по всем разбиениям n на две части с фиксированным обновлением в a.
LaTeX
$$$\text{finsuppAntidiag}(\text{insert } a\ s)\ n = (\text{antidiagonal } n).biUnion \\quad (\lambda p : μ \times μ, \\ (\text{finsuppAntidiag } s\ p.2).attach.map \\quad \langle (\lambda f, \text{update } f.1 a p.1), \\ (\lambda \langle f, hf \rangle \langle g, hg \rangle hfg => \dots) \rangle )$$$
Lean4
theorem finsuppAntidiag_insert {a : ι} {s : Finset ι} (h : a ∉ s) (n : μ) :
finsuppAntidiag (insert a s) n =
(antidiagonal n).biUnion
(fun p : μ × μ =>
(finsuppAntidiag s p.snd).attach.map
⟨fun f => Finsupp.update f.val a p.fst,
(fun ⟨f, hf⟩ ⟨g, hg⟩ hfg =>
Subtype.ext <| by
simp only [mem_finsuppAntidiag] at hf hg
simp only [DFunLike.ext_iff] at hfg ⊢
intro x
obtain rfl | hx := eq_or_ne x a
· replace hf := mt (hf.2 ·) h
replace hg := mt (hg.2 ·) h
rw [notMem_support_iff.mp hf, notMem_support_iff.mp hg]
· simpa only [coe_update, Function.update, dif_neg hx] using hfg x)⟩) :=
by
ext f
rw [mem_finsuppAntidiag_insert h, mem_biUnion]
simp_rw [mem_map, mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk, exists_prop, and_comm, eq_comm]
