A scaled exponential gap tends to zero when its exponent vanishes

Proved

AvramDividend.Classical.mesh_exponential_gap_tendsto_zero

by WillR · Oct 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

avram-classicalfinite-meshreal-limit

The exponential deficit of a real sequence tending to zero also tends to zero, even after multiplication by an arbitrary fixed real scalar. This is the analytic limit step for the Levy finite-mesh instantaneous-ruin argument.

Preamble

import Mathlib.Analysis.Complex.Exponential
import Mathlib.Topology.Instances.Real.Lemmas
import Mathlib.Topology.Algebra.Order.Field

open Filter

Formal statement

theorem AvramDividend.Classical.mesh_exponential_gap_tendsto_zero
    (r : ℕ → ℝ) (C : ℝ)
    (hr : Tendsto r atTop (nhds (0 : ℝ))) :
    Tendsto (fun n : ℕ => C * (1 - Real.exp (-(r n))))
      atTop (nhds (0 : ℝ)) := by sorry

Source

Mathlib continuity of Real.exp and Tendsto subtraction and multiplication.

View graph