Documentation

Mathlib.Analysis.SumOverResidueClass

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] [TopologicalAddGroup 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) :

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] [UniformAddGroup 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.