Infinite sums over ℕ and ℤ

This file contains lemmas about HasSum, Summable, and tsum applied to the important special case where the domain is ℕ or ℤ. For instance, we prove the formula ∑ i in range k, f i + ∑' i, f (i + k) = ∑' i, f i, in sum_add_tsum_nat_add, as well as several results relating sums on ℕ and ℤ.

theorem HasSum.tendsto_sum_nat {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] {a : α} {f : ℕ → α} (h : HasSum f a) : Filter.Tendsto (fun (n : ℕ) => Finset.sum (Finset.range n) fun (i : ℕ) => f i) Filter.atTop (nhds a)

If f : ℕ → α has sum a, then the partial sums ∑_{i=0}^{n-1} f i converge to a.

theorem Summable.hasSum_iff_tendsto_nat {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] {f : ℕ → α} {a : α} (hf : Summable f) : HasSum f a ↔ Filter.Tendsto (fun (n : ℕ) => Finset.sum (Finset.range n) fun (i : ℕ) => f i) Filter.atTop (nhds a)

theorem HasSum.sum_range_add {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] {f : ℕ → α} {k : ℕ} {a : α} (h : HasSum (fun (n : ℕ) => f (n + k)) a) : HasSum f ((Finset.sum (Finset.range k) fun (i : ℕ) => f i) + a)

theorem HasSum.even_add_odd {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] {a : α} {b : α} [ContinuousAdd α] {f : ℕ → α} (he : HasSum (fun (k : ℕ) => f (2 * k)) a) (ho : HasSum (fun (k : ℕ) => f (2 * k + 1)) b) : HasSum f (a + b)

theorem HasSum.sum_nat_of_sum_int {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] {a : α} [ContinuousAdd α] {f : ℤ → α} (hf : HasSum f a) : HasSum (fun (n : ℕ) => f ↑n + f (-↑n)) (a + f 0)

theorem tsum_iSup_decode₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [Encodable γ] [CompleteLattice β] (m : β → α) (m0 : m ⊥ = 0) (s : γ → β) : ∑' (i : ℕ), m (⨆ b ∈ Encodable.decode₂ γ i, s b) = ∑' (b : γ), m (s b)

You can compute a sum over an encodable type by summing over the natural numbers and taking a supremum. This is useful for outer measures.

theorem tsum_iUnion_decode₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [Encodable γ] (m : Set β → α) (m0 : m ∅ = 0) (s : γ → Set β) : ∑' (i : ℕ), m (⋃ b ∈ Encodable.decode₂ γ i, s b) = ∑' (b : γ), m (s b)

tsum_iSup_decode₂ specialized to the complete lattice of sets.

Some properties about measure-like functions. These could also be functions defined on complete sublattices of sets, with the property that they are countably sub-additive. R will probably be instantiated with (≤) in all applications.

theorem rel_iSup_tsum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] [Countable γ] [CompleteLattice β] (m : β → α) (m0 : m ⊥ = 0) (R : α → α → Prop) (m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))) (s : γ → β) : R (m (⨆ (b : γ), s b)) (∑' (b : γ), m (s b))

If a function is countably sub-additive then it is sub-additive on countable types

theorem rel_iSup_sum {α : Type u_1} {β : Type u_2} {δ : Type u_4} [AddCommMonoid α] [TopologicalSpace α] [CompleteLattice β] (m : β → α) (m0 : m ⊥ = 0) (R : α → α → Prop) (m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))) (s : δ → β) (t : Finset δ) : R (m (⨆ d ∈ t, s d)) (Finset.sum t fun (d : δ) => m (s d))

If a function is countably sub-additive then it is sub-additive on finite sets

