English
Dirichlet-type inequality: the partial sums of an alternating monotone sequence bound the limit from above.
Русский
Неравенство типа Дирихле: частичные суммы чередующейся монотонной последовательности ограничивают предел сверху.
LaTeX
$$$\forall {l} {f : \mathbb{N} \to E} [\text{Ring } E] [\text{PartialOrder } E] [\text{IsOrderedRing } E] (hfl: Tendsto (\lambda n \to \sum_{i< n} (-1)^i f(i)) atTop (nhds l)) (hfm: Monotone f) (k:\mathbb{N}), \\ l \le \sum_{i< 2k} (-1)^i f(i)$$$
Lean4
/-- Partial sums of an alternating monotone series with an odd 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))
(hfm : Monotone f) (k : ℕ) : ∑ i ∈ range (2 * k + 1), (-1) ^ i * f i ≤ l :=
by
have hm : Monotone (fun n ↦ ∑ i ∈ range (2 * n + 1), (-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 _ (2 * n + 1 + 1), sum_range_succ _ (2 * n + 1)]
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, le_sub_iff_add_le]
gcongr
exact hfm (by cutsat)
exact hm.ge_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; cutsat) tendsto_id)) _
