summable_iff_vanishing_norm — Mathlib

English

The sequence f is summable if and only if tails of sums over disjoint finite sets vanish in norm for every ε>0.

Русский

Последовательность f суммируема тогда и только тогда, когда хвостовые суммы по дисjointным конечным множествам сходятся к нулю в норме для любого ε>0.

LaTeX

$$$\\text{Summable } f \\iff \\forall \\varepsilon>0,\\ \\exists S: Finset\\ ι,\\forall T,\\ Disjoint(T,S)\\Rightarrow \\Bigl\\|\\sum_{i\\in T} f(i)\\Bigr| < \\varepsilon$$$

Lean4

theorem summable_iff_vanishing_norm [CompleteSpace E] {f : ι → E} :
    Summable f ↔ ∀ ε > (0 : ℝ), ∃ s : Finset ι, ∀ t, Disjoint t s → ‖∑ i ∈ t, f i‖ < ε := by
  rw [summable_iff_cauchySeq_finset, cauchySeq_finset_iff_vanishing_norm]

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