cauchySeq_alternating_series_of_tendsto_zero

English

If l > 1 and f(n+1)/f(n) tends to l, then not summable.

Русский

Если предел отношения больше единицы, сумма не сходится.

LaTeX

$$$\forall {f : \mathbb{N} \to E} [\text{NormedAddCommGroup } E] {l : \mathbb{R}} (hl: 1 < l) (h: Tendsto (\lambda n, ∥f(n+1)∥ / ∥f(n)∥) atTop (nhds l)) : Not (Summable f)$$$

Lean4

/-- The **alternating series test** for monotone sequences.
See also `Monotone.tendsto_alternating_series_of_tendsto_zero`. -/
theorem cauchySeq_alternating_series_of_tendsto_zero (hfa : Monotone 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

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