Summable.of_abs
theorem Summable.of_abs :
∀ {ι : Type u_1} {α : Type u_3} [inst : LinearOrderedAddCommGroup α] [inst_1 : UniformSpace α]
[inst_2 : UniformAddGroup α] [inst_3 : CompleteSpace α] {f : ι → α}, (Summable fun x => |f x|) → Summable f
The theorem `Summable.of_abs` states that for any types `ι` and `α`, given the conditions that `α` forms a linearly ordered additive commutative group, `α` is a uniform space, `α` is an uniform additive group, and `α` is a complete space, if a function `f` from `ι` to `α` is such that the absolute values `|f x|` are summable (i.e., the series of `|f x|` converges to a sum), then the function `f` itself is summable (the series of `f x` converges).
More concisely: If `f: ι → α` is a function from a index type `ι` to a linearly ordered, additive commutative, complete uniform group `α`, where the absolute values `|f x|` are summable, then `f` itself is summable.
|
Summable.abs
theorem Summable.abs :
∀ {ι : Type u_1} {α : Type u_3} [inst : LinearOrderedAddCommGroup α] [inst_1 : UniformSpace α]
[inst_2 : UniformAddGroup α] [inst_3 : CompleteSpace α] {f : ι → α}, Summable f → Summable fun x => |f x|
The theorem `Summable.abs` states that for any type `ι` and any type `α` that is a linearly ordered additive commutative group, a uniform space, a uniform additive group and a complete space, if a function `f` from `ι` to `α` is summable (i.e., it has an infinite sum), then the function that maps each `x` in `ι` to the absolute value of `f(x)` is also summable. In other words, if a function has a sum, then the function that takes the absolute values of the original function's values also has a sum.
More concisely: If `f` is a summable function from a linearly ordered, additive commutative group `ι` to a uniform additive group and complete space `α`, then the function `x ↦ |f x|` is also summable.
|
tsum_nonneg
theorem tsum_nonneg :
∀ {ι : Type u_1} {α : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderClosedTopology α] {g : ι → α}, (∀ (i : ι), 0 ≤ g i) → 0 ≤ ∑' (i : ι), g i
The theorem `tsum_nonneg` states that for any type `ι` and any type `α` that is an ordered additive commutative monoid (a structure with a concept of order and an operation of addition that is commutative) and also a topological space (a mathematical structure that allows for the definition of concepts like continuity and convergence), and with a topology that is closed with respect to the order, if we have a function `g` from `ι` to `α` such that all values of `g` are nonnegative (i.e., greater than or equal to zero), then the series sum of `g` over all `ι` is also nonnegative. In simpler terms, the sum of all nonnegative values in a series is also nonnegative.
More concisely: For any ordered additive commutative monoid and topology where the order is closed, if every element of a function from the index set to the monoid is nonnegative, then the series sum of the function is nonnegative.
|
sum_le_hasSum
theorem sum_le_hasSum :
∀ {ι : Type u_1} {α : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderClosedTopology α] {f : ι → α} {a : α} (s : Finset ι),
(∀ i ∉ s, 0 ≤ f i) → HasSum f a → (s.sum fun i => f i) ≤ a
The theorem `sum_le_hasSum` states that for any types `ι` and `α`, where `α` forms an ordered additive commutative monoid and has a topology such that its order topology is closed, and for any function `f` mapping `ι` to `α` and any element `a` of `α`, given a finite set `s` of `ι`, if for every element `i` not in `s`, `f(i)` is non-negative, and the series formed by `f` has a sum `a`, then the sum of `f(i)` for `i` in `s` is less than or equal to `a`. In mathematical terms, this states that if $\sum_{i \in \mathbb{N}} f(i)$ converges to a limit `a`, then the partial sum over any finite subset is always less than or equal to `a`, assuming non-negativity for terms outside the subset.
More concisely: For any function from a countable set to an ordered additive commutative monoid with a closed order topology, if the function's series has a sum and all terms outside a finite subset are non-negative, then the sum of terms in the finite subset is less than or equal to the series' sum.
|
tsum_le_tsum_of_inj
theorem tsum_le_tsum_of_inj :
∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderClosedTopology α] {f : ι → α} {g : κ → α} (e : ι → κ),
Function.Injective e →
(∀ c ∉ Set.range e, 0 ≤ g c) → (∀ (i : ι), f i ≤ g (e i)) → Summable f → Summable g → tsum f ≤ tsum g
This theorem states that for any types `ι`, `κ`, and `α`, where `α` has an ordered addition and a topology such that the order is closed, and given functions `f : ι → α` and `g : κ → α`, and an injective function `e : ι → κ`, if every element not in the range of `e` maps to a non-negative value under `g`, and each element in `ι` maps to a value in `α` under `f` that is less than or equal to the value mapped from the corresponding element under `g`, and if both `f` and `g` are summable, then the total sum of `f` is less than or equal to the total sum of `g`. In terms of mathematical notation, this can be written as: if $f : ι → α$ and $g : κ → α$ are functions, $e : ι → κ$ is an injective function, and $\forall c \notin range(e), 0 \leq g(c)$ and $\forall i \in ι, f(i) \leq g(e(i))$, and the series $\sum f$ and $\sum g$ are both convergent, then $\sum f \leq \sum g$.
More concisely: If `ι` and `κ` are types with ordered additions and topologies where the order is closed, `f : ι → α`, `g : κ → α`, `e : ι → κ` is an injective function, `e("i") <-∞` for all `i ∈ ι`, `g(c) ≥ 0` for all `c ∉ range(e)`, and both `f` and `g` have convergent sums, then `∑(i ∈ ι) f(i) ≤ ∑(j ∈ κ) g(j)`.
|
HasSum.nonneg
theorem HasSum.nonneg :
∀ {ι : Type u_1} {α : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderClosedTopology α] {g : ι → α} {a : α}, (∀ (i : ι), 0 ≤ g i) → HasSum g a → 0 ≤ a
This theorem states that for any types `ι` and `α`, where `α` is an ordered additive commutative monoid and also a topological space with an order-closed topology, given a function `g` from `ι` to `α` and an element `a` of type `α`, if all values of the function `g` are non-negative, and if the function `g` has a sum `a`, then `a` is also non-negative. In simpler terms, it means that if we sum up a bunch of non-negative values (according to the function `g`), the result can't be negative.
More concisely: For any ordered additive commutative monoid and topological space `α`, if `g : ι → α` is a function with non-negative values and has sum `a` in `α`, then `a` is non-negative.
|
le_tsum
theorem le_tsum :
∀ {ι : Type u_1} {α : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderClosedTopology α] {f : ι → α},
Summable f → ∀ (i : ι), (∀ (j : ι), j ≠ i → 0 ≤ f j) → f i ≤ ∑' (i : ι), f i
The theorem `le_tsum` states that for any given types `ι` and `α`, where `α` is an ordered additive commutative monoid with a topological space structure and its order is closed, and given a function `f` from `ι` to `α`, if `f` is summable, then for any element `i` in `ι`, if for all `j` in `ι` where `j` is not equal to `i`, `f j` is nonnegative, then the value of `f i` is less than or equal to the infinite sum of the values of `f`. In other words, any individual term in an infinite summation of nonnegative terms is less than or equal to the entire sum.
More concisely: If `f` is a summable function from a type `ι` to an ordered additive commutative monoid `α` with a topological space structure and closed order, then for any `i` in `ι` where `f` is nonnegative at all other indices, we have `f i ≤ ∑ j ∈ ι f j`.
|
sum_le_tsum
theorem sum_le_tsum :
∀ {ι : Type u_1} {α : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderClosedTopology α] {f : ι → α} (s : Finset ι),
(∀ i ∉ s, 0 ≤ f i) → Summable f → (s.sum fun i => f i) ≤ ∑' (i : ι), f i
This theorem states that for any type `ι`, any ordered additive commutative monoid `α` with a topological space structure and an order-closed topology, any function `f` from `ι` to `α`, and any finite set `s` of `ι`, if every element `i` not in `s` maps to a non-negative value under `f`, and if `f` is summable (i.e., the infinite sum of `f` over all elements of `ι` exists), then the finite sum of `f` over the elements in `s` is less than or equal to the infinite sum of `f` over all elements of `ι`. In mathematical notation, this can be written as: if `$\forall i \notin s, 0 \leq f(i)$` and the sum `$\sum_{i\in \ι} f(i)$` exists, then `$\sum_{i\in s} f(i) \leq \sum_{i\in \ι} f(i)$`.
More concisely: Given an ordered additive commutative monoid `α` with a topological space structure and an order-closed topology, for any type `ι`, function `f` from `ι` to `α`, and finite set `s` of `ι`, if every `i` not in `s` maps to a non-negative value under `f` and the infinite sum of `f` over all elements of `ι` exists, then the finite sum of `f` over the elements in `s` is less than or equal to the infinite sum of `f` over all elements of `ι`. In other words, if `$\forall i \notin s, 0 \leq f(i)$` and `$\sum_{i\in \ι} f(i)$` exists, then `$\sum_{i\in s} f(i) \leq \sum_{i\in \ι} f(i)$`.
|
tsum_le_of_sum_le
theorem tsum_le_of_sum_le :
∀ {ι : Type u_1} {α : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderClosedTopology α] {f : ι → α} {a₂ : α},
Summable f → (∀ (s : Finset ι), (s.sum fun i => f i) ≤ a₂) → ∑' (i : ι), f i ≤ a₂
The theorem `tsum_le_of_sum_le` states that for any types `ι` and `α`, given an instance of `OrderedAddCommMonoid α`, `TopologicalSpace α` and `OrderClosedTopology α`, a function `f` from `ι` to `α`, and a value `a₂` of type `α`, if `f` is summable and for all finite sets `s` of `ι`, the sum of `f i` for `i` in `s` is less than or equal to `a₂`, then the infinite sum of `f i` for `i` in `ι` is also less than or equal to `a₂`. In mathematical terms, if we have a function `f: ι → α` such that for any finite subset `s` of `ι`, the sum of `f(i)` over `i` in `s` is less than or equal to `a₂`, and the infinite sum of `f(i)` over all `i` in `ι` exists, then this infinite sum is less than or equal to `a₂`.
More concisely: If `f: ι → α` is a summable function over an ordered additive commutative monoid `α` in a topological space with an order-closed topology, and the sum of `f i` for all finite sets `s` of `ι` is bounded above by a constant `a₂`, then the infinite sum of `f i` is also less than or equal to `a₂`.
|
le_hasSum
theorem le_hasSum :
∀ {ι : Type u_1} {α : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderClosedTopology α] {f : ι → α} {a : α},
HasSum f a → ∀ (i : ι), (∀ (j : ι), j ≠ i → 0 ≤ f j) → f i ≤ a
This theorem states that for any type `ι` and `α`, where `α` is a ordered additive commutative monoid with a topology such that it is an order-closed topology, and for any function `f` from `ι` to `α` and any `α` value `a`, if `f` sums to `a`, then for any element `i` of `ι`, if all other elements `j` of `ι` maps to non-negative value by `f`, then the value of `f` at `i` is less than or equal to `a`. In simple words, it says if a function's sum is a certain value, any individual term in that sum is less than or equal to the sum itself given that all other terms are non-negative.
More concisely: If `f : ι → α` is a function from a type `ι` to an ordered additive commutative monoid `α` with an order-closed topology, such that the sum of `f` is `a` and for all `j ≠ i` in `ι`, `f j ≤ a`, then `f i ≤ a`.
|
tsum_lt_tsum
theorem tsum_lt_tsum :
∀ {ι : Type u_1} {α : Type u_3} [inst : OrderedAddCommGroup α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalAddGroup α] [inst_3 : OrderClosedTopology α] {f g : ι → α} {i : ι},
f ≤ g → f i < g i → Summable f → Summable g → ∑' (n : ι), f n < ∑' (n : ι), g n
The theorem `tsum_lt_tsum` states that for any types `ι` and `α`, where `α` is an ordered additive commutative group, a topological space, a topological additive group, and has an order-closed topology, if you have two functions `f` and `g` from `ι` to `α` and an element `i` of `ι`, then if `f` is pointwise less than or equal to `g`, `f i` is strictly less than `g i`, and both `f` and `g` are summable (i.e., their infinite sums exist), then the total sum of `f` over all `ι` is strictly less than the total sum of `g` over all `ι`. In other words, it guarantees that when a function is pointwise smaller, its infinite sum will also be smaller.
More concisely: If `ι` is a type, `α` is an ordered additive commutative group with an order-closed topology, `f` and `g` are functions from `ι` to `α` that are pointwise less than or equal, summable, and `f i` is strictly less than `g i` for all `i` in `ι`, then the sum of `f` over `ι` is strictly less than the sum of `g` over `ι`.
|
tsum_le_tsum
theorem tsum_le_tsum :
∀ {ι : Type u_1} {α : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderClosedTopology α] {f g : ι → α},
(∀ (i : ι), f i ≤ g i) → Summable f → Summable g → ∑' (i : ι), f i ≤ ∑' (i : ι), g i
The theorem `tsum_le_tsum` states that for any two functions `f` and `g` from a type `ι` to a type `α`, where `α` is an ordered additive commutative monoid and a topological space with an order-closed topology, if each value of `f` is less than or equal to the corresponding value of `g`, and both `f` and `g` are summable (i.e., each has an infinite sum), then the total sum of `f` is less than or equal to the total sum of `g`. Mathematically, this can be expressed as: if `∀ i : ι, f(i) ≤ g(i)`, `f` and `g` are summable, then `∑' f(i) ≤ ∑' g(i)`.
More concisely: If `f` and `g` are functions from a type `ι` to an ordered additive commutative monoid and topological space with order-closed topology, and `f(i) ≤ g(i)` for all `i : ι` and both `f` and `g` are summable, then `∑' f(i) ≤ ∑' g(i)`.
|
tsum_eq_zero_iff
theorem tsum_eq_zero_iff :
∀ {ι : Type u_1} {α : Type u_3} [inst : CanonicallyOrderedAddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderClosedTopology α] {f : ι → α}, Summable f → (∑' (i : ι), f i = 0 ↔ ∀ (x : ι), f x = 0)
The theorem `tsum_eq_zero_iff` states that for any types `ι` and `α`, where `α` forms a canonically ordered additive commutative monoid with an associated topological space and the order topology is closed, if a function `f : ι → α` is summable, then the infinite sum of `f` over all `ι` being equal to zero is equivalent to the statement that the function `f` is zero at every element of `ι`. In other words, a summable function's infinite sum is zero if and only if the function is zero everywhere.
More concisely: A summable function from a type `ι` to a canonically ordered, additive commutative monoid `α` with a closed order topology has the property that its infinite sum is zero if and only if the function is identically zero.
|
tsum_le_of_sum_range_le
theorem tsum_le_of_sum_range_le :
∀ {α : Type u_3} [inst : Preorder α] [inst_1 : AddCommMonoid α] [inst_2 : TopologicalSpace α]
[inst_3 : OrderClosedTopology α] [inst_4 : T2Space α] {f : ℕ → α} {c : α},
Summable f → (∀ (n : ℕ), ((Finset.range n).sum fun i => f i) ≤ c) → ∑' (n : ℕ), f n ≤ c
This theorem states that for any function `f` from natural numbers to a type `α` which has a preorder, an addition operation, a topology, an ordering compatible with its topology, and is Hausdorff, if `f` is summable and the sum of `f` for all natural numbers less than any given natural number `n` is less than or equal to a constant `c`, then the infinite series sum of `f` over all natural numbers is also less than or equal to `c`. This essentially shows that if all partial sums of a summable series are bounded by some constant `c`, then the total sum of the series is also bounded by `c`.
More concisely: If `f` is a summable function from natural numbers to a type `α` with a preorder, addition operation, topology, ordering compatible with its topology, and is Hausdorff, such that the sum of `f` for all natural numbers less than any given natural number is bounded by a constant `c`, then the infinite series sum of `f` is also bounded by `c`.
|
hasSum_lt
theorem hasSum_lt :
∀ {ι : Type u_1} {α : Type u_3} [inst : OrderedAddCommGroup α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalAddGroup α] [inst_3 : OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α} {i : ι},
f ≤ g → f i < g i → HasSum f a₁ → HasSum g a₂ → a₁ < a₂
This theorem states that for any types `ι` and `α`, where `α` is an ordered additive commutative group, a topological space, a topological additive group, and has an order-closed topology, if there are two functions `f` and `g` from `ι` to `α`, and two elements `a₁` and `a₂` of `α`, and an element `i` of `ι`, then if `f` is less than or equal to `g` everywhere, and `f` is strictly less than `g` at some point `i`, and if the sum of `f` is `a₁` and the sum of `g` is `a₂`, then `a₁` must be strictly less than `a₂`.
More concisely: If `f` and `g` are functions from a type `ι` to an ordered additive commutative group `α` with order-closed topology, and `f ≤ g` everywhere, `f(i) < g(i)` for some `i`, and the sums of `f` and `g` are `a₁` and `a₂` respectively, then `a₁ < a₂`.
|
hasSum_le
theorem hasSum_le :
∀ {ι : Type u_1} {α : Type u_3} [inst : OrderedAddCommMonoid α] [inst_1 : TopologicalSpace α]
[inst_2 : OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α},
(∀ (i : ι), f i ≤ g i) → HasSum f a₁ → HasSum g a₂ → a₁ ≤ a₂
This theorem states that for any types `ι` and `α`, where `α` is an ordered additive commutative monoid with a topological space structure and its order topology is closed, given two functions `f` and `g` from `ι` to `α` and two elements `a₁` and `a₂` in `α`, if for every `i` in `ι` the value of `f` at `i` is less than or equal to the value of `g` at `i`, and `f` has a sum `a₁` and `g` has a sum `a₂`, then `a₁` is less than or equal to `a₂`. In simpler terms, if each term in the sequence generated by `f` is less than or equal to the corresponding term in the sequence generated by `g`, and the sums of these sequences are `a₁` and `a₂` respectively, then the sum `a₁` is less than or equal to the sum `a₂`.
More concisely: Given functions `f` and `g` from a type `ι` to an ordered additive commutative monoid `α` with a closed order topology, if for all `i` in `ι`, `f i ≤ gi` and `Σ i, fi = a₁` and `Σ i, gi = a₂`, then `a₁ ≤ a₂`.
|