Documentation

Mathlib.Topology.Algebra.InfiniteSum.NatInt

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 #

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 : ) => iFinset.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.

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 : ) => iFinset.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.

theorem HasSum.Multipliable.tendsto_sum_tsum_nat {M : Type u_1} [AddCommMonoid M] [TopologicalSpace M] {f : M} (h : Summable f) :
Filter.Tendsto (fun (n : ) => iFinset.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.

theorem HasProd.Multipliable.tendsto_prod_tprod_nat {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {f : M} (h : Multipliable f) :
Filter.Tendsto (fun (n : ) => iFinset.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.

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 (iFinset.range k, f i + m)
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 ((∏ iFinset.range k, 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 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)
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 HasProd.even_mul_odd {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {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')
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 : ) => iFinset.range n, f i) Filter.atTop (nhds m)
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 : ) => iFinset.range n, 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)) :
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)) :
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)) :
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)) :
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 (⨆ bEncodable.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 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 (⨆ bEncodable.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.

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 (⋃ bEncodable.decode₂ β i, s b) = ∑' (b : β), m (s b)

tsum_iSup_decode₂ specialized to the complete lattice of sets.

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 (⋃ bEncodable.decode₂ β i, s b) = ∏' (b : β), m (s b)

tprod_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 : MMProp) (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_tprod {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {α : Type u_3} {β : Type u_4} [Countable β] [CompleteLattice α] (m : αM) (m0 : m = 1) (R : MMProp) (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

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 : MMProp) (m_iSup : ∀ (s : α), R (m (⨆ (i : ), s i)) (∑' (i : ), m (s i))) (s : γα) (t : Finset γ) :
R (m (⨆ dt, s d)) (∑ dt, m (s d))

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

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 : MMProp) (m_iSup : ∀ (s : α), R (m (⨆ (i : ), s i)) (∏' (i : ), m (s i))) (s : γα) (t : Finset γ) :
R (m (⨆ dt, s d)) (∏ dt, m (s d))

If a function is countably sub-multiplicative then it is sub-multiplicative 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 : MMProp) (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 rel_sup_mul {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {α : Type u_3} [CompleteLattice α] (m : αM) (m0 : m = 1) (R : MMProp) (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

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)) :
iFinset.range k, f i + ∑' (i : ), f (i + k) = ∑' (i : ), f i
theorem 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)) :
(∏ iFinset.range k, 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 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)
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 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
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 + iFinset.range k, f i)
theorem hasProd_nat_add_iff {G : Type u_2} [CommGroup G] {g : G} [TopologicalSpace G] [TopologicalGroup G] {f : G} (k : ) :
HasProd (fun (n : ) => f (n + k)) g HasProd f (g * iFinset.range k, 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 multipliable_nat_add_iff {G : Type u_2} [CommGroup G] [TopologicalSpace G] [TopologicalGroup G] {f : G} (k : ) :
(Multipliable fun (n : ) => f (n + k)) Multipliable 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 - iFinset.range k, f i) HasSum f g
theorem hasProd_nat_add_iff' {G : Type u_2} [CommGroup G] {g : G} [TopologicalSpace G] [TopologicalGroup G] {f : G} (k : ) :
HasProd (fun (n : ) => f (n + k)) (g / iFinset.range k, f i) HasProd 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) :
iFinset.range k, f i + ∑' (i : ), f (i + k) = ∑' (i : ), f i
theorem prod_mul_tprod_nat_add {G : Type u_2} [CommGroup G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] {f : G} (k : ) (h : Multipliable f) :
(∏ iFinset.range k, 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 tprod_eq_zero_mul {G : Type u_2} [CommGroup G] [TopologicalSpace G] [TopologicalGroup G] [T2Space G] {f : G} (hf : Multipliable 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, 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.

theorem tendsto_prod_nat_add {G : Type u_2} [CommGroup G] [TopologicalSpace G] [TopologicalGroup 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.

theorem cauchySeq_finset_iff_nat_tsum_vanishing {G : Type u_2} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G] {f : G} :
(CauchySeq fun (s : Finset ) => ns, f n) enhds 0, ∃ (N : ), t{n : | N n}, ∑' (n : t), f n e
theorem cauchySeq_finset_iff_nat_tprod_vanishing {G : Type u_2} [CommGroup G] [UniformSpace G] [UniformGroup G] {f : G} :
(CauchySeq fun (s : Finset ) => ns, f n) enhds 1, ∃ (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 enhds 0, ∃ (N : ), t{n : | N n}, ∑' (n : t), f n e
theorem multipliable_iff_nat_tprod_vanishing {G : Type u_2} [CommGroup G] [UniformSpace G] [UniformGroup G] [CompleteSpace G] {f : G} :
Multipliable f enhds 1, ∃ (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 Multipliable.nat_tprod_vanishing {G : Type u_2} [CommGroup G] [TopologicalSpace G] [TopologicalGroup G] {f : G} (hf : Multipliable f) ⦃e : Set G (he : e nhds 1) :
∃ (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)
theorem Multipliable.tendsto_atTop_one {G : Type u_2} [CommGroup G] [TopologicalSpace G] [TopologicalGroup G] {f : G} (hf : Multipliable f) :
Filter.Tendsto f Filter.atTop (nhds 1)

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 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
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 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))
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 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
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')
theorem HasProd.of_nat_of_neg_add_one {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {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')
@[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))) :
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))) :
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 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))
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 HasProd.int_rec {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {m : M} {m' : M} [ContinuousMul M] {f : M} {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.

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 Multipliable.int_rec {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f : M} {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).

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 tprod_int_rec {M : Type u_1} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [T2Space M] {f : M} {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.

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)
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)
@[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 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)
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 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
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')
theorem HasProd.of_add_one_of_neg_add_one {M : Type u_1} [CommMonoid M] [TopologicalSpace M] {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')
@[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))) :
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))) :
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 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))
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 HasProd.of_nat_of_neg {G : Type u_2} [CommGroup G] {g : G} {g' : G} [TopologicalSpace G] [TopologicalGroup G] {f : G} (hf₁ : HasProd (fun (n : ) => f n) g) (hf₂ : HasProd (fun (n : ) => f (-n)) g') :
HasProd 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)) :
theorem Multipliable.of_nat_of_neg {G : Type u_2} [CommGroup G] [TopologicalSpace G] [TopologicalGroup G] {f : G} (hf₁ : Multipliable fun (n : ) => f n) (hf₂ : Multipliable fun (n : ) => f (-n)) :
@[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)) :

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 tprod_of_nat_of_neg {G : Type u_2} [CommGroup G] [TopologicalSpace G] [TopologicalGroup 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
theorem summable_int_iff_summable_nat_and_neg_add_zero {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_nat_of_neg.

theorem multipliable_int_iff_multipliable_nat_and_neg {G : Type u_2} [CommGroup G] [UniformSpace G] [UniformGroup 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.