edist_le_tsum_of_edist_le_of_tendsto₀

English

In the same setting as the previous result, the distance from f(0) to the limit a is bounded by the total sum ∑ d(m) from m = 0 to ∞.

Русский

В той же постановке расстояние от f(0) до предела не превосходит полной суммы ∑ d(m).

LaTeX

$$$\operatorname{edist}(f(0), a) \leq \sum_{m \ge 0} d(m)$$$

Lean4

/-- If `edist (f n) (f (n+1))` is bounded above by a function `d : ℕ → ℝ≥0∞`,
then the distance from `f 0` to the limit is bounded by `∑'_{k=0}^∞ d k`. -/
theorem edist_le_tsum_of_edist_le_of_tendsto₀ {f : ℕ → α} (d : ℕ → ℝ≥0∞) (hf : ∀ n, edist (f n) (f n.succ) ≤ d n)
    {a : α} (ha : Tendsto f atTop (𝓝 a)) : edist (f 0) a ≤ ∑' m, d m := by
  simpa using edist_le_tsum_of_edist_le_of_tendsto d hf ha 0

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