Reindexing infinite sums between the integers and natural numbers

This file supplements Mathlib's results on infinite sums over ℕ and ℤ with a reindexing lemma for an integer-indexed family whose support is bounded below.

Main results

• TauCeti.hasSum_int_iff_natCast_sub: reindex a family supported in [-k, ∞) by n ↦ n - k.
• TauCeti.hasSum_mul_zpow_natCast_sub_iff: move an integer-power shift between the summands and their sum.

theorem TauCeti.hasSum_int_iff_natCast_sub {E : Type u_1} [AddCommMonoid E] [TopologicalSpace E] {k : ℤ} {f : ℤ → E} (hf : ∀ j < -k, f j = 0) {s : E} : HasSum f s ↔ HasSum (fun (n : ℕ) => f (↑n - k)) s

A sum over the integers whose terms vanish below -k can be reindexed over the natural numbers by n ↦ n - k.

theorem TauCeti.hasSum_mul_zpow_natCast_sub_iff {K : Type u_1} [Semifield K] [TopologicalSpace K] [IsTopologicalSemiring K] {a : ℕ → K} {q s : K} (hq : q ≠ 0) (k : ℤ) : HasSum (fun (n : ℕ) => a n * q ^ (↑n - k)) s ↔ HasSum (fun (n : ℕ) => a n * q ^ n) (q ^ k * s)

Multiplication by q ^ k converts a sum with powers q ^ (n - k) into one with powers q ^ n.