Infinite sums over ℕ and ℤ

This file contains lemmas about HasSum, Summable, and tsum applied to the important special cases 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 ℤ.

Sums over ℕ

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

If f : ℕ → M has sum m, then the partial sums ∑ i in range n, f i converge to m.

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

theorem HasSum.zero_add {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {m : M} [ContinuousAdd M] {f : ℕ → M} (h : HasSum (fun (n : ℕ) => f (n + 1)) m) : HasSum f (f 0 + m)

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

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

theorem Summable.comp_nat_add {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {f : ℕ → M} {k : ℕ} (h : Summable fun (n : ℕ) => f (n + k)) : Summable f

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

theorem tsum_iSup_decode₂ {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {α : Type u_3} {β : Type u_4} [Encodable β] [CompleteLattice α] (m : α → 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₂ {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {α : Type u_3} {β : Type u_4} [Encodable β] (m : Set α → M) (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 {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {α : Type u_3} {β : Type u_4} [Countable β] [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 0) (R : M → M → 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 {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {α : Type u_3} {γ : Type u_5} [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 0) (R : M → M → 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 {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {α : Type u_3} [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 0) (R : M → M → 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' {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [T2Space M] [ContinuousAdd M] {f : ℕ → M} {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' {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [T2Space M] [ContinuousAdd M] {f : ℕ → M} (hf : Summable fun (n : ℕ) => f (n + 1)) : ∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)

theorem tsum_even_add_odd {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [T2Space M] [ContinuousAdd M] {f : ℕ → M} (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 {G : Type u_2} [AddCommGroup G] {g : G} [TopologicalSpace G] [TopologicalAddGroup G] {f : ℕ → G} (k : ℕ) : HasSum (fun (n : ℕ) => f (n + k)) g ↔ HasSum f (g + Finset.sum (Finset.range k) fun (i : ℕ) => f i)

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

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

theorem sum_add_tsum_nat_add {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] {f : ℕ → G} (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 {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] {f : ℕ → G} (hf : Summable f) : ∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)

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

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

theorem cauchySeq_finset_iff_nat_tsum_vanishing {G : Type u_2} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G] {f : ℕ → G} : (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 {G : Type u_2} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G] [CompleteSpace G] {f : ℕ → G} : Summable f ↔ ∀ e ∈ nhds 0, ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e

theorem Summable.nat_tsum_vanishing {G : Type u_2} [AddCommGroup G] [TopologicalSpace 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_2} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {f : ℕ → G} (hf : Summable f) : Filter.Tendsto f Filter.atTop (nhds 0)

Sums over ℤ

In this section we prove a variety of lemmas relating sums over ℕ to sums over ℤ.

theorem HasSum.nat_add_neg_add_one {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {m : M} {f : ℤ → M} (hf : HasSum f m) : HasSum (fun (n : ℕ) => f ↑n + f (-(↑n + 1))) m

theorem Summable.nat_add_neg_add_one {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {f : ℤ → M} (hf : Summable f) : Summable fun (n : ℕ) => f ↑n + f (-(↑n + 1))

theorem tsum_nat_add_neg_add_one {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [T2Space M] {f : ℤ → M} (hf : Summable f) : ∑' (n : ℕ), (f ↑n + f (-(↑n + 1))) = ∑' (n : ℤ), f n

theorem HasSum.of_nat_of_neg_add_one {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {m : M} {m' : M} [ContinuousAdd M] {f : ℤ → M} (hf₁ : HasSum (fun (n : ℕ) => f ↑n) m) (hf₂ : HasSum (fun (n : ℕ) => f (-(↑n + 1))) m') : HasSum f (m + m')

@[deprecated HasSum.of_nat_of_neg_add_one]

theorem HasSum.nonneg_add_neg {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {m : M} {m' : M} [ContinuousAdd M] {f : ℤ → M} (hf₁ : HasSum (fun (n : ℕ) => f ↑n) m) (hf₂ : HasSum (fun (n : ℕ) => f (-(↑n + 1))) m') : HasSum f (m + m')

Alias of HasSum.of_nat_of_neg_add_one.

theorem Summable.of_nat_of_neg_add_one {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {f : ℤ → M} (hf₁ : Summable fun (n : ℕ) => f ↑n) (hf₂ : Summable fun (n : ℕ) => f (-(↑n + 1))) : Summable f

theorem tsum_of_nat_of_neg_add_one {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : ℤ → M} (hf₁ : Summable fun (n : ℕ) => f ↑n) (hf₂ : Summable fun (n : ℕ) => f (-(↑n + 1))) : ∑' (n : ℤ), f n = ∑' (n : ℕ), f ↑n + ∑' (n : ℕ), f (-(↑n + 1))

theorem HasSum.int_rec {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {m : M} {m' : M} [ContinuousAdd M] {f : ℕ → M} {g : ℕ → M} (hf : HasSum f m) (hg : HasSum g m') : HasSum (fun (t : ℤ) => Int.rec f g t) (m + m')

If f₀, f₁, f₂, ... and g₀, g₁, g₂, ... have sums a, b respectively, then the ℤ-indexed sequence: ..., g₂, g₁, g₀, f₀, f₁, f₂, ... (with f₀ at the 0-th position) has sum a + b.

theorem Summable.int_rec {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {f : ℕ → M} {g : ℕ → M} (hf : Summable f) (hg : Summable g) : Summable fun (t : ℤ) => Int.rec f g t

If f₀, f₁, f₂, ... and g₀, g₁, g₂, ... are both summable then so is the ℤ-indexed sequence: ..., g₂, g₁, g₀, f₀, f₁, f₂, ... (with f₀ at the 0-th position).

theorem tsum_int_rec {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : ℕ → M} {g : ℕ → M} (hf : Summable f) (hg : Summable g) : ∑' (n : ℤ), Int.rec f g n = ∑' (n : ℕ), f n + ∑' (n : ℕ), g n

If f₀, f₁, f₂, ... and g₀, g₁, g₂, ... are both summable, then the sum of the ℤ-indexed sequence: ..., g₂, g₁, g₀, f₀, f₁, f₂, ... (with f₀ at the 0-th position) is ∑' n, f n + ∑' n, g n.

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

@[deprecated HasSum.nat_add_neg]

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

Alias of HasSum.nat_add_neg.

theorem Summable.nat_add_neg {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {f : ℤ → M} (hf : Summable f) : Summable fun (n : ℕ) => f ↑n + f (-↑n)

theorem tsum_nat_add_neg {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : ℤ → M} (hf : Summable f) : ∑' (n : ℕ), (f ↑n + f (-↑n)) = ∑' (n : ℤ), f n + f 0

theorem HasSum.of_add_one_of_neg_add_one {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {m : M} {m' : M} [ContinuousAdd M] {f : ℤ → M} (hf₁ : HasSum (fun (n : ℕ) => f (↑n + 1)) m) (hf₂ : HasSum (fun (n : ℕ) => f (-(↑n + 1))) m') : HasSum f (m + f 0 + m')

@[deprecated HasSum.of_add_one_of_neg_add_one]

theorem HasSum.pos_add_zero_add_neg {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {m : M} {m' : M} [ContinuousAdd M] {f : ℤ → M} (hf₁ : HasSum (fun (n : ℕ) => f (↑n + 1)) m) (hf₂ : HasSum (fun (n : ℕ) => f (-(↑n + 1))) m') : HasSum f (m + f 0 + m')

Alias of HasSum.of_add_one_of_neg_add_one.

theorem Summable.of_add_one_of_neg_add_one {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {f : ℤ → M} (hf₁ : Summable fun (n : ℕ) => f (↑n + 1)) (hf₂ : Summable fun (n : ℕ) => f (-(↑n + 1))) : Summable f

theorem tsum_of_add_one_of_neg_add_one {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f : ℤ → M} (hf₁ : Summable fun (n : ℕ) => f (↑n + 1)) (hf₂ : Summable fun (n : ℕ) => f (-(↑n + 1))) : ∑' (n : ℤ), f n = ∑' (n : ℕ), f (↑n + 1) + f 0 + ∑' (n : ℕ), f (-(↑n + 1))

theorem HasSum.of_nat_of_neg {G : Type u_2} [AddCommGroup G] {g : G} {g' : G} [TopologicalSpace G] [TopologicalAddGroup G] {f : ℤ → G} (hf₁ : HasSum (fun (n : ℕ) => f ↑n) g) (hf₂ : HasSum (fun (n : ℕ) => f (-↑n)) g') : HasSum f (g + g' - f 0)

theorem Summable.of_nat_of_neg {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {f : ℤ → G} (hf₁ : Summable fun (n : ℕ) => f ↑n) (hf₂ : Summable fun (n : ℕ) => f (-↑n)) : Summable f

@[deprecated Summable.of_nat_of_neg]

theorem summable_int_of_summable_nat {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] {f : ℤ → G} (hf₁ : Summable fun (n : ℕ) => f ↑n) (hf₂ : Summable fun (n : ℕ) => f (-↑n)) : Summable f

Alias of Summable.of_nat_of_neg.

theorem tsum_of_nat_of_neg {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [T2Space G] {f : ℤ → G} (hf₁ : Summable fun (n : ℕ) => f ↑n) (hf₂ : Summable fun (n : ℕ) => f (-↑n)) : ∑' (n : ℤ), f n = ∑' (n : ℕ), f ↑n + ∑' (n : ℕ), f (-↑n) - f 0

theorem summable_int_iff_summable_nat_and_neg_add_one {G : Type u_2} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G] [CompleteSpace G] {f : ℤ → G} : Summable f ↔ (Summable fun (n : ℕ) => f ↑n) ∧ Summable fun (n : ℕ) => f (-(↑n + 1))

"iff" version of Summable.of_nat_of_neg_add_one.

theorem summable_int_iff_summable_nat_and_neg {G : Type u_2} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G] [CompleteSpace G] {f : ℤ → G} : Summable f ↔ (Summable fun (n : ℕ) => f ↑n) ∧ Summable fun (n : ℕ) => f (-↑n)

"iff" version of Summable.of_natCast_neg_natCast.