Divergence of sub-series of harmonic series

Stream: Is there code for X?

[Michael Stoll]

Do we have the following?

import Mathlib

example {k m : ℕ} (hm : m  ≠ 0) : ¬ Summable (Set.indicator {n | n % m = k} fun n : ℕ ↦ (1 / n : ℝ)) := sorry

(For the full series, there are docs#Real.not_summable_one_div_nat_cast and docs#Real.not_summable_nat_cast_inv .)

[Michael Stoll]

Here is a proof, FWIW.

import Mathlib.Analysis.PSeries

namespace Real

lemma not_summable_indicator_one_div_nat_cast {m : ℕ} (hm : m ≠ 0) (k : ZMod m) :
    ¬ Summable (Set.indicator {n : ℕ | (n : ZMod m) = k} fun n : ℕ ↦ (1 / n : ℝ)) := by
  have : NeZero m := ⟨hm⟩ -- instance needed in some cases below
  suffices : ¬ Summable fun n : ℕ ↦ (1 / (m * n + k.val) : ℝ)
  · set f : ℕ → ℝ := Set.indicator {n : ℕ | (n : ZMod m) = k} fun n : ℕ ↦ (1 / n : ℝ)
    contrapose! this
    let g : ℕ → ℕ := fun n ↦ m * n + k.val
    have hg : Function.Injective g
    · intro m n hmn
      simpa only [add_left_inj, mul_eq_mul_left_iff, hm, or_false] using hmn
    have hg' : ∀ n ∉ Set.range g, f n = 0
    · intro n hn
      contrapose! hn
      convert Set.mem_of_indicator_ne_zero hn
      ext n
      simp only [Set.mem_range, Set.mem_setOf_eq, ZMod.nat_coe_zmod_eq_iff]
      conv => enter [1, 1, y]; rw [add_comm, eq_comm]
    convert (Function.Injective.summable_iff hg hg').mpr this with n
    simp [g]
  by_contra! h
  refine not_summable_one_div_nat_cast <| (summable_nat_add_iff 2).mp <|
    (summable_mul_left_iff (one_div_ne_zero <| Nat.cast_ne_zero.mpr hm)).mp <|
    Summable.of_nonneg_of_le (fun n ↦ by positivity) (fun n ↦ ?_) <| (summable_nat_add_iff 1).mpr h
  field_simp
  rw [← ZMod.nat_cast_val k]
  gcongr
  norm_cast
  linarith only [ZMod.val_le k]