Summable.tendsto_cofinite_zero
theorem Summable.tendsto_cofinite_zero :
∀ {α : Type u_1} {G : Type u_5} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G]
[inst_2 : TopologicalAddGroup G] {f : α → G}, Summable f → Filter.Tendsto f Filter.cofinite (nhds 0)
This theorem, known as the "Series divergence test", states that if a function `f` is unconditionally summable (that is, the infinite sum of its values exists), then the values of `f(x)` tends to zero in the cofinite filter. The cofinite filter is defined as the collection of subsets whose complements are finite, so essentially, `f(x)` tends to zero when considered over all but a finite number of points. This is a fundamental result in analysis related to the behavior of sum of infinite series. The theorem applies to any function `f` from a type `α` to a topological add group `G`.
More concisely: If a function `f` from a type `α` to a topological add group `G` is unconditionally summable, then `f(x)` converges to zero in the cofinite filter.
|
HasSum.hasSum_compl_iff
theorem HasSum.hasSum_compl_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalAddGroup α] {f : β → α} {a₁ a₂ : α} {s : Set β},
HasSum (f ∘ Subtype.val) a₁ → (HasSum (f ∘ Subtype.val) a₂ ↔ HasSum f (a₁ + a₂))
The theorem `HasSum.hasSum_compl_iff` states that for any types `α` and `β`, where `α` is an additive commutative group and also a topological additive group, and for any function `f` from `β` to `α`, and any `α` values `a₁` and `a₂`, and any set `s` of type `β`, if the composition of `f` and the subtype value function has a sum `a₁`, then the composition of `f` and the subtype value function has a sum `a₂` if and only if the function `f` itself has a sum equal to `a₁ + a₂`. This theorem is about the relationship between the sum of function values over a set and the sum of function values over the complement of the set.
More concisely: For an additive commutative and topological group α, function f from β to α, and any sets s and its complement in β, if the sum of f over s equals a1 and the sum of f over the complement equals a2, then f has a sum equal to a1 + a2.
|
HasSum.neg
theorem HasSum.neg :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalAddGroup α] {f : β → α} {a : α}, HasSum f a → HasSum (fun b => -f b) (-a)
This theorem states that for any two types `α` and `β`, given `α` is an additive commutative group as well as it is a topological space and a topological additive group, if there exists a function `f` from `β` to `α` that has a sum `a`, then the function that negates `f` (i.e., `fun b => -f b`) has a sum of `-a`. Essentially, it says if a certain sum is valid for a function, then the negated sum also holds for the negated function.
More concisely: If `f` is a function from a topological additive group `β` to an additive commutative group `α` with a sum `a`, then the negated function `fun b => -f b` has a sum of `-a`.
|
HasSum.sub
theorem HasSum.sub :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalAddGroup α] {f g : β → α} {a₁ a₂ : α},
HasSum f a₁ → HasSum g a₂ → HasSum (fun b => f b - g b) (a₁ - a₂)
The theorem `HasSum.sub` states that for any two functions `f` and `g` from a type `β` to a type `α`, if `f` has a sum `a₁` and `g` has a sum `a₂` (where `α` is a topological add commutative group), then the function that maps each element of `β` to the difference of the corresponding values of `f` and `g` also has a sum, which is the difference of `a₁` and `a₂`. In mathematical terms, if $\sum f = a₁$ and $\sum g = a₂$, then $\sum (f-g) = a₁ - a₂$.
More concisely: If functions $f$ and $g$ from type $\beta$ to a topological add commutative group $\alpha$ have sums $a\_1$ and $a\_2$ respectively, then their difference $f-g$ has sum $a\_1 - a\_2$.
|
Summable.neg
theorem Summable.neg :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalAddGroup α] {f : β → α}, Summable f → Summable fun b => -f b
The theorem `Summable.neg` states that for any given types `α` and `β`, where `α` is an additive commutative group and topological space that forms a topological additive group, and a function `f` from `β` to `α` is summable (i.e., the series formed by the function `f` converges to a limit in `α`) then the function which maps each element `b` in `β` to the negative of `f(b)` is also summable. In other words, if a series converges, then its negated series also converges.
More concisely: If `f` is a summable function from a topological additive group `β` to an additive commutative group and topological space `α`, then the function mapping each `b` in `β` to the negative of `f(b)` is also summable.
|
Summable.subtype
theorem Summable.subtype :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [inst_2 : UniformAddGroup α]
{f : β → α} [inst_3 : CompleteSpace α], Summable f → ∀ (s : Set β), Summable (f ∘ Subtype.val)
The theorem `Summable.subtype` states that for any types `α` and `β`, and a function `f` from `β` to `α`, where `α` is an additive commutative group, has a uniform space and is a uniform additive group, and also `α` is a complete space, if `f` is summable then for any set `s` of type `β`, the composition of `f` and the `Subtype.val` function (which retrieves the underlying element from a subtype) is also summable. In other words, if a function `f` has an (infinite) sum, then the function which applies `f` to the elements of any subset of its domain also has an (infinite) sum.
More concisely: If `f` is a summable function from a set `β` to an additive commutative and complete group `α`, then the composition of `f` with the `Subtype.val` function is also summable.
|
tendsto_tsum_compl_atTop_zero
theorem tendsto_tsum_compl_atTop_zero :
∀ {α : Type u_1} {G : Type u_5} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G]
[inst_2 : TopologicalAddGroup G] (f : α → G),
Filter.Tendsto (fun s => ∑' (a : { x // x ∉ s }), f ↑a) Filter.atTop (nhds 0)
For any type `α`, any topological add group `G`, and any function `f` from `α` to `G`, the sum over the complement of a `finset` tends to `0` as the `finset` grows to cover the whole space. In other words, as we keep adding elements to the `finset` from the type `α` such that eventually all elements from `α` are included, the sum of the function values over the elements not in the `finset` (complement of the `finset`) gets closer and closer to `0`. This is true regardless of whether the series given by `f` converges, because if the series does not converge the sum over the complement of any `finset` is always `0`. The limit is taken with respect to the filter `atTop`, which represents the limit as we go to infinity, and the neighborhood filter of `0`, both in the topological space of the add group `G`.
More concisely: For any function `f` from a type `α` to a topological add group `G`, the sum of `f` over the complement of any increasing `finset` in `α` approaches 0 with respect to the filters `atTop` and the neighborhood filter of `0` in `G`.
|
Summable.trans_sub
theorem Summable.trans_sub :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalAddGroup α] {f g : β → α}, Summable g → (Summable fun b => f b - g b) → Summable f
The theorem `Summable.trans_sub` states that for any two functions `f` and `g` from a type `β` to a type `α`, where `α` is an additive commutative group with a topology that makes it a topological additive group, if the function `g` is summable and the function obtained by subtracting `g` from `f` is also summable, then the function `f` is summable. Here, a function is said to be summable if it has some (possibly infinite) sum. This theorem thus provides a condition under which we can be sure that a given function is summable.
More concisely: If `g` is summable and `f = g + h` for some summable function `h`, then `f` is summable.
|
tsum_eq_add_tsum_ite
theorem tsum_eq_add_tsum_ite :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalAddGroup α] {f : β → α} [inst_3 : T2Space α] [inst_4 : DecidableEq β],
Summable f → ∀ (b : β), ∑' (n : β), f n = f b + ∑' (n : β), if n = b then 0 else f n
The theorem `tsum_eq_add_tsum_ite` states that for any given summable function `f` mapping from type `β` to `α` (where `α` forms an additive commutative group and topological space, also `α` is a `T2Space` and `β` has decidable equality), and for any element `b` of `β`, the total sum of `f` over all `β` can be expressed as the sum of `f(b)` and the sum of `f` over all other elements of `β`. More specifically, we can break the total sum into two parts: the value of the function at a particular point, and the sum of the function at all other points, with the value at the chosen point replaced by zero in the second sum.
More concisely: For any summable function from a decidably equalible type to an additive commutative group and T2 space, the total sum is equal to the sum of the function value at a point and the sum of the function value at all other points with that point replaced by zero.
|
summable_iff_cauchySeq_finset
theorem summable_iff_cauchySeq_finset :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [inst_2 : CompleteSpace α]
{f : β → α}, Summable f ↔ CauchySeq fun s => s.sum fun b => f b
This theorem is known as the Cauchy criterion for infinite sums, or the Cauchy convergence test. It states that for any function `f` from type `β` to `α`, where `α` is a type with an addition operation and a uniform space structure, and `β` is any type, `f` is summable (meaning that the infinite sum of `f` exists and is finite) if and only if the function that maps each finite set `s` of elements of type `β` to the sum of `f(b)` for `b` in `s` is a Cauchy sequence. Here, a Cauchy sequence is a sequence where the difference between later terms gets arbitrarily small as the sequence progresses. This theorem is fundamental in the study of series and convergence in analysis.
More concisely: A function from a type to a type with an addition operation and a uniform space structure is summable if and only if the sequence of finite sums of its values forms a Cauchy sequence.
|
cauchySeq_finset_iff_tsum_vanishing
theorem cauchySeq_finset_iff_tsum_vanishing :
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [inst_2 : UniformAddGroup α]
{f : β → α},
(CauchySeq fun s => s.sum fun b => f b) ↔
∀ e ∈ nhds 0, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∑' (b : ↑t), f ↑b ∈ e
This theorem states that for any types `α` and `β`, with `α` being an additive commutative group equipped with a uniform space and being a uniform additive group, and `f` being a function from `β` to `α`, a sequence is a Cauchy sequence if and only if for every set `e` in the neighborhood of 0, there exists a finite set `s` such that for any set `t` of `β` that is disjoint from `s`, the infinite sum of the function `f` over `t` is an element of `e`. This essentially describes the conditions under which the sum of the elements of a sequence converges to a limit as the sequence becomes infinitely large.
More concisely: A sequence in an additive commutative group equipped with a uniform structure converges to a limit if and only if for every neighborhood of zero, there exists a finite set such that the sum of the function values of any disjoint finite subset is in the neighborhood.
|
Summable.comp_injective
theorem Summable.comp_injective :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommGroup α] [inst_1 : UniformSpace α]
[inst_2 : UniformAddGroup α] {f : β → α} [inst_3 : CompleteSpace α] {i : γ → β},
Summable f → Function.Injective i → Summable (f ∘ i)
The theorem `Summable.comp_injective` states that for any three types `α`, `β`, and `γ`, where `α` is an additive commutative group, a uniform space, a uniform additive group, and a complete space, if there is a function `f` from `β` to `α` which is summable, and another function `i` from `γ` to `β` which is injective, then the composition function `f ∘ i` (i.e., `f(i(x))` for all `x` in `γ`) is also summable. This means that if you have an infinite series that sums to a value and you apply an injective function to the indices of this series, the resulting series is also summable.
More concisely: If `f` is a summable function from an injective `i : γ → β` to an additive commutative group `α`, then the composition `f ∘ i` is also summable.
|