English
For any m≥2, any function f: ℕ→R, and any m-th modulus, one can express f as a sum over residue classes modulo m, using indicator functions of residue classes.
Русский
Для любого m≥2, любой функции f: ℕ→R и любого остатка по модулю m можно разложить f как сумму по классам по модулю m, используя индикаторные функции классов остатков.
LaTeX
$$$\\forall m\\in\\mathbb{N},\\ m\\neq 0,\\; \\forall f: \\mathbb{N}\\to R,\\; f = \\sum_{a:\\mathbb{Z}/m\\mathbb{Z}} \\mathbf{1}_{\\{n:\\mathbb{N} | (n\\bmod m)=a\\}} \\cdot f.$$$
Lean4
theorem sum_indicator_mod {R : Type*} [AddCommMonoid R] (m : ℕ) [NeZero m] (f : ℕ → R) :
f = ∑ a : ZMod m, {n : ℕ | (n : ZMod m) = a}.indicator f :=
by
ext n
simp only [Finset.sum_apply, Set.indicator_apply, Set.mem_setOf_eq, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte]
