tsum_mul_tsum
theorem tsum_mul_tsum :
∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : T3Space α]
[inst_2 : NonUnitalNonAssocSemiring α] [inst_3 : TopologicalSemiring α] {f : ι → α} {g : κ → α},
Summable f →
Summable g →
(Summable fun x => f x.1 * g x.2) → (∑' (x : ι), f x) * ∑' (y : κ), g y = ∑' (z : ι × κ), f z.1 * g z.2
The theorem `tsum_mul_tsum` states that for any two arbitrary types `ι` and `κ` and a type `α`, given that `α` is a topological space, a T3 space, a non-unital non-associative semiring, and a topological semiring, with two functions `f : ι → α` and `g : κ → α` that are both summable, and a function `(Summable fun x => f x.1 * g x.2)`, then the product of the infinite sums of `f` and `g` is equal to the infinite sum over the product of `f` and `g` across the cartesian product of `ι` and `κ`. In mathematical notation, this reads: if `f` and `g` are summable, then `(∑' (x : ι), f x) * ∑' (y : κ), g y = ∑' (z : ι × κ), f z.1 * g z.2`.
More concisely: For any topological semiring `α` and summable functions `f : ι → α` and `g : κ → α`, the infinite product of their sums equals the infinite sum of their pointwise products over the cartesian product of `ι` and `κ`.
|
HasSum.mul_right
theorem HasSum.mul_right :
∀ {ι : Type u_1} {α : Type u_4} [inst : NonUnitalNonAssocSemiring α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalSemiring α] {f : ι → α} {a₁ : α} (a₂ : α),
HasSum f a₁ → HasSum (fun i => f i * a₂) (a₁ * a₂)
This theorem, `HasSum.mul_right`, states that for any type `ι` and any non-unital, non-associative semiring `α` that is also a topological space and a topological semiring, if a function `f : ι → α` has a sum `a₁`, then the function `f i * a₂`, where `a₂` is a constant, also has a sum, equal to `a₁ * a₂`. This means that multiplying each term in a series by a constant multiplies the sum of the series by the same constant, a property often assumed in analysis and similar fields.
More concisely: For any non-unital, non-associative semiring `α` that is also a topological space and a topological semiring, if a function `f : ι → α` from a type `ι` has a sum `a₁`, then `(∑ i, f i) * a₂` has the sum `a₁ * a₂`, where `a₂` is a constant.
|
Summable.tsum_mul_left
theorem Summable.tsum_mul_left :
∀ {ι : Type u_1} {α : Type u_4} [inst : NonUnitalNonAssocSemiring α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalSemiring α] {f : ι → α} [inst_3 : T2Space α] (a : α),
Summable f → ∑' (i : ι), a * f i = a * ∑' (i : ι), f i
The theorem `Summable.tsum_mul_left` states that, for any index type `ι`, any type `α` that is a non-unital non-associative semiring and a topological space (and also a topological semiring and T2 space), for any function `f : ι → α`, and any element `a` of `α`, if `f` is summable, then the infinite sum of the series formed by multiplying each term of `f` by `a` equals the product of `a` and the infinite sum of `f`. Mathematically, it can be represented as if $\sum_{i} f(i)$ exists, then $\sum_{i} a*f(i) = a*\sum_{i} f(i)$.
More concisely: For any index type `ι`, any non-unital non-associative semiring and topological space `α`, if `f : ι → α` is summable and `a` is an element of `α`, then $\sum\_{i} a*f(i) = a*\sum\_{i} f(i)$.
|
tsum_mul_left
theorem tsum_mul_left :
∀ {ι : Type u_1} {α : Type u_4} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalSemiring α] {f : ι → α} {a : α} [inst_3 : T2Space α],
∑' (x : ι), a * f x = a * ∑' (x : ι), f x
This theorem states that for any type `ι`, and any type `α` that is a division semiring, a topological space, and a topological semiring, and for any function `f` from `ι` to `α`, and any element `a` of `α`, in a Hausdorff space (`T2Space`), the sum of the product of `a` and `f x` over all `x` in `ι` is equal to the product of `a` and the sum of `f x` over all `x` in `ι`. In simpler terms, this theorem asserts the distributivity of multiplication over infinite summation in a certain mathematical context.
More concisely: In a Hausdorff space, for any type `α` that is a division semiring, topological space, and topological semiring, and for any function `f` from `ι` to `α` and element `a` of `α`, the infinite sum of `a * f x` over `x` in `ι` equals the product of `a` and the infinite sum of `f x` over `x` in `ι`.
|
HasSum.mul_left
theorem HasSum.mul_left :
∀ {ι : Type u_1} {α : Type u_4} [inst : NonUnitalNonAssocSemiring α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalSemiring α] {f : ι → α} {a₁ : α} (a₂ : α),
HasSum f a₁ → HasSum (fun i => a₂ * f i) (a₂ * a₁)
This theorem states that for any index type `ι`, any type `α` that is a non-unital non-associative semiring and a topological space, and any function `f` from `ι` to `α`, if the sum of the series defined by `f` converges to a value `a₁`, then the sum of the series defined by the function `λi, a₂ * f(i)` (i.e., the series obtained by multiplying every term in the original series by a constant `a₂`) converges to `a₂ * a₁`. This is in essence a formalization of the property of constant multiples in series summation in mathematics.
More concisely: Given a non-unital non-associative semiring `α` and a topological space `ι`, if the series `∑ i : ι, f i` converges to `a₁` in `α`, then `∑ i : ι, a₂ * f i` converges to `a₂ * a₁` for any constant `a₂` in `α`.
|
Summable.mul_left
theorem Summable.mul_left :
∀ {ι : Type u_1} {α : Type u_4} [inst : NonUnitalNonAssocSemiring α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalSemiring α] {f : ι → α} (a : α), Summable f → Summable fun i => a * f i
The theorem `Summable.mul_left` states that for any type `ι`, a non-unital, non-associative semiring `α`, and a topological space `α` with a topological semiring structure, given a function `f : ι → α` and an element `a` in `α`, if the function `f` is summable, then the function defined as the product of `a` and `f` (i.e., `fun i => a * f i`) is also summable. In other words, multiplying a summable function by a scalar results in a summable function.
More concisely: If `α` is a non-unital, non-associative semiring with a topological structure, `ι` is a type, `f : ι → α` is a summable function, and `a` is an element of `α`, then the function `g : ι → α` defined as `g i := a * f i` is also summable.
|
tsum_mul_tsum_eq_tsum_sum_antidiagonal
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal :
∀ {α : Type u_4} {A : Type u_5} [inst : AddCommMonoid A] [inst_1 : Finset.HasAntidiagonal A]
[inst_2 : TopologicalSpace α] [inst_3 : NonUnitalNonAssocSemiring α] {f g : A → α} [inst_4 : T3Space α]
[inst_5 : TopologicalSemiring α],
Summable f →
Summable g →
(Summable fun x => f x.1 * g x.2) →
(∑' (n : A), f n) * ∑' (n : A), g n = ∑' (n : A), (Finset.antidiagonal n).sum fun kl => f kl.1 * g kl.2
The **Cauchy product formula** states that for any types `α` and `A` where `A` has a finset antidiagonal, `α` is a topological space and a non-unitary non-associative semiring, and `f` and `g` are functions from `A` to `α`. Additionally, `α` is a `T3Space` and a topological semiring, if `f` and `g` are summable and the product of `f` and `g` over the antidiagonal of each element in `A` is also summable, then the product of the infinite sums of `f` and `g` equals the infinite sum of the products of `f` and `g` over the antidiagonal of each element in `A`.
More concisely: If `α` is a topological T3 space and a non-unitary, non-associative semiring with finset antidiagonal, `f` and `g` are summable functions from `A` to `α`, and the antidiagonal products of `f` and `g` are summable, then the infinite sum of their products over the antidiagonal equals the product of their infinite sums.
|
tsum_mul_tsum_eq_tsum_sum_range
theorem tsum_mul_tsum_eq_tsum_sum_range :
∀ {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : NonUnitalNonAssocSemiring α] {f g : ℕ → α}
[inst_2 : T3Space α] [inst_3 : TopologicalSemiring α],
Summable f →
Summable g →
(Summable fun x => f x.1 * g x.2) →
(∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), (Finset.range (n + 1)).sum fun k => f k * g (n - k)
The Cauchy product formula theorem in Lean 4 states that for any non-unital non-associative semiring with a topological space structure, and given two functions `f` and `g` from natural numbers to elements of the semiring, if `f` and `g` are both summable and the product of `f` and `g` (where each term of the product is indexed by a pair of natural numbers) is also summable, then the infinite sum of `f` times the infinite sum of `g` equals the infinite sum over all natural numbers of the sum over the range up to `n+1` of the product of `f` and `g`, where each term of the product is indexed by a natural number and its complement to `n`.
More concisely: If `f` and `g` are summable functions from natural numbers to a non-unital non-associative semiring with a topological space structure such that their product is also summable, then the infinite series $\sum\_{i=0}^{\infty} f(i) \cdot \sum\_{j=0}^{\infty} g(j) = \sum\_{n=0}^{\infty} \left( \sum\_{i=0}^{n} f(i) \cdot g(n-i) \right)$.
|
tsum_mul_right
theorem tsum_mul_right :
∀ {ι : Type u_1} {α : Type u_4} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalSemiring α] {f : ι → α} {a : α} [inst_3 : T2Space α],
∑' (x : ι), f x * a = (∑' (x : ι), f x) * a
This theorem, `tsum_mul_right`, states that for any type `ι`, any type `α` that has a DivisionSemiring structure, a TopologicalSpace structure, and a TopologicalSemiring structure, any function `f` from `ι` to `α`, and any element `a` of `α`, where `α` also has a T2Space (also known as a Hausdorff space) structure, the sum of the product of `f x` and `a` for all `x` in `ι` is equal to the product of the sum of `f x` for all `x` in `ι` and `a`. In mathematical terms, it states that $\sum_{x \in \iota} (f(x) \cdot a) = (\sum_{x \in \iota} f(x)) \cdot a$. This is a distributive property of multiplication over infinite summation in a topological semiring.
More concisely: In a TopologicalSemiring with a T2Space structure, for any function `f` from a type `ι` to a type `α` with a DivisionRing structure and any element `a` of `α`, the sum of the products `f x * a` over all `x` in `ι` equals the product of the sum of `f x` over all `x` in `ι` and `a`.
|