Telescoping differences in additive submonoids

This file records criteria for differences and sums of terms in a sequence to belong to an additive submonoid, given membership of its consecutive differences.

Main results

• TauCeti.sub_mem_of_consecutive_sub_mem: a difference of two terms telescopes into an additive submonoid containing the intervening consecutive differences.
• TauCeti.sub_mem_closure_of_le: a difference f a - f b with a ≤ b ≤ n lies in the additive closure of the first n consecutive differences.
• AddSubmonoid.sub_mem_of_consecutive_sub_mem_fin: the corresponding result for a Fin-indexed family.
• AddSubmonoid.add_mem_of_consecutive_sub_mem_fin: a companion criterion for sums in a Fin-indexed family.

theorem TauCeti.sub_mem_of_consecutive_sub_mem {M : Type u_1} [AddCommGroup M] (S : AddSubmonoid M) (f : ℕ → M) {a b : ℕ} (hab : a ≤ b) (h : ∀ (k : ℕ), a ≤ k → k < b → f k - f (k + 1) ∈ S) : f a - f b ∈ S

A difference f a - f b telescopes into any additive submonoid containing all the consecutive differences f k - f (k + 1) for a ≤ k < b.

theorem TauCeti.sub_mem_closure_of_le {M : Type u_1} [AddCommGroup M] {n : ℕ} (f : ℕ → M) {a b : ℕ} (hb : b ≤ n) (hab : a ≤ b) : f a - f b ∈ AddSubmonoid.closure (Set.range fun (i : Fin n) => f ↑i - f (↑i + 1))

A difference f a - f b with a ≤ b ≤ n lies in the additive submonoid generated by the n consecutive differences f i - f (i + 1).

theorem AddSubmonoid.sub_mem_of_consecutive_sub_mem_fin {M : Type u_1} [AddCommGroup M] {m : ℕ} (S : AddSubmonoid M) (v : Fin m → M) (hS : ∀ (a b : Fin m), ↑a + 1 = ↑b → v a - v b ∈ S) {a b : Fin m} (hab : a ≤ b) : v a - v b ∈ S

A difference v a - v b of a Fin-indexed family with a ≤ b lies in any additive submonoid containing the consecutive differences v k - v (k + 1).

theorem AddSubmonoid.add_mem_of_consecutive_sub_mem_fin {M : Type u_1} [AddCommGroup M] {m : ℕ} (S : AddSubmonoid M) (v : Fin m → M) (hS : ∀ (a b : Fin m), ↑a + 1 = ↑b → v a - v b ∈ S) (hlast : ∀ (c : Fin m), ↑c + 1 = m → v c + v c ∈ S) (a b : Fin m) : v a + v b ∈ S

A sum v a + v b of a Fin-indexed family lies in any additive submonoid containing the consecutive differences v k - v (k + 1) and twice the last member, since it is (v a - v c) + (v b - v c) + (v c + v c) for the last index c.