mathlib3 documentation

topology.algebra.infinite_sum.ring

Infinite sum in a ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides lemmas about the interaction between infinite sums and multiplication.

Main results #

source
theorem has_sum.mul_left {ι : Type u_1} {α : Type u_4} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} {a₁ : α} (a₂ : α) (h : has_sum f a₁) :
has_sum (λ (i : ι), a₂ * f i) (a₂ * a₁)
source
theorem has_sum.mul_right {ι : Type u_1} {α : Type u_4} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} {a₁ : α} (a₂ : α) (hf : has_sum f a₁) :
has_sum (λ (i : ι), f i * a₂) (a₁ * a₂)
source
theorem summable.mul_left {ι : Type u_1} {α : Type u_4} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} (a : α) (hf : summable f) :
summable (λ (i : ι), a * f i)
source
theorem summable.mul_right {ι : Type u_1} {α : Type u_4} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} (a : α) (hf : summable f) :
summable (λ (i : ι), f i * a)
source
theorem summable.tsum_mul_left {ι : Type u_1} {α : Type u_4} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} [t2_space α] (a : α) (hf : summable f) :
∑' (i : ι), a * f i = a * ∑' (i : ι), f i
source
theorem summable.tsum_mul_right {ι : Type u_1} {α : Type u_4} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} [t2_space α] (a : α) (hf : summable f) :
∑' (i : ι), f i * a = (∑' (i : ι), f i) * a
source
theorem commute.tsum_right {ι : Type u_1} {α : Type u_4} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} [t2_space α] (a : α) (h : ∀ (i : ι), commute a (f i)) :
commute a (∑' (i : ι), f i)
source
theorem commute.tsum_left {ι : Type u_1} {α : Type u_4} [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} [t2_space α] (a : α) (h : ∀ (i : ι), commute (f i) a) :
commute (∑' (i : ι), f i) a
source
theorem has_sum.div_const {ι : Type u_1} {α : Type u_4} [division_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} {a : α} (h : has_sum f a) (b : α) :
has_sum (λ (i : ι), f i / b) (a / b)
source
theorem summable.div_const {ι : Type u_1} {α : Type u_4} [division_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} (h : summable f) (b : α) :
summable (λ (i : ι), f i / b)
source
theorem has_sum_mul_left_iff {ι : Type u_1} {α : Type u_4} [division_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} {a₁ a₂ : α} (h : a₂ ≠ 0) :
has_sum (λ (i : ι), a₂ * f i) (a₂ * a₁) ↔ has_sum f a₁
source
theorem has_sum_mul_right_iff {ι : Type u_1} {α : Type u_4} [division_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} {a₁ a₂ : α} (h : a₂ ≠ 0) :
has_sum (λ (i : ι), f i * a₂) (a₁ * a₂) ↔ has_sum f a₁
source
theorem has_sum_div_const_iff {ι : Type u_1} {α : Type u_4} [division_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} {a₁ a₂ : α} (h : a₂ ≠ 0) :
has_sum (λ (i : ι), f i / a₂) (a₁ / a₂) ↔ has_sum f a₁
source
theorem summable_mul_left_iff {ι : Type u_1} {α : Type u_4} [division_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} {a : α} (h : a ≠ 0) :
summable (λ (i : ι), a * f i) ↔ summable f
source
theorem summable_mul_right_iff {ι : Type u_1} {α : Type u_4} [division_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} {a : α} (h : a ≠ 0) :
summable (λ (i : ι), f i * a) ↔ summable f
source
theorem summable_div_const_iff {ι : Type u_1} {α : Type u_4} [division_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} {a : α} (h : a ≠ 0) :
summable (λ (i : ι), f i / a) ↔ summable f
source
theorem tsum_mul_left {ι : Type u_1} {α : Type u_4} [division_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} {a : α} [t2_space α] :
∑' (x : ι), a * f x = a * ∑' (x : ι), f x
source
theorem tsum_mul_right {ι : Type u_1} {α : Type u_4} [division_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} {a : α} [t2_space α] :
∑' (x : ι), f x * a = (∑' (x : ι), f x) * a
source
theorem tsum_div_const {ι : Type u_1} {α : Type u_4} [division_semiring α] [topological_space α] [topological_semiring α] {f : ι → α} {a : α} [t2_space α] :
∑' (x : ι), f x / a = (∑' (x : ι), f x) / a

Multipliying two infinite sums #

In this section, we prove various results about (∑' x : ι, f x) * (∑' y : κ, g y). Note that we always assume that the family λ x : ι × κ, f x.1 * g x.2 is summable, since there is no way to deduce this from the summmabilities of f and g in general, but if you are working in a normed space, you may want to use the analogous lemmas in analysis/normed_space/basic (e.g tsum_mul_tsum_of_summable_norm).

