tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm
theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] {f g : ℕ → R},
(Summable fun x => ‖f x‖) →
(Summable fun x => ‖g x‖) →
(∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), (Finset.range (n + 1)).sum fun k => f k * g (n - k)
This theorem, named `tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm`, states the Cauchy product formula for the product of two infinite sums indexed by the set of natural numbers, ℕ. Given a normed ring `R` and two sequences of elements in `R`, represented by functions `f` and `g` from ℕ to `R`, if both these sequences are absolutely summable (which is conveyed by the condition that the sum of the norms of the elements of each sequence exists), then the product of the two infinite sums equals to a new infinite sum. This new sum is defined as the sum, for each natural number `n`, of the product of `f k` and `g (n - k)`, where `k` ranges over the set of natural numbers less than or equal to `n` (given by `Finset.range (n + 1)`). This sums up the pairwise products of all possible partitions of `n` into two parts, corresponding to the Cauchy product of the two original series.
More concisely: Given two absolutely summable sequences of elements in a normed ring, their Cauchy product is equal to the sum of the infinite series where for each natural number n, the summand is the product of the ith term of the first sequence with the jth term of the second sequence, where i and j range over the set of natural numbers less than or equal to n and i < j.
|
tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm :
∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] {f g : ℕ → R},
(Summable fun x => ‖f x‖) →
(Summable fun x => ‖g x‖) →
(∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), (Finset.antidiagonal n).sum fun kl => f kl.1 * g kl.2
The theorem `tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm` states that for a certain type `R` which is a normed ring and a complete space, given two functions `f` and `g` from natural numbers to `R` such that the infinite sums of the norms of `f` and `g` exist (meaning, they are summable), the product of the infinite sums of `f` and `g` equals the infinite sum over natural numbers of the sum of the products `f(k) * g(l)` for each `(k, l)` in the antidiagonal of `n`. This is essentially the Cauchy product formula for the product of two infinite sums, expressed in terms of the antidiagonal of a set.
More concisely: Given two summable functions `f` and `g` from natural numbers to a complete normed ring `R`, the infinite sum of the product of `f(k)` and `g(l)` for all `(k, l)` on the antidiagonal of `\mathbb{N} x \mathbb{N}` equals the product of the infinite sums of `f` and `g`.
|
tsum_mul_tsum_of_summable_norm
theorem tsum_mul_tsum_of_summable_norm :
∀ {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : NormedRing R] [inst_1 : CompleteSpace R] {f : ι → R}
{g : ι' → R},
(Summable fun x => ‖f x‖) →
(Summable fun x => ‖g x‖) → (∑' (x : ι), f x) * ∑' (y : ι'), g y = ∑' (z : ι × ι'), f z.1 * g z.2
This theorem states that the product of two infinite sums, indexed by arbitrary types, is equal to an infinite sum of products. Specifically, if we have a normed ring `R` and complete space `R`, with two functions `f` and `g` mapping from types `ι` and `ι'` to `R` respectively, and if the norms of `f` and `g` are summable, then the product of the sum of `f` over all `x` in `ι` and the sum of `g` over all `y` in `ι'` is equal to the sum over all pairs `(z1, z2)` in `ι × ι'` of the product of `f z1` and `g z2`.
More concisely: Given normed rings `R` and complete spaces, if functions `f : ι -> R` and `g : ι' -> R` have summable norms, then the product of their sums equals the sum of their products: ∫(x : ι) f x ⊤ dμ × ∫(y : ι') g y dν = ∫((z1, z2) : ι × ι') (f z1 * g z2) d(μ × ν)
|