Summable.of_norm_bounded_eventually_nat
theorem Summable.of_norm_bounded_eventually_nat :
∀ {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : CompleteSpace E] {f : ℕ → E} (g : ℕ → ℝ),
Summable g → (∀ᶠ (i : ℕ) in Filter.atTop, ‖f i‖ ≤ g i) → Summable f
The theorem `Summable.of_norm_bounded_eventually_nat` states that for any sequence of elements `f` from a seminormed additive commutative group that is complete, if there exists a sequence of real numbers `g` that is summable and the absolute value (or norm) of the elements of `f` is eventually (as we go towards infinity) bounded by corresponding elements of `g`, then the sequence `f` is also summable. This is a variant of the direct comparison test for series in mathematical analysis.
More concisely: If `f` is a sequence of elements in a complete, seminormed additive commutative group, and there exists a summable sequence `g` of real numbers such that |`f(n)`| is eventually bounded by `g(n)`, then `f` is summable.
|
tsum_of_norm_bounded
theorem tsum_of_norm_bounded :
∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E} {g : ι → ℝ} {a : ℝ},
HasSum g a → (∀ (i : ι), ‖f i‖ ≤ g i) → ‖∑' (i : ι), f i‖ ≤ a
This theorem, `tsum_of_norm_bounded`, states that for any type `ι` and seminormed additive commutative group `E`, given functions `f : ι → E` and `g : ι → ℝ` and a real number `a`, if the series of `g` sums to `a` (i.e., `HasSum g a`) and for all `i` the norm of `f i` is less than or equal to `g i` then the norm of the series sum of `f`, `‖∑' (i : ι), f i‖`, is less than or equal to `a`. Note that it's not necessary for the series sum of `f` to be summable, and it might not be the case if `α` is not a complete space. This theorem is a quantitative result associated with the direct comparison test for series in real analysis.
More concisely: For any seminormed additive commutative group `E`, if functions `f : ι → E` and `g : ι → ℝ` satisfy `HasSum g a` and `‖f i‖ ≤ g i` for all `i`, then `‖∑' i, f i‖ ≤ a`.
|
Summable.of_norm_bounded_eventually
theorem Summable.of_norm_bounded_eventually :
∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : CompleteSpace E] {f : ι → E}
(g : ι → ℝ), Summable g → (∀ᶠ (i : ι) in Filter.cofinite, ‖f i‖ ≤ g i) → Summable f
This theorem, referred to as a variant of the direct comparison test for series, states that for any types `ι` and `E`, with `E` being a semi-normed additive commutative group and a complete space, and any functions `f : ι → E` and `g : ι → ℝ`, if `g` is summable and the norm of `f` at any point `i` is eventually bounded by `g` at `i` for almost all `i` (specifically, for all `i` outside a finite set), then `f` is also summable. In mathematical terms, we say that if $(g_i)_{i\in\mathbb{N}}$ is a summable sequence of real numbers and the norm $\|f_i\|$ of the elements of another sequence $(f_i)_{i\in\mathbb{N}}$ is bounded above by the corresponding $g_i$ for all but finitely many $i$, then $(f_i)_{i\in\mathbb{N}}$ is a summable sequence as well.
More concisely: If `g : ι -> ℝ` is summable and the norm of `f : ι -> E` is bounded by `g` at almost all points `i` in the type `ι`, where `E` is a semi-normed additive commutative group and complete space, then `f` is also summable.
|
Summable.of_norm
theorem Summable.of_norm :
∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : CompleteSpace E] {f : ι → E},
(Summable fun a => ‖f a‖) → Summable f
The theorem `Summable.of_norm` asserts that for any type `ι`, any seminormed additively commutative group `E` that is also a complete space, and any function `f` mapping elements of `ι` to `E`, if the norm of `f` for each element in its domain is summable, then the function `f` itself is summable. In other words, if the series of norms of `f` converges, then the series created by `f` also converges.
More concisely: If `ι` is a type, `E` is a complete, additively commutative seminormed group, and `f : ι → E` is a function such that the series of its norms is summable, then the series represented by `f` is also summable.
|
Summable.of_norm_bounded
theorem Summable.of_norm_bounded :
∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : CompleteSpace E] {f : ι → E}
(g : ι → ℝ), Summable g → (∀ (i : ι), ‖f i‖ ≤ g i) → Summable f
This theorem, often referred to as the "direct comparison test for series", asserts that if the norm of a function `f` is bounded by a real-valued function `g` that is summable, then `f` is also summable. Here, `f` is a function from an arbitrary type `ι` to a seminormed add commutative group `E` (which also forms a complete space), and `g` is a function from `ι` to real numbers. The function `f` is said to be summable if there exists some sum, even if it be an infinite one, for the series formed by `f`. This theorem thus provides a convenient criterion to ascertain the summability of a series in terms of another one known to be summable.
More concisely: If a function `f` from an index type `ι` to a seminormed add commutative group `E` (a complete space) is pointwise dominated by a summable real-valued function `g`, then `f` is also summable.
|
cauchySeq_finset_of_norm_bounded
theorem cauchySeq_finset_of_norm_bounded :
∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E} (g : ι → ℝ),
Summable g → (∀ (i : ι), ‖f i‖ ≤ g i) → CauchySeq fun s => s.sum fun i => f i
This theorem states that for any types `ι` and `E`, where `E` is a semi-normed additive commutative group, and any two functions `f : ι → E` and `g : ι → ℝ`, if `g` is summable and the norm of `f i` is less than or equal to `g i` for every `i` in `ι`, then the sequence of finite sums of `f` over any given set `s` is a Cauchy sequence. In other words, if we have a sequence of vectors (represented by the function `f`) such that their norms are bounded by a summable sequence (represented by the function `g`), the sequence of partial sums of these vectors is Cauchy, which implies it converges in the limit.
More concisely: If `ι` is any index type, `E` is a semi-normed additive commutative group, `f : ι → E`, and `g : ι → ℝ` is summable with `||f i|| ≤ g i` for all `i`, then the sequence of finite sums of `f` over any set `s` is a Cauchy sequence.
|
cauchySeq_range_of_norm_bounded
theorem cauchySeq_range_of_norm_bounded :
∀ {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ℕ → E} (g : ℕ → ℝ),
(CauchySeq fun n => (Finset.range n).sum fun i => g i) →
(∀ (i : ℕ), ‖f i‖ ≤ g i) → CauchySeq fun n => (Finset.range n).sum fun i => f i
This is a version of the direct comparison test for conditionally convergent series, specifically applied to Cauchy sequences. The theorem states that for any type `E` that forms a seminormed add commutative group, given a sequence `f` of elements of `E` and a sequence `g` of real numbers, if the series of `g` forms a Cauchy sequence when summed over the range up to `n`, and if the norm of each `f(i)` is less than or equal to `g(i)` for every natural number `i`, then the series of `f` also forms a Cauchy sequence when summed over the range up to `n`. This theorem is a companion to a similar one for absolutely convergent series, `cauchySeq_finset_of_norm_bounded`.
More concisely: If `(g : Sequence real) is a Cauchy sequence and for all `n`, `||f(n)|| ≤ g(n)` in a seminormed add commutative group `E`, then `(f : Sequence E)` is a Cauchy sequence.
|
norm_tsum_le_tsum_norm
theorem norm_tsum_le_tsum_norm :
∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E},
(Summable fun i => ‖f i‖) → ‖∑' (i : ι), f i‖ ≤ ∑' (i : ι), ‖f i‖
The theorem `norm_tsum_le_tsum_norm` states that for any seminormed additively commutative group `E` and any function `f` from some type `ι` to `E`, if the series of the norms of `f(i)` is summable, then the norm of the series of `f(i)` is less than or equal to the sum of the series of the norms of `f(i)`. Note that the theorem does not assume that the series of `f(i)` itself is summable, and this may not be the case if `E` is not a complete space. This theorem can be written in mathematical notation as: For all `i` in `ι`, if `∑' i, ‖f i‖` is summable, then `‖∑' i, f i‖ ≤ ∑' i, ‖f i‖`.
More concisely: For any seminormed additively commutative group `E` and function `f` from some type `ι` to `E`, if the series of norms of `f(i)` is summable, then the norm of the sum of `f(i)` is less than or equal to the sum of the series of their norms.
|
hasSum_of_subseq_of_summable
theorem hasSum_of_subseq_of_summable :
∀ {ι : Type u_1} {α : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E},
(Summable fun a => ‖f a‖) →
∀ {s : α → Finset ι} {p : Filter α} [inst_1 : p.NeBot],
Filter.Tendsto s p Filter.atTop →
∀ {a : E}, Filter.Tendsto (fun b => (s b).sum fun i => f i) p (nhds a) → HasSum f a
This theorem states that if a function `f` from an arbitrary type ι to a seminormed additive commutative group E is such that the norm of `f` is summable, and if for some sequence of finite subsets of ι (that exhausts the entire space) the sum of `f` over these subsets converges to a limit `a`, then this property holds for all finite subsets of ι, i.e., `f` is summable with sum `a`. In other words, if the sum of `f` over a certain sequence of finite subsets is approaching a limit under some filter `p`, and these subsets are growing to encompass the entire space under the same filter, then `f` has a sum `a` over the whole space.
More concisely: If a function from an arbitrary type to a seminormed additive commutative group is norm-summable and the sum over any exhausting sequence of finite subsets converges, then the function is summable with sum equal to the limit of the sum over the exhausting sequence.
|
nnnorm_tsum_le
theorem nnnorm_tsum_le :
∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E},
(Summable fun i => ‖f i‖₊) → ‖∑' (i : ι), f i‖₊ ≤ ∑' (i : ι), ‖f i‖₊
The theorem `nnnorm_tsum_le` states that for any type ι and any semi-normed additive commutative group E, if the series of the semi-norms of the elements of a sequence `f` (from ι to E) is summable, then the semi-norm of the series of the sequence `f` is less than or equal to the sum of the series of the semi-norms of the elements of `f`. Note that the summability of the series of `f` is not assumed and might not hold if `E` is not a complete space.
More concisely: If `(ι, ±||.||)` is a semi-normed additive commutative group, and the series `∑ i in ι ||f i||` is summable, then `||∑ i in ι f i|| ≤ ∑ i in ι ||f i||`.
|
tsum_of_nnnorm_bounded
theorem tsum_of_nnnorm_bounded :
∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E} {g : ι → NNReal} {a : NNReal},
HasSum g a → (∀ (i : ι), ‖f i‖₊ ≤ g i) → ‖∑' (i : ι), f i‖₊ ≤ a
The theorem `tsum_of_nnnorm_bounded` states the following:
Consider a sequence of terms `f : ι → E` in a semi-normed additive commutative group `E` and a sequence of nonnegative real numbers `g : ι → NNReal`. If the series formed by `g` is summable with sum `a` and if for every term in the sequence, the nonnegative norm of `f i` is less than or equal to `g i`, then the nonnegative norm of the sum of the series formed by `f` is less than or equal to `a`. It should be noted that we make no assumption about the summability of the series formed by `f`, and it may not be summable if `E` is not a complete space.
More concisely: If `g : ι -> NNReal` is a summable sequence of nonnegative real numbers with sum `a`, and `f : ι -> E` is a sequence of terms in a semi-normed additive commutative group `E` such that the nonnegative norm of each `f i` is less than or equal to `g i`, then the nonnegative norm of the sum of the `f i` is less than or equal to `a`.
|