aux_hasSum_of_le_geometric — Mathlib

English

If a countable index set exists, there is a positive summable sequence ε' with a HasSum bounded by ε.

Русский

Для счётного множества индексов существует положительная сходящаяся последовательность ε' с суммой, не превышающей заданное ε.

LaTeX

$$$$\exists ε' : ι \to \mathbb{R}, \; (\forall i, ε'_i > 0) \land \exists c, HasSum ε' c \land c \le ε.$$$$

Lean4

/-- If `dist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then `f` is a Cauchy sequence. -/
theorem aux_hasSum_of_le_geometric : HasSum (fun n : ℕ ↦ C * r ^ n) (C / (1 - r)) :=
  by
  rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ dist_nonneg.trans (hu n) with (rfl | ⟨_, r₀⟩)
  · simp [hasSum_zero]
  · refine HasSum.mul_left C ?_
    simpa using hasSum_geometric_of_lt_one r₀ hr

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