English
If a sequence f: ℕ → ℝ is decreasing and has a negative term, then f is not summable.
Русский
Если последовательность f: ℕ → ℝ убывающая и имеет отрицательный член, то она не суммируема.
LaTeX
$$$\\forall f:\\mathbb{N}\\to \\mathbb{R},\\; \\operatorname{Antitone} f \\Rightarrow \\forall n:\\mathbb{N},\\; f(n) < 0 \\Rightarrow \\neg \\mathrm{Summable}(f).$$$
Lean4
/-- If `f : ℕ → ℝ` is decreasing and has a negative term, then `f` restricted to a residue
class is not summable. -/
theorem not_summable_indicator_mod_of_antitone_of_neg {m : ℕ} [hm : NeZero m] {f : ℕ → ℝ} (hf : Antitone f) {n : ℕ}
(hn : f n < 0) (k : ZMod m) : ¬Summable ({n : ℕ | (n : ZMod m) = k}.indicator f) :=
by
rw [← ZMod.natCast_zmod_val k, summable_indicator_mod_iff_summable]
exact
not_summable_of_antitone_of_neg (hf.comp_monotone <| (Covariant.monotone_of_const m).add_const k.val) <|
(hf <| (Nat.le_mul_of_pos_left n Fin.pos').trans <| Nat.le_add_right ..).trans_lt hn
