cauchySeq_alternating_series_of_tendsto_zero

English

If f is antitone and tends to 0, the alternating partial sums are Cauchy.

Русский

Если f антимонотонна и стремится к 0, чередующиеся частичные суммы — Коши.

LaTeX

$$$\forall {f : \mathbb{N} \to E} [\text{Ring } E] [\text{PartialOrder } E] [\text{IsOrderedRing } E] [\text{TopologicalSpace } E] (hfl: \text{Antitone } f) (hf0: \text{Tendsto } f atTop (nhds 0)) : CauchySeq (\lambda n, \sum_{i< n} (-1)^i f(i))$$$

Lean4

/-- The **alternating series test** for antitone sequences.
See also `Antitone.tendsto_alternating_series_of_tendsto_zero`. -/
theorem cauchySeq_alternating_series_of_tendsto_zero (hfa : Antitone f) (hf0 : Tendsto f atTop (𝓝 0)) :
    CauchySeq fun n ↦ ∑ i ∈ range n, (-1) ^ i * f i :=
  by
  simp_rw [mul_comm]
  exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le

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