Range reindexing for finite sums

Generic identities for sums indexed by Finset.range and Finset.Ioo. These are used by coderivation/Taylor expansions, which reindex a cut-and-collapse double sum over a triangle to a square and enlarge a vanishing-off-the-block range, and by divided-power exponential calculations, which reindex a sum over antidiagonals to a rectangle.

Main results

• sum_Ioo_eq_sum_range: a sum over Ioo 0 n equals the sum over range n when the summand at 0 vanishes.
• sum_range_triangle: summing over pairs (c, p - c) with c ≤ p < K equals the square range K × range K when the family vanishes off the triangle.
• sum_range_add_antidiagonal_of_support: a sum over antidiagonals below k + l equals the rectangle range k × range l when the summand vanishes outside that rectangle.
• sum_sum_range_eq_of_eq_zero_right: enlarging both ranges of a double sum that vanishes outside a rectangle.
• sum_range_eq_of_eq_zero_off_pair and sum_range_eq_of_eq_zero_off_triple: convenient specializations to supports of size two and three.
• sum_range_add_add: splitting a range n sum into a prefix, a block, and a suffix.
• sum_range_min_add_two: the two-step recurrence satisfied by the sums ∑_{i ≤ min j r} c^i a (j + r − 2i).
• sum_range_min_zero: the base case j = 0 of that recurrence, which its j + 1 cannot state.
• two_mul_sum_range_pair: twice the sum of the products over the pairs i < j < k is the square of the sum minus the sum of the squares.

theorem TauCeti.sum_Ioo_eq_sum_range {N : Type u_1} [AddCommMonoid N] (n : ℕ) (g : ℕ → N) (hg : g 0 = 0) : ∑ c ∈ Finset.Ioo 0 n, g c = ∑ c ∈ Finset.range n, g c

Replacing a summation over Finset.Ioo 0 n by one over Finset.range n, provided the summand at 0 vanishes.

theorem TauCeti.sum_range_triangle {N : Type u_1} [AddCommMonoid N] (K : ℕ) (g : ℕ → ℕ → N) (hg : ∀ (c q : ℕ), K ≤ c + q → g c q = 0) : ∑ p ∈ Finset.range K, ∑ c ∈ Finset.range (p + 1), g c (p - c) = ∑ c ∈ Finset.range K, ∑ q ∈ Finset.range K, g c q

Summing a two-variable family over the pairs (c, p - c) with c ≤ p < K is the same as summing it over the square range K × range K, when the family vanishes off the triangle.

theorem TauCeti.sum_range_add_antidiagonal_of_support {N : Type u_1} [AddCommMonoid N] (k l : ℕ) (f : ℕ × ℕ → N) (hf : ∀ (i j : ℕ), k ≤ i ∨ l ≤ j → f (i, j) = 0) : ∑ n ∈ Finset.range (k + l), ∑ ij ∈ Finset.antidiagonal n, f ij = ∑ i ∈ Finset.range k, ∑ j ∈ Finset.range l, f (i, j)

A sum over all antidiagonals below k + l equals the sum over the rectangle range k × range l, provided the summand vanishes whenever the first coordinate is at least k or the second coordinate is at least l.

theorem TauCeti.sum_sum_range_eq_of_eq_zero_right {N : Type u_1} [AddCommMonoid N] {b K : ℕ} (hK : b ≤ K) (g : ℕ → ℕ → N) (hg : ∀ (p d : ℕ), b ≤ p ∨ b < d → g p d = 0) : ∑ p ∈ Finset.range b, ∑ d ∈ Finset.range (b + 1), g p d = ∑ p ∈ Finset.range K, ∑ d ∈ Finset.range (K + 1), g p d

Enlarging both ranges of a double sum that vanishes for b ≤ p or b < d.

theorem TauCeti.sum_range_eq_of_eq_zero_off_pair {N : Type u_1} [AddCommMonoid N] {t : ℕ} {f : ℕ → N} {a b : ℕ} {v : N} (ha : a < t) (hb : b < t) (hab : a ≠ b) (hz : ∀ j < t, j ≠ a → j ≠ b → f j = 0) (hv : f a + f b = v) : ∑ j ∈ Finset.range t, f j = v

