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 = Finset.sum Finset.univ fun (a : ZMod m) => Set.indicator {n : ℕ | ↑n = a} f

theorem summable_indicator_mod_iff_summable {R : Type u_1} [AddCommGroup R] [TopologicalSpace R] [TopologicalAddGroup R] (m : ℕ) [hm : NeZero m] (k : ℕ) (f : ℕ → R) : Summable (Set.indicator {n : ℕ | ↑n = ↑k} 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 (Set.indicator {n : ℕ | ↑n = k} 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 (Set.indicator {n : ℕ | ↑n = k} f)) : Summable (Set.indicator {n : ℕ | ↑n = l} 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 (Set.indicator {n : ℕ | ↑n = k} f) ↔ Summable f

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