tendsto_alternating_series_of_tendsto_zero

English

If f is monotone and tends to 0, then the alternating partial sums converge to some limit l.

Русский

Если f монотонна и стремится к 0, частичные суммы чередующегося ряда сходятся к некоторому пределу l.

LaTeX

$$$\forall {f : \mathbb{N} \to E} [\text{Monotone } f] (hf0: \text{Tendsto } f atTop (nhds 0)) : ∃ l, Tendsto (\lambda n, \sum_{i< n} (-1)^i f(i)) atTop (nhds l)$$$

Lean4

/-- The **alternating series test** for antitone sequences. -/
theorem tendsto_alternating_series_of_tendsto_zero (hfa : Antitone 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

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