English
If a finite sum of absolute values of an integer-valued function f over a finite set s is at most n, then one can express all those values as a sum of at most n signed terms indexed by a finite type β, with a prescribed zero outside s, and matching each f(a) for a ∈ s.
Русский
Пусть s — конечное множество, f : α → ℤ, и сумма ∑_{i∈s} |f(i)| ≤ n. Тогда существует конечный тип β и отображения sg n, g так, что сумма знаков в β дает значения f на s и ноль вне s, причём длина β равна n.
LaTeX
$$$\\exists \\beta, (\\mathrm{Fintype}\\,\\beta)\\, (\\mathrm{sgn}:\\beta \\to \\mathrm{SignType})\\, (g:\\beta \\to \\alpha),\\; (\\forall b, g\\,b \\notin s \\to (sgn\\,b)=0) \\\\ \\, (Fintype.card\\,\\beta)=n \\\\ \\, (\\forall a\\in s, \\sum_i (\\mathbf{1}_{g(i)=a}\\cdot (sgn\\,i)) = f(a)). $$$
Lean4
/-- We can decompose a sum of absolute value less than `n` into a sum of at most `n` signs. -/
theorem exists_signed_sum' [Nonempty α] [DecidableEq α] (s : Finset α) (f : α → ℤ) (n : ℕ)
(h : (∑ i ∈ s, (f i).natAbs) ≤ n) :
∃ (β : Type u) (_ : Fintype β) (sgn : β → SignType) (g : β → α),
(∀ b, g b ∉ s → sgn b = 0) ∧ Fintype.card β = n ∧ ∀ a ∈ s, (∑ i, if g i = a then (sgn i : ℤ) else 0) = f a :=
by
obtain ⟨β, _, sgn, g, hg, hβ, hf⟩ := exists_signed_sum s f
refine
⟨β ⊕ (Fin (n - ∑ i ∈ s, (f i).natAbs)), inferInstance, Sum.elim sgn 0,
Sum.elim g (Classical.arbitrary (Fin (n - Finset.sum s fun i => Int.natAbs (f i)) → α)), ?_, by simp [hβ, h],
fun a ha => by simp [hf _ ha]⟩
rintro (b | b) hb
· cases hb (hg _)
· rfl
