Documentation

Mathlib.Topology.Algebra.InfiniteSum.Ring

Infinite sum in a ring #

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

Main results #

theorem HasSum.mul_left {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} {a₁ : α} (a₂ : α) (h : HasSum f a₁) :
HasSum (fun (i : ι) => a₂ * f i) (a₂ * a₁)
theorem HasSum.mul_right {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} {a₁ : α} (a₂ : α) (hf : HasSum f a₁) :
HasSum (fun (i : ι) => f i * a₂) (a₁ * a₂)
theorem Summable.mul_left {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} (a : α) (hf : Summable f) :
Summable fun (i : ι) => a * f i
theorem Summable.mul_right {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} (a : α) (hf : Summable f) :
Summable fun (i : ι) => f i * a
theorem Summable.tsum_mul_left {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} [T2Space α] (a : α) (hf : Summable f) :
∑' (i : ι), a * f i = a * ∑' (i : ι), f i
theorem Summable.tsum_mul_right {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} [T2Space α] (a : α) (hf : Summable f) :
∑' (i : ι), f i * a = (∑' (i : ι), f i) * a
theorem Commute.tsum_right {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} [T2Space α] (a : α) (h : ∀ (i : ι), Commute a (f i)) :
Commute a (∑' (i : ι), f i)
theorem Commute.tsum_left {ι : Type u_1} {α : Type u_4} [NonUnitalNonAssocSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} [T2Space α] (a : α) (h : ∀ (i : ι), Commute (f i) a) :
Commute (∑' (i : ι), f i) a
theorem HasSum.div_const {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} {a : α} (h : HasSum f a) (b : α) :
HasSum (fun (i : ι) => f i / b) (a / b)
theorem Summable.div_const {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} (h : Summable f) (b : α) :
Summable fun (i : ι) => f i / b
theorem hasSum_mul_left_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} {a₁ : α} {a₂ : α} (h : a₂ 0) :
HasSum (fun (i : ι) => a₂ * f i) (a₂ * a₁) HasSum f a₁
theorem hasSum_mul_right_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} {a₁ : α} {a₂ : α} (h : a₂ 0) :
HasSum (fun (i : ι) => f i * a₂) (a₁ * a₂) HasSum f a₁
theorem hasSum_div_const_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} {a₁ : α} {a₂ : α} (h : a₂ 0) :
HasSum (fun (i : ι) => f i / a₂) (a₁ / a₂) HasSum f a₁
theorem summable_mul_left_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} {a : α} (h : a 0) :
(Summable fun (i : ι) => a * f i) Summable f
theorem summable_mul_right_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} {a : α} (h : a 0) :
(Summable fun (i : ι) => f i * a) Summable f
theorem summable_div_const_iff {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} {a : α} (h : a 0) :
(Summable fun (i : ι) => f i / a) Summable f
theorem tsum_mul_left {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} {a : α} [T2Space α] :
∑' (x : ι), a * f x = a * ∑' (x : ι), f x
theorem tsum_mul_right {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} {a : α} [T2Space α] :
∑' (x : ι), f x * a = (∑' (x : ι), f x) * a
theorem tsum_div_const {ι : Type u_1} {α : Type u_4} [DivisionSemiring α] [TopologicalSpace α] [TopologicalSemiring α] {f : ια} {a : α} [T2Space α] :
∑' (x : ι), f x / a = (∑' (x : ι), f x) / a

Multiplying 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 fun x : ι × κ ↦ f x.1 * g x.2 is summable, since there is no way to deduce this from the summabilities 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.Module.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 #

theorem HasSum.mul_eq {ι : Type u_1} {κ : Type u_2} {α : Type u_4} [TopologicalSpace α] [T3Space α] [NonUnitalNonAssocSemiring α] [TopologicalSemiring α] {f : ια} {g : κα} {s : α} {t : α} {u : α} (hf : HasSum f s) (hg : HasSum g t) (hfg : HasSum (fun (x : ι × κ) => f x.1 * g x.2) u) :
s * t = u
theorem HasSum.mul {ι : Type u_1} {κ : Type u_2} {α : Type u_4} [TopologicalSpace α] [T3Space α] [NonUnitalNonAssocSemiring α] [TopologicalSemiring α] {f : ια} {g : κα} {s : α} {t : α} (hf : HasSum f s) (hg : HasSum g t) (hfg : Summable fun (x : ι × κ) => f x.1 * g x.2) :
HasSum (fun (x : ι × κ) => f x.1 * g x.2) (s * t)
theorem tsum_mul_tsum {ι : Type u_1} {κ : Type u_2} {α : Type u_4} [TopologicalSpace α] [T3Space α] [NonUnitalNonAssocSemiring α] [TopologicalSemiring α] {f : ια} {g : κα} (hf : Summable f) (hg : Summable g) (hfg : Summable fun (x : ι × κ) => f x.1 * g x.2) :
(∑' (x : ι), f x) * ∑' (y : κ), g y = ∑' (z : ι × κ), f z.1 * g z.2

Product of two infinites sums indexed by arbitrary types. See also tsum_mul_tsum_of_summable_norm if f and g are absolutely 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.antidiagonal n. This in fact allows us to generalize to any type satisfying [Finset.HasAntidiagonal A]

theorem summable_mul_prod_iff_summable_mul_sigma_antidiagonal {α : Type u_4} {A : Type u_5} [AddCommMonoid A] [Finset.HasAntidiagonal A] [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f : Aα} {g : Aα} :
(Summable fun (x : A × A) => f x.1 * g x.2) Summable fun (x : (n : A) × { x : A × A // x Finset.antidiagonal n }) => f (↑x.snd).1 * g (↑x.snd).2

The family (k, l) : ℕ × ℕ ↦ f k * g l is summable if and only if the family (n, k, l) : Σ (n : ℕ), antidiagonal n ↦ f k * g l is summable.

theorem summable_sum_mul_antidiagonal_of_summable_mul {α : Type u_4} {A : Type u_5} [AddCommMonoid A] [Finset.HasAntidiagonal A] [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f : Aα} {g : Aα} [T3Space α] [TopologicalSemiring α] (h : Summable fun (x : A × A) => f x.1 * g x.2) :
Summable fun (n : A) => klFinset.antidiagonal n, f kl.1 * g kl.2
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal {α : Type u_4} {A : Type u_5} [AddCommMonoid A] [Finset.HasAntidiagonal A] [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f : Aα} {g : Aα} [T3Space α] [TopologicalSemiring α] (hf : Summable f) (hg : Summable g) (hfg : Summable fun (x : A × A) => f x.1 * g x.2) :
(∑' (n : A), f n) * ∑' (n : A), g n = ∑' (n : A), klFinset.antidiagonal n, f kl.1 * g kl.2

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

See also tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm if f and g are absolutely summable.

theorem summable_sum_mul_range_of_summable_mul {α : Type u_4} [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f : α} {g : α} [T3Space α] [TopologicalSemiring α] (h : Summable fun (x : × ) => f x.1 * g x.2) :
Summable fun (n : ) => kFinset.range (n + 1), f k * g (n - k)
theorem tsum_mul_tsum_eq_tsum_sum_range {α : Type u_4} [TopologicalSpace α] [NonUnitalNonAssocSemiring α] {f : α} {g : α} [T3Space α] [TopologicalSemiring α] (hf : Summable f) (hg : Summable g) (hfg : Summable fun (x : × ) => f x.1 * g x.2) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), kFinset.range (n + 1), 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.