Theorems · Theorem · measure theory

edist_le_tsum_of_edist_le_of_tendsto

∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal),
  (∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) →
    ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), edist (f n) a ≤ ∑' (m : ℕ), d (n + m)

If edist (f n) (f (n+1)) is bounded above by a function d : ℕ → ℝ≥0∞, then the distance from f n to the limit is bounded by ∑'_{k=n}^∞ d k.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpace