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