Uniform upper bounds converging to zero force a nonpositive constant

Proved

AvramDividend.Classical.uniform_upper_bound_tendsto_zero

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

avram-classicalfinite-meshlimitorder-closed

If a fixed real A is bounded above by every term of a sequence converging to zero, then A cannot be positive. The result is the deterministic limit step in the bounded-variation Lévy finite-mesh proof: the expected nonnegative drift deficit conditional on strict zero-barrier survival is bounded above by a mesh error tending to zero.

Preamble

import Mathlib.Topology.Order.OrderClosed
import Mathlib.Topology.Instances.Real.Lemmas

open Filter

Formal statement

theorem AvramDividend.Classical.uniform_upper_bound_tendsto_zero
    (A : ℝ) (b : ℕ → ℝ)
    (hb : Tendsto b atTop (nhds (0 : ℝ)))
    (hBound : ∀ n : ℕ, A ≤ b n) :
    A ≤ 0 := by sorry

Source

Mathlib le_of_tendsto and Filter.Eventually.of_forall.

View graph