summable_of_absolute_convergence_real

English

If there exists a real r such that the partial sums of |f| converge to r, then f is summable.

Русский

Если частичные суммы по модулю функции сходятся к пределу r, то функция суммируема.

LaTeX

$$$\\exists r\\,\\text{ Tendsto }\\left(n \\mapsto \\sum_{i=0}^{n} |f(i)|\\right)\\!\\!\\!\\!_{\\text{atTop}}\\mathcal{N}(r) \\Rightarrow \\text{Summable } f.$$$

Lean4

theorem summable_of_absolute_convergence_real {f : ℕ → ℝ} :
    (∃ r, Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)) → Summable f
  | ⟨r, hr⟩ => by
    refine .of_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg ?_ _).2 ?_⟩
    · exact fun i ↦ norm_nonneg _
    · simpa only using hr

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