English
If every absolutely convergent series in a normed additive group E converges, then E is a complete space.
Русский
Если каждая абсолютно сходящаяся по норме серия в нормированной аддитивной группе E сходится, то E полно.
LaTeX
$$$\big( \forall u:\mathbb{N}\to E,\ Summable(\|u\|) \Rightarrow \exists a,\ Tendsto\bigl(n \mapsto \sum_{i< n} u(i)\bigr)\ atTop (\mathcal{N}(a)) \big) \Rightarrow \text{CompleteSpace}(E)$$$
Lean4
/-- A normed additive group is complete if any absolutely convergent series converges in the
space. -/
theorem completeSpace_of_summable_imp_tendsto
(h : ∀ u : ℕ → E, Summable (‖u ·‖) → ∃ a, Tendsto (fun n => ∑ i ∈ range n, u i) atTop (𝓝 a)) : CompleteSpace E :=
by
apply Metric.complete_of_cauchySeq_tendsto
intro u hu
obtain ⟨f, hf₁, hf₂⟩ := Metric.exists_subseq_summable_dist_of_cauchySeq u hu
simp only [dist_eq_norm] at hf₂
let v n := u (f (n + 1)) - u (f n)
have hv_sum : (fun n => (∑ i ∈ range n, v i)) = fun n => u (f n) - u (f 0) :=
by
ext n
exact sum_range_sub (u ∘ f) n
obtain ⟨a, ha⟩ := h v hf₂
refine ⟨a + u (f 0), ?_⟩
refine tendsto_nhds_of_cauchySeq_of_subseq hu hf₁.tendsto_atTop ?_
rw [hv_sum] at ha
have h₁ : Tendsto (fun n => u (f n) - u (f 0) + u (f 0)) atTop (𝓝 (a + u (f 0))) := Tendsto.add_const _ ha
simpa only [sub_add_cancel] using h₁
