NormedAddCommGroup.summable_imp_tendsto_iff_completeSpace
theorem NormedAddCommGroup.summable_imp_tendsto_iff_completeSpace :
∀ {E : Type u_1} [inst : NormedAddCommGroup E],
(∀ (u : ℕ → E),
(Summable fun x => ‖u x‖) →
∃ a, Filter.Tendsto (fun n => (Finset.range n).sum fun i => u i) Filter.atTop (nhds a)) ↔
CompleteSpace E
This theorem states that in a normed additive group, every absolutely convergent series converges within the space if and only if the space is complete. More specifically, for any sequence `u` of elements in the normed additive group `E`, if the series formed by taking the norm of each element of `u` is summable, then there exists a value `a` such that the partial sums of the sequence `u` tend to `a` as the number of terms goes to infinity, if and only if `E` is a complete space. A complete space is one in which every Cauchy sequence converges to a limit within the space. In other words, the space has no "holes".
More concisely: In a normed additive group, a series of elements is absolutely convergent to a limit within the group if and only if the group is complete.
|
NormedAddCommGroup.completeSpace_of_summable_imp_tendsto
theorem NormedAddCommGroup.completeSpace_of_summable_imp_tendsto :
∀ {E : Type u_1} [inst : NormedAddCommGroup E],
(∀ (u : ℕ → E),
(Summable fun x => ‖u x‖) →
∃ a, Filter.Tendsto (fun n => (Finset.range n).sum fun i => u i) Filter.atTop (nhds a)) →
CompleteSpace E
The theorem states that for any type `E` that forms a normed additive group, if for any series of elements in `E` (represented by `u : ℕ → E`), the series that calculates the norm of each element is summable, then there exists a limit `a` such that the partial sums of the series (represented by `(Finset.range n).sum fun i => u i`) tend towards `a` as `n` tends towards infinity. If this condition is satisfied for all such series, then `E` is said to be a complete space. In more mathematical terms, a normed additive group is complete if any absolutely convergent series converges in the space.
More concisely: A normed additive group `E` is complete if every absolutely convergent series of elements in `E` converges to a limit in `E`.
|
NormedAddCommGroup.summable_imp_tendsto_of_complete
theorem NormedAddCommGroup.summable_imp_tendsto_of_complete :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : CompleteSpace E] (u : ℕ → E),
(Summable fun x => ‖u x‖) →
∃ a, Filter.Tendsto (fun n => (Finset.range n).sum fun i => u i) Filter.atTop (nhds a)
This theorem states that, in the context of a complete normed additive group, if a series of elements (denoted by `u : ℕ → E`) is absolutely convergent (i.e., the series of the norms `‖u x‖` is summable), then the series `u` itself converges in this space. More precisely, there exists an element `a` in the group such that the partial sums of the series `u`, when `n` tends to infinity (represented by `Filter.atTop`), tend to `a` in the neighborhood filter at `a` (given by `nhds a`). The convergence of the partial sums is what we mean by the convergence of the series. The completeness of the space is crucial for this result.
More concisely: In a complete normed additive group, the convergence of the series of norms implies the convergence of the original series.
|