We first establish results about arbitrary index types, ι and κ, and then we specialize to ι = κ = ℕ to prove the Cauchy product formula (see tsum_mul_tsum_eq_tsum_sum_antidiagonal).

Arbitrary index types #

source
theorem has_sum.mul_eq {ι : Type u_1} {κ : Type u_2} {α : Type u_4} [topological_space α] [t3_space α] [non_unital_non_assoc_semiring α] [topological_semiring α] {f : ι → α} {g : κ → α} {s t u : α} (hf : has_sum f s) (hg : has_sum g t) (hfg : has_sum (λ (x : ι × κ), f x.fst * g x.snd) u) :
s * t = u
source
theorem has_sum.mul {ι : Type u_1} {κ : Type u_2} {α : Type u_4} [topological_space α] [t3_space α] [non_unital_non_assoc_semiring α] [topological_semiring α] {f : ι → α} {g : κ → α} {s t : α} (hf : has_sum f s) (hg : has_sum g t) (hfg : summable (λ (x : ι × κ), f x.fst * g x.snd)) :
has_sum (λ (x : ι × κ), f x.fst * g x.snd) (s * t)
source
theorem tsum_mul_tsum {ι : Type u_1} {κ : Type u_2} {α : Type u_4} [topological_space α] [t3_space α] [non_unital_non_assoc_semiring α] [topological_semiring α] {f : ι → α} {g : κ → α} (hf : summable f) (hg : summable g) (hfg : summable (λ (x : ι × κ), f x.fst * g x.snd)) :
(∑' (x : ι), f x) * ∑' (y : κ), g y = ∑' (z : ι × κ), f z.fst * g z.snd

Product of two infinites sums indexed by arbitrary types. See also tsum_mul_tsum_of_summable_norm if f and g are abolutely summable.

ℕ-indexed families (Cauchy product) #

We prove two versions of the Cauchy product formula. The first one is tsum_mul_tsum_eq_tsum_sum_range, where the n-th term is a sum over finset.range (n+1) involving nat subtraction. In order to avoid nat subtraction, we also provide tsum_mul_tsum_eq_tsum_sum_antidiagonal, where the n-th term is a sum over all pairs (k, l) such that k+l=n, which corresponds to the finset finset.nat.antidiagonal n

source
theorem summable_mul_prod_iff_summable_mul_sigma_antidiagonal {α : Type u_4} [topological_space α] [non_unital_non_assoc_semiring α] {f g : ℕ → α} :
summable (λ (x : ℕ × ℕ), f x.fst * g x.snd) ↔ summable (λ (x : Σ (n : ℕ), ↥(finset.nat.antidiagonal n)), f ↑(x.snd).fst * g ↑(x.snd).snd)
source
theorem summable_sum_mul_antidiagonal_of_summable_mul {α : Type u_4} [topological_space α] [non_unital_non_assoc_semiring α] {f g : ℕ → α} [t3_space α] [topological_semiring α] (h : summable (λ (x : ℕ × ℕ), f x.fst * g x.snd)) :
summable (λ (n : ℕ), (finset.nat.antidiagonal n).sum (λ (kl : ℕ × ℕ), f kl.fst * g kl.snd))
source
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal {α : Type u_4} [topological_space α] [non_unital_non_assoc_semiring α] {f g : ℕ → α} [t3_space α] [topological_semiring α] (hf : summable f) (hg : summable g) (hfg : summable (λ (x : ℕ × ℕ), f x.fst * g x.snd)) :
(∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), (finset.nat.antidiagonal n).sum (λ (kl : ℕ × ℕ), f kl.fst * g kl.snd)

The Cauchy product formula for the product of two infinites sums indexed by ℕ, expressed by summing on finset.nat.antidiagonal.

See also tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm if f and g are absolutely summable.

source
theorem summable_sum_mul_range_of_summable_mul {α : Type u_4} [topological_space α] [non_unital_non_assoc_semiring α] {f g : ℕ → α} [t3_space α] [topological_semiring α] (h : summable (λ (x : ℕ × ℕ), f x.fst * g x.snd)) :
summable (λ (n : ℕ), (finset.range (n + 1)).sum (λ (k : ℕ), f k * g (n - k)))
source
theorem tsum_mul_tsum_eq_tsum_sum_range {α : Type u_4} [topological_space α] [non_unital_non_assoc_semiring α] {f g : ℕ → α} [t3_space α] [topological_semiring α] (hf : summable f) (hg : summable g) (hfg : summable (λ (x : ℕ × ℕ), f x.fst * g x.snd)) :
(∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), (finset.range (n + 1)).sum (λ (k : ℕ), f k * g (n - k))

The Cauchy product formula for the product of two infinites sums indexed by ℕ, expressed by summing on finset.range.

See also tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm if f and g are absolutely summable.