English
If f is summable on ℕ, then the total sum equals the sum over residues modulo N of the sums over each residue class.
Русский
Если f суммируема по ℕ, то сумма по всей последовательности равна сумме по остаткам modulo N: сумма по классам остатка, отдельно суммируемые.
LaTeX
$$$\\forall f: \\mathbb{N}\\to R,\\; \\mathrm{Summable}(f) \\Rightarrow \\sum_{n} f(n) = \\sum_{j\\in \\mathbb{Z}/N\\mathbb{Z}} \\sum_{m} f(j.val + N\\, m).$$$
Lean4
/-- If `f` is a summable function on `ℕ`, and `0 < N`, then we may compute `∑' n : ℕ, f n` by
summing each residue class mod `N` separately. -/
theorem sumByResidueClasses {R : Type*} [AddCommGroup R] [UniformSpace R] [IsUniformAddGroup R] [CompleteSpace R]
[T0Space R] {f : ℕ → R} (hf : Summable f) (N : ℕ) [NeZero N] : ∑' n, f n = ∑ j : ZMod N, ∑' m, f (j.val + N * m) :=
by
rw [← (residueClassesEquiv N).symm.tsum_eq f, Summable.tsum_prod, tsum_fintype, residueClassesEquiv,
Equiv.coe_fn_symm_mk]
exact hf.comp_injective (residueClassesEquiv N).symm.injective
