English
If a limit l exists for the alternating sum, then all odd-length partial sums provide lower bounds for l.
Русский
Если предел существует, нечётные частичные суммы дают нижние границы для л.
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)) (hfa: Antitone f) (k : \mathbb{N}), \\ \sum_{i< 2k+1} (-1)^i f(i) \le l$$$
Lean4
/-- Partial sums of an alternating antitone series with an even number of terms provide
lower bounds on the limit. -/
theorem alternating_series_le_tendsto (hfl : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i * f i) atTop (𝓝 l))
(hfa : Antitone f) (k : ℕ) : ∑ i ∈ range (2 * k), (-1) ^ i * f i ≤ l :=
by
have hm : Monotone (fun n ↦ ∑ i ∈ range (2 * n), (-1) ^ i * f i) :=
by
refine monotone_nat_of_le_succ (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,
le_sub_iff_add_le]
gcongr
exact hfa (by cutsat)
exact hm.ge_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; cutsat) tendsto_id)) _
