English
A decreasing sequence f is summable on a residue class modulo m if and only if it is summable on the entire sequence.
Русский
Убывающая последовательность f суммируема по остаточному классу по модулю m тогда и только тогда, когда она суммируема на всей последовательности.
LaTeX
$$$\\forall m\\in\\mathbb{N},\\; 0< m,\\; f:\\mathbb{N}\\to \\mathbb{R},\\; \\operatorname{Antitone} f\\Rightarrow \\mathrm{Summable}(\\{n: (n\\bmod m)=k\\}.indicator f) \\iff \\mathrm{Summable}(f).$$$
Lean4
/-- A decreasing sequence of real numbers is summable on a residue class
if and only if it is summable. -/
theorem summable_indicator_mod_iff {m : ℕ} [NeZero m] {f : ℕ → ℝ} (hf : Antitone f) (k : ZMod m) :
Summable ({n : ℕ | (n : ZMod m) = k}.indicator f) ↔ Summable f :=
by
refine ⟨fun H ↦ ?_, fun H ↦ Summable.indicator H _⟩
rw [Finset.sum_indicator_mod m f]
convert summable_sum (s := Finset.univ) fun a _ ↦ summable_indicator_mod_iff_summable_indicator_mod hf a H
simp only [Finset.sum_apply]
