English
There exists a finite indexing β, a sign function sgn: β → SignType, and a map g: β → α, such that every g(b) ∈ s, the cardinality of β equals the sum of natAbs of f over s, and for each a ∈ s, the sum over b with g(b) = a of sgn(b) equals f(a).
Русский
Существует конечная индексация β, функция знаков sgn: β → SignType и отображение g: β → α, такие что ∀ b, g(b) ∈ s, кардинал β равен сумме natAbs(f) по s, и для каждого a ∈ s сумма по b с g(b)=a равна f(a).
LaTeX
$$$\exists \beta \;\; (Fintype \beta) \; (\text{sgn}: \beta \to SignType) \; (g: \beta \to \alpha),\quad (\forall b, g b \in s) \land (Fintype.card \beta = \sum_{a \in s} (f a).natAbs) \land (\forall a \in s, \sum_{b} (\text{if } g b = a \text{ then } (\text{sgn} b : \mathbb{Z}) \text{ else } 0) = f a)$$$
Lean4
/-- We can decompose a sum of absolute value `n` into a sum of `n` signs. -/
theorem exists_signed_sum [DecidableEq α] (s : Finset α) (f : α → ℤ) :
∃ (β : Type u) (_ : Fintype β) (sgn : β → SignType) (g : β → α),
(∀ b, g b ∈ s) ∧
(Fintype.card β = ∑ a ∈ s, (f a).natAbs) ∧ ∀ a ∈ s, (∑ b, if g b = a then (sgn b : ℤ) else 0) = f a :=
let ⟨β, t, sgn, g, hg, ht, hf⟩ := exists_signed_sum_aux s f
⟨t, inferInstance, fun b => sgn b, fun b => g b, fun b => hg b, by simp [ht], fun a ha =>
(sum_attach t fun b ↦ ite (g b = a) (sgn b : ℤ) 0).trans <| hf _ ha⟩
