English
If a decreasing sequence f is summable on one residue class, then it is summable on every residue class modulo m.
Русский
Если убывающая последовательность f суммируема по одному остаточному классу по модулю m, то она суммируема по всем остаточным классам по модулю m.
LaTeX
$$$\\forall m\\in\\mathbb{N},\\; m>0,\\; f: \\mathbb{N}\\to \\mathbb{R},\\; \\operatorname{Antitone} f\\Rightarrow\\forall k,l:\\mathbb{Z}/m\\mathbb{Z},\\; \\Big(\\mathrm{Summable}((n:\\mathbb{N})\\; (n\\bmod m)=k)\\mathbf{1}.indicator f\\Big) \\Rightarrow \\mathrm{Summable}((n:\\mathbb{N})\\; (n\\bmod m)=l).indicator f.$$$
Lean4
/-- If `f : ℕ → ℝ` is decreasing and has a negative term, then `f` is not summable. -/
theorem not_summable_of_antitone_of_neg {f : ℕ → ℝ} (hf : Antitone f) {n : ℕ} (hn : f n < 0) : ¬Summable f :=
by
intro hs
have := hs.tendsto_atTop_zero
simp only [Metric.tendsto_atTop, dist_zero_right, Real.norm_eq_abs] at this
obtain ⟨N, hN⟩ := this (|f n|) (abs_pos_of_neg hn)
specialize hN (max n N) (n.le_max_right N)
contrapose! hN; clear hN
have H : f (max n N) ≤ f n := hf (n.le_max_left N)
rwa [abs_of_neg hn, abs_of_neg (H.trans_lt hn), neg_le_neg_iff]
