tsum_eq_zero_of_not_summable
theorem tsum_eq_zero_of_not_summable :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α},
¬Summable f → ∑' (b : β), f b = 0
The theorem `tsum_eq_zero_of_not_summable` states that for any types `α` and `β`, any additive commutative monoid structure on `α`, any topological space structure on `α`, and any function `f` from `β` to `α`, if the function `f` is not summable (i.e., it doesn't have an infinite sum), then the total sum of the series created by `f` is zero. In mathematical notation, we write this as: if ∃ a, such that ∑ f(n) does not converge to a (i.e., f is not summable), then ∑ f(n) = 0.
More concisely: If a function from a type to an additive commutative monoid with a topology, where the sum over the image of any non-convergent sequence does not exist, equals the additive identity of the monoid.
|
HasSum.tsum_eq
theorem HasSum.tsum_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
[inst_2 : T2Space α], HasSum f a → ∑' (b : β), f b = a
This theorem states that for all types `α` and `β`, where `α` is an additive commutative monoid and a topological space, and `β` is an arbitrary type with a function `f` from `β` to `α`, and a constant `a` of type `α`, if `α` is also a T2 space (also known as a Hausdorff space), and the sum of the function `f` over all `β` converges to `a` (expressed as `HasSum f a`), then the infinite sum (notated as `∑' (b : β), f b`) of `f` over all `β` is equal to `a`. In simpler terms, it says that if an infinite sum over a function converges, then the sum is equal to the value it converges to.
More concisely: If `α` is an additive commutative monoid, a topological space, and a T2 space, and `f : β → α` has a convergent sum `HasSum f a`, then `∑' (b : β), f b = a`.
|
hasSum_fintype
theorem hasSum_fintype :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : Fintype β]
(f : β → α), HasSum f (Finset.univ.sum fun b => f b)
The theorem `hasSum_fintype` states that for any given types `α` and `β`, where `α` is an additive commutative monoid and also a topological space, and `β` is a finite type, and any function `f` from `β` to `α`, the function `f` has a sum. This sum is computed by applying the function `f` to each element of the universal finite set of type `β` (`Finset.univ`), and then taking the sum of these results (using `Finset.sum`). In other words, we sum up the values of the function `f` over all elements of the finite type `β`.
More concisely: For any additive commutative monoid and topological space type `α`, finite type `β`, and function `f` from `β` to `α`, there exists a sum `∑ i in Finset.univ (f i)` of `f` over the universal set of type `β`.
|
HasSum.unique
theorem HasSum.unique :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a₁ a₂ : α}
[inst_2 : T2Space α], HasSum f a₁ → HasSum f a₂ → a₁ = a₂
This theorem states that for any function `f` from a type `β` to a type `α`, if `α` is an additive commutative monoid and a topological space with the Hausdorff property (T2 space), and if `a₁` and `a₂` are two elements of `α` such that `f` has sums `a₁` and `a₂`, then `a₁` and `a₂` must be equal. In other words, the series sum of `f` is unique within a Hausdorff topological space.
More concisely: If `f` is a function from a type `β` to an additive commutative monoid and Hausdorff topological space `α`, then for all `a₁, a₂ ∈ α` such that `f` has sums `a₁` and `a₂`, it follows that `a₁ = a₂`.
|
hasSum_subtype_iff_of_support_subset
theorem hasSum_subtype_iff_of_support_subset :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
{s : Set β}, Function.support f ⊆ s → (HasSum (f ∘ Subtype.val) a ↔ HasSum f a)
This theorem states that for any types `α` and `β`, given an addition-commutative monoid structure on `α` and a topological space structure on `α`, for any function `f` from `β` to `α` and any element `a` of `α`, and for a set `s` of `β`, if the support of function `f` (i.e., the set of points `x` such that `f(x) ≠ 0`) is a subset of set `s`, then the proposition "the sum of the function `f` composed with the projection function `Subtype.val` has a limit of `a`" is logically equivalent to the proposition "the sum of the function `f` also has a limit of `a`". Here, the sum is over the elements in the subtype defined by the predicate corresponding to set `s`.
More concisely: For any addition-commutative monoid `α` with a topology, function `f` from type `β` to `α`, and subsets `s` of `β`, if `f`'s support is contained in `s` and the sum of `f` has a limit as the elements in the subtype of `β` defined by `s` approach, then the sum of `f` composed with the projection function from the subtype to `α` also has a limit equal to the limit of `a` in `α`.
|
HasSum.summable
theorem HasSum.summable :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α},
HasSum f a → Summable f
The theorem `HasSum.summable` states that for any types `α` and `β`, given an additive commutative monoid structure on `α` and a topological space structure on `α`, if a function `f` from `β` to `α` has a sum `a` (denoted by `HasSum f a`), then `f` is summable (denoted by `Summable f`). In mathematical terms, if an infinite series associated with function `f` converges to a sum `a`, then the series is considered summable.
More concisely: If `α` is an additive commutative monoid with a topology, and `f : β → α` has a sum `a`, then `f` is summable to `a`.
|
tsum_def
theorem tsum_def :
∀ {α : Type u_4} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {β : Type u_5} (f : β → α),
tsum f = if h : Summable f then if (Function.support f).Finite then finsum f else Exists.choose h else 0
The theorem `tsum_def` states that for any type `α` that forms an additive commutative monoid and has a topological space structure, and any function `f` from type `β` to `α`, the sum `∑' i, f i` is defined as follows: If `f` is summable (i.e., it has an infinite sum), then if the support of `f` (the set of points `x` for which `f x ≠ 0`) is finite, it equals the finite sum of `f`; otherwise, it equals some value obtained from the summability of `f`. If `f` is not summable, then the sum is 0.
More concisely: For any additive commutative monoid type `α` with topological space structure and summable function `f` from type `β` to `α` with finite support, the sum `∑' i, f i` equals the finite sum of `f`; otherwise, it equals the value obtained from `f`'s summability. If `f` is not summable, the sum is 0.
|
hasSum_sum_of_ne_finset_zero
theorem hasSum_sum_of_ne_finset_zero :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {s : Finset β},
(∀ b ∉ s, f b = 0) → HasSum f (s.sum fun b => f b)
The theorem `hasSum_sum_of_ne_finset_zero` states that for any types `α` and `β`, given `α` is an additive commutative monoid and also a topological space, for any function `f` from `β` to `α` and any finite set `s` of type `β`, if the function `f` yields zero for all elements not in the set `s`, then the function `f` has a sum which is equivalent to the sum of `f b` for each element `b` in the set `s`.
In mathematical terms, if a function `f` is zero outside of a finite set `s`, then the series represented by `f` converges to the sum of `f(x)` for each `x` in `s`.
More concisely: Given a function `f` from a finite set `s` to an additive commutative monoid and topological space `α`, if `f` is zero outside of `s`, then the sum of `f` equals the sum of `f(x)` for all `x` in `s`.
|
Summable.hasSum_iff
theorem Summable.hasSum_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
[inst_2 : T2Space α], Summable f → (HasSum f a ↔ ∑' (b : β), f b = a)
The theorem `Summable.hasSum_iff` provides a condition to check if a series has a specific sum in a given topological space. For any types `α` and `β`, along with a function `f : β → α`, an element `a : α`, and an instance of `α` being a `T2` space (also known as a Hausdorff space), if the series of `f` is summable, then the series `f` has a sum `a` if and only if the infinite summation of `f` over all `b` in `β` equals `a`.
More concisely: For a function `f : β → α` with type `α` being a T2 space, `a : α`, and summable series `∑ x in β, f x`, the series `∑ x in β, f x` has sum `a` if and only if the limit of `∑ x in β, f x` as `β` approaches infinity exists and equals `a`.
|
Function.Injective.hasSum_iff
theorem Function.Injective.hasSum_iff :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
{a : α} {g : γ → β}, Function.Injective g → (∀ x ∉ Set.range g, f x = 0) → (HasSum (f ∘ g) a ↔ HasSum f a)
The theorem `Function.Injective.hasSum_iff` states that for any types `α`, `β`, and `γ`, given an addition commutative monoid structure and a topological space structure on `α`, a function `f : β → α`, a value `a : α`, and an injective function `g : γ → β`, if `f x = 0` for all `x` not in the range of `g`, then the sum of the sequence `(f ∘ g)` converges to `a` if and only if the sum of the sequence `f` converges to `a`. Here, `HasSum` is a predicate stating that a sequence (represented by a function from the natural numbers) converges to a particular value.
More concisely: Given a commutative monoid with addition on types `α`, a topological space `α`, a function `f : β → α`, an injective function `g : γ → β`, value `a : α`, and sequences `(x_n : β)` in the range of `g` and `(y_n : γ)`, if `f ∘ g (y_n) = 0` for all `y_n ≠ y_m`, then the sequence `(f (g (y_n)))` converges to `a` if and only if the sequence `(f x_n)` converges to `a`.
|
Finset.hasSum
theorem Finset.hasSum :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α),
HasSum (f ∘ Subtype.val) (s.sum fun b => f b)
The theorem `Finset.hasSum` asserts that, for all types `α` and `β` with `α` being an additive commutative monoid and a topological space, and for any finite set `s` of type `β` and any function `f` from `β` to `α`, the sum of the function `f` after applying the subtype value function (`Subtype.val`) has a sum, and that sum is equal to the sum of `f` over the elements of the finite set `s`. Essentially, it states that the sum of the function values over the elements of `s` is the same whether we consider those elements as pure elements of type `β` or as elements of the subtype of `β`.
More concisely: For any additive commutative monoid and topological space type `α`, finite set `s` of type `β`, and function `f` from `β` to `α`, the sum of `f` over the elements of `s` is equal to the sum of `Subtype.val (s : Set β) . f` in `α`.
|
Summable.hasSum
theorem Summable.hasSum :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α},
Summable f → HasSum f (∑' (b : β), f b)
The theorem `Summable.hasSum` states that for any types `α` and `β`, where `α` is a type with an addition operation (`AddCommMonoid`) and a topology (`TopologicalSpace`), and `f` is a function from `β` to `α`, if `f` is summable (`Summable f`), then the function `f` has a sum (`HasSum f`) that equals to the total sum of `f` over all elements of `β` (expressed as `∑' (b : β), f b`). In other words, if a function `f` is summable, then the sum of its values over all inputs equals to the sum associated with `f`.
More concisely: If `f` is a summable function from a topological space `β` to an additive commutative monoid `α`, then the function `f` has a sum equal to the sum of `f` over all elements of `β`.
|