English
If f is monotone and summable, then the alternating series converges to the alternating sum tsum f with standard convergence properties.
Русский
Если f монотонна и суммируема, чередующийся ряд сходится к сумме tsum f.
LaTeX
$$$\forall {f : \mathbb{N} \to E} [\text{Ring } E] [\text{UniformSpace } E] [\text{CompleteSpace } E] (hfs:\text{Summable } f) : Tendsto (\lambda n, (\sum_{i< n} (-1)^i f(i))) atTop (nhds ( tsum (\lambda i, (-1)^i f(i) )))$$$
Lean4
/-- Partial sums of an alternating monotone series with an even number of terms provide
upper bounds on the limit. -/
theorem tendsto_le_alternating_series (hfl : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i * f i) atTop (𝓝 l))
(hfm : Monotone f) (k : ℕ) : l ≤ ∑ i ∈ range (2 * k), (-1) ^ i * f i :=
by
have ha : Antitone (fun n ↦ ∑ i ∈ range (2 * n), (-1) ^ i * f i) :=
by
refine antitone_nat_of_succ_le (fun n ↦ ?_)
rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring, sum_range_succ, sum_range_succ]
simp_rw [_root_.pow_succ', show (-1 : E) ^ (2 * n) = 1 by simp, neg_one_mul, one_mul, ← sub_eq_add_neg,
sub_le_iff_le_add]
gcongr
exact hfm (by cutsat)
exact ha.le_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; cutsat) tendsto_id)) _
