Theorems · Theorem · sequences and series

edist_le_of_edist_le_geometric_of_tendsto

∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (r C : ENNReal) {f : ℕ → α},
  (∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n) →
    ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), edist (f n) a ≤ C * r ^ n / (1 - r)

If edist (f n) (f (n+1)) is bounded by C * r^n, then the distance from f n to the limit of f is bounded above by C * r^n / (1 - r).

Defined in

Mathlib.Analysis.SpecificLimits.Basic

Cited by

3 results in Mathlib

Foundations

Depth 151 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpace