English
For any modulus m > 0 and any residue class k ∈ Z/mZ, the subseries of the harmonic series consisting of terms with n ≡ k (mod m) diverges; i.e., the indicator-weighted series ∑_{n ≡ k (mod m)} 1/n is not summable.
Русский
Для любого модуля m>0 и любого класса остатка k по модулю m, подпоследовательность гармонического ряда по n ≡ k (mod m) расходится; тож сумма не суммируема.
LaTeX
$$For all $m>0$ and $k\\in\\mathbb{Z}/m\\mathbb{Z}$, the subseries $$\\sum_{n\\equiv k\\,(\\mathrm{mod}\\ m)} \\frac{1}{n}$$ diverges (i.e., is not summable).$$
Lean4
/-- The harmonic series restricted to a residue class is not summable. -/
theorem not_summable_indicator_one_div_natCast {m : ℕ} (hm : m ≠ 0) (k : ZMod m) :
¬Summable ({n : ℕ | (n : ZMod m) = k}.indicator fun n : ℕ ↦ (1 / n : ℝ)) :=
by
have : NeZero m :=
⟨hm⟩ -- instance is needed below
rw [← summable_nat_add_iff 1] -- shift by one to avoid non-monotonicity at zero
have h (n : ℕ) :
{n : ℕ | (n : ZMod m) = k - 1}.indicator (fun n : ℕ ↦ (1 / (n + 1 :) : ℝ)) n =
if (n : ZMod m) = k - 1 then (1 / (n + 1) : ℝ) else (0 : ℝ) :=
by simp only [indicator_apply, mem_setOf_eq, cast_add, cast_one]
simp_rw [indicator_apply, mem_setOf, cast_add, cast_one, ← eq_sub_iff_add_eq, ← h]
rw [summable_indicator_mod_iff (fun n₁ n₂ h ↦ by gcongr) (k - 1)]
exact mt (summable_nat_add_iff (f := fun n : ℕ ↦ 1 / (n : ℝ)) 1).mp not_summable_one_div_natCast
