# 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} [] (m : ) [] (f : R) :
f = Finset.univ.sum fun (a : ZMod m) => {n : | n = a}.indicator f
theorem summable_indicator_mod_iff_summable {R : Type u_1} [] [] (m : ) [hm : ] (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 : ) {n : } (hn : f n < 0) :

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 : ] {f : } (hf : ) {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 : } [] {f : } (hf : ) {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 : } [] {f : } (hf : ) (k : ZMod m) :
Summable ({n : | n = k}.indicator f)

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