cauchySeq_finset_of_summable_norm

English

If the norm of f is summable and a subsequence of finite-sums converges to a along some filter, then the full sum HasSum f a.

Русский

Если норма f образует суммируемую последовательность и подпоследовательность частичных сумм сходится к a, то сумма f существует и равна a.

LaTeX

$$$\\text{Summable } \\|f\\| \\Rightarrow \\forall \\text{ s},\\ \\text{Tendsto } s p \\text{ atTop} \\rightarrow \\text{HasSum } f a$$$

Lean4

theorem cauchySeq_finset_of_summable_norm {f : ι → E} (hf : Summable fun a => ‖f a‖) :
    CauchySeq fun s : Finset ι => ∑ a ∈ s, f a :=
  cauchySeq_finset_of_norm_bounded hf fun _i => le_rfl

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