English
For monotone alternating sums, upper/lower estimates hold for even/odd truncations of the limit.
Русский
Для монотонных чередующихся сумм верны верхние и нижние оценки для четных и нечетных усечений лимита.
LaTeX
$$$\forall {l} {f : \mathbb{N} \to E} [\text{Ring } E] [\text{PartialOrder } E] [\text{IsOrderedRing } E] (hfl: Tendsto (\lambda n, \sum_{i< n} (-1)^i f(i)) atTop (nhds l)) (hfm: Monotone f) (k : \mathbb{N}), \\ l \le \sum_{i< 2k+1} (-1)^i f(i) \quad \&\quad \sum_{i< 2k} (-1)^i f(i) \le l$$
Lean4
/-- Partial sums of an alternating antitone series with an odd 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))
(hfa : Antitone f) (k : ℕ) : l ≤ ∑ i ∈ range (2 * k + 1), (-1) ^ i * f i :=
by
have ha : Antitone (fun n ↦ ∑ i ∈ range (2 * n + 1), (-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, neg_neg, one_mul, ← sub_eq_add_neg,
sub_add_eq_add_sub, sub_le_iff_le_add]
gcongr
exact hfa (by cutsat)
exact ha.le_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; cutsat) tendsto_id)) _
