summable_imp_tendsto_of_complete — Mathlib

English

A dual formulation: if the normed group is complete, then every summable norm sequence yields a convergent partial sums limit.

Русский

Двойственная формулировка: полнота означат, что любая суммируемая по норме последовательность порождает сходящуюся частичную сумму.

LaTeX

$$$\text{CompleteSpace}(E) \Rightarrow (\forall u:\mathbb{N}\to E,\ Summable(\|u\|) \Rightarrow \exists a,\ Tendsto(n \mapsto \sum_{i< n} u(i)) atTop (\mathcal{N}(a)))$$$

Lean4

/-- In a complete normed additive group, every absolutely convergent series converges in the
space. -/
theorem summable_imp_tendsto_of_complete [CompleteSpace E] (u : ℕ → E) (hu : Summable (‖u ·‖)) :
    ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a) :=
  by
  refine cauchySeq_tendsto_of_complete <| cauchySeq_of_summable_dist ?_
  simp [dist_eq_norm, sum_range_succ, hu]

Похожие утверждения