tendsto_alternating_series_of_tendsto_zero

English

If f is monotone, f(n)→0, then the alternating series converges in the sense of Cauchy or tends to a limit.

Русский

Если f монотонна и f(n)→0, то чередующийся ряд сходится и имеет предел.

LaTeX

$$$\forall {f : \mathbb{N} \to \mathbb{R}} (hfa: \text{Monotone } f) (hf0: \text{Tendsto } f \text{ atTop } (nhds 0)) : CauchySeq (\lambda n, \sum_{i< n} (-1)^i f(i))$$$

Lean4

/-- The **alternating series test** for monotone sequences. -/
theorem tendsto_alternating_series_of_tendsto_zero (hfa : Monotone f) (hf0 : Tendsto f atTop (𝓝 0)) :
    ∃ l, Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i * f i) atTop (𝓝 l) :=
  cauchySeq_tendsto_of_complete <| hfa.cauchySeq_alternating_series_of_tendsto_zero hf0

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