tendsto_alternating_series_tsum — Mathlib

English

In alternating monotone bounds, even- and odd-term partial sums bound the limit from above and below respectively.

Русский

В чередующихся монотонных частичных суммах нечетные/четные частичные суммы ограничивают предел сверху/снизу соответствующе.

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)^i f(i) \le l$$$

Lean4

theorem tendsto_alternating_series_tsum {E} [Ring E] [UniformSpace E] [IsUniformAddGroup E] [CompleteSpace E]
    {f : ℕ → E} (hfs : Summable f) :
    Tendsto (fun n => (∑ i ∈ range n, (-1) ^ i * f i)) atTop (𝓝 (∑' i : ℕ, (-1) ^ i * f i)) :=
  Summable.tendsto_sum_tsum_nat hfs.alternating

Похожие утверждения