dist_le_of_le_geometric_two_of_tendsto

English

There exists a positive summable ε' with HasSum and sum c less than ε on a countable index.

Русский

Существует положительная сходящаяся последовательность ε', у которой HasSum ε' и сумма меньше ε.

LaTeX

$$$$\exists ε' : ι \to \mathbb{R}_{>0}, \ HasSum ε' c \land c < ε.$$$$

Lean4

/-- If `dist (f n) (f (n+1))` is bounded by `(C / 2) / 2^n`, then the distance from
`f n` to the limit of `f` is bounded above by `C / 2^n`. -/
theorem dist_le_of_le_geometric_two_of_tendsto {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
    dist (f n) a ≤ C / 2 ^ n :=
  by
  convert dist_le_tsum_of_dist_le_of_tendsto _ hu₂ (summable_geometric_two' C) ha n
  simp only [add_comm n, pow_add, ← div_div]
  symm
  exact ((hasSum_geometric_two' C).div_const _).tsum_eq

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