English
A sequence f: ℕ→G in a topological abelian group is summable on a residue class modulo m if and only if the subsequence n ↦ f(mn + k) is summable.
Русский
Последовательность f: ℕ→G в топологической абelian-группе суммируема по классу по модулю m тогда и только тогда, когда подпоследовательность n ↦ f(mn + k) суммируема.
LaTeX
$$$\\forall m\\in\\mathbb{N},\\; m>0,\\; k\\in \\mathbb{Z}/m\\mathbb{Z},\\; f:\\mathbb{N}\\to G:\\; \\mathrm{Summable}((n\\mapsto \\mathbf{1}_{\\{n: (n\\bmod m)=k\\}}(n)\\, f(n))) \\iff \\mathrm{Summable}(n\\mapsto f(mn+k)).$$$
Lean4
/-- A sequence `f` with values in an additive topological group `R` is summable on the
residue class of `k` mod `m` if and only if `f (m*n + k)` is summable. -/
theorem summable_indicator_mod_iff_summable {R : Type*} [AddCommGroup R] [TopologicalSpace R] [IsTopologicalAddGroup R]
(m : ℕ) [hm : NeZero m] (k : ℕ) (f : ℕ → R) :
Summable ({n : ℕ | (n : ZMod m) = k}.indicator f) ↔ Summable fun n ↦ f (m * n + k) :=
by
trans Summable ({n : ℕ | (n : ZMod m) = k ∧ k ≤ n}.indicator f)
· rw [← (finite_lt_nat k).summable_compl_iff (f := {n : ℕ | (n : ZMod m) = k}.indicator f)]
simp only [summable_subtype_iff_indicator, indicator_indicator, inter_comm, setOf_and, compl_setOf, not_lt]
· let g : ℕ → ℕ := fun n ↦ m * n + k
have hg : Function.Injective g := fun m n hmn ↦ by simpa [g, hm.ne] using hmn
have hg' : ∀ n ∉ range g, {n : ℕ | (n : ZMod m) = k ∧ k ≤ n}.indicator f n = 0 :=
by
intro n hn
contrapose! hn
exact (Nat.range_mul_add m k).symm ▸ mem_of_indicator_ne_zero hn
convert (Function.Injective.summable_iff hg hg').symm using 3
simp only [Function.comp_apply, mem_setOf_eq, Nat.cast_add, Nat.cast_mul, CharP.cast_eq_zero, zero_mul, zero_add,
le_add_iff_nonneg_left, zero_le, and_self, indicator_of_mem, g]