theorem rel_sup_add {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [CompleteLattice β] (m : β → α) (m0 : m ⊥ = 0) (R : α → α → Prop) (m_iSup : ∀ (s : ℕ → β), R (m (⨆ (i : ℕ), s i)) (∑' (i : ℕ), m (s i))) (s₁ : β) (s₂ : β) : R (m (s₁ ⊔ s₂)) (m s₁ + m s₂)

If a function is countably sub-additive then it is binary sub-additive

theorem sum_add_tsum_nat_add' {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [ContinuousAdd α] {f : ℕ → α} {k : ℕ} (h : Summable fun (n : ℕ) => f (n + k)) : (Finset.sum (Finset.range k) fun (i : ℕ) => f i) + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i

theorem tsum_eq_zero_add' {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [ContinuousAdd α] {f : ℕ → α} (hf : Summable fun (n : ℕ) => f (n + 1)) : ∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)

theorem tsum_even_add_odd {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] [ContinuousAdd α] {f : ℕ → α} (he : Summable fun (k : ℕ) => f (2 * k)) (ho : Summable fun (k : ℕ) => f (2 * k + 1)) : ∑' (k : ℕ), f (2 * k) + ∑' (k : ℕ), f (2 * k + 1) = ∑' (k : ℕ), f k

theorem hasSum_nat_add_iff {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : ℕ → α} (k : ℕ) {a : α} : HasSum (fun (n : ℕ) => f (n + k)) a ↔ HasSum f (a + Finset.sum (Finset.range k) fun (i : ℕ) => f i)

theorem summable_nat_add_iff {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : ℕ → α} (k : ℕ) : (Summable fun (n : ℕ) => f (n + k)) ↔ Summable f

theorem hasSum_nat_add_iff' {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : ℕ → α} (k : ℕ) {a : α} : HasSum (fun (n : ℕ) => f (n + k)) (a - Finset.sum (Finset.range k) fun (i : ℕ) => f i) ↔ HasSum f a

theorem sum_add_tsum_nat_add {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [T2Space α] {f : ℕ → α} (k : ℕ) (h : Summable f) : (Finset.sum (Finset.range k) fun (i : ℕ) => f i) + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i

theorem tsum_eq_zero_add {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [T2Space α] {f : ℕ → α} (hf : Summable f) : ∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)

theorem tendsto_sum_nat_add {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] [T2Space α] (f : ℕ → α) : Filter.Tendsto (fun (i : ℕ) => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)

For f : ℕ → α, then ∑' k, f (k + i) tends to zero. This does not require a summability assumption on f, as otherwise all sums are zero.

theorem HasSum.int_rec {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {a : α} {b : α} {f : ℕ → α} {g : ℕ → α} (hf : HasSum f a) (hg : HasSum g b) : HasSum (Int.rec f g) (a + b)

If f₀, f₁, f₂, ... and g₀, g₁, g₂, ... are both convergent then so is the ℤ-indexed sequence: ..., g₂, g₁, g₀, f₀, f₁, f₂, ....

theorem HasSum.nonneg_add_neg {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {a : α} {b : α} {f : ℤ → α} (hnonneg : HasSum (fun (n : ℕ) => f ↑n) a) (hneg : HasSum (fun (n : ℕ) => f (-↑(Nat.succ n))) b) : HasSum f (a + b)

theorem HasSum.pos_add_zero_add_neg {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {a : α} {b : α} {f : ℤ → α} (hpos : HasSum (fun (n : ℕ) => f (↑n + 1)) a) (hneg : HasSum (fun (n : ℕ) => f (-↑(Nat.succ n))) b) : HasSum f (a + f 0 + b)

theorem summable_int_of_summable_nat {α : Type u_1} [AddCommGroup α] [TopologicalSpace α] [TopologicalAddGroup α] {f : ℤ → α} (hp : Summable fun (n : ℕ) => f ↑n) (hn : Summable fun (n : ℕ) => f (-↑n)) : Summable f

theorem cauchySeq_finset_iff_nat_tsum_vanishing {α : Type u_1} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] {f : ℕ → α} : (CauchySeq fun (s : Finset ℕ) => Finset.sum s fun (n : ℕ) => f n) ↔ ∀ e ∈ nhds 0, ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e

theorem summable_iff_nat_tsum_vanishing {α : Type u_1} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α] [CompleteSpace α] {f : ℕ → α} : Summable f ↔ ∀ e ∈ nhds 0, ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e

theorem Summable.nat_tsum_vanishing {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] {f : ℕ → G} (hf : Summable f) ⦃e : Set G⦄ (he : e ∈ nhds 0) : ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e

theorem Summable.tendsto_atTop_zero {G : Type u_5} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] {f : ℕ → G} (hf : Summable f) : Filter.Tendsto f Filter.atTop (nhds 0)