English
The piAntidiag construction collects all functions with support in a fixed set and prescribed total, aggregating finite sums into a Finset of functions.
Русский
Конструкция piAntidiag собирает все функции с опорой в заданном множестве и заданной суммой, образуя Finset функций.
LaTeX
$$$\text{piAntidiag}(s,n) = \text{Finset of }f: s\to ?\text{ such that } \sum_{i\in s} f(i)=n$$$
Lean4
@[simp]
theorem mem_piAntidiag : f ∈ piAntidiag s n ↔ s.sum f = n ∧ ∀ i, f i ≠ 0 → i ∈ s :=
by
rw [piAntidiag]
induction Fintype.truncEquivFinOfCardEq (Fintype.card_coe s) using Trunc.ind with
| _ e
simp only [Trunc.lift_mk, mem_map, mem_finAntidiagonal, Embedding.coeFn_mk]
constructor
· rintro ⟨f, ⟨hf, rfl⟩, rfl⟩
rw [sum_dite_of_true fun _ ↦ id]
exact ⟨Fintype.sum_equiv e _ _ (by simp), by simp +contextual⟩
· rintro ⟨rfl, hf⟩
refine ⟨f ∘ (↑) ∘ e.symm, ?_, by grind⟩
rw [← sum_attach s]
exact Fintype.sum_equiv e.symm _ _ (by simp)
