tsum_eq_single
theorem tsum_eq_single :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} (b : β),
(∀ (b' : β), b' ≠ b → f b' = 0) → ∑' (b : β), f b = f b
The theorem `tsum_eq_single` states that for any types `α` and `β`, given an addition commutative monoid on `α` and a topology on `α`, and a function `f` from `β` to `α`, for any element `b` in `β`, if the function `f` maps every other element of `β` except `b` to zero, then the infinite summation over all elements `b` in `β` of `f(b)` is equal to `f(b)`. In other words, in an infinite sum, if all terms are zero except for one term, then the sum equals to the value of that one term.
More concisely: For any commutative monoid addition on type `α`, topology on `α`, and function `f` from type `β` to `α`, if for all `b' in β \ {b}, `f(b') = 0`, then `∑(b ∈ β) f(b) = f(b)`.
|
tsum_zero
theorem tsum_zero :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α], ∑' (x : β), 0 = 0 := by
sorry
This theorem states that for any types `α` and `β`, given `α` is an additive commutative monoid and also a topological space, the infinite sum (`tsum`) of zeros over all elements of `β` is zero. The infinite sum is a concept from the field of analysis, where summing an arbitrary number of elements (possibly infinite) in a specific order can produce a well-defined result. In this case, since all the elements are zero, the sum is zero.
More concisely: For any additive commutative monoid and topological space `α`, the infinite sum of zeros over all elements of `α` is equal to the zero element.
|
tsum_setElem_eq_tsum_setElem_diff
theorem tsum_setElem_eq_tsum_setElem_diff :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} (s t : Set β),
(∀ b ∈ t, f b = 0) → ∑' (a : ↑s), f ↑a = ∑' (a : ↑(s \ t)), f ↑a
The theorem `tsum_setElem_eq_tsum_setElem_diff` states that for any two sets `s` and `t` of some type `β` and a function `f` from `β` to `α` (where `α` is a type with addition and a topology), if all elements `b` in `t` satisfy `f b = 0`, then the total sum (`tsum`) of `f a` for all `a` in `s` is equal to the total sum of `f a` for all `a` in the difference set `s \ t` (meaning all elements in `s` that are not in `t`).
More concisely: Given sets `s` and `t` of type `β`, and a function `f` from `β` to a type `α` with additive structure and a topology, if `f(b) = 0` for all `b` in `t`, then `tsum (f ∘ χ_s) = tsum (f ∘ χ_(s \ t))`, where `χ_s` denotes the characteristic function of set `s`.
|
tsum_eq_add_tsum_ite'
theorem tsum_eq_add_tsum_ite' :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : T2Space α]
[inst_3 : ContinuousAdd α] [inst_4 : DecidableEq β] {f : β → α} (b : β),
Summable (Function.update f b 0) → ∑' (x : β), f x = f b + ∑' (x : β), if x = b then 0 else f x
This theorem, named `tsum_eq_add_tsum_ite'`, states that for all types `α` and `β`, given an addition commutative monoid structure, a topological space structure, a T2 space structure, continuous addition property on `α`, and a decidable equality operation on `β`. If we have a function `f` that maps from `β` to `α` and a specific element `b` of type `β`, and if the function `f` updated at point `b` to return `0` is summable, then the total sum of `f` over all `β` equals the value of `f` at `b` plus the total sum of `f` over all `β` excluding `b` (where the excluded `b` is replaced with `0` in the sum). In terms of mathematical notation, this theorem states that $\sum_{x} f(x) = f(b) + \sum_{x \neq b} f(x)$, under the given conditions.
More concisely: Given a commutative monoid with addition, a T2 topological space, continuous addition, and decidable equality on a type `β`, if `f: β → α` is summable and `b ∈ β` with `f(b) = 0`, then $\sum\_{x \in β} f(x) = f(b) + \sum\_{x \neq b} f(x)$.
|
tsum_subtype
theorem tsum_subtype :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : Set β) (f : β → α),
∑' (x : ↑s), f ↑x = ∑' (x : β), s.indicator f x
This theorem, `tsum_subtype`, states that for any types `α` and `β`, given that `α` forms an additive commutative monoid and has a topological space structure, and for a set `s` of elements of type `β` and a function `f` from `β` to `α`, the sum of `f` over the elements of `s` is equal to the sum of the indicator function of `s` applied to `f` over all elements of `β`. Here, the indicator function of a set `s` applied to `f` and `x` returns `f x` if `x` is in `s`, and `0` otherwise.
In mathematical notation, this could be denoted as $\sum_{x \in s} f(x) = \sum_{x \in \mathbb{B}} \mathbb{1}_{s}(x) f(x)$, where $\mathbb{1}_{s}(x)$ is the indicator function of the set `s` applied to `x`.
More concisely: For any additive commutative monoid type `α` with topological space structure, and for a set `s` and function `f` from a type `β` to `α`, the sum of `f` over `s` equals the sum of the indicator function of `s` applied to `f` over all elements of `β`.
|
tsum_eq_tsum_diff_singleton
theorem tsum_eq_tsum_diff_singleton :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} (s : Set β)
{b : β}, f b = 0 → ∑' (a : ↑s), f ↑a = ∑' (a : ↑(s \ {b})), f ↑a
The theorem `tsum_eq_tsum_diff_singleton` states that for any types `α` and `β`, given that `α` has an additive commutative monoid structure and a topological space structure, and given a function `f` from `β` to `α` and a set `s` of elements of type `β`, if the function `f` applied to an element `b` of `β` equals zero, then the sum of `f a` for all `a` in `s` is equal to the sum of `f a` for all `a` in the set `s` excluding `b`. Here, the sum `∑'` refers to the tsum or infinite series sum. In simpler terms, if a function returns zero for a certain element, removing that element from the set does not change the total sum.
More concisely: For any additive commutative monoid `α` with topological space structure, function `f` from a set `β` to `α`, and set `s` of elements in `β` such that `f(b) = 0` for some `b` in `s`, the sum of `f(a)` for all `a` in `s` equals the sum of `f(a)` for all `a` in `s` excluding `b`.
|
hasSum_ite_eq
theorem hasSum_ite_eq :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (b : β)
[inst_2 : DecidablePred fun x => x = b] (a : α), HasSum (fun b' => if b' = b then a else 0) a
The theorem `hasSum_ite_eq` states that for any types `α` and `β`, where `α` is an additive commutative monoid and also a topological space, and for any element `b` of type `β`, and for any `DecidablePred` instance that asserts whether an element equals to `b` or not, and for any element `a` of type `α`, the function that assigns `a` to `b` and `0` to all other values of type `β` has a sum, and that sum is `a`. In other words, if we sum up a function over all `b'` in `β` such that `b'` equals `b` contributes `a` to the sum and all other elements contribute `0`, then the total sum is `a`.
More concisely: For any additive commutative monoid and topological space α, any type β with a DecidablePred instance, and any b ∈ β and a ∈ α, the function that maps every element to 0 except for b which maps to a, has the property that the sum of this function equals a.
|
HasSum.add_compl
theorem HasSum.add_compl :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a b : α}
[inst_2 : ContinuousAdd α] {s : Set β},
HasSum (f ∘ Subtype.val) a → HasSum (f ∘ Subtype.val) b → HasSum f (a + b)
This theorem states that for any types `α` and `β`, given an addition commutative monoid structure and a topological space structure on `α`, and a continuous addition on `α`, if we have a function `f` from `β` to `α` and two elements `a` and `b` of `α`, and a set `s` of `β`, then if the sum of applying `f` to each element of the subtype defined by `s` equals `a` and the sum of applying `f` to each element of the complement of `s` equals `b`, then the sum of applying `f` to each element in `β` equals `a + b`. In other words, the total sum of `f` over the whole space is the sum of the sum over a subset and the sum over its complement.
More concisely: Given a commutative monoid `α` with topological space and continuous addition structures, and a function `f` from a topological space `β` to `α`, if the sum of `f` over every subset `s` of `β` equals `a` and the sum over `β \ s` equals `b`, then the sum of `f` over all of `β` equals `a + b`.
|
HasSum.add_isCompl
theorem HasSum.add_isCompl :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a b : α}
[inst_2 : ContinuousAdd α] {s t : Set β},
IsCompl s t → HasSum (f ∘ Subtype.val) a → HasSum (f ∘ Subtype.val) b → HasSum f (a + b)
The theorem `HasSum.add_isCompl` states that for any types `α` and `β`, with `α` being an additive commutative monoid and also a topological space, and `f` being a function from `β` to `α`, if we have two sets `s` and `t` that are complements of each other (`IsCompl s t`), and we know that the series of `f` applied to the elements of `s` and `t` (denoted as `(f ∘ Subtype.val)`) respectively have sum `a` and `b` (`HasSum (f ∘ Subtype.val) a` and `HasSum (f ∘ Subtype.val) b`), then the series formed by applying `f` to all elements of `β` (the union of `s` and `t`) has sum `a + b`. It also assumes that the addition operation in `α` is continuous (`ContinuousAdd α`). In essence, this theorem is a statement about the sum of a disjoint partition of a series.
More concisely: For any additive commutative monoid `α` that is a topological space, continuous addition, and functions `f : β -> α` from a type `β`, if `s` and `t` are complementary sets and `HasSum (f ∘ Subtype.val) a` and `HasSum (f ∘ Subtype.val) b` hold, then `HasSum (f) (a + b)`.
|
Equiv.tsum_eq
theorem Equiv.tsum_eq :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (e : γ ≃ β)
(f : β → α), ∑' (c : γ), f (e c) = ∑' (b : β), f b
This theorem, `Equiv.tsum_eq`, states that for any types `α`, `β`, and `γ` where `α` is an additive commutative monoid and is also a topological space, given a bijective function `e` from `γ` to `β` and another function `f` from `β` to `α`, the sum over all `γ` of `f` applied to `e(c)` (where `c` is a value of type `γ`) is equal to the sum over all `β` of `f(b)`. Essentially, this means that summing over a function applied to a bijective transformation yields the same result as summing over the function itself.
More concisely: Given an additive commutative monoid and topological space α, a bijective function e from γ to β, and a function f from β to α, the sum over all c in γ of f(e(c)) equals the sum over all b in β of f(b).
|
hasSum_single
theorem hasSum_single :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} (b : β),
(∀ (b' : β), b' ≠ b → f b' = 0) → HasSum f (f b)
This theorem states that for any two types `α` and `β`, given that `α` is an additive commutative monoid and a topological space, and `f` is a function from `β` to `α`, if for any element `b'` of `β` that is not equal to a certain element `b`, the function `f` returns `0`, then the sum of the function `f` over all `b` has a sum equal to `f(b)`. In essence, this theorem tells us that the sum of a function applied to all elements of a type is equal to the function applied to a single specific element, provided that the function returns zero for all other elements.
More concisely: If `f : β → α` is a function from a commutative monoid and topological space `β` to an abelian group `α`, such that `∀b₁ ≠ b, f b₁ = 0`, then `∑b : β, f b = f (summation binding b)`.
|
Function.Injective.tsum_eq
theorem Function.Injective.tsum_eq :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {g : γ → β},
Function.Injective g → ∀ {f : β → α}, Function.support f ⊆ Set.range g → ∑' (c : γ), f (g c) = ∑' (b : β), f b
This theorem, `Function.Injective.tsum_eq`, states that given types `α`, `β`, and `γ`, with `α` being an additive commutative monoid and also a topological space, an injective function `g` from `γ` to `β`, and another function `f` from `β` to `α`, if the support of function `f` (the set of points where `f` is not zero) is a subset of the range of function `g` (the set of all possible outputs of `g`), then the sum over `γ` of `f` applied to `g` is equal to the sum over `β` of `f`. In mathematical terms, it states that if $f: \beta \rightarrow \alpha$, $g: \gamma \rightarrow \beta$ is injective and the support of $f$ is contained in the range of $g$, then $\sum_{c \in \gamma} f(g(c)) = \sum_{b \in \beta} f(b)$.
More concisely: If `α` is an additive commutative monoid and topological space, `γ` is a type, `β` is a type, `α ⊑ β`, `g: γ → β` is injective, and the support of `f: β → α` is contained in the range of `g`, then $\sum_{c ∈ γ} f(g(c)) = \sum_{b ∈ β} f(b)$.
|
eq_add_of_hasSum_ite
theorem eq_add_of_hasSum_ite :
∀ {α : Type u_5} {β : Type u_6} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid α] [inst_2 : T2Space α]
[inst_3 : ContinuousAdd α] [inst_4 : DecidableEq β] {f : β → α} {a : α},
HasSum f a → ∀ (b : β) (a' : α), HasSum (fun n => if n = b then 0 else f n) a' → a = a' + f b
This theorem, named `eq_add_of_hasSum_ite`, is about the relationship between the sums of a function `f` and an `if-then-else` expression involving `f`. This relationship holds under certain conditions on the types and the function. Precisely, for a function `f` mapping from type `β` to a topological space `α` which is also an additive commutative monoid, if `f` has a sum equal to `a`, then for any element `b` of type `β` and any `a'` in `α`, if the `if-then-else` expression `(fun n => if n = b then 0 else f n)` has a sum equal to `a'`, then `a` is equal to `a'` plus `f b`. The function `f` is assumed to satisfy certain topological conditions, namely continuity in the topological structure of `α` and the `T2Space` (also known as the Hausdorff condition). The equality check in the `if-then-else` expression is decidable for all elements of type `β`.
More concisely: If `f` is a continuous, additive commutative monoid homomorphism from a T2 space `β` to an additive commutative monoid `α`, with decidable equality on `β`, such that `f` has a sum `a` and the `if-then-else` expression `(λn, if n = b then 0 else f n)` has a sum `a'`, then `a = a' + f b`.
|
tsum_subtype_eq_of_support_subset
theorem tsum_subtype_eq_of_support_subset :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {s : Set β},
Function.support f ⊆ s → ∑' (x : ↑s), f ↑x = ∑' (x : β), f x
The theorem `tsum_subtype_eq_of_support_subset` states that for any types `α` and `β`, given an additive commutative monoid structure and a topological space structure on `α`, and any function `f` from `β` to `α`, and any set `s` of type `β`, if the support of the function `f` (the set of points `x` where `f x ≠ 0`) is a subset of `s`, then the sum of `f` over the subtype induced by `s` is equal to the sum of `f` over all elements of `β`. Here, the sum is expressed using the `tsum` notation, which denotes an infinite sum in the context of a topological space.
More concisely: For any additive commutative monoid-valued function `f` on a topological space `β`, if the support of `f` is a subset of a set `s` in `β`, then the sum of `f` over the subtype induced by `s` equals the sum of `f` over all of `β`.
|
tsum_add
theorem tsum_add :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α}
[inst_2 : T2Space α] [inst_3 : ContinuousAdd α],
Summable f → Summable g → ∑' (b : β), (f b + g b) = ∑' (b : β), f b + ∑' (b : β), g b
The theorem `tsum_add` states that for any two functions `f` and `g` from a type `β` to a type `α`, if `α` is an additive commutative monoid, a topological space, a Hausdorff space (`T2Space`), and the addition operation on `α` is continuous (`ContinuousAdd`), then if both `f` and `g` are summable (meaning that their infinite series converges to some value), the sum of the infinite series of the sum of `f` and `g` (for each element in `β`) is equal to the sum of the individual infinite series of `f` and `g`. In other words, we have $\sum_{b\in \beta} (f(b) + g(b)) = \sum_{b\in \beta} f(b) + \sum_{b\in \beta} g(b)$.
More concisely: Given functions `f` and `g` from a type `β` to an additive commutative monoid `α`, which is a T2 space with continuous addition, if both `f` and `g` have convergent infinite series, then their series sum is commutative and distributive over the pointwise addition of `f` and `g`, i.e., ∫(β, α, f + g) = ∫(β, α, f) + ∫(β, α, g).
|
Summable.map_iff_of_equiv
theorem Summable.map_iff_of_equiv :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
[inst_2 : AddCommMonoid γ] [inst_3 : TopologicalSpace γ] {G : Type u_5} [inst_4 : EquivLike G α γ]
[inst_5 : AddEquivClass G α γ] (g : G),
Continuous ⇑g → Continuous (EquivLike.inv g) → (Summable (⇑g ∘ f) ↔ Summable f)
This theorem, named `Summable.map_iff_of_equiv`, states a special condition for the equivalence of summability of two functions. Specifically, for any types `α`, `β`, `γ`, and `G`, with `α` and `γ` equipped with an add commutative monoid structure and a topological space structure, and `G` is of equivalence-like type between `α` and `γ` and also forms an additive equivalence class between `α` and `γ`, we consider a function `f` from `β` to `α` and a function `g` from `G`. If the application of `g` (denoted as `⇑g`) and the inversion of `g` (denoted as `EquivLike.inv g`) are both continuous functions, then the summability of the composition of `g` and `f` (denoted as `⇑g ∘ f`) is equivalent to the summability of `f`. In simpler terms, under these conditions, if the infinite sum of the function values obtained by applying `f` and then `g` exists, then the infinite sum of the function values obtained by applying `f` also exists, and vice versa.
More concisely: If `g` is an additive equivalence class between `α` and `γ`, is an equivalence-like type between them, forms continuous functions, and `f` is a function from `β` to `α`, then the summability of `g ∘ f` is equivalent to the summability of `f`.
|
Finset.tsum_subtype'
theorem Finset.tsum_subtype' :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α),
∑' (x : ↑↑s), f ↑x = s.sum fun x => f x
The theorem `Finset.tsum_subtype'` states that for any types `α` and `β`, given an additive commutative monoid over `α` and a topological space over `α`, for a finite set `s` of type `β` and a function `f` from `β` to `α`, the sum of `f x` for `x` in the double-coercion of `s` (which treats `s` as a subtype, then as an infinite sum) is equal to the finite sum of `f x` over `s`. In other words, it says that the infinite sum over the elements of a finite set is the same as the finite sum over those elements, even when the finite set is treated as a subtype.
More concisely: For any additive commutative monoid over type `α`, topological space over `α`, finite set `s` of type `β`, and function `f` from `β` to `α`, the double-coercion sum of `f x` over `s` equals the finite sum of `f x` over `s`.
|
tsum_image
theorem tsum_image :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {g : γ → β}
(f : β → α) {s : Set γ}, Set.InjOn g s → ∑' (x : ↑(g '' s)), f ↑x = ∑' (x : ↑s), f (g ↑x)
The theorem `tsum_image` states that for all types `α`, `β`, and `γ` where `α` is an additive commutative monoid and a topological space, given a function `g` from `γ` to `β`, a function `f` from `β` to `α`, and a set `s` of type `γ`, if `g` is injective on `s`, then the sum over the set of the image of `g` applied to `s` (i.e., `g '' s`) of `f` applied to the image is equal to the sum over `s` of `f` composed with `g`. In mathematical notation, this is saying that
`∑_{x ∈ g(s)} f(x) = ∑_{x ∈ s} f(g(x))`
where `∑` denotes the sum over a set, the injectivity of `g` on `s` ensures that each element in `s` is mapped to a unique element in `g(s)`, and `f` is then applied to each of these unique elements.
More concisely: For any additive commutative monoid and topological space α, injective function g from γ to β, function f from β to α, and set s of type γ, the sum of f applied to the images of s under g equals the sum of f composed with g over s: ∑\_{x ∈ g(s)} f(x) = ∑\_{x ∈ s} f(g(x)).
|
hasSum_sum
theorem hasSum_sum :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : ContinuousAdd α] {f : γ → β → α} {a : γ → α} {s : Finset γ},
(∀ i ∈ s, HasSum (f i) (a i)) → HasSum (fun b => s.sum fun i => f i b) (s.sum fun i => a i)
This theorem states that for any types `α`, `β`, and `γ`, given `α` has an additive commutative monoid structure and a topological space structure such that addition is continuous, if you have a function `f` mapping each `γ` to a function from `β` to `α`, and you have a finset `s` of `γ` and a function `a` mapping each `γ` to `α` such that for each `i` in `s`, the function `f i` has a sum equivalent to `a i` (as expressed by `HasSum (f i) (a i)`), then the function mapping each `β` to the sum of `f i b` for each `i` in `s` has a sum equal to the sum of `a i` for each `i` in `s` (as expressed by `HasSum (fun b => Finset.sum s fun i => f i b) (Finset.sum s fun i => a i)`). In simpler terms, this is a generalization of the idea that the sum of the sums is the sum of the total.
More concisely: Given types `α` with additive commutative monoid and topological space structures where addition is continuous, and functions `f: γ → β → α` and `a: γ → α` such that `HasSum (f i) (a i)` for all `i` in a finite set `s`, the function `β → Finset.sum s (λ i, f i) b` has a sum equal to `Finset.sum s a`.
|
HasSum.add
theorem HasSum.add :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α} {a b : α}
[inst_2 : ContinuousAdd α], HasSum f a → HasSum g b → HasSum (fun b => f b + g b) (a + b)
This theorem, `HasSum.add`, states that for all types `α` and `β`, where `α` is an additive commutative monoid and a topological space, and `α` also has the property of continuous addition, if there are two functions `f` and `g` from `β` to `α` such that `f` has a sum `a` and `g` has a sum `b`, then the function that maps each element of `β` to the sum of its images under `f` and `g` has a sum of `a + b`. In other words, the sum of the sums of two functions is equal to the sum of the function that is their pointwise sum.
More concisely: For additive commutative monoid and topological space types `α` endowed with continuous addition, if functions `f` and `g` from type `β` to `α` have sums `a` and `b` respectively, then the function `h` defined by `h x = f x + g x` has sum `a + b`.
|
tsum_eq_sum
theorem tsum_eq_sum :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {s : Finset β},
(∀ b ∉ s, f b = 0) → ∑' (b : β), f b = s.sum fun b => f b
The theorem `tsum_eq_sum` states that for any types `α` and `β`, with `α` equipped with an additive commutative monoid structure and a topological space structure, and for any function `f` from `β` to `α` and any finite set `s` of elements of type `β`, if the function `f` evaluates to `0` for all elements not in `s`, then the unbounded sum (denoted by `∑'`) of `f` over all elements of type `β` equals the finite sum (denoted by `Finset.sum`) of `f` over the elements of the finite set `s`. In mathematical terms, if `f(b) = 0` for all `b` not in `s`, then `∑' (b : β), f(b) = ∑ x in s, f(x)`.
More concisely: For any additive commutative monoid- and topological space-structured type `α` with function `f` from a finite set `s` of `α`'s elements to `α`, if `f(b) = 0` for all `b` outside `s`, then the unbounded sum of `f` equals the finite sum over `s`.
|
Summable.map_iff_of_leftInverse
theorem Summable.map_iff_of_leftInverse :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
[inst_2 : AddCommMonoid γ] [inst_3 : TopologicalSpace γ] {G : Type u_5} {G' : Type u_6} [inst_4 : FunLike G α γ]
[inst_5 : AddMonoidHomClass G α γ] [inst_6 : FunLike G' γ α] [inst_7 : AddMonoidHomClass G' γ α] (g : G)
(g' : G'), Continuous ⇑g → Continuous ⇑g' → Function.LeftInverse ⇑g' ⇑g → (Summable (⇑g ∘ f) ↔ Summable f)
The theorem `Summable.map_iff_of_leftInverse` states that for any types `α`, `β`, `γ`, if `α` and `γ` are both additively commutative monoids and topological spaces, and for any terms `f` of type `β → α`, `g` of a type `G` that has a function-like behavior from `α` to `γ`, and `g'` of a type `G'` that has a function-like behavior from `γ` to `α`, if both `g` and `g'` are continuous and `g'` is a left inverse to `g` (meaning that applying `g'` after `g` gives the identity on `α`), then `f` is summable if and only if the composition `g ∘ f` is summable.
In simpler terms, this theorem states that if you have a summable function `f` and a pair of continuous functions `g` and `g'` acting like an inverse pair, then the function obtained by applying `g` to `f` is also summable, and vice versa.
More concisely: If `α`, `β`, `γ` are additively commutative monoids and topological spaces, `f: β -> α`, `g: α -> γ`, `g': γ -> α` are continuous functions with `g'` being a left inverse to `g`, then `Summable f <-> Summable (g ∘ f)`.
|
HasSum.update'
theorem HasSum.update' :
∀ {α : Type u_5} {β : Type u_6} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid α] [inst_2 : T2Space α]
[inst_3 : ContinuousAdd α] [inst_4 : DecidableEq β] {f : β → α} {a a' : α},
HasSum f a → ∀ (b : β) (x : α), HasSum (Function.update f b x) a' → a + x = a' + f b
The theorem `HasSum.update'` states that for all types `α` and `β`, where `α` is a topological space, a T2 space, and has a continuous addition operation, and `β` has a decidable equality, given a function `f : β → α` and values `a` and `a'` of type `α`, if the function `f` has a sum `a`, then for any `b` in `β` and `x` in `α`, if the function obtained by updating `f` at `b` with `x` (`Function.update f b x`) has a sum `a'`, then the sum `a` plus `x` is equal to the sum `a'` plus the value of `f` at `b` (`f b`). This theorem essentially provides a relationship between the sums of a function and its update under certain conditions.
More concisely: If `α` is a T2 topological space with a continuous addition operation and `β` has decidable equality, given a function `f : β → α` with sum `a`, and for all `b ∈ β` and `x ∈ α`, if `Function.update f b x` has sum `a'`, then `a + x = a' + f b`.
|
Finset.tsum_subtype
theorem Finset.tsum_subtype :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α),
∑' (x : { x // x ∈ s }), f ↑x = s.sum fun x => f x
This theorem, `Finset.tsum_subtype`, states that for any types `α` and `β`, given an additive commutative monoid structure on `α` and a topological space structure on `α`, for any finite set `s` of type `β` and any function `f` from `β` to `α`, the infinite sum or topological sum (denoted by `∑'`) over all elements `x` in `s` of `f` applied to the subtype `x` (where the subtype is defined by the property that `x` is in `s`) is equal to the finite sum (denoted by `Finset.sum`) over all elements `x` in `s` of `f` applied to `x`. This is an important property that connects the concept of an infinite sum in topology with the finite sum operation on finite sets.
More concisely: For any additive commutative monoid `α` with topological space structure, and any finite set `s` and function `f` from a type `β` to `α`, the infinite topological sum over `s` of `f` applied to the subtype of `s` is equal to the finite sum over `s` of `f` applied to each element.
|
hasSum_subtype_iff_indicator
theorem hasSum_subtype_iff_indicator :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
{s : Set β}, HasSum (f ∘ Subtype.val) a ↔ HasSum (s.indicator f) a
This theorem establishes a relationship between the summability of a function `f` over a subset `s` of a type `β`, and the summability of the indicator function of `s` applied to `f`. Specifically, it states that for any types `α` and `β`, with `α` being an additive commutative monoid and also a topological space, a function `f` from `β` to `α`, a value `a` of type `α`, and a set `s` of type `β`, the function `f` has a sum `a` over the elements of `s` if and only if the indicator function of `s` applied to `f` has a sum `a`. The indicator function is defined such that it equals `f` at each point in `s` and `0` elsewhere.
More concisely: For any additive commutative monoid and topological space type β, function f from β to an additive commutative monoid α, value a of type α, and set s of type β, the function f has a sum a over s if and only if the indicator function of s applied to f has a sum a.
|
tsum_congr_set_coe
theorem tsum_congr_set_coe :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) {s t : Set β},
s = t → ∑' (x : ↑s), f ↑x = ∑' (x : ↑t), f ↑x
This theorem states that for any types `α` and `β`, given an addition-commutative monoid structure and a topological space structure on `α`, and a function `f` mapping elements of `β` to `α`, if we have two sets `s` and `t` of type `β` and they are equal, then the total sum (notated as `∑'`) of the function `f` applied to the elements of the coerced set `s` (notated as `↑s`) is equal to the total sum of the function `f` applied to the elements of the coerced set `t` (notated as `↑t`). In mathematical terms, for equal sets `s` and `t`, it states that ∑_{x ∈ s} f(x) = ∑_{x ∈ t} f(x).
More concisely: For any addition-commutative monoid `α` with a topological space structure, and function `f` from a type `β` to `α`, if `s` and `t` are equal sets in `β`, then ∑$_{x \in s}$ `f`(`x`) = ∑$_{x \in t}$ `f`(`x`).
|
HasSum.map
theorem HasSum.map :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
{a : α} [inst_2 : AddCommMonoid γ] [inst_3 : TopologicalSpace γ],
HasSum f a →
∀ {G : Type u_5} [inst_4 : FunLike G α γ] [inst : AddMonoidHomClass G α γ] (g : G),
Continuous ⇑g → HasSum (⇑g ∘ f) (g a)
The theorem `HasSum.map` states that for any types `α`, `β`, and `γ`, given an additively commutative monoid structure and a topological space structure on `α` and `γ`, a function `f` from `β` to `α`, and a value `a` of type `α` such that `f` has a sum `a`, then for any type `G` that is function-like from `α` to `γ` and has an additive monoid homomorphism class, if a function `g` of type `G` is continuous, then the composition of `g` with `f` (`g ∘ f`) has sum equal to `g a`. In other words, it's stating that the sum of the image of a function under a continuous homomorphism is the homomorphism of the sum, provided the original function has a sum.
More concisely: Given additively commutative monoids and topological spaces `α`, `β`, `γ`, a continuous additive homomorphism `g` from `α` to `γ`, a function `f` from `β` to `α` with sum `a` in `α`, and an element `b` in `β` such that `f(b) = a`, then `g(a) = g(∑ i. f(bi)) = ∑ i. g(fi)`, where the sums are taken over the index set of `f`.
|
hasSum_zero
theorem hasSum_zero :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α], HasSum (fun x => 0) 0 := by
sorry
This theorem states that for any types `α` and `β`, where `α` is a commutative monoid under addition and is also equipped with a topology, the sum of the constant zero function (which maps every element of type `β` to `0` in `α`) is `0`. In other words, if you add up all the zeros produced by this function, the result is zero.
More concisely: For any commutative monoid `α` with topology and function `zero : β → α`, the sum of `zero` is equal to the additive identity `0` in `α`.
|
Equiv.hasSum_iff
theorem Equiv.hasSum_iff :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
{a : α} (e : γ ≃ β), HasSum (f ∘ ⇑e) a ↔ HasSum f a
This theorem states that for any types `α`, `β`, and `γ`, where `α` is an additive commutative monoid and also has a topology, for any function `f` mapping `β` to `α` and any element `a` of `α`, given an equivalence `e` between `γ` and `β`, the function `f` has a sum equal to `a` when composed with the inverse of `e` if and only if the function `f` has a sum equal to `a`. This means that the sum total of the composed function does not change under the transformation of `e`.
More concisely: For any additive commutative monoid `α` with a topology, function `f` from `β` to `α`, element `a` in `α`, and equivalence `e` between `γ` and `β`, if `f` has a sum equal to `a` in `α` then `f ∘ e^{-1}` also has a sum equal to `a`.
|
tsum_fintype
theorem tsum_fintype :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] [inst_2 : Fintype β]
(f : β → α), ∑' (b : β), f b = Finset.univ.sum fun b => f b
The theorem `tsum_fintype` states that for any types `α` and `β`, where `α` is a commutative monoid with a topology and `β` is a finite type, and for any function `f` from `β` to `α`, the infinite sum (notated as `∑' (b : β), f b`) equals the sum of `f b` as `b` ranges over the universal finite set of type `β`. In other words, for finite types, the infinite series sum is equivalent to the sum taken over all elements of the type.
More concisely: For any commutative monoid with a topology `α`, finite type `β`, and function `f` from `β` to `α`, the infinite sum `∑' (b : β), f b` equals the sum of `f b` over all elements in `β`.
|
tsum_congr
theorem tsum_congr :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α},
(∀ (b : β), f b = g b) → ∑' (b : β), f b = ∑' (b : β), g b
This theorem states that for any two functions `f` and `g` from an arbitrary type `β` to a type `α`, given that `α` forms an additive commutative monoid and has a defined topological space, if all values of `f` and `g` are equal for every item in `β`, then the summation of `f` over all elements of `β` is equal to the summation of `g` over all elements of `β`. In other words, if two functions produce the same output for every input, then the infinite sum of their outputs will also be the same.
More concisely: If two functions from an arbitrary type to an additive commutative monoid with a topological space have equal values for all elements, then their summations over the entire type are equal.
|
Equiv.summable_iff
theorem Equiv.summable_iff :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
(e : γ ≃ β), Summable (f ∘ ⇑e) ↔ Summable f
The theorem `Equiv.summable_iff` states that for any three types `α`, `β`, `γ` where `α` is an additive commutative monoid and also a topological space, and given a function `f` from `β` to `α` and a bijection `e` from `γ` to `β`, the composition of `f` with `e` is summable if and only if `f` itself is summable. In other words, changing the domain of the summable function via a bijection doesn't affect its summability.
More concisely: For any additive commutative monoid and topological space `α`, function `f` from a set `β` to `α`, and bijection `e` from `γ` to `β`, the composition of `f` with `e` is summable if and only if `f` is summable.
|