hasSum_iff_tendsto_nat_of_summable_norm

English

If the norms are summable, then HasSum f a is equivalent to the partial sums ∑_{i< n} f(i) tending to a as n→∞.

Русский

Если нормы суммируемы, то HasSum f a эквивалентно тому, что частичные суммы ∑_{i< n} f(i) стремятся к a при n→∞.

LaTeX

$$$\\text{Summable } \\|f_i\\| \\Rightarrow \\bigl( \\text{HasSum } f a \\iff \\text{Tendsto } n \\mapsto \\sum_{i< n} f(i)\\to a\\bigr)$$$

Lean4

theorem hasSum_iff_tendsto_nat_of_summable_norm {f : ℕ → E} {a : E} (hf : Summable fun i => ‖f i‖) :
    HasSum f a ↔ Tendsto (fun n : ℕ => ∑ i ∈ range n, f i) atTop (𝓝 a) :=
  ⟨fun h => h.tendsto_sum_nat, fun h => hasSum_of_subseq_of_summable hf tendsto_finset_range h⟩

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