not_summable_iff_tendsto_nat_atTop

English

¬Summable f is equivalent to Tendsto of partial sums to atTop atTop to atTop.

Русский

Не суммируема f тогда и только тогда, когда частичные суммы не стремятся к пределу; вероятность

LaTeX

$$$\\\\forall f : \\\\\\mathbb{N} \\rightarrow \\\\mathbb{R}_{\\\\ge 0}, \\\\neg \\\\mathrm{Summable}(f) \\\\iff \\\\mathrm{Tendsto}\\left(n \\mapsto \\sum_{i=0}^{n-1} f(i)\\right)\\\\left(atTop\\\\right) (atTop) $$$

Lean4

theorem not_summable_iff_tendsto_nat_atTop {f : ℕ → ℝ≥0} :
    ¬Summable f ↔ Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop atTop :=
  by
  constructor
  · intro h
    refine ((tendsto_of_monotone ?_).resolve_right h).comp ?_
    exacts [Finset.sum_mono_set _, tendsto_finset_range]
  · rintro hnat ⟨r, hr⟩
    exact not_tendsto_nhds_of_tendsto_atTop hnat _ (hasSum_iff_tendsto_nat.1 hr)

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