Sums over residue classes

We consider infinite sums over functions f on ℕ, restricted to a residue class mod m.

The main result is summable_indicator_mod_iff, which states that when f : ℕ → ℝ is decreasing, then the sum over f restricted to any residue class mod m ≠ 0 converges if and only if the sum over all of ℕ converges.

theorem Finset.sum_indicator_mod {R : Type u_1} [AddCommMonoid R] (m : ℕ) [NeZero m] (f : ℕ → R) : f = ∑ a : ZMod m, {n : ℕ | ↑n = a}.indicator f

theorem summable_indicator_mod_iff_summable {R : Type u_1} [AddCommGroup R] [TopologicalSpace R] [IsTopologicalAddGroup R] (m : ℕ) [hm : NeZero m] (k : ℕ) (f : ℕ → R) : Summable ({n : ℕ | ↑n = ↑k}.indicator f) ↔ Summable fun (n : ℕ) => f (m * n + k)

A sequence f with values in an additive topological group R is summable on the residue class of k mod m if and only if f (m*n + k) is summable.

theorem not_summable_of_antitone_of_neg {f : ℕ → ℝ} (hf : Antitone f) {n : ℕ} (hn : f n < 0) : ¬Summable f

If f : ℕ → ℝ is decreasing and has a negative term, then f 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 = k}.indicator f)

If f : ℕ → ℝ is decreasing and has a negative term, then f restricted to a residue class is not summable.

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 = k}.indicator f)) : Summable ({n : ℕ | ↑n = l}.indicator f)

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 {m : ℕ} [NeZero m] {f : ℕ → ℝ} (hf : Antitone f) (k : ZMod m) : Summable ({n : ℕ | ↑n = k}.indicator f) ↔ Summable f

A decreasing sequence of real numbers is summable on a residue class if and only if it is summable.

theorem Nat.sumByResidueClasses {R : Type u_1} [AddCommGroup R] [UniformSpace R] [IsUniformAddGroup R] [CompleteSpace R] [T0Space R] {f : ℕ → R} (hf : Summable f) (N : ℕ) [NeZero N] : ∑' (n : ℕ), f n = ∑ j : ZMod N, ∑' (m : ℕ), f (j.val + N * m)

If f is a summable function on ℕ, and 0 < N, then we may compute ∑' n : ℕ, f n by summing each residue class mod N separately.