A sum over Finset.range t whose terms vanish outside two distinct positions is the sum of the terms at those positions.

theorem TauCeti.sum_range_eq_of_eq_zero_off_triple {N : Type u_1} [AddCommMonoid N] {t : ℕ} {f : ℕ → N} {a b d : ℕ} {v : N} (ha : a < t) (hb : b < t) (hd : d < t) (hab : a ≠ b) (had : a ≠ d) (hbd : b ≠ d) (hz : ∀ j < t, j ≠ a → j ≠ b → j ≠ d → f j = 0) (hv : f a + f b + f d = v) : ∑ j ∈ Finset.range t, f j = v

A sum over Finset.range t whose terms vanish outside three pairwise distinct positions is the sum of the terms at those positions.

theorem TauCeti.sum_range_add_add {N : Type u_1} [AddCommMonoid N] (g : ℕ → N) {p d n : ℕ} (h : p + d ≤ n) : ∑ j ∈ Finset.range n, g j = ∑ j ∈ Finset.range p, g j + ∑ j ∈ Finset.range d, g (p + j) + ∑ j ∈ Finset.range (n - p - d), g (p + d + j)

Splitting a sum over range n into a prefix of length p, a block of length d, and the remaining suffix.

The two-step recurrence of the sums ∑_{i ≤ min j r} c^i a (j + r − 2i)

theorem TauCeti.sum_range_min_add_two {R : Type u_1} [Semiring R] (a : ℕ → R) (c : R) (j r : ℕ) : ∑ i ∈ Finset.range (min (j + 2) (r + 1) + 1), c ^ i * a (j + 2 + (r + 1) - 2 * i) + c * ∑ i ∈ Finset.range (min j (r + 1) + 1), c ^ i * a (j + (r + 1) - 2 * i) = ∑ i ∈ Finset.range (min (j + 1) (r + 2) + 1), c ^ i * a (j + 1 + (r + 2) - 2 * i) + c * ∑ i ∈ Finset.range (min (j + 1) r + 1), c ^ i * a (j + 1 + r - 2 * i)

A two-step recurrence for the sums S j r = ∑_{i ≤ min j r} c^i a (j + r − 2i): S (j+2) (r+1) + c · S j (r+1) = S (j+1) (r+2) + c · S (j+1) r.

This is the identity the Fourier coefficients of the Hecke operators at a prime power satisfy (TauCeti/NumberTheory/ModularForms/HeckeSlash/Nebentypus/Prime/Power.lean), with a t the coefficient at p^t m and c = χ(p) p^{k−1}; the min is what makes it hold with no relation between j and r.

theorem TauCeti.sum_range_min_zero {R : Type u_1} [Semiring R] (a : ℕ → R) (c : R) (r : ℕ) : ∑ i ∈ Finset.range (min 0 (r + 2) + 1), c ^ i * a (0 + (r + 2) - 2 * i) + c * ∑ i ∈ Finset.range (min 0 r + 1), c ^ i * a (0 + r - 2 * i) = ∑ i ∈ Finset.range (min 1 (r + 1) + 1), c ^ i * a (1 + (r + 1) - 2 * i)

The base case of the two-step recurrence, at j = 0. S 0 (r+2) + c · S 0 r = S 1 (r+1) for S j r = ∑_{i ≤ min j r} c^i a (j + r − 2i).

sum_range_min_add_two states the recurrence only from j + 1 upwards — its second index is j + 1, never 0 — so the degenerate case where the min pins two of the sums to a single term is stated separately here. Together the two cover every j.

theorem TauCeti.two_mul_sum_range_pair {R : Type u_1} [CommRing R] (k : ℕ) (d : ℕ → R) : 2 * ∑ j ∈ Finset.range k, ∑ i ∈ Finset.range j, d i * d j = (∑ i ∈ Finset.range k, d i) ^ 2 - ∑ i ∈ Finset.range k, d i ^ 2

Twice the sum over pairs i < j < k is the square of the sum minus the sum of squares.