English
If a decreasing sequence f is summable on residue k modulo m, then it is summable on residue l modulo m for any l.
Русский
Если последовательность f убывающая и суммируема по остатоку k по модулю m, то она суммируема по любому остатку l по модулю m.
LaTeX
$$$\\forall m\\in\\mathbb{N},\\; f:\\mathbb{N}\\to \\mathbb{R},\\; \\operatorname{Antitone} f\\Rightarrow \\forall k,l\\in \\mathbb{Z}/m\\mathbb{Z},\\; \\mathrm{Summable}((\\{n:\\mathbb{N} | (n\\bmod m)=k\\}.indicator f)) \\Rightarrow \\mathrm{Summable}((\\{n:\\mathbb{N} | (n\\bmod m)=l\\}.indicator f)).$$$
Lean4
/-- If a decreasing sequence of real numbers is summable on one residue class
modulo `m`, then it is also summable on every other residue class mod `m`. -/
theorem summable_indicator_mod_iff_summable_indicator_mod {m : ℕ} [NeZero m] {f : ℕ → ℝ} (hf : Antitone f) {k : ZMod m}
(l : ZMod m) (hs : Summable ({n : ℕ | (n : ZMod m) = k}.indicator f)) :
Summable ({n : ℕ | (n : ZMod m) = l}.indicator f) :=
by
by_cases hf₀ : ∀ n, 0 ≤ f n
· rw [← ZMod.natCast_zmod_val k, summable_indicator_mod_iff_summable] at hs
have hl : (l.val + m : ZMod m) = l := by
simp only [ZMod.natCast_val, ZMod.cast_id', id_eq, CharP.cast_eq_zero, add_zero]
rw [← hl, ← Nat.cast_add, summable_indicator_mod_iff_summable]
exact
hs.of_nonneg_of_le (fun _ ↦ hf₀ _) fun _ ↦
hf <| Nat.add_le_add Nat.le.refl (k.val_lt.trans_le <| m.le_add_left l.val).le
· push_neg at hf₀
obtain ⟨n, hn⟩ := hf₀
exact (not_summable_indicator_mod_of_antitone_of_neg hf hn k hs).elim
