# Infinite sums and products over `ℕ` and `ℤ` #

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

## Sums over `ℕ` #

source
theorem HasProd.tendsto_prod_nat {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {m : M} {f : ℕ → M} (h : HasProd f m) :
Filter.Tendsto (fun (n : ℕ) => ∏ i ∈ Finset.range n, f i) Filter.atTop (nhds m)

If `f : ℕ → M` has product `m`, then the partial products `∏ i ∈ range n, f i` converge to `m`.

source
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 : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds m)

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

source
theorem Multipliable.tendsto_prod_tprod_nat {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {f : ℕ → M} (h : Multipliable f) :
Filter.Tendsto (fun (n : ℕ) => ∏ i ∈ Finset.range n, f i) Filter.atTop (nhds (∏' (i : ℕ), f i))

If `f : ℕ → M` is multipliable, then the partial products `∏ i ∈ range n, f i` converge to `∏' i, f i`.

source
theorem Summable.tendsto_sum_tsum_nat {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {f : ℕ → M} (h : Summable f) :
Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds (∑' (i : ℕ), f i))

If `f : ℕ → M` is summable, then the partial sums `∑ i ∈ range n, f i` converge to `∑' i, f i`.

source
theorem HasProd.prod_range_mul {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {m : M} [ContinuousMul M] {f : ℕ → M} {k : ℕ} (h : HasProd (fun (n : ℕ) => f (n + k)) m) :
HasProd f ((∏ i ∈ Finset.range k, f i) * m)
source
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 (∑ i ∈ Finset.range k, f i + m)
source
theorem HasProd.zero_mul {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {m : M} [ContinuousMul M] {f : ℕ → M} (h : HasProd (fun (n : ℕ) => f (n + 1)) m) :
HasProd f (f 0 * m)
source
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)
source
theorem HasProd.even_mul_odd {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {m m' : M} [ContinuousMul M] {f : ℕ → M} (he : HasProd (fun (k : ℕ) => f (2 * k)) m) (ho : HasProd (fun (k : ℕ) => f (2 * k + 1)) m') :
HasProd f (m * m')
source
theorem HasSum.even_add_odd {M : Type u_1} [AddCommMonoid M] [TopologicalSpace 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')
source
theorem Multipliable.hasProd_iff_tendsto_nat {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {m : M} [T2Space M] {f : ℕ → M} (hf : Multipliable f) :
HasProd f m ↔ Filter.Tendsto (fun (n : ℕ) => ∏ i ∈ Finset.range n, f i) Filter.atTop (nhds m)
source
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 : ℕ) => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds m)
source
theorem Multipliable.comp_nat_add {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f : ℕ → M} {k : ℕ} (h : Multipliable fun (n : ℕ) => f (n + k)) :
Multipliable f
source
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
source
theorem Multipliable.even_mul_odd {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f : ℕ → M} (he : Multipliable fun (k : ℕ) => f (2 * k)) (ho : Multipliable fun (k : ℕ) => f (2 * k + 1)) :
Multipliable f
source
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
source
theorem tprod_iSup_decode₂ {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {α : Type u_3} {β : Type u_4} [Encodable β] [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (s : β → α) :
∏' (i : ℕ), m (⨆ b ∈ Encodable.decode₂ β i, s b) = ∏' (b : β), m (s b)

You can compute a product over an encodable type by multiplying over the natural numbers and taking a supremum.

source
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.

source
theorem tprod_iUnion_decode₂ {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {α : Type u_3} {β : Type u_4} [Encodable β] (m : Set α → M) (m0 : m ∅ = 1) (s : β → Set α) :
∏' (i : ℕ), m (⋃ b ∈ Encodable.decode₂ β i, s b) = ∏' (b : β), m (s b)

`tprod_iSup_decode₂` specialized to the complete lattice of sets.

source
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.

source
theorem rel_iSup_tprod {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {α : Type u_3} {β : Type u_4} [Countable β] [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (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-multiplicative then it is sub-multiplicative on countable types

source
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

source
theorem rel_iSup_prod {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {α : Type u_3} {γ : Type u_5} [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (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)) (∏ d ∈ t, m (s d))

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

source
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)) (∑ d ∈ t, m (s d))

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

source
theorem rel_sup_mul {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {α : Type u_3} [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (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-multiplicative then it is binary sub-multiplicative

source
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

source
theorem Multipliable.prod_mul_tprod_nat_mul' {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [T2Space M] [ContinuousMul M] {f : ℕ → M} {k : ℕ} (h : Multipliable fun (n : ℕ) => f (n + k)) :
(∏ i ∈ Finset.range k, f i) * ∏' (i : ℕ), f (i + k) = ∏' (i : ℕ), f i
source
theorem Summable.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)) :
∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i
source
theorem tprod_eq_zero_mul' {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [T2Space M] [ContinuousMul M] {f : ℕ → M} (hf : Multipliable fun (n : ℕ) => f (n + 1)) :
∏' (b : ℕ), f b = f 0 * ∏' (b : ℕ), f (b + 1)
source
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)
source
theorem tprod_even_mul_odd {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [T2Space M] [ContinuousMul M] {f : ℕ → M} (he : Multipliable fun (k : ℕ) => f (2 * k)) (ho : Multipliable fun (k : ℕ) => f (2 * k + 1)) :
(∏' (k : ℕ), f (2 * k)) * ∏' (k : ℕ), f (2 * k + 1) = ∏' (k : ℕ), f k
source
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
source
theorem hasProd_nat_add_iff {G : Type u_2} [CommGroup G] {g : G} [TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} (k : ℕ) :
HasProd (fun (n : ℕ) => f (n + k)) g ↔ HasProd f (g * ∏ i ∈ Finset.range k, f i)
source
theorem hasSum_nat_add_iff {G : Type u_2} [AddCommGroup G] {g : G} [TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G} (k : ℕ) :
HasSum (fun (n : ℕ) => f (n + k)) g ↔ HasSum f (g + ∑ i ∈ Finset.range k, f i)
source
theorem multipliable_nat_add_iff {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} (k : ℕ) :
(Multipliable fun (n : ℕ) => f (n + k)) ↔ Multipliable f
source
theorem summable_nat_add_iff {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G} (k : ℕ) :
(Summable fun (n : ℕ) => f (n + k)) ↔ Summable f
source
theorem hasProd_nat_add_iff' {G : Type u_2} [CommGroup G] {g : G} [TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} (k : ℕ) :
HasProd (fun (n : ℕ) => f (n + k)) (g / ∏ i ∈ Finset.range k, f i) ↔ HasProd f g
source
theorem hasSum_nat_add_iff' {G : Type u_2} [AddCommGroup G] {g : G} [TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G} (k : ℕ) :
HasSum (fun (n : ℕ) => f (n + k)) (g - ∑ i ∈ Finset.range k, f i) ↔ HasSum f g
source
theorem Multipliable.prod_mul_tprod_nat_add {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {f : ℕ → G} (k : ℕ) (h : Multipliable f) :
(∏ i ∈ Finset.range k, f i) * ∏' (i : ℕ), f (i + k) = ∏' (i : ℕ), f i
source
theorem Summable.sum_add_tsum_nat_add {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {f : ℕ → G} (k : ℕ) (h : Summable f) :
∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i
source
theorem Multipliable.tprod_eq_zero_mul {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {f : ℕ → G} (hf : Multipliable f) :
∏' (b : ℕ), f b = f 0 * ∏' (b : ℕ), f (b + 1)
source
theorem Summable.tsum_eq_zero_add {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {f : ℕ → G} (hf : Summable f) :
∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)
source
theorem tendsto_prod_nat_add {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] (f : ℕ → G) :
Filter.Tendsto (fun (i : ℕ) => ∏' (k : ℕ), f (k + i)) Filter.atTop (nhds 1)

For `f : ℕ → G`, the product `∏' k, f (k + i)` tends to one. This does not require a multipliability assumption on `f`, as otherwise all such products are one.

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

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

source
theorem cauchySeq_finset_iff_nat_tprod_vanishing {G : Type u_2} [CommGroup G] [UniformSpace G] [IsUniformGroup G] {f : ℕ → G} :
(CauchySeq fun (s : Finset ℕ) => ∏ n ∈ s, f n) ↔ ∀ e ∈ nhds 1, ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
source
theorem cauchySeq_finset_iff_nat_tsum_vanishing {G : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] {f : ℕ → G} :
(CauchySeq fun (s : Finset ℕ) => ∑ n ∈ s, f n) ↔ ∀ e ∈ nhds 0, ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e
source
theorem multipliable_iff_nat_tprod_vanishing {G : Type u_2} [CommGroup G] [UniformSpace G] [IsUniformGroup G] [CompleteSpace G] {f : ℕ → G} :
Multipliable f ↔ ∀ e ∈ nhds 1, ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
source
theorem summable_iff_nat_tsum_vanishing {G : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] {f : ℕ → G} :
Summable f ↔ ∀ e ∈ nhds 0, ∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e
source
theorem Multipliable.nat_tprod_vanishing {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ nhds 1) :
∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
source
theorem Summable.nat_tsum_vanishing {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G} (hf : Summable f) ⦃e : Set G⦄ (he : e ∈ nhds 0) :
∃ (N : ℕ), ∀ t ⊆ {n : ℕ | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e
source
theorem Multipliable.tendsto_atTop_one {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} (hf : Multipliable f) :
Filter.Tendsto f Filter.atTop (nhds 1)
source
theorem Summable.tendsto_atTop_zero {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup 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 `ℤ`.

source
theorem HasProd.nat_mul_neg_add_one {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {m : M} {f : ℤ → M} (hf : HasProd f m) :
HasProd (fun (n : ℕ) => f ↑n * f (-(↑n + 1))) m
source
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
source
theorem Multipliable.nat_mul_neg_add_one {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {f : ℤ → M} (hf : Multipliable f) :
Multipliable fun (n : ℕ) => f ↑n * f (-(↑n + 1))
source
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))
source
theorem tprod_nat_mul_neg_add_one {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [T2Space M] {f : ℤ → M} (hf : Multipliable f) :
∏' (n : ℕ), f ↑n * f (-(↑n + 1)) = ∏' (n : ℤ), f n
source
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
source
theorem HasProd.of_nat_of_neg_add_one {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {m m' : M} [ContinuousMul M] {f : ℤ → M} (hf₁ : HasProd (fun (n : ℕ) => f ↑n) m) (hf₂ : HasProd (fun (n : ℕ) => f (-(↑n + 1))) m') :
HasProd f (m * m')
source
theorem HasSum.of_nat_of_neg_add_one {M : Type u_1} [AddCommMonoid M] [TopologicalSpace 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')
source
theorem Multipliable.of_nat_of_neg_add_one {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f : ℤ → M} (hf₁ : Multipliable fun (n : ℕ) => f ↑n) (hf₂ : Multipliable fun (n : ℕ) => f (-(↑n + 1))) :
Multipliable f
source
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
source
theorem tprod_of_nat_of_neg_add_one {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [T2Space M] {f : ℤ → M} (hf₁ : Multipliable fun (n : ℕ) => f ↑n) (hf₂ : Multipliable fun (n : ℕ) => f (-(↑n + 1))) :
∏' (n : ℤ), f n = (∏' (n : ℕ), f ↑n) * ∏' (n : ℕ), f (-(↑n + 1))
source
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))
source
theorem HasProd.int_rec {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {m m' : M} [ContinuousMul M] {f g : ℕ → M} (hf : HasProd f m) (hg : HasProd g m') :
HasProd (fun (t : ℤ) => Int.rec f g t) (m * m')

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

source
theorem HasSum.int_rec {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {m m' : M} [ContinuousAdd M] {f 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`.

source
theorem Multipliable.int_rec {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f g : ℕ → M} (hf : Multipliable f) (hg : Multipliable g) :
Multipliable fun (t : ℤ) => Int.rec f g t

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

source
theorem Summable.int_rec {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {f 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).

source
theorem tprod_int_rec {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [T2Space M] {f g : ℕ → M} (hf : Multipliable f) (hg : Multipliable g) :
∏' (n : ℤ), Int.rec f g n = (∏' (n : ℕ), f n) * ∏' (n : ℕ), g n

If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both multipliable, then the product of the `ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) is `(∏' n, f n) * ∏' n, g n`.

source
theorem tsum_int_rec {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] [T2Space M] {f 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`.

source
theorem HasProd.nat_mul_neg {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {m : M} [ContinuousMul M] {f : ℤ → M} (hf : HasProd f m) :
HasProd (fun (n : ℕ) => f ↑n * f (-↑n)) (m * f 0)
source
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)
source
theorem Multipliable.nat_mul_neg {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f : ℤ → M} (hf : Multipliable f) :
Multipliable fun (n : ℕ) => f ↑n * f (-↑n)
source
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)
source
theorem tprod_nat_mul_neg {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [T2Space M] {f : ℤ → M} (hf : Multipliable f) :
∏' (n : ℕ), f ↑n * f (-↑n) = (∏' (n : ℤ), f n) * f 0
source
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
source
theorem HasProd.of_add_one_of_neg_add_one {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {m m' : M} [ContinuousMul M] {f : ℤ → M} (hf₁ : HasProd (fun (n : ℕ) => f (↑n + 1)) m) (hf₂ : HasProd (fun (n : ℕ) => f (-(↑n + 1))) m') :
HasProd f (m * f 0 * m')
source
theorem HasSum.of_add_one_of_neg_add_one {M : Type u_1} [AddCommMonoid M] [TopologicalSpace 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')
source
theorem Multipliable.of_add_one_of_neg_add_one {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f : ℤ → M} (hf₁ : Multipliable fun (n : ℕ) => f (↑n + 1)) (hf₂ : Multipliable fun (n : ℕ) => f (-(↑n + 1))) :
Multipliable f
source
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
source
theorem tprod_of_add_one_of_neg_add_one {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [T2Space M] {f : ℤ → M} (hf₁ : Multipliable fun (n : ℕ) => f (↑n + 1)) (hf₂ : Multipliable fun (n : ℕ) => f (-(↑n + 1))) :
∏' (n : ℤ), f n = (∏' (n : ℕ), f (↑n + 1)) * f 0 * ∏' (n : ℕ), f (-(↑n + 1))
source
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))
source
theorem HasProd.of_nat_of_neg {G : Type u_2} [CommGroup G] {g g' : G} [TopologicalSpace G] [IsTopologicalGroup G] {f : ℤ → G} (hf₁ : HasProd (fun (n : ℕ) => f ↑n) g) (hf₂ : HasProd (fun (n : ℕ) => f (-↑n)) g') :
HasProd f (g * g' / f 0)
source
theorem HasSum.of_nat_of_neg {G : Type u_2} [AddCommGroup G] {g g' : G} [TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℤ → G} (hf₁ : HasSum (fun (n : ℕ) => f ↑n) g) (hf₂ : HasSum (fun (n : ℕ) => f (-↑n)) g') :
HasSum f (g + g' - f 0)
source
theorem Multipliable.of_nat_of_neg {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] {f : ℤ → G} (hf₁ : Multipliable fun (n : ℕ) => f ↑n) (hf₂ : Multipliable fun (n : ℕ) => f (-↑n)) :
Multipliable f
source
theorem Summable.of_nat_of_neg {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℤ → G} (hf₁ : Summable fun (n : ℕ) => f ↑n) (hf₂ : Summable fun (n : ℕ) => f (-↑n)) :
Summable f
source
theorem Multipliable.tprod_of_nat_of_neg {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {f : ℤ → G} (hf₁ : Multipliable fun (n : ℕ) => f ↑n) (hf₂ : Multipliable fun (n : ℕ) => f (-↑n)) :
∏' (n : ℤ), f n = ((∏' (n : ℕ), f ↑n) * ∏' (n : ℕ), f (-↑n)) / f 0
source
theorem Summable.tsum_of_nat_of_neg {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup 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
source
theorem multipliable_int_iff_multipliable_nat_and_neg_add_one {G : Type u_2} [CommGroup G] [UniformSpace G] [IsUniformGroup G] [CompleteSpace G] {f : ℤ → G} :
Multipliable f ↔ (Multipliable fun (n : ℕ) => f ↑n) ∧ Multipliable fun (n : ℕ) => f (-(↑n + 1))

"iff" version of `Multipliable.of_nat_of_neg_add_one`.

source
theorem summable_int_iff_summable_nat_and_neg_add_zero {G : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup 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`.

source
theorem multipliable_int_iff_multipliable_nat_and_neg {G : Type u_2} [CommGroup G] [UniformSpace G] [IsUniformGroup G] [CompleteSpace G] {f : ℤ → G} :
Multipliable f ↔ (Multipliable fun (n : ℕ) => f ↑n) ∧ Multipliable fun (n : ℕ) => f (-↑n)

"iff" version of `Multipliable.of_nat_of_neg`.

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

"iff" version of `Summable.of_nat_of_neg`.

source
theorem Summable.alternating {α : Type u_3} [Ring α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {f : ℕ → α} (hf : Summable f) :
Summable fun (n : ℕ) => (-1) ^ n * f n
source
theorem multipliable_pnat_iff_multipliable_succ {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {f : ℕ → M} :
(Multipliable fun (x : ℕ+) => f ↑x) ↔ Multipliable fun (x : ℕ) => f (x + 1)
source
theorem summable_pnat_iff_summable_succ {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {f : ℕ → M} :
(Summable fun (x : ℕ+) => f ↑x) ↔ Summable fun (x : ℕ) => f (x + 1)
source
@[deprecated multipliable_pnat_iff_multipliable_succ (since := "2025-09-31")]
theorem pnat_multipliable_iff_multipliable_succ {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {f : ℕ → M} :
(Multipliable fun (x : ℕ+) => f ↑x) ↔ Multipliable fun (x : ℕ) => f (x + 1)

Alias of `multipliable_pnat_iff_multipliable_succ`.

source
theorem tprod_pnat_eq_tprod_succ {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {f : ℕ → M} :
∏' (n : ℕ+), f ↑n = ∏' (n : ℕ), f (n + 1)
source
theorem tsum_pnat_eq_tsum_succ {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {f : ℕ → M} :
∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f (n + 1)
source
theorem tprod_zero_pnat_eq_tprod_nat {G : Type u_2} [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {f : ℕ → G} (hf : Multipliable f) :
f 0 * ∏' (n : ℕ+), f ↑n = ∏' (n : ℕ), f n
source
theorem tsum_zero_pnat_eq_tsum_nat {G : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [T2Space G] {f : ℕ → G} (hf : Summable f) :
f 0 + ∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f n
source
theorem tprod_int_eq_zero_mul_tprod_pnat_sq {G : Type u_2} [CommGroup G] [UniformSpace G] [IsUniformGroup G] [CompleteSpace G] [T2Space G] {f : ℤ → G} (hf : ∀ (n : ℤ), f (-n) = f n) (hf2 : Multipliable f) :
∏' (n : ℤ), f n = f 0 * (∏' (n : ℕ+), f ↑↑n) ^ 2
source
theorem tsum_int_eq_zero_add_two_mul_tsum_pnat {G : Type u_2} [AddCommGroup G] [UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] [T2Space G] {f : ℤ → G} (hf : ∀ (n : ℤ), f (-n) = f n) (hf2 : Summable f) :
∑' (n : ℤ), f n = f 0 + 2 • ∑' (n : ℕ+), f ↑↑n